MAJ JMeq sur Type + typos (sur propositions de Pierre Castéran)

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

2 files changed, 90 insertions, 87 deletions

diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index a80f6cacb..df8bc9f10 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -518,7 +518,7 @@ of {\coq}, in which a general parameter $a$ of an inductive
 type $I$ had to appear only in applications of the form $I\,\dots\,a$.
 
 Since version $8.1$, if $a$ is a general parameter of an inductive 
-type $I$, the type of an argument of a construtor of $I$ may be
+type $I$, the type of an argument of a constructor of $I$ may be
 of the form  $I\,\dots\,t_a$ , where $t_a$ is any term.
 Notice that the final type of the constructors must be of the form
 $I\,\dots\,a$, since these constructors describe how to form 
@@ -2848,7 +2848,7 @@ For Acc_intro: Arguments A, R are implicit
 \dots
 \end{alltt}
 
-\noindent This inductive predicate characterize those elements $x$ of
+\noindent This inductive predicate characterizes those elements $x$ of
 $A$ such that any descending $R$-chain $\ldots x_2\;R\;x_1\;R\;x$
 starting from $x$ is finite. A well-founded relation is a relation
 such that all the elements of $A$ are accessible.  
@@ -3121,11 +3121,11 @@ equality \citecoq{JMeq} \cite{conor:motive}
 which allows us to consider terms of different types, even if this
 equality can only be proven for terms in the same type.
 The axiom \citecoq{JMeq\_eq}, from the library \citecoq{JMeq} allows us to convert a
-heterogeneous equality to a standard one \footnote{At this date (July 28th 2006), the type of JMeq still uses Set instead of Type; the two following theorems are thus less generic than we can expect}.
+heterogeneous equality to a standard one.
 
 \begin{alltt}
 Lemma vector0_is_vnil_aux : 
-   {\prodsym} (A:Set)(n:nat)(v:vector A n), 
+   {\prodsym} (A:Type)(n:nat)(v:vector A n), 
       n= 0 {\arrow} JMeq v (Vnil A).
 Proof.
  destruct v.
@@ -3137,7 +3137,7 @@ Qed.
 Our property of vectors of null length can be easily proven:
 
 \begin{alltt}
-Lemma vector0_is_vnil : {\prodsym} (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : {\prodsym} (A:Type)(v:vector A 0), v = Vnil A.
  intros a v;apply JMeq_eq.
  apply vector0_is_vnil_aux.
  trivial.
diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v
index d79b85df1..7bede1737 100644
--- a/doc/RecTutorial/RecTutorial.v
+++ b/doc/RecTutorial/RecTutorial.v
@@ -1,3 +1,7 @@
+Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3).
+
+
+
 Inductive nat : Set := 
  | O : nat 
  | S : nat->nat.
@@ -31,10 +35,17 @@ Qed.
 
 Lemma zero_lt_three : 0 < 3.
 Proof.
- unfold lt.
  repeat constructor. 
 Qed.
 
+Print zero_lt_three.
+
+Inductive le'(n:nat):nat -> Prop :=
+ | le'_n : le' n n
+ | le'_S : forall p, le' (S n) p -> le' n p.
+
+Hint Constructors le'.
+
 
 Require Import List.
 
@@ -46,12 +57,15 @@ Check (nil (A:=nat)).
 
 Check (nil (A:= nat -> nat)).
 
-Check (fun A: Set => (cons (A:=A))).
+Check (fun A: Type => (cons (A:=A))).
 
 Check (cons 3 (cons 2 nil)).
 
+Check (nat :: bool ::nil).
 
+Check ((3<=4) :: True ::nil).
 
+Check (Prop::Set::nil).
 
 Require Import Bvector.
 
@@ -59,22 +73,10 @@ Print vector.
 
 Check (Vnil nat).
 
-Check (fun (A:Set)(a:A)=> Vcons _ a _ (Vnil _)).
+Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)).
 
 Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
 
-
-
-
-
-
-
-
-
-
-
-
-
 Lemma eq_3_3 : 2 + 1 = 3.
 Proof.
  reflexivity.
@@ -151,10 +153,10 @@ Extraction max.
 
 
 
-Inductive tree(A:Set)   : Set :=
+Inductive tree(A:Type)   : Type :=
     node : A -> forest A -> tree A 
 with
