From ba09fcb015b19e083d64f901d11381feee2c033e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 28 Dec 2006 21:05:12 +0000
Subject: 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
---
 .depend.coq                |  2 +-
 theories/Logic/Eqdep_dec.v |  7 +++++++
 theories/NArith/BinPos.v   | 32 +++++++++++++++++++++-----------
 3 files changed, 29 insertions(+), 12 deletions(-)

diff --git a/.depend.coq b/.depend.coq
index ef98c6a5a9..7024658570 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -150,7 +150,7 @@ theories/Bool/DecBool.vo: theories/Bool/DecBool.v
 theories/Bool/Sumbool.vo: theories/Bool/Sumbool.v
 theories/Bool/BoolEq.vo: theories/Bool/BoolEq.v theories/Bool/Bool.vo
 theories/Bool/Bvector.vo: theories/Bool/Bvector.v theories/Bool/Bool.vo theories/Bool/Sumbool.vo theories/Arith/Arith.vo
-theories/NArith/BinPos.vo: theories/NArith/BinPos.v
+theories/NArith/BinPos.vo: theories/NArith/BinPos.v theories/Logic/Eqdep_dec.vo theories/Logic/EqdepFacts.vo
 theories/NArith/Pnat.vo: theories/NArith/Pnat.v theories/NArith/BinPos.vo theories/Arith/Le.vo theories/Arith/Lt.vo theories/Arith/Gt.vo theories/Arith/Plus.vo theories/Arith/Mult.vo theories/Arith/Minus.vo
 theories/NArith/BinNat.vo: theories/NArith/BinNat.v theories/NArith/BinPos.vo
 theories/NArith/NArith.vo: theories/NArith/NArith.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo contrib/setoid_ring/NArithRing.vo
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index e491a4d5c9..b45aa23fe8 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 03d29db35f..8123d8d85e 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.
 
-- 
cgit v1.2.3