Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type à

égalité décidable + maj dépendances


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9467 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 28 insertions, 11 deletions

diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index e491a4d5c..b45aa23fe 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -158,6 +158,13 @@ Proof.
   apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)).
 Qed.
 
+(** We deduce the injectivity of dependent equality for decidable types *)
+Theorem eq_dep_eq_dec :
+  forall A:Type,
+    (forall x y:A, {x = y} + {x <> y}) ->
+     forall (P:A->Type) (p:A) (x y:P p), eq_dep A P p x p y -> x = y.
+Proof (fun A eq_dec => eq_rect_eq__eq_dep_eq A (eq_rect_eq_dec eq_dec)).
+
 Unset Implicit Arguments.
 
 (************************************************************************)
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 03d29db35..8123d8d85 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -535,21 +535,31 @@ Definition PeanoView_iter (P:positive->Type)
   | PeanoSucc _ q => f _ (iter _ q)
   end).
 
-Require Import JMeq.
+Require Import Eqdep_dec EqdepFacts.
+
+Theorem eq_dep_eq_positive :
+  forall (P:positive->Type) (p:positive) (x y:P p), 
+  eq_dep positive P p x p y -> x = y.
+Proof.
+apply eq_dep_eq_dec.
+decide equality.
+Qed.
 
 Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'.  
 Proof.
 intros. 
-induction q. apply JMeq_eq. cut (xH=xH). pattern xH at 1 2 5, q'. destruct q'. trivial.
-destruct p0; intros; discriminate.
-trivial.
-apply JMeq_eq.
-cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. 
-intro. destruct p; discriminate.
-intro. unfold p0 in H. apply Psucc_inj in H.
-generalize q'. rewrite H. intro.
-rewrite (IHq q'0).
-trivial.
+induction q. 
+apply eq_dep_eq_positive. 
+  cut (xH=xH). pattern xH at 1 2 5, q'. destruct q'. trivial.
+  destruct p0; intros; discriminate.
+  trivial.
+apply eq_dep_eq_positive.
+  cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. 
+  intro. destruct p; discriminate.
+  intro. unfold p0 in H. apply Psucc_inj in H.
+  generalize q'. rewrite H. intro.
+  rewrite (IHq q'0).
+  trivial.
 trivial.
 Qed.