-  forest (A: Set)    : Set := 
+  forest (A: Type)    : Type := 
     nochild  : forest A |
     addchild : tree A -> forest A -> forest A.
 
@@ -315,13 +317,13 @@ Proof.
 Qed.
 
 Definition Vtail_total 
-   (A : Set) (n : nat) (v : vector A n) : vector A (pred n):=
+   (A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
 match v in (vector _ n0) return (vector A (pred n0)) with
 | Vnil => Vnil A
 | Vcons _ n0 v0 => v0
 end.
 
-Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
+Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n).
  intros A n v; case v.  
  simpl.
  exact (Vnil A).
@@ -461,9 +463,7 @@ Inductive ltree  (A:Set) : Set :=
 Inductive prop : Prop :=
  prop_intro : Prop -> prop.
 
-Lemma prop_inject: prop.
-Proof prop_intro prop.
-
+Check (prop_intro prop).
 
 Inductive ex_Prop  (P : Prop -> Prop) : Prop :=
   exP_intro : forall X : Prop, P X -> ex_Prop P.
@@ -492,27 +492,6 @@ because proofs can be eliminated only to build proofs
 
 *)
 
-(*
-Check (match prop_inject with (prop_intro P p) => P end).
-
-Error:
-Incorrect elimination of "prop_inject" in the inductive type  
-"prop", the return type has sort "Type" while it should be 
-"Prop"
-
-Elimination of an inductive object of sort "Prop"
-is not allowed on a predicate in sort "Type"
-because proofs can be eliminated only to build proofs
-
-*)
-Print prop_inject.
-
-(*
-prop_inject = 
-prop_inject = prop_intro prop (fun H : prop => H)
-     : prop
-*)
-
 
 Inductive  typ : Type := 
   typ_intro : Type -> typ. 
@@ -645,7 +624,7 @@ Qed.
  apply inj_pred with (n:= S n) (m := S m); assumption.
 Qed.
 
-Lemma list_inject : forall (A:Set)(a b :A)(l l':list A),
+Lemma list_inject : forall (A:Type)(a b :A)(l l':list A),
                      a :: b :: l = b :: a :: l' -> a = b /\ l = l'.
 Proof.
  intros A a b l l' e.
@@ -812,20 +791,20 @@ Fixpoint nat_double_ind (n m:nat){struct n} : P n m :=
 End Principle_of_Double_Induction.
 
 Section Principle_of_Double_Recursion.
-Variable    P               : nat -> nat -> Set.
+Variable    P               : nat -> nat -> Type.
 Hypothesis  base_case1      : forall x:nat, P 0 x.
 Hypothesis  base_case2      : forall x:nat, P (S x) 0.
 Hypothesis  inductive_step   : forall n m:nat, P n m -> P (S n) (S m).
-Fixpoint nat_double_rec (n m:nat){struct n} : P n m := 
+Fixpoint nat_double_rect (n m:nat){struct n} : P n m := 
   match n, m return P n m with 
          |   0 ,     x    =>  base_case1 x 
          |  (S x),    0   => base_case2 x
-         |  (S x), (S y)  => inductive_step x y (nat_double_rec x y)
+         |  (S x), (S y)  => inductive_step x y (nat_double_rect x y)
      end.
 End Principle_of_Double_Recursion.
 
 Definition min : nat -> nat -> nat  := 
-  nat_double_rec (fun (x y:nat) => nat)
+  nat_double_rect (fun (x y:nat) => nat)
                  (fun (x:nat) => 0)
                  (fun (y:nat) => 0)
                  (fun (x y r:nat) => S r).
@@ -846,10 +825,10 @@ Qed.
 Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
 Proof.
  intros n p.
- apply nat_double_rec with (P:= fun (n q:nat) => {q=p}+{q <> p}).
+ apply nat_double_rect with (P:= fun (n q:nat) => {q=p}+{q <> p}).
 Undo.
  pattern p,n.
- elim n using nat_double_rec.
+ elim n using nat_double_rect.
  destruct x; auto.
  destruct x; auto.
  intros n0 m H; case H.
@@ -861,6 +840,28 @@ Definition eq_nat_dec' : forall n p:nat, {n=p}+{n <> p}.
  decide equality.
 Defined.
 
+
+
+Require Import Le.
+Lemma le'_le : forall n p, le' n p -> n <= p.
+Proof.
+ induction 1;auto with arith.
+Qed.
+
+Lemma le'_n_Sp : forall n p, le' n p -> le' n (S p).
+Proof.
+ induction 1;auto.
+Qed.
+
+Hint Resolve le'_n_Sp.
+
+ 
+Lemma le_le' : forall n p, n<=p -> le' n p.
+Proof.
+ induction 1;auto with arith.
+Qed. 
+
+
 Print Acc.
 
 
@@ -968,13 +969,13 @@ let rec div_aux x y =
            | Right -> div_aux (minus x y) y)
 *)
 
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
 Proof.
  intros A v;inversion v.
 Abort.
 
 (*
- Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), 
+ Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), 
                                   n= 0 -> v = Vnil A.
 
 Toplevel input, characters 40281-40287
