title: How to prove equivalence between those two types - algorithm' and algorithm''?
body: <p>What I’m doing wrong here (either I'm too inexperienced to finish the proof or there's some mistake before it)? I can’t quite prove the equivalence between these two types. Any help is appreciated.</p>
  <p>This is part of my efforts to prove the log_2(n!) bound for sorting (for specific n=8). The <code>algorithm''</code> type corresponds to decision tree.</p>
  <pre><code>Require Import List Lia.
  Set Implicit Arguments.
  
  Inductive value := x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7.
  Inductive variable := aux | num: value -&gt; variable.
  Definition variable_eq_dec (x y: variable): {x=y} + {x&lt;&gt;y}.
  Proof.
    destruct x, y.
    + left; auto.
    + right; abstract congruence.
    + right; abstract congruence.
    + destruct v, v0; try (left; abstract congruence); (right; abstract congruence).
  Defined.
  
  Inductive assignment := assign: variable -&gt; variable -&gt; assignment.
  Inductive comparison := GT: forall (more less: value), comparison.
  
  Definition instantation := variable -&gt; nat.
  
  Definition run_assignment (a: assignment) (i: instantation): instantation :=
    match a with
    | assign v1 v2 =&gt; fun x =&gt; if variable_eq_dec x v1 then i v2 else i x end.
  
  Fixpoint run_assignment_list (L: list assignment): instantation -&gt; instantation :=
    match L with
    | nil =&gt; fun i =&gt; i
    | a :: l =&gt; fun i =&gt; run_assignment_list l (run_assignment a i)
    end.
  
  Inductive algorithm': nat -&gt; Type :=
  | leaf': algorithm' 0
  | conditional': forall n (c: comparison) (pos_assignments neg_assignments: list assignment) (pos neg: algorithm' n), algorithm' (S n).
  
  Inductive algorithm'': nat -&gt; Type :=
  | leaf'': list assignment -&gt; algorithm'' 0
  | conditional'': forall n (c: comparison) (pos neg: algorithm'' n), algorithm'' (S n).
  
  Definition run_algorithm' n (a: algorithm' n): instantation -&gt; instantation.
  Proof.
    induction a.
    + exact (fun x =&gt; x).
    + intro i. destruct c. exact (if Compare_dec.gt_dec (i (num more)) (i (num less))
                         then IHa1 (run_assignment_list pos_assignments i)
                         else IHa2 (run_assignment_list neg_assignments i)).
  Defined.
  
  Definition run_algorithm'' n (a: algorithm'' n) (i: instantation): instantation.
  Proof.
    induction a.
    + exact (run_assignment_list l i).
    + destruct c.
      exact (if Compare_dec.gt_dec (i (num more)) (i (num less)) then IHa1 else IHa2).
  Defined.
  
  Fixpoint append_assignments n (a: algorithm'' n) (L: list assignment): algorithm'' n :=
    match a with
    | leaf'' L0 =&gt; leaf'' (L ++ L0)
    | conditional'' c pos neg =&gt; conditional'' c (append_assignments pos L) (append_assignments neg L)
    end.
  
  Fixpoint algorithm'_to_algorithm'' n (a: algorithm' n): algorithm'' n :=
    match a with
    | leaf' =&gt; leaf'' nil
    | conditional' c Lpos Lneg pos neg =&gt;
        conditional'' c (append_assignments (algorithm'_to_algorithm'' pos) Lpos)
                        (append_assignments (algorithm'_to_algorithm'' neg) Lneg)
    end.
  
  Theorem algorithm'_algorithm''_equiv n (a: algorithm' n):
    forall (i: instantation) (x: variable), run_algorithm' a i x = run_algorithm'' (algorithm'_to_algorithm'' a) i x.
  Proof.
  Admitted.
  </code></pre>