-
-
Save LessnessRandomness/eb1bf0ef8abd9d96766be3b0418f6d5f to your computer and use it in GitHub Desktop.
Last Qed takes forever
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Require Import Permutation List Omega. | |
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. | |
Inductive step := | |
| assignments: forall (L: list assignment), step | |
| conditional: forall (c: comparison) (positive negative: step), step. | |
Definition algorithm := list step. | |
Definition instantation := variable -> nat. | |
Definition is_increasing (i: instantation) := | |
i (num x0) <= i (num x1) /\ | |
i (num x1) <= i (num x2) /\ | |
i (num x2) <= i (num x3) /\ | |
i (num x3) <= i (num x4) /\ | |
i (num x4) <= i (num x5) /\ | |
i (num x5) <= i (num x6) /\ | |
i (num x6) <= i (num x7). | |
Definition list_of_values (i: instantation) := | |
i (num x0) :: i (num x1) :: i (num x2) :: i (num x3) :: i (num x4) :: i (num x5) :: i (num x6) :: i (num x7) :: nil. | |
Definition is_permutation (i1 i2: instantation) := Permutation (list_of_values i1) (list_of_values i2). | |
Definition is_sorted (start result: instantation) := is_increasing result /\ is_permutation start result. | |
Definition run_assignment (values: instantation) (a: assignment): instantation. | |
Proof. | |
destruct a as [v1 v2]. | |
exact (fun i => if variable_eq_dec i v1 then values v2 else values i). | |
Defined. | |
Definition run_step (values: instantation) (s: step): instantation. | |
Proof. | |
induction s. | |
+ induction L. | |
- exact values. | |
- exact (run_assignment IHL a). | |
+ destruct c. | |
exact (if Compare_dec.gt_dec (values (num more)) (values (num less)) then IHs1 else IHs2). | |
Defined. | |
Definition run_algorithm (values: instantation) (algo: algorithm): instantation. | |
Proof. | |
induction algo. | |
+ exact values. | |
+ exact (run_step IHalgo a). | |
Defined. | |
Definition run_algorithm_tail (values: instantation) (s: step) (algo: algorithm): | |
run_algorithm values (algo ++ s :: nil) = run_algorithm (run_step values s) algo. | |
Proof. | |
induction algo. | |
+ simpl. auto. | |
+ simpl. rewrite IHalgo. auto. | |
Qed. | |
Definition count_comparisons_in_step (s: step): nat. | |
Proof. | |
induction s. | |
+ exact 0. | |
+ exact (PeanoNat.Nat.max IHs1 IHs2). | |
Qed. | |
Definition do_nothing := assignments nil. | |
Definition swap (x y: value) := | |
assign (num y) aux :: | |
assign (num x) (num y) :: | |
assign aux (num x) :: | |
nil. | |
Definition property (L: list comparison) (i: instantation): Prop. | |
Proof. | |
induction L. | |
+ exact True. | |
+ destruct a. exact (IHL /\ i (num less) <= i (num more)). | |
Defined. | |
Definition step1 := conditional (GT x0 x1) (assignments (swap x0 x1)) do_nothing. | |
Definition prop1 := GT x1 x0 :: nil. | |
Definition step2 := conditional (GT x2 x3) (assignments (swap x2 x3)) do_nothing. | |
Definition prop2 := GT x3 x2 :: prop1. | |
Definition step3 := conditional (GT x4 x5) (assignments (swap x4 x5)) do_nothing. | |
Definition prop3 := GT x5 x4 :: prop2. | |
Definition step4 := conditional (GT x6 x7) (assignments (swap x6 x7)) do_nothing. | |
Definition prop4 := GT x7 x6 :: prop3. | |
Definition step5 := conditional (GT x1 x3) (assignments (swap x1 x3 ++ swap x0 x2)) do_nothing. | |
Definition prop5 := GT x3 x1 :: prop4. | |
Definition step6 := conditional (GT x5 x7) (assignments (swap x5 x7 ++ swap x4 x6)) do_nothing. | |
Definition prop6 := GT x7 x5 :: prop5. | |
Definition step7 := conditional (GT x3 x7) (assignments (swap x0 x4 ++ swap x1 x5 ++ swap x2 x6 ++ swap x3 x7)) do_nothing. | |
Definition prop7 := GT x7 x3 :: prop6. | |
Definition step8_9 := conditional (GT x5 x3) | |
do_nothing | |
(conditional (GT x5 x1) | |
(assignments (swap x3 x5 ++ swap x2 x4)) | |
(assignments (swap x3 x5 ++ swap x2 x4 ++ swap x1 x5 ++ swap x0 x4))). | |
Definition prop9 := GT x5 x3 :: prop5. | |
Ltac T1 after := intros; repeat split; simpl in *; unfold after; clear after; | |
repeat destruct gt_dec; repeat (destruct variable_eq_dec; try congruence); omega. | |
Ltac T2 after list_of_values := intros; unfold after, list_of_values; simpl; destruct gt_dec; repeat (destruct variable_eq_dec; try congruence). | |
Definition step1_condition (before: instantation): | |
let after := run_algorithm before (step1 :: nil) in | |
property prop1 after. | |
Proof. | |
T1 after. | |
Qed. | |
Definition step2_after_step1_condition (before: instantation) | |
(H: property prop1 before): | |
let after := run_algorithm before (step2 :: nil) in | |
property prop2 after. | |
Proof. | |
T1 after. | |
Qed. | |
Definition step3_after_step2_condition (before: instantation) | |
(H: property prop2 before): | |
let after := run_algorithm before (step3 :: nil) in | |
property prop3 after. | |
Proof. | |
T1 after. | |
Qed. | |
Definition step4_after_step3_condition (before: instantation) | |
(H: property prop3 before): | |
let after := run_algorithm before (step4 :: nil) in | |
property prop4 after. | |
Proof. | |
T1 after. | |
Qed. | |
Definition step5_after_step4_condition (before: instantation) | |
(H: property prop4 before): | |
let after := run_algorithm before (step5 :: nil) in | |
property prop5 after. | |
Proof. | |
T1 after. | |
Qed. | |
Definition step6_after_step5_condition (before: instantation) | |
(H: property prop5 before): | |
let after := run_algorithm before (step6 :: nil) in | |
property prop6 after. | |
Proof. | |
T1 after. | |
Qed. | |
Definition step7_after_step6_condition (before: instantation) | |
(H: property prop6 before): | |
let after := run_algorithm before (step7 :: nil) in | |
property prop7 after. | |
Proof. | |
T1 after. | |
Qed. | |
Definition step9_after_step7_condition (before: instantation) | |
(H: property prop7 before): | |
let after := run_algorithm before (step8_9 :: nil) in | |
property prop9 after. | |
Proof. | |
T1 after. | |
Qed. | |
Definition step1_permutation (before: instantation): | |
let after := run_algorithm before (step1 :: nil) in | |
Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
T2 after list_of_values. | |
+ repeat constructor. | |
+ repeat constructor. | |
Qed. | |
Definition step2_permutation (before: instantation): | |
let after := run_algorithm before (step2 :: nil) in | |
Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
T2 after list_of_values. | |
+ repeat constructor. | |
+ repeat constructor. | |
Qed. | |
Definition step3_permutation (before: instantation): | |
let after := run_algorithm before (step3 :: nil) in | |
Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
T2 after list_of_values. | |
+ repeat constructor. | |
+ repeat constructor. | |
Qed. | |
Definition step4_permutation (before: instantation): | |
let after := run_algorithm before (step4 :: nil) in | |
Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
T2 after list_of_values. | |
+ repeat constructor. | |
+ repeat constructor. | |
Qed. | |
Definition step5_permutation (before: instantation): | |
let after := run_algorithm before (step5 :: nil) in | |
Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
T2 after list_of_values. | |
+ pose proof (@Permutation_app_tail _ | |
(before (num x0) :: before (num x1) :: before (num x2) :: before (num x3) :: nil) | |
(before (num x2) :: before (num x3) :: before (num x0) :: before (num x1) :: nil) | |
(before (num x4) :: before (num x5) :: before (num x6) :: before (num x7) :: nil)). | |
simpl in H. apply H. | |
pose proof (Permutation_rev (before (num x0) :: before (num x1) :: before (num x2) :: before (num x3) :: nil)). | |
pose proof (Permutation_app_comm (before (num x0) :: before (num x1) :: nil) (before (num x2) :: before (num x3) :: nil)). | |
simpl in H1. apply H1. | |
+ repeat constructor. | |
Qed. | |
Definition step6_permutation (before: instantation): | |
let after := run_algorithm before (step6 :: nil) in | |
Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
T2 after list_of_values. | |
+ repeat constructor. | |
pose proof (Permutation_app_comm (before (num x4) :: before (num x5) :: nil) (before (num x6) :: before (num x7) :: nil)). | |
simpl in H. apply H. | |
+ repeat constructor. | |
Qed. | |
Definition step7_permutation (before: instantation): | |
let after := run_algorithm before (step7 :: nil) in | |
Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
T2 after list_of_values. | |
+ pose proof (Permutation_app_comm | |
(before (num x0) :: before (num x1) :: before (num x2) :: before (num x3) :: nil) | |
(before (num x4) :: before (num x5) :: before (num x6) :: before (num x7) :: nil)). | |
simpl in H. apply H. | |
+ repeat constructor. | |
Qed. | |
Definition step9_permutation (before: instantation): | |
let after := run_algorithm before (step8_9 :: nil) in | |
Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
intro. unfold after; clear after. simpl. unfold list_of_values. | |
repeat destruct gt_dec; repeat (destruct variable_eq_dec; try congruence). | |
+ apply Permutation_refl. | |
+ repeat constructor. | |
pose proof (@Permutation_app_tail _ | |
(before (num x2) :: before (num x3) :: before (num x4) :: before (num x5) :: nil) | |
(before (num x4) :: before (num x5) :: before (num x2) :: before (num x3) :: nil) | |
(before (num x6) :: before (num x7) :: nil)). | |
simpl in H. apply H. | |
pose proof (Permutation_app_comm | |
(before (num x2) :: before (num x3) :: nil) | |
(before (num x4) :: before (num x5) :: nil)). | |
simpl in H0. apply H0. | |
+ apply (@Permutation_app_tail _ | |
(before (num x0) :: before (num x1) :: before (num x2) :: before (num x3) :: before (num x4) :: before (num x5) :: nil) | |
(before (num x4) :: before (num x5) :: before (num x0) :: before (num x1) :: before (num x2) :: before (num x3) :: nil) | |
(before (num x6) :: before (num x7) :: nil)). | |
apply (Permutation_app_comm | |
(before (num x0) :: before (num x1) :: before (num x2) :: before (num x3) :: nil) | |
(before (num x4) :: before (num x5) :: nil)). | |
Qed. | |
Theorem step9_condition (before: instantation): | |
let after := run_algorithm before (step8_9 :: step7 :: step6 :: step5 :: step4 :: step3 :: step2 :: step1 :: nil) in | |
property prop9 after /\ Permutation (list_of_values before) (list_of_values after). | |
Proof. | |
intro; unfold after; clear after. | |
replace (step8_9 :: step7 :: step6 :: step5 :: step4 :: step3 :: step2 :: step1 :: nil) | |
with ((((((((step8_9 :: nil) ++ step7 :: nil) ++ step6 :: nil) ++ step5 :: nil) ++ step4 :: nil) ++ step3 :: nil) ++ | |
step2 :: nil) ++ step1 :: nil) by auto. | |
repeat rewrite run_algorithm_tail. split. | |
+ apply step9_after_step7_condition. apply step7_after_step6_condition. | |
apply step6_after_step5_condition. apply step5_after_step4_condition. apply step4_after_step3_condition. | |
apply step3_after_step2_condition. apply step2_after_step1_condition. apply step1_condition. | |
+ eapply Permutation_trans. apply step1_permutation. | |
eapply Permutation_trans. apply step2_permutation. | |
eapply Permutation_trans. apply step3_permutation. | |
eapply Permutation_trans. apply step4_permutation. | |
eapply Permutation_trans. apply step5_permutation. | |
eapply Permutation_trans. apply step6_permutation. | |
eapply Permutation_trans. apply step7_permutation. | |
apply step9_permutation. | |
Qed. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment