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.
This is part of my efforts to prove the log_2(n!) bound for sorting (for specific n=8). The algorithm'' type corresponds to decision tree.
Require Import List Lia.
Set Implicit Arguments.
Inductive value := x0 | x1 | x2 | x3 | x4 | x5 | x6 | x7.
Inductive variable := aux | num: value -> variable.
Definition variable_eq_dec (x y: variable): {x=y} + {x<>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 -> variable -> assignment.
Inductive comparison := GT: forall (more less: value), comparison.
Definition instantation := variable -> nat.
Definition run_assignment (a: assignment) (i: instantation): instantation :=
match a with
| assign v1 v2 => fun x => if variable_eq_dec x v1 then i v2 else i x end.
Fixpoint run_assignment_list (L: list assignment): instantation -> instantation :=
match L with
| nil => fun i => i
| a :: l => fun i => run_assignment_list l (run_assignment a i)
end.
Inductive algorithm': nat -> 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 -> Type :=
| leaf'': list assignment -> algorithm'' 0
| conditional'': forall n (c: comparison) (pos neg: algorithm'' n), algorithm'' (S n).
Definition run_algorithm' n (a: algorithm' n): instantation -> instantation.
Proof.
induction a.
+ exact (fun x => 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 => leaf'' (L ++ L0)
| conditional'' c pos neg => 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' => leaf'' nil
| conditional' c Lpos Lneg pos neg =>
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.
Your statement appears to be false. Here is a counter example.
Definition mya1 : algorithm' 2 :=
conditional' (GT x0 x1)
((assign (num x0) (num x2)) :: (assign (num x1) (num x3)) :: nil)
((assign (num x0) (num x4)) :: (assign (num x1) (num x5)) :: nil)
(conditional' (GT x2 x3)
((assign (num x2) (num x6)) :: (assign (num x3) (num x7)) :: nil)
((assign (num x0) (num x4)) :: (assign (num x1) (num x5)) :: nil)
leaf' leaf')
(conditional' (GT x3 x0)
((assign (num x2) (num x7)) :: (assign (num x3) (num x6)) :: nil)
((assign (num x0) (num x4)) :: (assign (num x1) (num x5)) :: nil)
leaf' leaf').
Definition myi x :=
if variable_eq_dec x (num x0) then 3 else
if variable_eq_dec x (num x1) then 4 else
if variable_eq_dec x (num x2) then 6 else
if variable_eq_dec x (num x3) then 5 else
if variable_eq_dec x (num x4) then 7 else
if variable_eq_dec x (num x5) then 8 else
if variable_eq_dec x (num x6) then 9 else
0.
The following command returns 6
Compute run_algorithm' mya1 myi (num x2).
While the following returns 0.
Compute run_algorithm'' (algorithm'_to_algorithm'' mya1) myi (num x2).
I found the counter example by attempting to do the proof by induction on a. Here is my script.
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.
induction a.
easy.
simpl.
intros i x.
destruct c.
destruct (Compare_dec.gt_dec (i (num more)) (i (num less))) as [cmp1 | cmp2].
rewrite IHa1.
This leads me to a goal that is more about append_assigments and run_assignment_list, which I state in this manner.
Lemma algorithm''_list n (a : algorithm'' n) (l: list assignment) i x :
run_algorithm'' a (run_assignment_list l i) x =
run_algorithm'' (append_assignments a l) i x.
In the course of making this proof, by induction on a, I could see that there was a mismatch of execution between the two sides of the equality. Analyzing it further lead to the counterexample.