Make compile with Coq 8.2pl1.

Ignore-this: 3ef12e67a2cdda3c0a39e50d123c1c36 darcs-hash:20100410130523-bab43-da5a6e771720f916b109bbd0e0dbad255e9ef989.gz
Eelis · Apr 10, 2010 · f053508 · f053508
1 parent 443d031
commit f053508
Show file tree

Hide file tree

Showing 6 changed files with 47 additions and 59 deletions.
diff --git a/README.html b/README.html
@@ -12,7 +12,7 @@ <h1>Readme</h1>
     <hr/><h2>1. Prerequisites</h2>
 
     <ul>
-      <li><a href='http://coq.inria.fr/'>Coq</a> &ge; 8.2beta2</li>
+      <li><a href='http://coq.inria.fr/'>Coq</a> &ge; 8.2pl1</li>
       <li><a href='http://www.scons.org/'>SCons</a> &ge; 0.98 (SCons is a modern make-replacement based on Python)</li>
     </ul>
 

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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...