Skip to content

Instantly share code, notes, and snippets.

@LessnessRandomness
Created October 11, 2020 05:04
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save LessnessRandomness/eb1bf0ef8abd9d96766be3b0418f6d5f to your computer and use it in GitHub Desktop.
Save LessnessRandomness/eb1bf0ef8abd9d96766be3b0418f6d5f to your computer and use it in GitHub Desktop.
Last Qed takes forever
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