@@ -990,7 +991,10 @@ The term "Vnil A" has type "vector A 0" while it is expected to have type
 *)
  Require Import JMeq.
 
-Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), 
+
+(* On devrait changer Set en Type ? *)
+
+Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n), 
                                   n= 0 -> JMeq v (Vnil A).
 Proof.
  destruct v.
@@ -998,7 +1002,7 @@ Proof.
  intro; discriminate.
 Qed.
 
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
 Proof.
  intros a v;apply JMeq_eq.
  apply vector0_is_vnil_aux.
@@ -1011,20 +1015,20 @@ Implicit Arguments Vnil [A].
 Implicit Arguments Vhead [A n].
 Implicit Arguments Vtail [A n].
 
-Definition Vid : forall (A : Set)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
 Proof.
  destruct n; intro v.
  exact Vnil.
  exact (Vcons  (Vhead v) (Vtail v)).
 Defined.
 
-Eval simpl in (fun (A:Set)(v:vector A 0) => (Vid _ _ v)).
+Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)).
 
-Eval simpl in (fun (A:Set)(v:vector A 0) => v).
+Eval simpl in (fun (A:Type)(v:vector A 0) => v).
 
 
 
-Lemma Vid_eq : forall (n:nat) (A:Set)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
 Proof.
  destruct v. 
  reflexivity.
@@ -1040,7 +1044,7 @@ Defined.
 
 
 Theorem decomp :
-  forall (A : Set) (n : nat) (v : vector A (S n)),
+  forall (A : Type) (n : nat) (v : vector A (S n)),
   v = Vcons (Vhead v) (Vtail v).
 Proof.
  intros.
@@ -1051,7 +1055,7 @@ Defined.
 
 
 Definition vector_double_rect : 
-    forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
+    forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
         P 0 Vnil Vnil ->
         (forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
              P (S n) (Vcons a v1) (Vcons  b v2)) ->
@@ -1071,7 +1075,7 @@ Definition bitwise_or n v1 v2 : vector bool n :=
                         (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
 
 
-Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:vector A p){struct v}
+Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v}
                   : option A :=
   match n,v  with
     _   , Vnil => None
@@ -1097,10 +1101,10 @@ Qed.
 
  Set Implicit Arguments.
 
- CoInductive Stream (A:Set) : Set   :=
+ CoInductive Stream (A:Type) : Type   :=
  |  Cons : A -> Stream A -> Stream A.
 
- CoInductive LList (A: Set) : Set :=
+ CoInductive LList (A: Type) : Type :=
  |  LNil : LList A
  |  LCons : A -> LList A -> LList A.
 
@@ -1108,25 +1112,25 @@ Qed.
  
 
 
- Definition head (A:Set)(s : Stream A) := match s with Cons a s' => a end.
+ Definition head (A:Type)(s : Stream A) := match s with Cons a s' => a end.
 
- Definition tail (A : Set)(s : Stream A) :=
+ Definition tail (A : Type)(s : Stream A) :=
       match s with Cons a s' => s' end.
 
- CoFixpoint repeat (A:Set)(a:A) : Stream A := Cons a (repeat a).
+ CoFixpoint repeat (A:Type)(a:A) : Stream A := Cons a (repeat a).
 
- CoFixpoint iterate (A: Set)(f: A -> A)(a : A) : Stream A:=
+ CoFixpoint iterate (A: Type)(f: A -> A)(a : A) : Stream A:=
     Cons a (iterate f (f a)).
 
