diff --git a/README.html b/README.html index 126bb95..49bd9c3 100644 --- a/README.html +++ b/README.html @@ -12,7 +12,7 @@

Readme

1. Prerequisites

diff --git a/src/indices.v b/src/indices.v index 8986590..4eed392 100644 --- a/src/indices.v +++ b/src/indices.v @@ -166,19 +166,18 @@ Section contents. intro. apply (NoDup_map_inv' (@nb_val (length ol))). rewrite vec.List_map. - apply Permutation_NoDup with (vec.to_list (vec.nb_nats b (length l))). - unfold vec.nb_nats. - rewrite <- vec.List_map. - apply NoDup_map. - intros. - apply natBelow_unique... - apply vec.NoDup_nats. - apply Permutation_sym. - apply vec.List_Permutation. - apply (vec_IndexSeq_nats_perm _ H0). + assert (Permutation (vec.map nb_val H) (vec.to_list (vec.nb_nats b (length l)))). + apply vec.List_Permutation, vec_IndexSeq_nats_perm... + rewrite H1. + unfold vec.nb_nats. + rewrite <- vec.List_map. + apply NoDup_map. + intros. + apply natBelow_unique... + apply vec.NoDup_nats. Qed. - Lemma IndexSeq_inv l b: IndexSeq b l -> forall t, In t l-> b <= t < b + length l. + Lemma IndexSeq_inv l b: IndexSeq b l -> forall t, In t l -> b <= t < b + length l. Proof with auto with arith. intro. rewrite <- (vec.list_round_trip l). diff --git a/src/insertion_sort.v b/src/insertion_sort.v index 083efcb..8a46595 100644 --- a/src/insertion_sort.v +++ b/src/insertion_sort.v @@ -20,6 +20,7 @@ Require Import Omega. Require Import arith_lems. Require Import list_utils. Require Import Morphisms. +Require Import Relation_Definitions. Require vec. Definition numbers := 3 :: 2 :: 5 :: 9 :: 7 :: 6 :: 1 :: 0 :: 4 :: 8 :: nil. diff --git a/src/list_utils.v b/src/list_utils.v index 0f0562b..bd452a3 100644 --- a/src/list_utils.v +++ b/src/list_utils.v @@ -5,7 +5,7 @@ Require Export List. Require Import Program Omega Factorial - Bool util Morphisms Relations RelationClasses. + Bool util Morphisms Relations RelationClasses Permutation. Hint Resolve in_map Permutation_refl. @@ -139,19 +139,23 @@ Proof. induction l; firstorder. Qed. Implicit Arguments In_map_inv [T U f l y]. -Lemma Permutation_NoDup {X} (a: list X): NoDup a -> forall b, Permutation a b -> NoDup b. -Proof with auto. - intros. - induction H0... - inversion_clear H. - apply NoDup_cons... - intro. - apply H1. - apply Permutation_in with l'... - apply Permutation_sym... - inversion_clear H. - inversion_clear H1. - apply NoDup_cons; firstorder. +Instance In_Permutation A (x: A): Morphism (Permutation ==> iff) (In x). +Proof. + repeat intro. + pose proof (Permutation_in). + pose proof (Permutation_sym). + firstorder. +Qed. + +Instance Permutation_NoDup {X}: Morphism (Permutation ==> iff) (@NoDup X). +Proof with firstorder. + pose proof NoDup_cons. + intros ??? E. + induction E; [firstorder | | | firstorder]. + split; intro A; inversion_clear A; apply NoDup_cons... + rewrite <- E... + rewrite E... + split; intro A; inversion_clear A; inversion_clear H1... Qed. Hint Resolve incl_tran. @@ -195,18 +199,12 @@ Proof with auto. Qed. Instance filter_perm X: Morphism (pointwise_relation _ eq ==> Permutation ==> Permutation) (@filter X). -Proof with eauto. +Proof with auto. repeat intro. - induction H0... - simpl. - rewrite H. + induction H0; rewrite H in *; simpl... destruct (y x0)... - simpl. - repeat rewrite H. - rewrite (filter_eq_morphism H (refl_equal l)). destruct (y y0); destruct (y x0)... - rewrite (filter_eq_morphism H (refl_equal l)) in *. - rewrite (filter_eq_morphism H (refl_equal l')) in *... + eauto. Qed. Lemma complementary_filter_perm A (p: A -> bool) (l: list A): @@ -568,7 +566,7 @@ Inductive elemsR A B (R: A -> B -> Prop): list A -> list B -> Prop := Hint Constructors elemsR. -Instance elemsR_trans `{R: relation A} {TR: Transitive R}: Transitive (elemsR R). +Instance elemsR_trans A `{R: relation A} {TR: Transitive R}: Transitive (elemsR R). Proof with auto. do 4 intro. induction x. @@ -621,7 +619,7 @@ Section Permuted. Lemma permuted_refl l: Permuted l l. Proof. induction l; auto. Qed. - Global Hint Immediate permuted_refl. + Hint Immediate permuted_refl. Lemma elemsR_permuted l l': elemsR R l l' -> Permuted l l'. Proof. induction l; intros; inversion_clear H; auto. Qed. @@ -777,7 +775,7 @@ Instance Reflexive_Permutation T: Reflexive Permutation := @Permutation_refl T. Instance Reflexive_Symmetric T: Symmetric Permutation := @Permutation_sym T. Instance Reflexive_Transitive T: Transitive Permutation := @perm_trans T. -Instance app_Permutation_mor: Morphism (Permutation ==> Permutation ==> Permutation) (@app T). +Instance app_Permutation_mor T: Morphism (Permutation ==> Permutation ==> Permutation) (@app T). Proof. repeat intro. apply Permutation_app; assumption. Qed. Instance map_Permutation_mor T U (f: T -> U): Morphism (Permutation ==> Permutation) (map f) := diff --git a/src/qs_cases.v b/src/qs_cases.v index c8a7a1b..9c438d3 100644 --- a/src/qs_cases.v +++ b/src/qs_cases.v @@ -96,17 +96,12 @@ Section contents. Hint Immediate vec.remove_perm. Lemma pivot_not_In_flt cr: ~ In (vec.nth v pi) (flt pi cr). - Proof. - unfold flt. - intros. - intro. - destruct (In_filter_inv _ _ _ H). - cset (Permutation_sym (vec.List_Permutation (vec.remove_perm pi v))). - simpl in H2. - cset (Permutation_NoDup ndi H2). - inversion_clear H3. - apply H4. - assumption. + Proof with auto. + intros cr H. + pose proof ndi as H0. + rewrite (Permutation_sym (vec.List_Permutation (vec.remove_perm pi v))) in H0. + inversion_clear H0... + destruct (In_filter_inv _ _ _ H)... Qed. Lemma NoDup_comparisons (x: Index ee ol) (l: list (Index ee ol)): @@ -291,10 +286,8 @@ Section contents. apply le_INR. apply eq_count_NoDup. apply NoDup_comparisons. - apply Permutation_NoDup with v... - apply IndexSeq_NoDup with b... - apply Permutation_sym... - apply (vec.List_Permutation (vec.remove_perm pi v)). + rewrite (vec.List_Permutation (vec.remove_perm pi v)). + apply IndexSeq_NoDup with b... destruct H; subst; [left | right]; apply pivot_not_In_flt. intros. unfold U.M. diff --git a/src/qs_sound_cmps.v b/src/qs_sound_cmps.v index 0430471..ab5cbed 100644 --- a/src/qs_sound_cmps.v +++ b/src/qs_sound_cmps.v @@ -135,12 +135,9 @@ Section contents. subst. apply ne_le_impl_lt... intro. - cset (vec.List_Permutation (vec.perm_sym (vec.remove_perm x v))). - simpl in H6. - cset (Permutation_NoDup H1 H6). - assert (~ In (vec.nth v x) (vec.remove v x)). - inversion_clear H7... - apply H8. + rewrite (vec.List_Permutation (vec.perm_sym (vec.remove_perm x v))) in H1. + inversion_clear H1. + apply H6. cset(natBelow_unique _ _ H5). subst x1... subst...