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

1 files changed, 15 insertions, 0 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.
+