summaryrefslogtreecommitdiff
path: root/test-suite/success/RecTutorial.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/RecTutorial.v')
-rw-r--r--test-suite/success/RecTutorial.v171
1 files changed, 79 insertions, 92 deletions
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d4e6a82e..459645f6 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -1,3 +1,5 @@
+Module Type LocalNat.
+
Inductive nat : Set :=
| O : nat
| S : nat->nat.
@@ -5,7 +7,8 @@ Check nat.
Check O.
Check S.
-Reset nat.
+End LocalNat.
+
Print nat.
@@ -55,13 +58,13 @@ Check (cons 3 (cons 2 nil)).
Require Import Bvector.
-Print vector.
+Print Vector.t.
-Check (Vnil nat).
+Check (Vector.nil nat).
-Check (fun (A:Set)(a:A)=> Vcons _ a _ (Vnil _)).
+Check (fun (A:Set)(a:A)=> Vector.cons _ a _ (Vector.nil _)).
-Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))).
@@ -315,16 +318,16 @@ Proof.
Qed.
Definition Vtail_total
- (A : Set) (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
+ (A : Set) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):=
+match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with
+| Vector.nil => Vector.nil A
+| Vector.cons _ n0 v0 => v0
end.
-Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
+Definition Vtail' (A:Set)(n:nat)(v:Vector.t A n) : Vector.t A (pred n).
case v.
simpl.
- exact (Vnil A).
+ exact (Vector.nil A).
simpl.
auto.
Defined.
@@ -375,18 +378,18 @@ Inductive itree : Set :=
Definition isingle l := inode l (fun i => ileaf).
-Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
+Definition t1 := inode 0 (fun n => isingle (Z.of_nat (2*n))).
Definition t2 := inode 0
(fun n : nat =>
- inode (Z_of_nat n)
- (fun p => isingle (Z_of_nat (n*p)))).
+ inode (Z.of_nat n)
+ (fun p => isingle (Z.of_nat (n*p)))).
Inductive itree_le : itree-> itree -> Prop :=
| le_leaf : forall t, itree_le ileaf t
| le_node : forall l l' s s',
- Zle l l' ->
+ Z.le l l' ->
(forall i, exists j:nat, itree_le (s i) (s' j)) ->
itree_le (inode l s) (inode l' s').
@@ -421,7 +424,7 @@ Qed.
Inductive itree_le' : itree-> itree -> Prop :=
| le_leaf' : forall t, itree_le' ileaf t
| le_node' : forall l l' s s' g,
- Zle l l' ->
+ Z.le l l' ->
(forall i, itree_le' (s i) (s' (g i))) ->
itree_le' (inode l s) (inode l' s').
@@ -477,10 +480,10 @@ Qed.
-(*
-Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
+Fail Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
match p with exP_intro X HX => X end).
+(*
Error:
Incorrect elimination of "p" in the inductive type
"ex_Prop", the return type has sort "Type" while it should be
@@ -489,12 +492,11 @@ Incorrect elimination of "p" in the inductive type
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
-
*)
-(*
-Check (match prop_inject with (prop_intro P p) => P end).
+Fail Check (match prop_inject with (prop_intro p) => p end).
+(*
Error:
Incorrect elimination of "prop_inject" in the inductive type
"prop", the return type has sort "Type" while it should be
@@ -503,13 +505,12 @@ Incorrect elimination of "prop_inject" in the inductive type
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_inject = prop_intro prop
: prop
*)
@@ -520,30 +521,28 @@ Inductive typ : Type :=
Definition typ_inject: typ.
split.
exact typ.
+Fail Defined.
(*
-Defined.
-
Error: Universe Inconsistency.
*)
Abort.
-(*
-Inductive aSet : Set :=
+Fail Inductive aSet : Set :=
aSet_intro: Set -> aSet.
-
-
+(*
User error: Large non-propositional inductive types must be in Type
-
*)
Inductive ex_Set (P : Set -> Prop) : Type :=
exS_intro : forall X : Set, P X -> ex_Set P.
+Module Type Version1.
+
Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
-Goal (comes_from_the_left _ _ (or_introl True I)).
+Goal (comes_from_the_left _ _ (or_introl True I)).
split.
Qed.
@@ -553,21 +552,15 @@ Goal ~(comes_from_the_left _ _ (or_intror True I)).
*)
Abort.
-Reset comes_from_the_left.
-
-(*
+End Version1.
-
-
-
-
-
- Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
+Fail Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
match H with
| or_introl p => True
| or_intror q => False
end.
+(*
Error:
Incorrect elimination of "H" in the inductive type
"or", the return type has sort "Type" while it should be
@@ -576,7 +569,6 @@ Incorrect elimination of "H" in the inductive type
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
-
*)
Definition comes_from_the_left_sumbool
@@ -737,6 +729,7 @@ Fixpoint plus'' (n p:nat) {struct n} : nat :=
| S m => plus'' m (S p)
end.
+Module Type even_test_v1.
Fixpoint even_test (n:nat) : bool :=
match n
@@ -745,8 +738,9 @@ Fixpoint even_test (n:nat) : bool :=
| S (S p) => even_test p
end.
+End even_test_v1.
-Reset even_test.
+Module even_test_v2.
Fixpoint even_test (n:nat) : bool :=
match n
@@ -761,12 +755,8 @@ with odd_test (n:nat) : bool :=
| S p => even_test p
end.
-
-
Eval simpl in even_test.
-
-
Eval simpl in (fun x : nat => even_test x).
Eval simpl in (fun x : nat => plus 5 x).
@@ -774,6 +764,8 @@ Eval simpl in (fun x : nat => even_test (plus 5 x)).
Eval simpl in (fun x : nat => even_test (plus x 5)).
+End even_test_v2.
+
Section Principle_of_Induction.
Variable P : nat -> Prop.
@@ -866,14 +858,13 @@ Print Acc.
Require Import Minus.
-(*
-Fixpoint div (x y:nat){struct x}: nat :=
+Fail Fixpoint div (x y:nat){struct x}: nat :=
if eq_nat_dec x 0
then 0
else if eq_nat_dec y 0
then x
else S (div (x-y) y).
-
+(*
Error:
Recursive definition of div is ill-formed.
In environment
@@ -966,37 +957,33 @@ 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:Set)(v:Vector.t A 0), v = Vector.nil A.
Proof.
intros A v;inversion v.
Abort.
-(*
- Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
- n= 0 -> v = Vnil A.
-Toplevel input, characters 40281-40287
-> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A.
-> ^^^^^^
+Fail Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
+ n= 0 -> v = Vector.nil A.
+(*
Error: In environment
A : Set
n : nat
-v : vector A n
-e : n = 0
-The term "Vnil A" has type "vector A 0" while it is expected to have type
- "vector A n"
+v : Vector.t A n
+The term "[]" has type "Vector.t A 0" while it is expected to have type
+ "Vector.t A n"
*)
Require Import JMeq.
-Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
- n= 0 -> JMeq v (Vnil A).
+Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
+ n= 0 -> JMeq v (Vector.nil A).
Proof.
destruct v.
auto.
intro; discriminate.
Qed.
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
Proof.
intros a v;apply JMeq_eq.
apply vector0_is_vnil_aux.
@@ -1004,56 +991,56 @@ Proof.
Qed.
-Implicit Arguments Vcons [A n].
-Implicit Arguments Vnil [A].
-Implicit Arguments Vhead [A n].
-Implicit Arguments Vtail [A n].
+Implicit Arguments Vector.cons [A n].
+Implicit Arguments Vector.nil [A].
+Implicit Arguments Vector.hd [A n].
+Implicit Arguments Vector.tl [A n].
-Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
Proof.
destruct n; intro v.
- exact Vnil.
- exact (Vcons (Vhead v) (Vtail v)).
+ exact Vector.nil.
+ exact (Vector.cons (Vector.hd v) (Vector.tl v)).
Defined.
-Eval simpl in (fun (A:Set)(v:vector A 0) => (Vid _ _ v)).
+Eval simpl in (fun (A:Set)(v:Vector.t A 0) => (Vid _ _ v)).
-Eval simpl in (fun (A:Set)(v:vector A 0) => v).
+Eval simpl in (fun (A:Set)(v:Vector.t A 0) => v).
-Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v).
Proof.
destruct v.
reflexivity.
reflexivity.
Defined.
-Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
+Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil.
Proof.
intros.
- change (Vnil (A:=A)) with (Vid _ 0 v).
+ change (Vector.nil (A:=A)) with (Vid _ 0 v).
apply Vid_eq.
Defined.
Theorem decomp :
- forall (A : Set) (n : nat) (v : vector A (S n)),
- v = Vcons (Vhead v) (Vtail v).
+ forall (A : Set) (n : nat) (v : Vector.t A (S n)),
+ v = Vector.cons (Vector.hd v) (Vector.tl v).
Proof.
intros.
- change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
+ change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _ (S n) v).
apply Vid_eq.
Defined.
Definition vector_double_rect :
- forall (A:Set) (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)) ->
- forall n (v1 v2 : vector A n), P n v1 v2.
+ forall (A:Set) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type),
+ P 0 Vector.nil Vector.nil ->
+ (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 ->
+ P (S n) (Vector.cons a v1) (Vector.cons b v2)) ->
+ forall n (v1 v2 : Vector.t A n), P n v1 v2.
induction n.
intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
auto.
@@ -1063,24 +1050,24 @@ Defined.
Require Import Bool.
-Definition bitwise_or n v1 v2 : vector bool n :=
- vector_double_rect bool (fun n v1 v2 => vector bool n)
- Vnil
- (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
+Definition bitwise_or n v1 v2 : Vector.t bool n :=
+ vector_double_rect bool (fun n v1 v2 => Vector.t bool n)
+ Vector.nil
+ (fun n v1 v2 a b r => Vector.cons (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:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v}
: option A :=
match n,v with
- _ , Vnil => None
- | 0 , Vcons b _ _ => Some b
- | S n', Vcons _ p' v' => vector_nth A n' p' v'
+ _ , Vector.nil => None
+ | 0 , Vector.cons b _ _ => Some b
+ | S n', Vector.cons _ p' v' => vector_nth A n' p' v'
end.
Implicit Arguments vector_nth [A p].
-Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b,
+Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b,
vector_nth i v1 = Some a ->
vector_nth i v2 = Some b ->
vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 06:43:15 +0000