diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /test-suite/success/RecTutorial.v | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'test-suite/success/RecTutorial.v')
-rw-r--r-- | test-suite/success/RecTutorial.v | 171 |
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). |