- CoFixpoint map (A B:Set)(f: A -> B)(s : Stream A) : Stream B:=
+ CoFixpoint map (A B:Type)(f: A -> B)(s : Stream A) : Stream B:=
   match s with Cons a tl => Cons (f a) (map f tl) end.
 
-Eval simpl in (fun (A:Set)(a:A) => repeat a).
+Eval simpl in (fun (A:Type)(a:A) => repeat a).
 
-Eval simpl in (fun (A:Set)(a:A) => head (repeat a)).
+Eval simpl in (fun (A:Type)(a:A) => head (repeat a)).
 
 
-CoInductive EqSt (A: Set) : Stream A -> Stream A -> Prop :=
+CoInductive EqSt (A: Type) : Stream A -> Stream A -> Prop :=
   eqst : forall s1 s2: Stream A,
       head s1 = head s2 ->
       EqSt (tail s1) (tail s2) ->
@@ -1134,7 +1138,7 @@ CoInductive EqSt (A: Set) : Stream A -> Stream A -> Prop :=
 
 
 Section Parks_Principle.
-Variable A : Set.
+Variable A : Type.
 Variable    R      : Stream A -> Stream A -> Prop.
 Hypothesis  bisim1 : forall s1 s2:Stream A, R s1 s2 ->
                                           head s1 = head s2.
@@ -1149,7 +1153,7 @@ CoFixpoint park_ppl     : forall s1 s2:Stream A, R s1 s2 ->
 End Parks_Principle.
 
 
-Theorem map_iterate : forall (A:Set)(f:A->A)(x:A),
+Theorem map_iterate : forall (A:Type)(f:A->A)(x:A),
                        EqSt (iterate f (f x)) (map f (iterate f x)).
 Proof.
  intros A f x.
@@ -1167,7 +1171,7 @@ Ltac infiniteproof f :=
   cofix f; constructor; [clear f| simpl; try (apply f; clear f)].
 
 
-Theorem map_iterate' : forall (A:Set)(f:A->A)(x:A),
+Theorem map_iterate' : forall (A:Type)(f:A->A)(x:A),
                        EqSt (iterate f (f x)) (map f (iterate f x)).
 infiniteproof map_iterate'.
  reflexivity.
@@ -1176,12 +1180,12 @@ Qed.
 
 Implicit Arguments LNil [A].
 
-Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
+Lemma Lnil_not_Lcons : forall (A:Type)(a:A)(l:LList A),
                                LNil <> (LCons a l).
  intros;discriminate.
 Qed.
 
-Lemma injection_demo : forall (A:Set)(a b : A)(l l': LList A),
+Lemma injection_demo : forall (A:Type)(a b : A)(l l': LList A),
                        LCons a (LCons b l) = LCons b (LCons a l') ->
                        a = b /\ l = l'.
 Proof.
@@ -1189,19 +1193,19 @@ Proof.
 Qed.
 
 
-Inductive Finite (A:Set) : LList A -> Prop :=
+Inductive Finite (A:Type) : LList A -> Prop :=
 |  Lnil_fin : Finite (LNil (A:=A))
 |  Lcons_fin : forall a l, Finite l -> Finite (LCons a l).
 
-CoInductive Infinite  (A:Set) : LList A -> Prop :=
+CoInductive Infinite  (A:Type) : LList A -> Prop :=
 | LCons_inf : forall a l, Infinite l -> Infinite (LCons a l).
 
-Lemma LNil_not_Infinite : forall (A:Set), ~ Infinite (LNil (A:=A)).
+Lemma LNil_not_Infinite : forall (A:Type), ~ Infinite (LNil (A:=A)).
 Proof.
   intros A H;inversion H.
 Qed.
 
-Lemma Finite_not_Infinite : forall (A:Set)(l:LList A),
+Lemma Finite_not_Infinite : forall (A:Type)(l:LList A),
                                 Finite l -> ~ Infinite l.
 Proof.
  intros A l H; elim H.
@@ -1211,7 +1215,7 @@ Proof.
  trivial.
 Qed.
 
-Lemma Not_Finite_Infinite : forall (A:Set)(l:LList A),
+Lemma Not_Finite_Infinite : forall (A:Type)(l:LList A),
                             ~ Finite l -> Infinite l.
 Proof.
  cofix H.
@@ -1226,4 +1230,3 @@ Qed.
 
 
 
-