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 | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'test-suite/success')
67 files changed, 1994 insertions, 538 deletions
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v index b533db6e..97cf316c 100644 --- a/test-suite/success/AdvancedCanonicalStructure.v +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -79,19 +79,17 @@ Record interp_pair :Type := link: abs = interp repr }. Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) . -proof. -let a:interp_pair,b:interp_pair. -reconsider thesis as (a * b = interp a * interp b). -thus thesis by (link a),(link b). -end proof. +Proof. +intros a b. +change (a * b = interp a * interp b). +rewrite (link a), (link b); reflexivity. Qed. Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b). -proof. -let a:interp_pair,b:interp_pair. -reconsider thesis as ((a -> b) = (interp a -> interp b)). -thus thesis using rewrite (link a);rewrite (link b);reflexivity. -end proof. +Proof. +intros a b. +change ((a -> b) = (interp a -> interp b)). +rewrite (link a), (link b); reflexivity. Qed. Canonical Structure ProdCan (a b:interp_pair) := diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v index 32d85779..a9249086 100644 --- a/test-suite/success/CaseAlias.v +++ b/test-suite/success/CaseAlias.v @@ -1,3 +1,4 @@ +(*********************************************) (* This has been a bug reported by Y. Bertot *) Inductive expr : Set := | b : expr -> expr -> expr @@ -19,3 +20,72 @@ Fixpoint f2 (t : expr) : expr := | x => b x a end. +(*********************************************) +(* Test expansion of aliases *) +(* Originally taken from NMake_gen.v *) + + Local Notation SizePlus n := (S (S (S (S (S (S n)))))). + Local Notation Size := (SizePlus O). + + Parameter zn2z : Type -> Type. + Parameter w0 : Type. + Fixpoint word (w : Type) (n : nat) {struct n} : Type := + match n with + | 0 => w + | S n0 => zn2z (word w n0) + end. + + Definition w1 := zn2z w0. + Definition w2 := zn2z w1. + Definition w3 := zn2z w2. + Definition w4 := zn2z w3. + Definition w5 := zn2z w4. + Definition w6 := zn2z w5. + + Definition dom_t n := match n with + | 0 => w0 + | 1 => w1 + | 2 => w2 + | 3 => w3 + | 4 => w4 + | 5 => w5 + | 6 => w6 + | SizePlus n => word w6 n + end. +Parameter plus_t : forall n m : nat, word (dom_t n) m -> dom_t (m + n). + +(* This used to fail because of a bug in expansion of SizePlus wrongly + reusing n as an alias for the subpattern *) +Definition plus_t1 n : forall m, word (dom_t n) m -> dom_t (m+n) := + match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with + | SizePlus (S n') as n => plus_t n + | _ as n => + fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with + | SizePlus (S (S m')) as m => plus_t n m + | _ => fun x => x + end + end. + +(* Test (useless) intermediate alias *) +Definition plus_t2 n : forall m, word (dom_t n) m -> dom_t (m+n) := + match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with + | S (S (S (S (S (S (S n'))))) as n) as n'' => plus_t n'' + | _ as n => + fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with + | SizePlus (S (S m')) as m => plus_t n m + | _ => fun x => x + end + end. + +(*****************************************************************************) +(* Check that alias expansion behaves consistently from versions to versions *) + +Definition g m := + match pred m with + | 0 => 0 + | n => n (* For compatibility, right-hand side should be (S n), not (pred m) *) + end. + +Goal forall m, g m = match pred m with 0 => 0 | S n => S n end. +intro; reflexivity. +Abort. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index e63972ce..c9a3c08e 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -100,7 +100,7 @@ Type (fun x : nat => match x return nat with | x => x end). -Section testlist. +Module Type testlist. Parameter A : Set. Inductive list : Set := | nil : list @@ -119,7 +119,6 @@ Definition titi (a : A) (l : list) := | nil => l | cons b l => l end. -Reset list. End testlist. @@ -543,7 +542,7 @@ Type end). (* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe - * it has to synthtize the predicate on O (which he can't) + * it has to synthesize the predicate on O (which he can't) *) Type match 0 as n return match n with @@ -611,31 +610,52 @@ Type | Consn n a (Consn m b l) => n + m end). -(* -Type [A:Set][n:nat][l:(Listn A n)] - <[_:nat](Listn A O)>Cases l of - (Niln as b) => b - | (Consn n a (Niln as b))=> (Niln A) - | (Consn n a (Consn m b l)) => (Niln A) - end. - -Type [A:Set][n:nat][l:(Listn A n)] - Cases l of - (Niln as b) => b - | (Consn n a (Niln as b))=> (Niln A) - | (Consn n a (Consn m b l)) => (Niln A) - end. +(* This example was deactivated in Cristina's code + +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l return Listn A O with + | Niln as b => b + | Consn n a (Niln as b) => (Niln A) + | Consn n a (Consn m b l) => (Niln A) + end). +*) + +(* This one is (still) failing: too weak unification + +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l with + | Niln as b => b + | Consn n a (Niln as b) => (Niln A) + | Consn n a (Consn m b l) => (Niln A) + end). +*) + +(* This one is failing: alias L not chosen of the right type + +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l return Listn A (S 0) with + | Niln as b => Consn A O O b + | Consn n a Niln as L => L + | Consn n a _ => Consn A O O (Niln A) + end). *) -(******** This example rises an error unconstrained_variables! -Type [A:Set][n:nat][l:(Listn A n)] - Cases l of - (Niln as b) => (Consn A O O b) - | ((Consn n a Niln) as L) => L - | (Consn n a _) => (Consn A O O (Niln A)) - end. + +(******** This example (still) failed + +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l return Listn A (S 0) with + | Niln as b => Consn A O O b + | Consn n a Niln as L => L + | Consn n a _ => Consn A O O (Niln A) + end). + **********) -(* To test tratement of as-patterns in depth *) +(* To test treatment of as-patterns in depth *) Type (fun (A : Set) (l : List A) => match l with @@ -892,71 +912,77 @@ Type | LeS n m _ => (S n, S m) end). - +Module Type F_v1. Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) := match h in (Le n m) return (Le n (S m)) with | LeO m' => LeO (S m') | LeS n' m' h' => LeS n' (S m') (F n' m' h') end. +End F_v1. -Reset F. - +Module Type F_v2. Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) := match h in (Le n m) return (Le n (S m)) with | LeS n m h => LeS n (S m) (F n m h) | LeO m => LeO (S m) end. +End F_v2. (* Rend la longueur de la liste *) -Definition length1 (n : nat) (l : listn n) := + +Module Type L1. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => 1 | _ => 0 end. +End L1. -Reset length1. -Definition length1 (n : nat) (l : listn n) := +Module Type L1'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => 1 | _ => 0 end. +End L1'. - -Definition length2 (n : nat) (l : listn n) := +Module Type L2. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => S n | _ => 0 end. +End L2. -Reset length2. - -Definition length2 (n : nat) (l : listn n) := +Module Type L2'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ _) => S (S m) | consn n _ _ => S n | _ => 0 end. +End L2'. -Definition length3 (n : nat) (l : listn n) := +Module Type L3. +Definition length (n : nat) (l : listn n) := match l return nat with | consn n _ (consn m _ l) => S n | consn n _ _ => 1 | _ => 0 end. +End L3. - -Reset length3. - -Definition length3 (n : nat) (l : listn n) := +Module Type L3'. +Definition length (n : nat) (l : listn n) := match l with | consn n _ (consn m _ l) => S n | consn n _ _ => 1 | _ => 0 end. - +End L3'. Type match LeO 0 return nat with | LeS n m h => n + m @@ -1064,7 +1090,7 @@ Type | Consn n a (Consn m b l) => fun _ : nat => n + m end). -(* Alsos tests for multiple _ patterns *) +(* Also tests for multiple _ patterns *) Type (fun (A : Set) (n : nat) (l : Listn A n) => match l in (Listn _ n) return (Listn A n) with @@ -1072,14 +1098,14 @@ Type | Consn _ _ _ as b => b end). -(** Horrible error message! +(** This one was said to raised once an "Horrible error message!" *) -Type [A:Set][n:nat][l:(Listn A n)] - Cases l of - (Niln as b) => b - | ((Consn _ _ _ ) as b)=> b - end. -******) +Type + (fun (A:Set) (n:nat) (l:Listn A n) => + match l with + | Niln as b => b + | Consn _ _ _ as b => b + end). Type match niln in (listn n) return (listn n) with @@ -1235,7 +1261,7 @@ Type match (0, 0) with | (x, y) => (S x, S y) end. - +Module Type test_concat. Parameter concat : forall A : Set, List A -> List A -> List A. @@ -1252,6 +1278,7 @@ Type | _, _ => Nil nat end. +End test_concat. Inductive redexes : Set := | VAR : nat -> redexes @@ -1274,7 +1301,6 @@ Type (fun n : nat => match n with | _ => 0 end). -Reset concat. Parameter concat : forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m). @@ -1362,6 +1388,7 @@ Type (* I.e. to test manipulation of elimination predicate *) (* ===================================================================== *) +Module Type test_term. Parameter LTERM : nat -> Set. Inductive TERM : Type := @@ -1376,7 +1403,8 @@ Type | oper op1 l1, oper op2 l2 => False | _, _ => False end. -Reset LTERM. + +End test_term. @@ -1472,6 +1500,7 @@ Type end. +Module Type ff. Parameter ff : forall n m : nat, n <> m -> S n <> S m. Parameter discr_r : forall n : nat, 0 <> S n. @@ -1484,6 +1513,7 @@ Type | S x => or_intror (S x = 0) (discr_l x) end). +Module Type eqdec. Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := match n, m return (n = m \/ n <> m) with @@ -1497,7 +1527,9 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := end end. -Reset eqdec. +End eqdec. + +Module Type eqdec'. Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := match n return (forall m : nat, n = m \/ n <> m) with @@ -1519,6 +1551,7 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := end end. +End eqdec'. Inductive empty : forall n : nat, listn n -> Prop := intro_empty : empty 0 niln. @@ -1533,7 +1566,10 @@ Type | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y) end). -Reset ff. +End ff. + +Module Type ff'. + Parameter ff : forall n m : nat, n <> m -> S n <> S m. Parameter discr_r : forall n : nat, 0 <> S n. Parameter discr_l : forall n : nat, S n <> 0. @@ -1545,6 +1581,7 @@ Type | S x => or_intror (S x = 0) (discr_l x) end). +Module Type eqdec. Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := match n, m return (n = m \/ n <> m) with @@ -1557,7 +1594,10 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := | or_intror h => or_intror (S x = S y) (ff x y h) end end. -Reset eqdec. + +End eqdec. + +Module Type eqdec'. Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := match n return (forall m : nat, n = m \/ n <> m) with @@ -1579,6 +1619,8 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := end end. +End eqdec'. +End ff'. (* ================================================== *) (* Pour tester parametres *) @@ -1823,3 +1865,9 @@ Type (fun n => match n with | Z0 => true | _ => false end). + +(* Check that types with unknown sort, as A below, are not fatal to + the pattern-matching compilation *) + +Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y := + match p with eq_refl => u end. diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 29721843..bfead53c 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -26,6 +26,40 @@ Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C := end. End Folding. +(** Testing post-processing of nested dependencies *) + +Check fun x:{x|x=0}*nat+nat => match x with + | inl ((exist 0 eq_refl),0) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + +Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with + | inl (exist (exist 0 eq_refl) I) => None + | _ => Some 0 + end. + + (* the next two examples were failing from r14703 (Nov 22 2011) to r14732 *) + (* due to a bug in dependencies postprocessing (revealed by CoLoR) *) + +Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with + | exist2 (x,y) eq_refl I => None + end. + +Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with + | inl (exist (exist2 (x,y) eq_refl I) I) => None + | _ => Some 0 + end. + (* -------------------------------------------------------------------- *) (* Example to test patterns matching on dependent families *) (* This exemple extracted from the developement done by Nacira Chabane *) @@ -188,7 +222,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci. de l'arite de chaque operateur *) -Section Sig. +Module Sig. Record Signature : Type := {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}. @@ -243,7 +277,7 @@ Type | _, _ => False end. - +Module Type Version1. Definition equalT (t1 t2 : TERM) : Prop := match t1, t2 with @@ -260,12 +294,15 @@ Definition EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) | _, _ => False end. +End Version1. + -Reset equalT. (* ------------------------------------------------------------------*) (* Initial exemple (without patterns) *) (*-------------------------------------------------------------------*) +Module Version2. + Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 return (TERM -> Prop) with | var v1 => @@ -313,11 +350,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version2. (* ---------------------------------------------------------------- *) (* Version with simple patterns *) (* ---------------------------------------------------------------- *) -Reset equalT. + +Module Version3. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 with @@ -354,8 +393,9 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version3. -Reset equalT. +Module Version4. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 with @@ -389,10 +429,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := end end. +End Version4. + (* ---------------------------------------------------------------- *) (* Version with multiple patterns *) (* ---------------------------------------------------------------- *) -Reset equalT. + +Module Version5. Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := match t1, t2 with @@ -411,6 +454,7 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := | _, _ => False end. +End Version5. (* ------------------------------------------------------------------ *) @@ -506,3 +550,23 @@ Definition test (s:step E E) := | Step nil _ (cons E nil) _ Plus l l' => true | _ => false end. + +(* Testing regression of bug 2454 ("get" used not be type-checkable when + defined with its type constraint) *) + +Inductive K : nat -> Type := KC : forall (p q:nat), K p. + +Definition get : K O -> nat := fun x => match x with KC p q => q end. + +(* Checking correct order of substitution of realargs *) +(* (was broken from revision 14664 to 14669) *) +(* Example extracted from contrib CoLoR *) + +Inductive EQ : nat -> nat -> Prop := R x y : EQ x y. + +Check fun e t (d1 d2:EQ e t) => + match d1 in EQ e1 t1, d2 in EQ e2 t2 return + (e1,t1) = (e2,t2) -> (e1,t1) = (e,t) -> 0=0 + with + | R _ _, R _ _ => fun _ _ => eq_refl + end. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index d5b94ab4..21a9722d 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v index dffad323..a7596741 100644 --- a/test-suite/success/Discriminate.v +++ b/test-suite/success/Discriminate.v @@ -32,3 +32,9 @@ intros. ediscriminate (H O). instantiate (1:=O). Abort. + +(* Check discriminate on identity *) + +Goal ~ identity 0 1. +discriminate. +Qed. diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 08e8aed2..9301cd27 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Field.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (**** Tests of Field with real numbers ****) Require Import Reals RealField. diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index b17adef6..ccce3bbe 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -9,7 +9,7 @@ Functional Scheme iszero_ind := Induction for iszero Sort Prop. Lemma toto : forall n : nat, n = 0 -> iszero n = true. intros x eg. - functional induction iszero x; simpl in |- *. + functional induction iszero x; simpl. trivial. inversion eg. Qed. @@ -212,19 +212,19 @@ Function plus_x_not_five'' (n m : nat) {struct n} : nat := Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. intros a b. - functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto. + functional induction plus_x_not_five'' a b; intros hyp; simpl; auto. Qed. Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. intros n m. - functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto. + functional induction nat_equal_bool n m; simpl; intros hyp; auto. rewrite <- hyp in y; simpl in y;tauto. inversion hyp. Qed. Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. intros n m. - functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto. + functional induction nat_equal_bool n m; simpl; intros eg; auto. inversion eg. inversion eg. Qed. @@ -245,7 +245,7 @@ Qed. Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. intros n. -unfold plus in |- *. +unfold plus. functional induction plus n 0; intros. auto with arith. apply le_n_S. @@ -266,7 +266,7 @@ Function mod2 (n : nat) : nat := Lemma princ_mod2 : forall n : nat, mod2 n <= n. intros n. - functional induction mod2 n; simpl in |- *; auto with arith. + functional induction mod2 n; simpl; auto with arith. Qed. Function isfour (n : nat) : bool := @@ -284,7 +284,7 @@ Function isononeorfour (n : nat) : bool := Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). intros n. - functional induction isononeorfour n; intros istr; simpl in |- *; + functional induction isononeorfour n; intros istr; simpl; inversion istr. apply istrue0. destruct n. inversion istr. @@ -367,7 +367,7 @@ Function ftest2 (n m : nat) {struct n} : nat := Lemma test2' : forall n m : nat, ftest2 n m <= 2. intros n m. - functional induction ftest2 n m; simpl in |- *; intros; auto. + functional induction ftest2 n m; simpl; intros; auto. Qed. Function ftest3 (n m : nat) {struct n} : nat := @@ -387,7 +387,7 @@ auto. intros. auto. intros. -simpl in |- *. +simpl. auto. Qed. @@ -408,7 +408,7 @@ auto. intros. auto. intros. -simpl in |- *. +simpl. auto. Qed. @@ -451,7 +451,7 @@ Qed. Lemma essai6 : forall n m : nat, ftest6 n m <= 2. intros n m. - functional induction ftest6 n m; simpl in |- *; auto. + functional induction ftest6 n m; simpl; auto. Qed. (* Some tests with modules *) diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 4aa00e68..cc8cec47 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -2,31 +2,26 @@ (* Checks that qualified names are accepted *) (* New-style syntax *) -Hint Resolve refl_equal: core arith. -Hint Immediate trans_equal. -Hint Unfold sym_equal: core. +Hint Resolve eq_refl: core arith. +Hint Immediate eq_trans. +Hint Unfold eq_sym: core. Hint Constructors eq: foo bar. -Hint Extern 3 (_ = _) => apply refl_equal: foo bar. +Hint Extern 3 (_ = _) => apply eq_refl: foo bar. (* Old-style syntax *) -Hint Resolve refl_equal sym_equal. -Hint Resolve refl_equal sym_equal: foo. -Hint Immediate refl_equal sym_equal. -Hint Immediate refl_equal sym_equal: foo. -Hint Unfold fst sym_equal. -Hint Unfold fst sym_equal: foo. - -(* What's this stranged syntax ? *) -Hint Destruct h6 := 4 Conclusion (_ <= _) => fun H => apply H. -Hint Destruct h7 := 4 Discardable Hypothesis (_ <= _) => fun H => apply H. -Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H. +Hint Resolve eq_refl eq_sym. +Hint Resolve eq_refl eq_sym: foo. +Hint Immediate eq_refl eq_sym. +Hint Immediate eq_refl eq_sym: foo. +Hint Unfold fst eq_sym. +Hint Unfold fst eq_sym: foo. (* Checks that local names are accepted *) Section A. Remark Refl : forall (A : Set) (x : A), x = x. - Proof. exact refl_equal. Defined. - Definition Sym := sym_equal. - Let Trans := trans_equal. + Proof. exact @eq_refl. Defined. + Definition Sym := eq_sym. + Let Trans := eq_trans. Hint Resolve Refl: foo. Hint Resolve Sym: bar. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 203fbbb7..da5dd5e4 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -54,6 +54,15 @@ Check | Build_B x0 x1 => f x0 x1 end). +(* Check inductive types with local definitions (constructors) *) + +Inductive I1 : Set := C1 (_:I1) (_:=0). + +Check (fun x:I1 => + match x with + | C1 i n => (i,n) + end). + (* Check implicit parameters of inductive types (submitted by Pierre Casteran and also implicit in #338) *) @@ -78,3 +87,23 @@ Record P:Type := {PA:Set; PB:Set}. Definition F (p:P) := (PA p) -> (PB p). Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F. + +(* Check that test for binders capturing implicit arguments is not stronger + than needed (problem raised by Cedric Auger) *) + +Set Implicit Arguments. +Inductive bool_comp2 (b: bool): bool -> Prop := +| Opp2: forall q, (match b return Prop with + | true => match q return Prop with + true => False | + false => True end + | false => match q return Prop with + true => True | + false => False end end) -> bool_comp2 b q. + +(* This one is still to be made acceptable... + +Set Implicit Arguments. +Inductive I A : A->Prop := C a : (forall A, A) -> I a. + + *) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 5091b44c..b068f729 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -73,15 +73,15 @@ Require Import Bvector. Inductive I : nat -> Set := | C1 : I 1 - | C2 : forall k i : nat, vector (I i) k -> I i. + | C2 : forall k i : nat, Vector.t (I i) k -> I i. -Inductive SI : forall k : nat, I k -> vector nat k -> nat -> Prop := +Inductive SI : forall k : nat, I k -> Vector.t nat k -> nat -> Prop := SC2 : - forall (k i vf : nat) (v : vector (I i) k) (xi : vector nat i), + forall (k i vf : nat) (v : Vector.t (I i) k) (xi : Vector.t nat i), SI (C2 v) xi vf. Theorem SUnique : - forall (k : nat) (f : I k) (c : vector nat k) v v', + forall (k : nat) (f : I k) (c : Vector.t nat k) v v', SI f c v -> SI f c v' -> v = v'. Proof. induction 1. @@ -129,3 +129,10 @@ Proof. an inconsistent state that disturbed "inversion" *) intros. inversion H. Abort. + +(* Bug #2314 (simplified): check that errors do not show as anomalies *) + +Goal True -> True. +intro. +Fail inversion H using False. +Fail inversion foo using True_ind. diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v index 53bcc63a..d55ae384 100644 --- a/test-suite/success/LegacyField.v +++ b/test-suite/success/LegacyField.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Field.v 7693 2005-12-21 23:50:17Z herbelin $ *) - (**** Tests of Field with real numbers ****) Require Import Reals LegacyRfield. diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v index 660ca3cb..c2d87a44 100644 --- a/test-suite/success/MatchFail.v +++ b/test-suite/success/MatchFail.v @@ -12,13 +12,13 @@ Ltac compute_POS := let v := constr:X1 in match constr:v with | 1%positive => fail 1 - | _ => rewrite (BinInt.Zpos_xI v) + | _ => rewrite (BinInt.Pos2Z.inj_xI v) end | |- context [(Zpos (xO ?X1))] => let v := constr:X1 in match constr:v with | 1%positive => fail 1 - | _ => rewrite (BinInt.Zpos_xO v) + | _ => rewrite (BinInt.Pos2Z.inj_xO v) end end. diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v index 74228bbb..51516166 100644 --- a/test-suite/success/Mod_params.v +++ b/test-suite/success/Mod_params.v @@ -20,59 +20,31 @@ End Q. #trace Nametab.exists_cci;; *) -Module M. -Reset M. -Module M (X: SIG). -Reset M. -Module M (X Y: SIG). -Reset M. -Module M (X: SIG) (Y: SIG). -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG). -Reset M. -Module M (X: SIG) (Y: SIG). -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG). -Reset M. -Module M : SIG. -Reset M. -Module M (X: SIG) : SIG. -Reset M. -Module M (X Y: SIG) : SIG. -Reset M. -Module M (X: SIG) (Y: SIG) : SIG. -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG) : SIG. -Reset M. -Module M (X: SIG) (Y: SIG) : SIG. -Reset M. -Module M (X Y: SIG) (Z1 Z: SIG) : SIG. -Reset M. -Module M := F Q. -Reset M. -Module M (X: FSIG) := X Q. -Reset M. -Module M (X Y: FSIG) := X Q. -Reset M. -Module M (X: FSIG) (Y: SIG) := X Y. -Reset M. -Module M (X Y: FSIG) (Z1 Z: SIG) := X Z. -Reset M. -Module M (X: FSIG) (Y: SIG) := X Y. -Reset M. -Module M (X Y: FSIG) (Z1 Z: SIG) := X Z. -Reset M. -Module M : SIG := F Q. -Reset M. -Module M (X: FSIG) : SIG := X Q. -Reset M. -Module M (X Y: FSIG) : SIG := X Q. -Reset M. -Module M (X: FSIG) (Y: SIG) : SIG := X Y. -Reset M. -Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. -Reset M. -Module M (X: FSIG) (Y: SIG) : SIG := X Y. -Reset M. -Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. -Reset M. +Module M01. End M01. +Module M02 (X: SIG). End M02. +Module M03 (X Y: SIG). End M03. +Module M04 (X: SIG) (Y: SIG). End M04. +Module M05 (X Y: SIG) (Z1 Z: SIG). End M05. +Module M06 (X: SIG) (Y: SIG). End M06. +Module M07 (X Y: SIG) (Z1 Z: SIG). End M07. +Module M08 : SIG. End M08. +Module M09 (X: SIG) : SIG. End M09. +Module M10 (X Y: SIG) : SIG. End M10. +Module M11 (X: SIG) (Y: SIG) : SIG. End M11. +Module M12 (X Y: SIG) (Z1 Z: SIG) : SIG. End M12. +Module M13 (X: SIG) (Y: SIG) : SIG. End M13. +Module M14 (X Y: SIG) (Z1 Z: SIG) : SIG. End M14. +Module M15 := F Q. +Module M16 (X: FSIG) := X Q. +Module M17 (X Y: FSIG) := X Q. +Module M18 (X: FSIG) (Y: SIG) := X Y. +Module M19 (X Y: FSIG) (Z1 Z: SIG) := X Z. +Module M20 (X: FSIG) (Y: SIG) := X Y. +Module M21 (X Y: FSIG) (Z1 Z: SIG) := X Z. +Module M22 : SIG := F Q. +Module M23 (X: FSIG) : SIG := X Q. +Module M24 (X Y: FSIG) : SIG := X Q. +Module M25 (X: FSIG) (Y: SIG) : SIG := X Y. +Module M26 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. +Module M27 (X: FSIG) (Y: SIG) : SIG := X Y. +Module M28 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. diff --git a/test-suite/success/Mod_type.v b/test-suite/success/Mod_type.v index b847833f..d5e1a38c 100644 --- a/test-suite/success/Mod_type.v +++ b/test-suite/success/Mod_type.v @@ -17,3 +17,15 @@ Module Bar : BAR. Module Foo := Fu. End Bar. + +(* Check bug #2809: correct printing of modules with notations *) + +Module C. + Inductive test : Type := + | c1 : test + | c2 : nat -> test. + + Notation "! x" := (c2 x) (at level 50). +End C. + +Print C. (* Should print test_rect without failing *) diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 661a8757..2371d32c 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -17,10 +17,12 @@ Check (nat |= nat --> nat). (* Check that first non empty definition at an empty level can be of any associativity *) -Definition marker := O. +Module Type v1. Notation "x +1" := (S x) (at level 8, left associativity). -Reset marker. +End v1. +Module Type v2. Notation "x +1" := (S x) (at level 8, right associativity). +End v2. (* Check that empty levels (here 8 and 2 in pattern) are added in the right order *) @@ -59,3 +61,43 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end). Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). Check [ 0 ]. Check [ 0 # ; 1 ]. + +(* Check well-scoping of alpha-renaming of private binders *) +(* see bug #2248 (thanks to Marc Lasson) *) + +Notation "{ q , r | P }" := (fun (p:nat*nat) => let (q, r) := p in P). +Check (fun p => {q,r| q + r = p}). + +(* Check that declarations of empty levels are correctly backtracked *) + +Section B. +Notation "*" := 5 (at level 0) : nat_scope. +Notation "[ h ] p" := (h + p) (at level 8, p at level 9, h at level 7) : nat_scope. +End B. + +(* Should succeed *) +Definition n := 5 * 5. + +(* Check that lonely notations (here FOO) do not modify the visibility + of scoped interpretations (bug #2634 fixed in r14819) *) + +Notation "x ++++ y" := (mult x y) (at level 40). +Notation "x ++++ y" := (plus x y) : A_scope. +Open Scope A_scope. +Notation "'FOO' x" := (S x) (at level 40). +Goal (2 ++++ 3) = 5. +reflexivity. +Abort. + +(* Check correct failure handling when a non-constructor notation is + used in cases pattern (bug #2724 in 8.3 and 8.4beta) *) + +Notation "'FORALL' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + +Fail Check fun x => match x with S (FORALL x, _) => 0 end. + +(* Bug #2708: don't check for scope of variables used as binder *) + +Parameter traverse : (nat -> unit) -> (nat -> unit). +Notation traverse_var f l := (traverse (fun l => f l) l). diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v index 518d22e9..d316e4a0 100644 --- a/test-suite/success/Nsatz.v +++ b/test-suite/success/Nsatz.v @@ -1,51 +1,27 @@ -Require Import Nsatz ZArith Reals List Ring_polynom. +(* compile en user 3m39.915s sur cachalot *) +Require Import Nsatz. (* Example with a generic domain *) -Variable A: Type. -Variable Ad: Domain A. +Section test. -Definition Ari : Ring A:= (@domain_ring A Ad). -Existing Instance Ari. - -Existing Instance ring_setoid. -Existing Instance ring_plus_comp. -Existing Instance ring_mult_comp. -Existing Instance ring_sub_comp. -Existing Instance ring_opp_comp. - -Add Ring Ar: (@ring_ring A (@domain_ring A Ad)). - -Instance zero_ring2 : Zero A := {zero := ring0}. -Instance one_ring2 : One A := {one := ring1}. -Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}. -Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}. -Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}. -Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}. - -Infix "==" := ring_eq (at level 70, no associativity). - -Ltac nsatzA := simpl; unfold Ari; nsatz_domain. - -Goal forall x y:A, x == y -> x+0 == y*1+0. -nsatzA. -Qed. +Context {A:Type}`{Aid:Integral_domain A}. Lemma example3 : forall x y z, x+y+z==0 -> x*y+x*z+y*z==0-> - x*y*z==0 -> x*x*x==0. + x*y*z==0 -> x^3%Z==0. Proof. -Time nsatzA. -Admitted. +Time nsatz. +Qed. Lemma example4 : forall x y z u, x+y+z+u==0 -> x*y+x*z+x*u+y*z+y*u+z*u==0-> x*y*z+x*y*u+x*z*u+y*z*u==0-> - x*y*z*u==0 -> x*x*x*x==0. + x*y*z*u==0 -> x^4%Z==0. Proof. -Time nsatzA. +Time nsatz. Qed. Lemma example5 : forall x y z u v, @@ -53,15 +29,17 @@ Lemma example5 : forall x y z u v, x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v==0-> x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v==0-> x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z==0 -> - x*y*z*u*v==0 -> x*x*x*x*x ==0. + x*y*z*u*v==0 -> x^5%Z==0. Proof. -Time nsatzA. +Time nsatz. Qed. Goal forall x y:Z, x = y -> (x+0)%Z = (y*1+0)%Z. nsatz. Qed. +Require Import Reals. + Goal forall x y:R, x = y -> (x+0)%R = (y*1+0)%R. nsatz. Qed. @@ -70,85 +48,17 @@ Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R. nsatz. Qed. -Section Examples. - -Delimit Scope PE_scope with PE. -Infix "+" := PEadd : PE_scope. -Infix "*" := PEmul : PE_scope. -Infix "-" := PEsub : PE_scope. -Infix "^" := PEpow : PE_scope. -Notation "[ n ]" := (@PEc Z n) (at level 0). - -Open Scope R_scope. - -Lemma example1 : forall x y, - x+y=0 -> - x*y=0 -> - x^2=0. -Proof. - nsatz. -Qed. - -Lemma example2 : forall x, x^2=0 -> x=0. -Proof. - nsatz. -Qed. - -(* -Notation X := (PEX Z 3). -Notation Y := (PEX Z 2). -Notation Z_ := (PEX Z 1). -*) -Lemma example3b : forall x y z, - x+y+z=0 -> - x*y+x*z+y*z=0-> - x*y*z=0 -> x^3=0. -Proof. -Time nsatz. -Qed. - -(* -Notation X := (PEX Z 4). -Notation Y := (PEX Z 3). -Notation Z_ := (PEX Z 2). -Notation U := (PEX Z 1). -*) -Lemma example4b : forall x y z u, - x+y+z+u=0 -> - x*y+x*z+x*u+y*z+y*u+z*u=0-> - x*y*z+x*y*u+x*z*u+y*z*u=0-> - x*y*z*u=0 -> x^4=0. -Proof. -Time nsatz. -Qed. - -(* -Notation x_ := (PEX Z 5). -Notation y_ := (PEX Z 4). -Notation z_ := (PEX Z 3). -Notation u_ := (PEX Z 2). -Notation v_ := (PEX Z 1). -Notation "x :: y" := (List.cons x y) -(at level 60, right associativity, format "'[hv' x :: '/' y ']'"). -Notation "x :: y" := (List.app x y) -(at level 60, right associativity, format "x :: y"). -*) - -Lemma example5b : forall x y z u v, - x+y+z+u+v=0 -> - x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0-> - x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0-> - x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 -> - x*y*z*u*v=0 -> x^5=0. -Proof. -Time nsatz. -Qed. - -End Examples. +End test. Section Geometry. +(* See the interactive pictures of Laurent Théry + on http://www-sop.inria.fr/marelle/CertiGeo/ + and research paper on + https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr +*) -Open Scope R_scope. +Require Import List. +Require Import Reals. Record point:Type:={ X:R; @@ -170,60 +80,122 @@ Definition equal2(A B:point):= (X A)=(X B) /\ (Y A)=(Y B). Definition equal3(A B:point):= - ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0. + ((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0. Definition nequal2(A B:point):= (X A)<>(X B) \/ (Y A)<>(Y B). Definition nequal3(A B:point):= - not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0). + not (((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0). Definition middle(A B I:point):= - 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B). + 2%R*(X I)=(X A)+(X B) /\ 2%R*(Y I)=(Y A)+(Y B). Definition distance2(A B:point):= - (X B - X A)^2 + (Y B - Y A)^2. + (X B - X A)^2%Z + (Y B - Y A)^2%Z. (* AB = CD *) Definition samedistance2(A B C D:point):= - (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2. + (X B - X A)^2%Z + (Y B - Y A)^2%Z = (X D - X C)^2%Z + (Y D - Y C)^2%Z. Definition determinant(A O B:point):= (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O). Definition scalarproduct(A O B:point):= (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O). Definition norm2(A O B:point):= - ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2). - - -Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)). -intuition. -Qed. - -Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C). -intuition. + ((X A - X O)^2%Z+(Y A - Y O)^2%Z)*((X B - X O)^2%Z+(Y B - Y O)^2%Z). + +Definition equaldistance(A B C D:point):= + ((X B) - (X A))^2%Z + ((Y B) - (Y A))^2%Z = + ((X D) - (X C))^2%Z + ((Y D) - (Y C))^2%Z. + +Definition equaltangente(A B C D E F:point):= + let s1:= determinant A B C in + let c1:= scalarproduct A B C in + let s2:= determinant D E F in + let c2:= scalarproduct D E F in + s1 * c2 = s2 * c1. + +Ltac cnf2 f := + match f with + | ?A \/ (?B /\ ?C) => + let c1 := cnf2 (A\/B) in + let c2 := cnf2 (A\/C) in constr:(c1/\c2) + | (?B /\ ?C) \/ ?A => + let c1 := cnf2 (B\/A) in + let c2 := cnf2 (C\/A) in constr:(c1/\c2) + | (?A \/ ?B) \/ ?C => + let c1 := cnf2 (B\/C) in cnf2 (A \/ c1) + | _ => f + end +with cnf f := + match f with + | ?A \/ ?B => + let c1 := cnf A in + let c2 := cnf B in + cnf2 (c1 \/ c2) + | ?A /\ ?B => + let c1 := cnf A in + let c2 := cnf B in + constr:(c1 /\ c2) + | _ => f + end. + +Ltac scnf := + match goal with + | |- ?f => let c := cnf f in + assert c;[repeat split| tauto] + end. + +Ltac disj_to_pol f := + match f with + | ?a = ?b \/ ?g => let p := disj_to_pol g in constr:((a - b)* p) + | ?a = ?b => constr:(a - b) + end. + +Lemma fastnsatz1:forall x y:R, x - y = 0 -> x = y. +nsatz. Qed. -Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d). -intros. -assert ( (a-b = 0) \/ (c-d = 0)). -apply Rmult_integral. -trivial. -destruct H0. -left; nsatz. -right; nsatz. -Qed. +Ltac fastnsatz:= + try trivial; try apply fastnsatz1; try trivial; nsatz. + +Ltac proof_pol_disj := + match goal with + | |- ?g => let p := disj_to_pol g in + let h := fresh "hp" in + assert (h:p = 0); + [idtac| + prod_disj h p] + | _ => idtac + end +with prod_disj h p := + match goal with + | |- ?a = ?b \/ ?g => + match p with + | ?q * ?p1 => + let h0 := fresh "hp" in + let h1 := fresh "hp" in + let h2 := fresh "hp" in + assert (h0:a - b = 0 \/ p1 = 0); + [apply Rmult_integral; exact h| + destruct h0 as [h1|h2]; + [left; fastnsatz| + right; prod_disj h2 p1]] + end + | _ => fastnsatz + end. -Ltac geo_unfold := - unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal; - unfold equal2; unfold equal3; unfold nequal2; unfold nequal3; - unfold middle; unfold samedistance2; - unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2. +(* +Goal forall a b c d e f:R, a=b \/ c=d \/ e=f \/ e=a. +intros. scnf; proof_pol_disj . +admit.*) -Ltac geo_end := - repeat ( - repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end); - repeat (apply a1 || apply a2 || apply a3); - repeat split). +Ltac geo_unfold := + unfold collinear, parallel, notparallel, orthogonal, + equal2, equal3, nequal2, nequal3, + middle, samedistance2, + determinant, scalarproduct, norm2, distance2, + equaltangente, determinant, scalarproduct, equaldistance. Ltac geo_rewrite_hyps:= repeat (match goal with @@ -231,14 +203,41 @@ Ltac geo_rewrite_hyps:= | h:Y _ = _ |- _ => rewrite h in *; clear h end). +Ltac geo_split_hyps:= + repeat (match goal with + | h:_ /\ _ |- _ => destruct h + end). + Ltac geo_begin:= geo_unfold; intros; geo_rewrite_hyps; - geo_end. + geo_split_hyps; + scnf; proof_pol_disj. (* Examples *) +Lemma medians: forall A B C A1 B1 C1 H:point, + middle B C A1 -> + middle A C B1 -> + middle A B C1 -> + collinear A A1 H -> collinear B B1 H -> + collinear C C1 H + \/ collinear A B C. +Proof. geo_begin. +idtac "Medians". + Time nsatz. +(*Finished transaction in 2. secs (2.69359u,0.s) +*) Qed. + +Lemma Pythagore: forall A B C:point, + orthogonal A B A C -> + distance2 A C + distance2 A B = distance2 B C. +Proof. geo_begin. +idtac "Pythagore". +Time nsatz. +(*Finished transaction in 0. secs (0.354946u,0.s) +*) Qed. Lemma Thales: forall O A B C D:point, collinear O A C -> collinear O B D -> @@ -246,9 +245,268 @@ Lemma Thales: forall O A B C D:point, (distance2 O B * distance2 O C = distance2 O D * distance2 O A /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B) \/ collinear O A B. -repeat geo_begin. +geo_begin. +idtac "Thales". +Time nsatz. (*Finished transaction in 2. secs (1.598757u,0.s)*) +Time nsatz. +Qed. + +Lemma segments_of_chords: forall A B C D M O:point, + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + collinear A B M -> + collinear C D M -> + (distance2 M A) * (distance2 M B) = (distance2 M C) * (distance2 M D) + \/ parallel A B C D. +Proof. +geo_begin. +idtac "segments_of_chords". +Time nsatz. +(*Finished transaction in 3. secs (2.704589u,0.s) +*) Qed. + + +Lemma isoceles: forall A B C:point, + equaltangente A B C B C A -> + distance2 A B = distance2 A C + \/ collinear A B C. +Proof. geo_begin. Time nsatz. +(*Finished transaction in 1. secs (1.140827u,0.s)*) Qed. + +Lemma minh: forall A B C D O E H I:point, + X A = 0 -> Y A = 0 -> Y O = 0 -> + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + orthogonal A C B D -> + collinear A C E -> + collinear B D E -> + collinear A B H -> + orthogonal E H A B -> + collinear C D I -> + middle C D I -> + collinear H E I + \/ (X C)^2%Z * (X B)^5%Z * (X O)^2%Z + * (X C - 2%Z * X O)^3%Z * (-2%Z * X O + X B)=0 + \/ parallel A C B D. +Proof. geo_begin. +idtac "minh". +Time nsatz with radicalmax :=1%N strategy:=1%Z + parameters:=(X O::X B::X C::nil) + variables:= (@nil R). +(*Finished transaction in 13. secs (10.102464u,0.s) +*) +Qed. + +Lemma Pappus: forall A B C A1 B1 C1 P Q S:point, + X A = 0 -> Y A = 0 -> Y B = 0 -> Y C = 0 -> + collinear A1 B1 C1 -> + collinear A B1 P -> collinear A1 B P -> + collinear A C1 Q -> collinear A1 C Q -> + collinear B C1 S -> collinear B1 C S -> + collinear P Q S + \/ (Y A1 - Y B1)^2%Z=0 \/ (X A = X B1) + \/ (X A1 = X C) \/ (X C = X B1) + \/ parallel A B1 A1 B \/ parallel A C1 A1 C \/ parallel B C1 B1 C. +Proof. +geo_begin. +idtac "Pappus". +Time nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil) + variables:= (X B + :: X A1 + :: Y A1 + :: X B1 + :: Y B1 + :: X C + :: Y C1 + :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil). +(*Finished transaction in 8. secs (7.795815u,0.000999999999999s) +*) +Qed. + +Lemma Simson: forall A B C O D E F G:point, + X A = 0 -> Y A = 0 -> + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + orthogonal E D B C -> + collinear B C E -> + orthogonal F D A C -> + collinear A C F -> + orthogonal G D A B -> + collinear A B G -> + collinear E F G + \/ (X C)^2%Z = 0 \/ (Y C)^2%Z = 0 \/ (X B)^2%Z = 0 \/ (Y B)^2%Z = 0 \/ (Y C - Y B)^2%Z = 0 + \/ equal3 B A + \/ equal3 A C \/ (X C - X B)^2%Z = 0 + \/ equal3 B C. +Proof. +geo_begin. +idtac "Simson". +Time nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X B::Y B::X C::Y C::Y D::nil) + variables:= (@nil R). (* compute -[X Y]. *) +(*Finished transaction in 8. secs (7.550852u,0.s) +*) +Qed. + +Lemma threepoints: forall A B C A1 B1 A2 B2 H1 H2 H3:point, + (* H1 intersection of bisections *) + middle B C A1 -> orthogonal H1 A1 B C -> + middle A C B1 -> orthogonal H1 B1 A C -> + (* H2 intersection of medians *) + collinear A A1 H2 -> collinear B B1 H2 -> + (* H3 intersection of altitudes *) + collinear B C A2 -> orthogonal A A2 B C -> + collinear A C B2 -> orthogonal B B2 A C -> + collinear A A1 H3 -> collinear B B1 H3 -> + collinear H1 H2 H3 + \/ collinear A B C. +Proof. geo_begin. +idtac "threepoints". +Time nsatz. +(*Finished transaction in 7. secs (6.282045u,0.s) +*) Qed. + +Lemma Feuerbach: forall A B C A1 B1 C1 O A2 B2 C2 O2:point, + forall r r2:R, + X A = 0 -> Y A = 0 -> X B = 1 -> Y B = 0-> + middle A B C1 -> middle B C A1 -> middle C A B1 -> + distance2 O A1 = distance2 O B1 -> + distance2 O A1 = distance2 O C1 -> + collinear A B C2 -> orthogonal A B O2 C2 -> + collinear B C A2 -> orthogonal B C O2 A2 -> + collinear A C B2 -> orthogonal A C O2 B2 -> + distance2 O2 A2 = distance2 O2 B2 -> + distance2 O2 A2 = distance2 O2 C2 -> + r^2%Z = distance2 O A1 -> + r2^2%Z = distance2 O2 A2 -> + distance2 O O2 = (r + r2)^2%Z + \/ distance2 O O2 = (r - r2)^2%Z + \/ collinear A B C. +Proof. geo_begin. +idtac "Feuerbach". +Time nsatz. +(*Finished transaction in 21. secs (19.021109u,0.s)*) +Qed. + + + + +Lemma Euler_circle: forall A B C A1 B1 C1 A2 B2 C2 O:point, + middle A B C1 -> middle B C A1 -> middle C A B1 -> + orthogonal A B C C2 -> collinear A B C2 -> + orthogonal B C A A2 -> collinear B C A2 -> + orthogonal A C B B2 -> collinear A C B2 -> + distance2 O A1 = distance2 O B1 -> + distance2 O A1 = distance2 O C1 -> + (distance2 O A2 = distance2 O A1 + /\distance2 O B2 = distance2 O A1 + /\distance2 O C2 = distance2 O A1) + \/ collinear A B C. +Proof. geo_begin. +idtac "Euler_circle 3 goals". +Time nsatz. +(*Finished transaction in 13. secs (11.208296u,0.124981s)*) +Time nsatz. +(*Finished transaction in 10. secs (8.846655u,0.s)*) +Time nsatz. +(*Finished transaction in 11. secs (9.186603u,0.s)*) +Qed. + + + +Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point, + X S = 0 -> Y S = 0 -> Y A = 0 -> + collinear A S A1 -> collinear B S B1 -> collinear C S C1 -> + collinear B1 C1 P -> collinear B C P -> + collinear A1 C1 Q -> collinear A C Q -> + collinear A1 B1 R -> collinear A B R -> + collinear P Q R + \/ X A = X B \/ X A = X C \/ X B = X C \/ X A = 0 \/ Y B = 0 \/ Y C = 0 + \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1. +Proof. +geo_begin. +idtac "Desargues". +Time +let lv := rev (X A + :: X B + :: Y B + :: X C + :: Y C + :: Y A1 :: X A1 + :: Y B1 + :: Y C1 + :: X R + :: Y R + :: X Q + :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in +nsatz with radicalmax :=1%N strategy:=0%Z + parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil) + variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*) +Qed. + +Lemma chords: forall O A B C D M:point, + equaldistance O A O B -> + equaldistance O A O C -> + equaldistance O A O D -> + collinear A B M -> collinear C D M -> + scalarproduct A M B = scalarproduct C M D + \/ parallel A B C D. +Proof. geo_begin. +idtac "chords". + Time nsatz. +(*Finished transaction in 4. secs (3.959398u,0.s)*) +Qed. + +Lemma Ceva: forall A B C D E F M:point, + collinear M A D -> collinear M B E -> collinear M C F -> + collinear B C D -> collinear E A C -> collinear F A B -> + (distance2 D B) * (distance2 E C) * (distance2 F A) = + (distance2 D C) * (distance2 E A) * (distance2 F B) + \/ collinear A B C. +Proof. geo_begin. +idtac "Ceva". Time nsatz. +(*Finished transaction in 105. secs (104.121171u,0.474928s)*) +Qed. + +Lemma bissectrices: forall A B C M:point, + equaltangente C A M M A B -> + equaltangente A B M M B C -> + equaltangente B C M M C A + \/ equal3 A B. +Proof. geo_begin. +idtac "bissectrices". Time nsatz. +(*Finished transaction in 2. secs (1.937705u,0.s)*) +Qed. + +Lemma bisections: forall A B C A1 B1 C1 H:point, + middle B C A1 -> orthogonal H A1 B C -> + middle A C B1 -> orthogonal H B1 A C -> + middle A B C1 -> + orthogonal H C1 A B + \/ collinear A B C. +Proof. geo_begin. +idtac "bisections". +Time nsatz. (*Finished transaction in 2. secs (2.024692u,0.002s)*) +Qed. + +Lemma altitudes: forall A B C A1 B1 C1 H:point, + collinear B C A1 -> orthogonal A A1 B C -> + collinear A C B1 -> orthogonal B B1 A C -> + collinear A B C1 -> orthogonal C C1 A B -> + collinear A A1 H -> collinear B B1 H -> + collinear C C1 H + \/ equal2 A B + \/ collinear A B C. +Proof. geo_begin. +idtac "altitudes". +Time nsatz. (*Finished transaction in 3. secs (3.001544u,0.s)*) +Time nsatz. (*Finished transaction in 4. secs (3.113527u,0.s)*) Qed. Lemma hauteurs:forall A B C A1 B1 C1 H:point, @@ -261,26 +519,16 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point, \/ collinear A B C. geo_begin. - -(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*) -(*Finished transaction in 3. secs (2.363641u,0.s)*) -(*Time nsatz_domainR. trop long! *) +idtac "hauteurs". Time let lv := constr:(Y A1 - :: X A1 - :: Y B1 - :: X B1 - :: Y A0 - :: Y B - :: X B - :: X A0 - :: X H - :: Y C - :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in - nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi; - discrR. -(* Finished transaction in 6. secs (5.579152u,0.001s) *) + :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C + :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in +nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R) + variables := lv. +(*Finished transaction in 5. secs (4.360337u,0.008999s)*) Qed. + End Geometry. diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v index f4996734..17531064 100644 --- a/test-suite/success/OmegaPre.v +++ b/test-suite/success/OmegaPre.v @@ -14,38 +14,38 @@ Open Scope Z_scope. (* zify_op *) -Goal forall a:Z, Zmax a a = a. +Goal forall a:Z, Z.max a a = a. intros. omega with *. Qed. -Goal forall a b:Z, Zmax a b = Zmax b a. +Goal forall a b:Z, Z.max a b = Z.max b a. intros. omega with *. Qed. -Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c. +Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. omega with *. Qed. -Goal forall a b:Z, Zmax a b + Zmin a b = a + b. +Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. omega with *. Qed. -Goal forall a:Z, (Zabs a)*(Zsgn a) = a. +Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. zify. intuition; subst; omega. (* pure multiplication: omega alone can't do it *) Qed. -Goal forall a:Z, Zabs a = a -> a >= 0. +Goal forall a:Z, Z.abs a = a -> a >= 0. intros. omega with *. Qed. -Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1. +Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. omega with *. Qed. @@ -119,7 +119,7 @@ Qed. (* mix of datatypes *) -Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p. +Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. omega with *. Qed. diff --git a/test-suite/success/PCase.v b/test-suite/success/PCase.v new file mode 100644 index 00000000..67d680ba --- /dev/null +++ b/test-suite/success/PCase.v @@ -0,0 +1,66 @@ + +(** Some tests of patterns containing matchs ending with joker branches. + Cf. the new form of the [constr_pattern] constructor [PCase] + in [pretyping/pattern.ml] *) + +(* A universal match matcher *) + +Ltac kill_match := + match goal with + |- context [ match ?x with _ => _ end ] => destruct x + end. + +(* A match matcher restricted to a given type : nat *) + +Ltac kill_match_nat := + match goal with + |- context [ match ?x in nat with _ => _ end ] => destruct x + end. + +(* Another way to restrict to a given type : give a branch *) + +Ltac kill_match_nat2 := + match goal with + |- context [ match ?x with S _ => _ | _ => _ end ] => destruct x + end. + +(* This should act only on empty match *) + +Ltac kill_match_empty := + match goal with + |- context [ match ?x with end ] => destruct x + end. + +Lemma test1 (b:bool) : if b then True else O=O. +Proof. + Fail kill_match_nat. + Fail kill_match_nat2. + Fail kill_match_empty. + kill_match. exact I. exact eq_refl. +Qed. + +Lemma test2a (n:nat) : match n with O => True | S n => (n = n) end. +Proof. + Fail kill_match_empty. + kill_match_nat. exact I. exact eq_refl. +Qed. + +Lemma test2b (n:nat) : match n with O => True | S n => (n = n) end. +Proof. + kill_match_nat2. exact I. exact eq_refl. +Qed. + +Lemma test2c (n:nat) : match n with O => True | S n => (n = n) end. +Proof. + kill_match. exact I. exact eq_refl. +Qed. + +Lemma test3a (f:False) : match f return Prop with end. +Proof. + kill_match_empty. +Qed. + +Lemma test3b (f:False) : match f return Prop with end. +Proof. + kill_match. +Qed. diff --git a/test-suite/success/PrintSortedUniverses.v b/test-suite/success/PrintSortedUniverses.v new file mode 100644 index 00000000..81326580 --- /dev/null +++ b/test-suite/success/PrintSortedUniverses.v @@ -0,0 +1,2 @@ +Require Reals. +Print Sorted Universes. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 81bdbc29..3b7f0d84 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -1,3 +1,9 @@ +(* Before loading Program, check non-anomaly on missing library Program *) + +Fail Program Definition f n (e:n=n): {n|n=0} := match n,e with 0, refl => 0 | _, _ => 0 end. + +(* Then we test Program properly speaking *) + Require Import Arith Program. Require Import ZArith Zwf. @@ -16,14 +22,14 @@ Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat := Print merge. -Print Zlt. +Print Z.lt. Print Zwf. -Open Local Scope Z_scope. +Local Open Scope Z_scope. Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z := match n ?= m with - | Lt => Zwfrec n (Zpred m) + | Lt => Zwfrec n (Z.pred m) | _ => 0 end. diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v index bd473fa6..fa659273 100644 --- a/test-suite/success/ROmegaPre.v +++ b/test-suite/success/ROmegaPre.v @@ -14,38 +14,38 @@ Open Scope Z_scope. (* zify_op *) -Goal forall a:Z, Zmax a a = a. +Goal forall a:Z, Z.max a a = a. intros. romega with *. Qed. -Goal forall a b:Z, Zmax a b = Zmax b a. +Goal forall a b:Z, Z.max a b = Z.max b a. intros. romega with *. Qed. -Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c. +Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c. intros. romega with *. Qed. -Goal forall a b:Z, Zmax a b + Zmin a b = a + b. +Goal forall a b:Z, Z.max a b + Z.min a b = a + b. intros. romega with *. Qed. -Goal forall a:Z, (Zabs a)*(Zsgn a) = a. +Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a. intros. zify. intuition; subst; romega. (* pure multiplication: omega alone can't do it *) Qed. -Goal forall a:Z, Zabs a = a -> a >= 0. +Goal forall a:Z, Z.abs a = a -> a >= 0. intros. romega with *. Qed. -Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1. +Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1. intros. romega with *. Qed. @@ -119,7 +119,7 @@ Qed. (* mix of datatypes *) -Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p. +Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p. intros. romega with *. Qed. 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). diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v index 89b3032c..c2d5cb2f 100644 --- a/test-suite/success/Reg.v +++ b/test-suite/success/Reg.v @@ -39,7 +39,7 @@ Lemma essai7 : derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1. reg. apply Rlt_0_1. -red in |- *; intro; rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0; +red; intro; rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0; assumption. Qed. @@ -127,7 +127,7 @@ Lemma essai23 : (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1. reg. left; apply Rlt_0_1. -right; unfold Rminus in |- *; rewrite Rplus_opp_r; reflexivity. +right; unfold Rminus; rewrite Rplus_opp_r; reflexivity. Qed. Lemma essai24 : @@ -135,8 +135,8 @@ Lemma essai24 : reg. replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R. apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ]. -unfold Rsqr in |- *; ring. -red in |- *; intro; cut (0 < x * x + 1)%R. +unfold Rsqr; ring. +red; intro; cut (0 < x * x + 1)%R. intro; rewrite H in H0; elim (Rlt_irrefl _ H0). apply Rplus_le_lt_0_compat; [ replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ] diff --git a/test-suite/success/Reset.v b/test-suite/success/Reset.v deleted file mode 100644 index b71ea69d..00000000 --- a/test-suite/success/Reset.v +++ /dev/null @@ -1,7 +0,0 @@ -(* Check Reset Section *) - -Section A. -Definition B := Prop. -End A. - -Reset A. diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v new file mode 100644 index 00000000..dd5aa81d --- /dev/null +++ b/test-suite/success/Scheme.v @@ -0,0 +1,4 @@ +(* This failed in 8.3pl2 *) + +Scheme Induction for eq Sort Prop. +Check eq_ind_dep. diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index 55d8343e..a79d28fa 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -3,6 +3,6 @@ Require Import ZArith. Module A. -Definition opp := Zopp. +Definition opp := Z.opp. End A. Check (A.opp 3). diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index 324d340a..73ef3720 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Tauto.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (**** Tactics Tauto and Intuition ****) (**** Tauto: diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 6cc443bb..e9d6a969 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v index b356f277..361c787e 100644 --- a/test-suite/success/Try.v +++ b/test-suite/success/Try.v @@ -2,7 +2,7 @@ non-existent names in Unfold [cf bug #263] *) Lemma lem1 : True. -try unfold i_dont_exist in |- *. +try unfold i_dont_exist. trivial. Qed. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index a6f9fa23..0d8bf556 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -8,8 +8,8 @@ Qed. Require Import ZArith. Goal (forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y)%Z. -intros; apply Znot_le_gt, Zgt_lt in H. -apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto. +intros; apply Znot_le_gt, Z.gt_lt in H. +apply Zmult_lt_reg_r, Z.lt_le_incl in H0; auto. Qed. (* Test application under tuples *) @@ -97,13 +97,14 @@ Qed. (* Check use of unification of bindings types in specialize *) +Module Type Test. Variable P : nat -> Prop. Variable L : forall (l : nat), P l -> P l. Goal P 0 -> True. intros. specialize L with (1:=H). Abort. -Reset P. +End Test. (* Two examples that show that hnf_constr is used when unifying types of bindings (a simplification of a script from Field_Theory) *) @@ -202,6 +203,13 @@ try apply H. unfold ID; apply H0. Qed. +(* Test hyp in "apply -> ... in hyp" is correctly instantiated by Ltac *) + +Goal (True <-> False) -> True -> False. +intros Heq H. +match goal with [ H : True |- _ ] => apply -> Heq in H end. +Abort. + (* Test coercion below product and on non meta-free terms in with bindings *) (* Cf wishes #1408 from E. Makarov *) @@ -258,7 +266,7 @@ Qed. (* This works because unfold calls clos_norm_flags which calls nf_evar *) Lemma eapply_evar_unfold : let x:=O in O=x -> 0=O. -intros x H; eapply trans_equal; +intros x H; eapply eq_trans; [apply H | unfold x;match goal with |- ?x = ?x => reflexivity end]. Qed. @@ -326,13 +334,12 @@ exact (refl_equal 4). Qed. (* From 12612, descent in conjunctions is more powerful *) -(* The following, which was failing badly in bug 1980, is now accepted - (even if somehow surprising) *) +(* The following, which was failing badly in bug 1980, is now + properly rejected, as descend in conjunctions builds an + ill-formed elimination from Prop to Type. *) Goal True. -eapply ex_intro. -instantiate (2:=fun _ :True => True). -instantiate (1:=I). +Fail eapply ex_intro. exact I. Qed. @@ -391,3 +398,35 @@ intro x; apply x. *) + +Section A. + +Variable map : forall (T1 T2 : Type) (f : T1 -> T2) (t11 t12 : T1), + identity (f t11) (f t12). + +Variable mapfuncomp : forall (X Y Z : Type) (f : X -> Y) (g : Y -> Z) (x x' : X), + identity (map Y Z g (f x) (f x')) (map X Z (fun x0 : X => g (f x0)) x x'). + +Goal forall X:Type, forall Y:Type, forall f:X->Y, forall x : X, forall x' : X, + forall g : Y -> X, + let gf := (fun x : X => g (f x)) : X -> X in + identity (map Y X g (f x) (f x')) (map X X gf x x'). +intros. +apply mapfuncomp. +Abort. + +End A. + +(* Check "with" clauses refer to names as they are printed *) + +Definition hide p := forall n:nat, p = n. + +Goal forall n, (forall n, n=0) -> hide n -> n=0. +unfold hide. +intros n H H'. +(* H is displayed as (forall n, n=0) *) +apply H with (n:=n). +Undo. +(* H' is displayed as (forall n0, n=n0) *) +apply H' with (n0:=0). +Qed. diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v new file mode 100644 index 00000000..9b691e25 --- /dev/null +++ b/test-suite/success/auto.v @@ -0,0 +1,26 @@ +(* Wish #2154 by E. van der Weegen *) + +(* auto was not using f_equal-style lemmas with metavariables occuring + only in the type of an evar of the concl, but not directly in the + concl itself *) + +Parameters + (F: Prop -> Prop) + (G: forall T, (T -> Prop) -> Type) + (L: forall A (P: A -> Prop), G A P -> forall x, F (P x)) + (Q: unit -> Prop). + +Hint Resolve L. + +Goal G unit Q -> F (Q tt). + intro. + auto. +Qed. + +(* Test implicit arguments in "using" clause *) + +Goal forall n:nat, nat * nat. +auto using (pair O). +Undo. +eauto using (pair O). +Qed. diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewrite.v index 68f2f7ce..5e9064f8 100644 --- a/test-suite/success/autorewritein.v +++ b/test-suite/success/autorewrite.v @@ -19,5 +19,11 @@ Proof. apply H;reflexivity. Qed. +(* Check autorewrite does not solve existing evars *) +(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *) +Hint Rewrite <- plus_n_O : base1. +Goal forall y, exists x, y+x = y. +eexists. autorewrite with base1. +Fail reflexivity. diff --git a/test-suite/success/bullet.v b/test-suite/success/bullet.v new file mode 100644 index 00000000..1099f3e1 --- /dev/null +++ b/test-suite/success/bullet.v @@ -0,0 +1,5 @@ +Goal True /\ True. +split. +- exact I. +- exact I. +Qed. diff --git a/test-suite/success/change.v b/test-suite/success/change.v index 5ac6ce82..7bed7ecb 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -14,7 +14,7 @@ Abort. (* Check the combination of at, with and in (see bug #2146) *) Goal 3=3 -> 3=3. intro H. -change 3 at 2 with (1+2) in |- *. +change 3 at 2 with (1+2). change 3 at 2 with (1+2) in H |-. change 3 with (1+2) in H at 1 |- * at 1. (* Now check that there are no more 3's *) @@ -25,8 +25,16 @@ Qed. change 3 at 1 with (1+2) at 3. change 3 at 1 with (1+2) in *. change 3 at 1 with (1+2) in H at 2 |-. -change 3 at 1 with (1+2) in |- * at 3. +change 3 at 1 with (1+2) at 3. change 3 at 1 with (1+2) in H |- *. change 3 at 1 with (1+2) in H, H|-. -change 3 in |- * at 1. +change 3 at 1. *) + +(* Test that pretyping checks allowed elimination sorts *) + +Goal True. +Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x). +Fail change True with + match ex_intro _ True (eq_refl True) with ex_intro x _ => x end. +Abort. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 908b5f77..4292ecb6 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -81,3 +81,53 @@ Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True). Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x. +(* Check that coercions are made visible only when modules are imported *) + +Module A. + Module B. Coercion b2n (b:bool) := if b then 0 else 1. End B. + Fail Check S true. +End A. +Import A. +Fail Check S true. + +(* Tests after the inheritance condition constraint is relaxed *) + +Inductive list (A : Type) : Type := + nil : list A | cons : A -> list A -> list A. +Inductive vect (A : Type) : nat -> Type := + vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n). +Fixpoint size A (l : list A) : nat := match l with nil => 0 | cons _ tl => 1+size _ tl end. + +Section test_non_unif_but_complete. +Fixpoint l2v A (l : list A) : vect A (size A l) := + match l as l return vect A (size A l) with + | nil => vnil A + | cons x xs => vcons A (size A xs) x (l2v A xs) + end. + +Local Coercion l2v : list >-> vect. +Check (fun l : list nat => (l : vect _ _)). + +End test_non_unif_but_complete. + +Section what_we_could_do. +Variables T1 T2 : Type. +Variable c12 : T1 -> T2. + +Class coercion (A B : Type) : Type := cast : A -> B. +Instance atom : coercion T1 T2 := c12. +Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C) (B * D) := + fun x => (c1 (fst x), c2 (snd x)). + +Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) := + match l as l return vect B (size A l) with + | nil => vnil B + | cons x xs => vcons _ _ (c x) (l2v2 xs) end. + +Local Coercion l2v2 : list >-> vect. + +(* This shows that there is still something to do to take full profit + of coercions *) +Fail Check (fun l : list (T1 * T1) => (l : vect _ _)). +Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)). +Section what_we_could_do.
\ No newline at end of file diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v index f6ebacae..05d2c98f 100644 --- a/test-suite/success/conv_pbs.v +++ b/test-suite/success/conv_pbs.v @@ -221,3 +221,8 @@ with universal_completeness_stoup (Gamma:context)(A:formula){struct A} (ProofForallL x t (subst_formula (remove_assoc _ x rho) A) (eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _))))) end. + + +(* A simple example that raised an uncaught exception at some point *) + +Fail Check fun x => @eq_refl x <: true = true. diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v index bc1757fd..52575eca 100644 --- a/test-suite/success/decl_mode.v +++ b/test-suite/success/decl_mode.v @@ -138,7 +138,7 @@ Coercion IZR: Z >->R.*) Open Scope R_scope. Lemma square_abs_square: - forall p,(INR (Zabs_nat p) * INR (Zabs_nat p)) = (IZR p * IZR p). + forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p). proof. assume p:Z. per cases on p. @@ -147,7 +147,7 @@ proof. suppose it is (Zpos z). thus thesis. suppose it is (Zneg z). - have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (Zneg z))) = + have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) = (IZR (Zpos z) * IZR (Zpos z))). ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))). thus ~= (IZR (Zneg z) * IZR (Zneg z)). @@ -165,15 +165,15 @@ proof. have H_in_R:(INR q<>0:>R) by H. have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field. have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def. - have (INR (Zabs_nat p * Zabs_nat p) - = (INR (Zabs_nat p) * INR (Zabs_nat p))) + have (INR (Z.abs_nat p * Z.abs_nat p) + = (INR (Z.abs_nat p) * INR (Z.abs_nat p))) by mult_INR. ~= (IZR p* IZR p) by square_abs_square. ~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *) ~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring. ~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0. ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR. - then (Zabs_nat p * Zabs_nat p = 2* (q * q))%nat. + then (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat. ~= ((q*q)+(q*q))%nat. ~= (Div2.double (q*q)). then (q=0%nat) by main_theorem. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index fe0165d0..12ddbda8 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,5 +1,11 @@ Require Import Coq.Program.Program Coq.Program.Equality. +Goal forall (H: forall n m : nat, n = m -> n = 0) x, x = tt. +intros. +dependent destruction x. +reflexivity. +Qed. + Variable A : Set. Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n). @@ -62,7 +68,7 @@ where " Γ ⊢ Ï„ " := (term Γ Ï„) : type_scope. Hint Constructors term : lambda. -Open Local Scope context_scope. +Local Open Scope context_scope. Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps. @@ -84,6 +90,29 @@ Proof with simpl in * ; eqns ; eauto with lambda. intro. eapply app... Defined. +Lemma weakening_ctx : forall Γ Δ Ï„, Γ ; Δ ⊢ Ï„ -> + forall Δ', Γ ; Δ' ; Δ ⊢ Ï„. +Proof with simpl in * ; eqns ; eauto with lambda. + intros Γ Δ Ï„ H. + + dependent induction H. + + destruct Δ as [|Δ Ï„'']... + induction Δ'... + + destruct Δ as [|Δ Ï„'']... + induction Δ'... + + destruct Δ as [|Δ Ï„'']... + apply abs. + specialize (IHterm Γ (empty, Ï„))... + + apply abs. + specialize (IHterm Γ (Δ, Ï„'', Ï„))... + + intro. eapply app... +Defined. + Lemma exchange : forall Γ Δ α β Ï„, term (Γ, α, β ; Δ) Ï„ -> term (Γ, β, α ; Δ) Ï„. Proof with simpl in * ; eqns ; eauto. intros until 1. @@ -105,6 +134,8 @@ Proof with simpl in * ; eqns ; eauto. eapply app... Defined. + + (** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *) Set Implicit Arguments. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 8013e1d3..fc40ea96 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -74,3 +74,22 @@ destruct H. destruct H0. reflexivity. Qed. + +(* These did not work before 8.4 *) + +Goal (exists x, x=0) -> True. +destruct 1 as (_,_); exact I. +Abort. + +Goal (exists x, x=0 /\ True) -> True. +destruct 1 as (_,(_,H)); exact H. +Abort. + +Goal (exists x, x=0 /\ True) -> True. +destruct 1 as (_,(_,x)); exact x. +Abort. + +Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0. +intros. +destruct (g _). (* This was failing in at least r14571 *) +Abort. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 1862ad10..49bf8b15 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index ff880d00..df73383a 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,12 +16,7 @@ Qed. Lemma lem2 : forall x y : T, {x = y} + {x <> y}. intros x y. - decide equality x y. -Qed. - -Lemma lem3 : forall x y : T, {x = y} + {x <> y}. -intros x y. - decide equality y x. + decide equality. Qed. Lemma lem4 : forall x y : T, {x = y} + {x <> y}. diff --git a/test-suite/success/eta.v b/test-suite/success/eta.v new file mode 100644 index 00000000..08078012 --- /dev/null +++ b/test-suite/success/eta.v @@ -0,0 +1,19 @@ +(* Kernel test (head term is a constant) *) +Check (fun a : S = S => a : S = fun x => S x). + +(* Kernel test (head term is a variable) *) +Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => f x). + +(* Test type inference (head term is syntactically rigid) *) +Check (fun (a : list = list) => a : list = fun A => _ A). + +(* Test type inference (head term is a variable) *) +(* This one is still to be done... +Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => _ x). +*) + +(* Test tactic unification *) +Goal (forall f:nat->nat, (fun x => f x) = (fun x => f x)) -> S = S. +intro H; apply H. +Qed. + diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 6423ad14..e6088091 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -238,3 +238,144 @@ eapply f_equal with (* should fail because ill-typed *) end) in H || injection H. Abort. + +(* A legitimate simple eapply that was failing in coq <= 8.3. + Cf. in Unification.w_merge the addition of an extra pose_all_metas_as_evars + on 30/9/2010 +*) + +Lemma simple_eapply_was_failing : + (forall f:nat->nat, exists g, f = g) -> True. +Proof. + assert (modusponens : forall P Q, P -> (P->Q) -> Q) by auto. + intros. + eapply modusponens. + simple eapply H. + (* error message with V8.3 : + Impossible to unify "?18" with "fun g : nat -> nat => ?6 = g". *) +Abort. + +(* Regression test *) + +Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0. + +(* This example revealed an incorrect evar restriction at some time + around October 2011 *) + +Goal forall (A:Type) (a:A) (P:forall A, A -> Prop), (P A a) /\ (P A a). +intros. +refine ((fun H => conj (proj1 H) (proj2 H)) _). +Abort. + +(* The argument of e below failed to be inferred from r14219 (Oct 2011) to *) +(* r14753 after the restrictions made on detecting Miller's pattern in the *) +(* presence of alias, only the second-order unification procedure was *) +(* able to solve this problem but it was deactivated for 8.4 in r14219 *) + +Definition k0 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, n = a) o := + match o with (* note: match introduces an alias! *) + | Some a => e _ (j a) + | None => O + end. + +Definition k1 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j a). + +Definition k2 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b). + +(* Other examples about aliases involved in pattern unification *) + +Definition k3 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, let a' := a in n = a') a (b:=a) := e _ (j b). + +Definition k4 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, let a' := S a in n = a') a (b:=a) := e _ (j b). + +Definition k5 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, let a' := S a in exists n : nat, n = a') a (b:=a) := e _ (j b). + +Definition k6 + (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat) + (j : forall a, exists n : nat, let n' := S n in n' = a) a (b:=a) := e _ (j b). + +Definition k7 + (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat) + (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b). + +(* An example that uses materialize_evar under binders *) +(* Extracted from bigop.v in the mathematical components library *) + +Section Bigop. + +Variable bigop : forall R I: Type, + R -> (R -> R -> R) -> list I -> (I->Prop) -> (I -> R) -> R. + +Hypothesis eq_bigr : +forall (R : Type) (idx : R) (op : R -> R -> R) + (I : Type) (r : list I) (P : I -> Prop) (F1 F2 : I -> R), + (forall i : I, P i -> F1 i = F2 i) -> + bigop R I idx op r (fun i : I => P i) (fun i : I => F1 i) = idx. + +Hypothesis big_tnth : +forall (R : Type) (idx : R) (op : R -> R -> R) + (I : Type) (r : list I) (P : I -> Prop) (F : I -> R), + bigop R I idx op r (fun i : I => P i) (fun i : I => F i) = idx. + +Hypothesis big_tnth_with_letin : +forall (R : Type) (idx : R) (op : R -> R -> R) + (I : Type) (r : list I) (P : I -> Prop) (F : I -> R), + bigop R I idx op r (fun i : I => let i:=i in P i) (fun i : I => F i) = idx. + +Variable R : Type. +Variable idx : R. +Variable op : R -> R -> R. +Variable I : Type. +Variable J : Type. +Variable rI : list I. +Variable rJ : list J. +Variable xQ : J -> Prop. +Variable P : I -> Prop. +Variable Q : I -> J -> Prop. +Variable F : I -> J -> R. + +(* Check unification under binders *) + +Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth _ _ _ _ rI _ _)) + : (bigop R J idx op rJ + (fun j : J => let k:=j in xQ k) + (fun j : J => let k:=j in + bigop R I idx + op rI + (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx. + +(* Check also with let-in *) + +Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth_with_letin _ _ _ _ rI _ _)) + : (bigop R J idx op rJ + (fun j : J => let k:=j in xQ k) + (fun j : J => let k:=j in + bigop R I idx + op rI + (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx. + +End Bigop. + +(* Check the use of (at least) an heuristic to solve problems of the form + "?x[t] = ?y" where ?y occurs in t without easily knowing if ?y can + eventually be erased in t *) + +Section evar_evar_occur. + Variable id : nat -> nat. + Variable f : forall x, id x = 0 -> id x = 0 -> x = 1 /\ x = 2. + Variable g : forall y, id y = 0 /\ id y = 0. + (* Still evars in the resulting type, but constraints should be solved *) + Check match g _ with conj a b => f _ a b end. +End evar_evar_occur. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 4fec6e7f..acd1da66 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -342,7 +342,7 @@ case H1. exact H0. intros. exact n. -Qed. +Defined. Extraction oups. (* let oups h0 = diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index be4e0684..8623f718 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -9,17 +9,16 @@ Inductive rBoolOp : Set := | rAnd : rBoolOp | rEq : rBoolOp. -Definition rlt (a b : rNat) : Prop := - (a ?= b)%positive Datatypes.Eq = Datatypes.Lt. +Definition rlt (a b : rNat) : Prop := Pos.compare_cont a b Eq = Lt. Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}. intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m); generalize (nat_of_P_gt_Gt_compare_morphism n m); - generalize (Pcompare_Eq_eq n m); case ((n ?= m)%positive Datatypes.Eq). + generalize (Pcompare_Eq_eq n m); case (Pos.compare_cont n m Eq). intros H' H'0 H'1; right; right; auto. -intros H' H'0 H'1; left; unfold rlt in |- *. +intros H' H'0 H'1; left; unfold rlt. apply nat_of_P_lt_Lt_compare_complement_morphism; auto. -intros H' H'0 H'1; right; left; unfold rlt in |- *. +intros H' H'0 H'1; right; left; unfold rlt. apply nat_of_P_lt_Lt_compare_complement_morphism; auto. apply H'0; auto. Defined. diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v index af81e53d..ebd90a40 100644 --- a/test-suite/success/hyps_inclusion.v +++ b/test-suite/success/hyps_inclusion.v @@ -19,14 +19,16 @@ red in H. (* next tactic was failing wrt bug #1325 because type-checking the goal detected a syntactically different type for the section variable H *) case 0. -Reset A. +Abort. +End A. (* Variant with polymorphic inductive types for bug #1325 *) -Section A. +Section B. Variable H:not True. Inductive I (n:nat) : Type := C : H=H -> I n. Goal I 0. red in H. case 0. -Reset A. +Abort. +End B. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index ce3e692f..e8019a90 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -107,3 +107,20 @@ Context {A:Set}. Definition h (a:A) := a. End C. Check h 0. + +(* Check implicit arguments in arity of inductive types. The three + following examples used to fail before r13671 *) + +Inductive I {A} (a:A) : forall {n:nat}, Prop := + | C : I a (n:=0). + +Inductive I2 (x:=0) : Prop := + | C2 {p:nat} : p = 0 -> I2. +Check C2 eq_refl. + +Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop := + | C3 : I3 a (n:=0). + +(* Check global implicit declaration over ref not in section *) + +Section D. Global Arguments eq [A] _ _. End D. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index 7626ecc4..9316ac03 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 3c8d8ea9..cc8e8dd8 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -41,3 +41,26 @@ Proof. auto. auto. Qed. + +(* Check selection of occurrences by pattern *) + +Goal forall x, S x = S (S x). +intros. +induction (S _) in |- * at -2. +now_show (0=1). +Undo 2. +induction (S _) in |- * at 1 3. +now_show (0=1). +Undo 2. +induction (S _) in |- * at 1. +now_show (0=S (S x)). +Undo 2. +induction (S _) in |- * at 2. +now_show (S x=0). +Undo 2. +induction (S _) in |- * at 3. +now_show (S x=1). +Undo 2. +Fail induction (S _) in |- * at 4. +Abort. + diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 02618c2c..c2eb8bd7 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -2,7 +2,7 @@ (* Submitted by Pierre Crégut *) (* Checks substitution of x *) -Ltac f x := unfold x in |- *; idtac. +Ltac f x := unfold x; idtac. Lemma lem1 : 0 + 0 = 0. f plus. @@ -86,7 +86,7 @@ assert t. exact H. intro H1. apply H. -symmetry in |- *. +symmetry . assumption. Qed. @@ -105,7 +105,7 @@ sym'. exact H. intro H1. apply H. -symmetry in |- *. +symmetry . assumption. Qed. @@ -193,7 +193,7 @@ Abort. (* Used to fail in V8.1 *) Tactic Notation "test" constr(t) integer(n) := - set (k := t) in |- * at n. + set (k := t) at n. Goal forall x : nat, x = 1 -> x + x + x = 3. intros x H. @@ -244,6 +244,29 @@ reflexivity. apply I. Qed. +(* Test binding of open terms with non linear matching *) + +Ltac f_non_linear t := + match t with + (forall x y, ?u = 0) -> (forall y x, ?u = 0) => + assert (forall x y:nat, u = u) + end. + +Goal True. +f_non_linear ((forall x y, x+y = 0) -> (forall x y, y+x = 0)). +reflexivity. +f_non_linear ((forall a b, a+b = 0) -> (forall a b, b+a = 0)). +reflexivity. +f_non_linear ((forall a b, a+b = 0) -> (forall x y, y+x = 0)). +reflexivity. +f_non_linear ((forall x y, x+y = 0) -> (forall a b, b+a = 0)). +reflexivity. +f_non_linear ((forall x y, x+y = 0) -> (forall y x, x+y = 0)). +reflexivity. +f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *) +|| exact I. +Qed. + (* Test regular failure when clear/intro breaks soundness of the interpretation of terms in current environment *) @@ -275,3 +298,7 @@ evar(foo:nat). let evval := eval compute in foo in not_eq evval 1. let evval := eval compute in foo in not_eq 1 evval. Abort. + +(* Check that this returns an error and not an anomaly (see r13667) *) + +Fail Local Tactic Notation "myintro" := intro. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 41aa3b3e..5fe760bf 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 5a008f18..56cab0f6 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -9,4 +9,4 @@ End S. (* Check f nat nat : Set. *) -Check I nat nat : Set. +Check I nat nat : Set.
\ No newline at end of file diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v new file mode 100644 index 00000000..bf302df4 --- /dev/null +++ b/test-suite/success/proof_using.v @@ -0,0 +1,67 @@ +Section Foo. + +Variable a : nat. + +Lemma l1 : True. +Fail Proof using non_existing. +Proof using a. +exact I. +Qed. + +Lemma l2 : True. +Proof using a. +Admitted. + +Lemma l3 : True. +Proof using a. +admit. +Qed. + +End Foo. + +Check (l1 3). +Check (l2 3). +Check (l3 3). + +Section Bar. + +Variable T : Type. +Variable a b : T. +Variable H : a = b. + +Lemma l4 : a = b. +Proof using H. +exact H. +Qed. + +End Bar. + +Check (l4 _ 1 1 _ : 1 = 1). + +Section S1. + +Variable v1 : nat. + +Section S2. + +Variable v2 : nat. + +Lemma deep : v1 = v2. +Proof using v1 v2. +admit. +Qed. + +Lemma deep2 : v1 = v2. +Proof using v1 v2. +Admitted. + +End S2. + +Check (deep 3 : v1 = 3). +Check (deep2 3 : v1 = 3). + +End S1. + +Check (deep 3 4 : 3 = 4). +Check (deep2 3 4 : 3 = 4). + diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v new file mode 100644 index 00000000..0befe054 --- /dev/null +++ b/test-suite/success/remember.v @@ -0,0 +1,16 @@ +(* Testing remember and co *) + +Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0. +intros. +Fail remember nat as X. +Fail remember nat as X in H. (* This line used to succeed in 8.3 *) +Fail remember nat as X. +Abort. + +(* Testing Ltac interpretation of remember (was not working up to r16181) *) + +Goal (1 + 2 + 3 = 6). +let name := fresh "fresh" in +remember (1 + 2) as x eqn:name. +rewrite fresh. +Abort. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 3bce52fe..08c406be 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -108,3 +108,24 @@ intros. rewrite (H _). reflexivity. Qed. + +(* Example of rewriting of a degenerated pattern using the right-most + argument of the goal. This is sometimes used in contribs, even if + ad hoc. Here, we have the extra requirement that checking types + needs delta-conversion *) + +Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p). +Definition P := (nat * nat)%type. +Goal forall x:P, x = x. +intros. rewrite s. +Abort. + +(* Test second-order unification and failure of pattern-unification *) + +Goal forall (P: forall Y, Y -> Prop) Y a, Y = nat -> (True -> P Y a) -> False. +intros. +(* The next line used to succeed between June and November 2011 *) +(* causing ill-typed rewriting *) +Fail rewrite H in H0. +Abort. + diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v new file mode 100644 index 00000000..9edfd825 --- /dev/null +++ b/test-suite/success/searchabout.v @@ -0,0 +1,60 @@ + +(** Test of the different syntaxes of SearchAbout, in particular + with and without the [ ... ] delimiters *) + +SearchAbout plus. +SearchAbout plus mult. +SearchAbout "plus_n". +SearchAbout plus "plus_n". +SearchAbout "*". +SearchAbout "*" "+". + +SearchAbout plus inside Peano. +SearchAbout plus mult inside Peano. +SearchAbout "plus_n" inside Peano. +SearchAbout plus "plus_n" inside Peano. +SearchAbout "*" inside Peano. +SearchAbout "*" "+" inside Peano. + +SearchAbout plus outside Peano Logic. +SearchAbout plus mult outside Peano Logic. +SearchAbout "plus_n" outside Peano Logic. +SearchAbout plus "plus_n" outside Peano Logic. +SearchAbout "*" outside Peano Logic. +SearchAbout "*" "+" outside Peano Logic. + +SearchAbout -"*" "+" outside Logic. +SearchAbout -"*"%nat "+"%nat outside Logic. + +SearchAbout [plus]. +SearchAbout [plus mult]. +SearchAbout ["plus_n"]. +SearchAbout [plus "plus_n"]. +SearchAbout ["*"]. +SearchAbout ["*" "+"]. + +SearchAbout [plus] inside Peano. +SearchAbout [plus mult] inside Peano. +SearchAbout ["plus_n"] inside Peano. +SearchAbout [plus "plus_n"] inside Peano. +SearchAbout ["*"] inside Peano. +SearchAbout ["*" "+"] inside Peano. + +SearchAbout [plus] outside Peano Logic. +SearchAbout [plus mult] outside Peano Logic. +SearchAbout ["plus_n"] outside Peano Logic. +SearchAbout [plus "plus_n"] outside Peano Logic. +SearchAbout ["*"] outside Peano Logic. +SearchAbout ["*" "+"] outside Peano Logic. + +SearchAbout [-"*" "+"] outside Logic. +SearchAbout [-"*"%nat "+"%nat] outside Logic. + + +(** The example in the Reference Manual *) + +Require Import ZArith. + +SearchAbout Z.mul Z.add "distr". +SearchAbout "+"%Z "*"%Z "distr" -positive -Prop. +SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/test-suite/success/set.v b/test-suite/success/set.v index 23019275..8116e897 100644 --- a/test-suite/success/set.v +++ b/test-suite/success/set.v @@ -1,8 +1,19 @@ +(* This used to fail in 8.0pl1 *) + Goal forall n, n+n=0->0=n+n. intros. - -(* This used to fail in 8.0pl1 *) set n in * |-. +Abort. + +(* This works from 8.4pl1, since merging of different instances of the + same metavariable in a pattern is done modulo conversion *) + +Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1"). + +Goal forall (f:forall n, n=0 -> Prop) n (H:(n+n).+1=0), f (n.+1+n) H. +intros. +set (f _ _). +Abort. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 033b3f48..653b5bf9 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -18,10 +18,10 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t. Lemma setoid_set : Setoid_Theory set same. -unfold same in |- *; split ; red. -red in |- *; auto. +unfold same; split ; red. +red; auto. -red in |- *. +red. intros. elim (H a); auto. @@ -33,19 +33,19 @@ Qed. Add Setoid set same setoid_set as setsetoid. Add Morphism In : In_ext. -unfold same in |- *; intros a s t H; elim (H a); auto. +unfold same; intros a s t H; elim (H a); auto. Qed. Lemma add_aux : forall s t : set, same s t -> forall a b : A, In a (Add b s) -> In a (Add b t). -unfold same in |- *; simple induction 2; intros. +unfold same; simple induction 2; intros. rewrite H1. -simpl in |- *; left; reflexivity. +simpl; left; reflexivity. elim (H a). intros. -simpl in |- *; right. +simpl; right. apply (H2 H1). Qed. @@ -74,15 +74,15 @@ setoid_replace (remove a (Add a Empty)) with Empty. auto. -unfold same in |- *. +unfold same. split. -simpl in |- *. +simpl. case (eq_dec a a). intros e ff; elim ff. intros; absurd (a = a); trivial. -simpl in |- *. +simpl. intro H; elim H. Qed. @@ -130,3 +130,38 @@ intros f0 Q H. setoid_rewrite H. tauto. Qed. + +(** Check proper refreshing of the lemma application for multiple + different instances in a single setoid rewrite. *) + +Section mult. + Context (fold : forall {A} {B}, (A -> B) -> A -> B). + Context (add : forall A, A -> A). + Context (fold_lemma : forall {A B f} {eqA : relation B} x, eqA (fold A B f (add A x)) (fold _ _ f x)). + Context (ab : forall B, A -> B). + Context (anat : forall A, nat -> A). + +Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). +Proof. intros. + setoid_rewrite fold_lemma. + change (fold A A (fun x0 : A => ab A x0) x = anat A (fold A nat (ab nat) x)). +Abort. + +End mult. + +(** Current semantics for rewriting with typeclass constraints in the lemma + does not fix the instance at the first unification, use [at], or simply rewrite for + this semantics. *) + +Require Import Arith. + +Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}. +Instance: Foo nat. admit. Defined. +Instance: Foo bool. admit. Defined. + +Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. +Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort. + +Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. +Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort. + diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v new file mode 100644 index 00000000..d4191b93 --- /dev/null +++ b/test-suite/success/simpl_tuning.v @@ -0,0 +1,149 @@ +(* as it is dynamically inferred by simpl *) +Arguments minus !n / m. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (match y with O => S x | S _ => _ end = 0) => idtac end. +Abort. + +(* we avoid exposing a match *) +Arguments minus n m : simpl nomatch. + +Lemma foo x : minus 0 x = 0. +simpl. +match goal with |- (0 = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* we unfold as soon as we have 1 args, but we avoid exposing a match *) +Arguments minus n / m : simpl nomatch. + +Lemma foo : minus 0 = fun x => 0. +simpl. +match goal with |- minus 0 = _ => idtac end. +Abort. +(* This does not work as one may expect. The point is that simpl is implemented + as "strong (whd_simpl_state)" and after unfolding minus you have + (fun m => match 0 => 0 | S n => ...) that is already in whd and exposes + a match, that of course "strong" would reduce away but at that stage + we don't know, and reducing by hand under the lambda is against whd *) + +(* extra tuning for the usual heuristic *) +Arguments minus !n / m : simpl nomatch. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* full control *) +Arguments minus !n !m /. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +(* omitting /, that being immediately after the last ! is irrelevant *) +Arguments minus !n !m. + +Lemma foo x y : S (S x) - S y = 0. +simpl. +match goal with |- (S x - y = 0) => idtac end. +Abort. + +Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0. +simpl. +match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end. +Abort. + +Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := + fun x => (f (fst x), g (snd x)). + +Delimit Scope foo_scope with F. +Notation "@@" := nat (only parsing) : foo_scope. +Notation "@@" := (fun x => x) (only parsing). + +Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. + +Lemma foo x : @pf @@ nat @@ nat nat @@ x = pf @@ @@ x. +Abort. + +Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). + +(* fcomp is unfolded if applied to 6 args *) +Arguments fcomp {A B C}%type f g x /. + +Notation "f \o g" := (fcomp f g) (at level 50). + +Lemma foo (f g h : nat -> nat) x : pf (f \o g) h x = pf f h (g (fst x), snd x). +simpl. +match goal with |- (pf (f \o g) h x = _) => idtac end. +case x; intros x1 x2. +simpl. +match goal with |- (pf (f \o g) h _ = pf f h _) => idtac end. +unfold pf; simpl. +match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end. +Abort. + +Definition volatile := fun x : nat => x. +Arguments volatile /. + +Lemma foo : volatile = volatile. +simpl. +match goal with |- (fun _ => _) = _ => idtac end. +Abort. + +Set Implicit Arguments. + +Section S1. + +Variable T1 : Type. + +Section S2. + +Variable T2 : Type. + +Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat := + match n, m with + | 0,_ => 0 + | S _, 0 => n + | S n', S m' => f x y n' v m' end. + +Global Arguments f x y !n !v !m. + +Lemma foo x y n m : f x y (S n) tt m = f x y (S n) tt (S m). +simpl. +match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end. +Abort. + +End S2. + +Lemma foo T x y n m : @f T x y (S n) tt m = @f T x y (S n) tt (S m). +simpl. +match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end. +Abort. + +End S1. + +Arguments f : clear implicits and scopes. + diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 57837321..c5f032be 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -5,20 +5,20 @@ intros. (* "compatibility" mode: specializing a global name means a kind of generalize *) -specialize trans_equal. intros _. -specialize trans_equal with (1:=H)(2:=H0). intros _. -specialize trans_equal with (x:=a)(y:=b)(z:=c). intros _. -specialize trans_equal with (1:=H)(z:=c). intros _. -specialize trans_equal with nat a b c. intros _. -specialize (@trans_equal nat). intros _. -specialize (@trans_equal _ a b c). intros _. -specialize (trans_equal (x:=a)). intros _. -specialize (trans_equal (x:=a)(y:=b)). intros _. -specialize (trans_equal H H0). intros _. -specialize (trans_equal H0 (z:=b)). intros _. +specialize eq_trans. intros _. +specialize eq_trans with (1:=H)(2:=H0). intros _. +specialize eq_trans with (x:=a)(y:=b)(z:=c). intros _. +specialize eq_trans with (1:=H)(z:=c). intros _. +specialize eq_trans with nat a b c. intros _. +specialize (@eq_trans nat). intros _. +specialize (@eq_trans _ a b c). intros _. +specialize (eq_trans (x:=a)). intros _. +specialize (eq_trans (x:=a)(y:=b)). intros _. +specialize (eq_trans H H0). intros _. +specialize (eq_trans H0 (z:=b)). intros _. (* local "in place" specialization *) -assert (Eq:=trans_equal). +assert (Eq:=eq_trans). specialize Eq. specialize Eq with (1:=H)(2:=H0). Undo. @@ -38,10 +38,10 @@ specialize (Eq _ _ _ b H0). Undo. presque ok... *) (* 2) echoue moins lorsque zero premise de mangé *) -specialize trans_equal with (1:=Eq). (* mal typé !! *) +specialize eq_trans with (1:=Eq). (* mal typé !! *) (* 3) *) -specialize trans_equal with _ a b c. intros _. +specialize eq_trans with _ a b c. intros _. (* Anomaly: Evar ?88 was not declared. Please report. *) *) diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v new file mode 100644 index 00000000..73df5ca9 --- /dev/null +++ b/test-suite/success/telescope_canonical.v @@ -0,0 +1,72 @@ +Structure Inner := mkI { is :> Type }. +Structure Outer := mkO { os :> Inner }. +Canonical Structure natInner := mkI nat. +Canonical Structure natOuter := mkO natInner. +Definition hidden_nat := nat. +Axiom P : forall S : Outer, is (os S) -> Prop. +Lemma test1 (n : hidden_nat) : P _ n. +Admitted. + +Structure Pnat := mkP { getp : nat }. +Definition my_getp := getp. +Axiom W : nat -> Prop. + +(* Fix *) +Canonical Structure add1Pnat n := mkP (plus n 1). +Definition test_fix n := (refl_equal _ : W (my_getp _) = W (n + 1)). + +(* Case *) +Definition pred n := match n with 0 => 0 | S m => m end. +Canonical Structure predSS n := mkP (pred n). +Definition test_case x := (refl_equal _ : W (my_getp _) = W (pred x)). +Fail Definition test_case' := (refl_equal _ : W (my_getp _) = W (pred 0)). + +Canonical Structure letPnat' := mkP 0. +Definition letin := (let n := 0 in n). +Definition test4 := (refl_equal _ : W (getp _) = W letin). +Definition test41 := (refl_equal _ : W (my_getp _) = W letin). +Definition letin2 (x : nat) := (let n := x in n). +Canonical Structure letPnat'' x := mkP (letin2 x). +Definition test42 x := (refl_equal _ : W (my_getp _) = W (letin2 x)). +Fail Definition test42' x := (refl_equal _ : W (my_getp _) = W x). + +Structure Morph := mkM { f :> nat -> nat }. +Definition my_f := f. +Axiom Q : (nat -> nat) -> Prop. + +(* Lambda *) +Canonical Structure addMorh x := mkM (plus x). +Definition test_lam x := (refl_equal _ : Q (my_f _) = Q (plus x)). +Definition test_lam' := (refl_equal _ : Q (my_f _) = Q (plus 0)). + +(* Simple tests to justify Sort and Prod as "named". + They are already normal, so they cannot loose their names, + but still... *) +Structure Sot := mkS { T : Type }. +Axiom R : Type -> Prop. +Canonical Structure tsot := mkS (Type). +Definition test_sort := (refl_equal _ : R (T _) = R Type). +Canonical Structure tsot2 := mkS (nat -> nat). +Definition test_prod := (refl_equal _ : R (T _) = R (nat -> nat)). + +(* Var *) +Section Foo. +Variable v : nat. +Definition my_v := v. +Canonical Structure vP := mkP my_v. +Definition test_var := (refl_equal _ : W (getp _) = W my_v). +Canonical Structure vP' := mkP v. +Definition test_var' := (refl_equal _ : W (my_getp _) = W my_v). +End Foo. + +(* Rel *) +Definition test_rel v := (refl_equal _ : W (my_getp _) = W (my_v v)). +Goal True. +pose (x := test_rel 2). +match goal with x := _ : W (my_getp (vP 2)) = _ |- _ => idtac end. +apply I. +Qed. + + + + diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 66c4e080..62ecb1aa 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v index 8b7764e5..42e32ccc 100644 --- a/test-suite/success/unicode_utf8.v +++ b/test-suite/success/unicode_utf8.v @@ -75,7 +75,7 @@ Notation "x ≤ y" := (x<=y) (at level 70, no associativity). Require Import ZArith. Open Scope Z_scope. -Locate "≤". (* still le, not Zle *) +Locate "≤". (* still le, not Z.le *) Notation "x ≤ y" := (x<=y) (at level 70, no associativity). Locate "≤". Close Scope Z_scope. diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index ddf122e8..997dceb4 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -21,6 +21,12 @@ Proof. intros; apply H. Qed. + (* Feature introduced June 2011 *) + +Lemma l7 : forall x (P:nat->Prop), (forall f, P (f x)) -> P (x+x). +Proof. +intros x P H; apply H. +Qed. (* Example submitted for Zenon *) @@ -90,12 +96,14 @@ intros. apply H. Qed. +(* Feature deactivated in commit 14189 (see commit log) (* Test instanciation of evars by unification *) Goal (forall x, 0 + x = 0 -> True) -> True. intros; eapply H. rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *) Abort. +*) (* Check handling of identity equation between evars *) (* The example failed to pass until revision 10623 *) @@ -135,4 +143,44 @@ Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) -> forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f. Proof. intros. - rewrite H. + rewrite H with (f:=f0). +Abort. + +(* Three tests provided by Dan Grayson as part of a custom patch he + made for a more powerful "destruct" for handling Voevodsky's + Univalent Foundations. The test checks if second-order matching in + tactic unification is able to guess by itself on which dependent + terms to abstract so that the elimination predicate is well-typed *) + +Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) : + identity (fxe x) (fxe x). +Proof. destruct (fxe x). apply identity_refl. Defined. + +(* a harder example *) + +Definition UU := Type . +Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t. +Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0. +Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1. +Proof. intros t. exact t. Defined. + +Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k). +Proof. + destruct k. + apply idpath. +Defined. + +(* an example with two constructors *) + +Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := +| newfoo1 : foo' x0 x0 +| newfoo2 : foo' x0 x0 . +Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} : + foo' x0 x1 -> foo' x0 x1. +Proof. intros t. exact t. Defined. +Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k). +Proof. + destruct k. + apply idpath. + apply idpath. +Defined. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 469cbeb7..e00701fb 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -16,7 +16,7 @@ auto. Qed. Lemma lem3 : forall P : Prop, P. -intro P; pattern P in |- *. +intro P; pattern P. apply lem2. Abort. @@ -34,7 +34,7 @@ Require Import Relations. Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X). Proof. - unfold transitive in |- *. + unfold transitive. intros X f g h H1 H2. inversion H1. Abort. diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes-coercion.v new file mode 100644 index 00000000..d7504340 --- /dev/null +++ b/test-suite/success/universes-coercion.v @@ -0,0 +1,22 @@ +(* This example used to emphasize the absence of LEGO-style universe + polymorphism; Matthieu's improvements of typing on 2011/3/11 now + makes (apparently) that Amokrane's automatic eta-expansion in the + coercion mechanism works; this makes its illustration as a "weakness" + of universe polymorphism obsolete (example submitted by Randy Pollack). + + Note that this example is not an evidence that the current + non-kernel eta-expansion behavior is the most expected one. +*) + +Parameter K : forall T : Type, T -> T. +Check (K (forall T : Type, T -> T) K). + +(* + note that the inferred term is + "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))" + which is not eta-equivalent to + "(K (forall T : Type, T -> T) K" + because the eta-expansion of the latter + "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)" + assuming K of type "forall T (* u2 *) : Type, T -> T" +*) |