Modification de la table des tactic Definitions pour eviter l'ecriture

de fonctions dans les .vo
ajout de lemmes dans EqNat, Logic_Type
suppression de PolyListSyntax qui redefinissait le Infix de append
Recherche d'instances a reecrire dans les Cases et les FixPoint


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

4 files changed, 50 insertions, 8 deletions

diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index dde9daa4c..ecce3f840 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -51,3 +51,18 @@ Fixpoint  beq_nat [n:nat] : nat -> bool :=
              | (S _)   O     => false
              | (S n1) (S m1) => (beq_nat n1 m1)
           end.
+
+Lemma beq_nat_refl : (x:nat)true=(beq_nat x x).
+Proof.
+  Induction x; Simpl; Auto.
+Qed.
+
+Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y.
+Proof.
+  Double Induction 1 2; Simpl.
+    Reflexivity.
+    Intros; Discriminate H0.
+    Intros; Discriminate H0.
+    Intros; Case (H0 ? H1); Reflexivity.
+Defined.
+
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 1cd3ad8be..b78fcb93b 100755
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -165,6 +165,41 @@ Definition identityT_rect_r :
  Intros A x P H y H0; Case sym_idT with 1:= H0; Trivial.
 Defined.
 
+Inductive sigT [A:Set; P:A->Prop] : Type := existT : (x:A)(P x)->(sigT A P).
+
+Section sigT_proj.
+
+  Variable A : Set.
+  Variable P : A->Prop.
+
+  Definition projT1 := [H:(sigT A P)]
+    let (x, _) = H in x.
+  Definition projT2 := [H:(sigT A P)]<[H:(sigT A P)](P (projT1 H))>
+    let (_, h) = H in h.
+
+End sigT_proj.
+
+Inductive prodT [A,B:Type] : Type := pairT : A -> B -> (prodT A B).
+
+Section prodT_proj.
+
+  Variables A, B : Type.
+
+  Definition fstT := [H:(prodT A B)]Cases H of (pairT x _) => x end.
+  Definition sndT := [H:(prodT A B)]Cases H of (pairT _ y) => y end.
+
+End prodT_proj.
+
+Definition prodT_uncurry : (A,B,C:Type)((prodT A B)->C)->A->B->C :=
+  [A,B,C:Type; f:((prodT A B)->C); x:A; y:B]
+  (f (pairT A B x y)).
+
+Definition prodT_curry : (A,B,C:Type)(A->B->C)->(prodT A B)->C :=
+  [A,B,C:Type; f:(A->B->C); p:(prodT A B)]
+  Cases p of
+  | (pairT x y) => (f x y)
+  end.
+
 Hints Immediate sym_idT sym_not_idT : core v62.
 
 
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
deleted file mode 100644
index a19a3dcc1..000000000
--- a/theories/Lists/PolyListSyntax.v
+++ /dev/null
@@ -1,7 +0,0 @@
-
-(* $Id$ *)
-
-(* Syntax for list concatenation *)
-Require PolyList.
-
-Infix RIGHTA 7 "^" app.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 1944b60cd..546d97f90 100755
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -11,7 +11,6 @@
 
 Require Relation_Definitions.
 Require PolyList.
-Require PolyListSyntax.
 
 (* Some operators to build relations *)