From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- test-suite/success/AdvancedCanonicalStructure.v | 18 +- test-suite/success/CaseAlias.v | 70 +++ test-suite/success/Cases.v | 83 ++-- test-suite/success/CasesDep.v | 54 +++ test-suite/success/Check.v | 2 +- test-suite/success/Discriminate.v | 6 + test-suite/success/Field.v | 4 +- test-suite/success/Hints.v | 2 +- test-suite/success/Inductive.v | 29 ++ test-suite/success/Inversion.v | 15 +- test-suite/success/LegacyField.v | 4 +- test-suite/success/Notations.v | 27 ++ test-suite/success/Nsatz.v | 574 +++++++++++++++++------- test-suite/success/PCase.v | 66 +++ test-suite/success/PrintSortedUniverses.v | 2 + test-suite/success/ProgramWf.v | 6 + test-suite/success/RecTutorial.v | 98 ++-- test-suite/success/Scheme.v | 4 + test-suite/success/Tauto.v | 4 +- test-suite/success/TestRefine.v | 2 +- test-suite/success/apply.v | 34 +- test-suite/success/auto.v | 26 ++ test-suite/success/autorewrite.v | 29 ++ test-suite/success/autorewritein.v | 23 - test-suite/success/bullet.v | 5 + test-suite/success/change.v | 8 + test-suite/success/coercions.v | 8 + test-suite/success/conv_pbs.v | 5 + test-suite/success/destruct.v | 19 + test-suite/success/eauto.v | 2 +- test-suite/success/eqdecide.v | 9 +- test-suite/success/eta.v | 19 + test-suite/success/evars.v | 71 +++ test-suite/success/extraction.v | 4 +- test-suite/success/fix.v | 5 +- test-suite/success/implicit.v | 17 + test-suite/success/inds_type_sec.v | 2 +- test-suite/success/induct.v | 25 +- test-suite/success/ltac.v | 27 ++ test-suite/success/mutual_ind.v | 2 +- test-suite/success/polymorphism.v | 2 +- test-suite/success/proof_using.v | 61 +++ test-suite/success/remember.v | 8 + test-suite/success/rewrite.v | 21 + test-suite/success/searchabout.v | 60 +++ test-suite/success/setoid_test.v | 35 ++ test-suite/success/simpl_tuning.v | 149 ++++++ test-suite/success/telescope_canonical.v | 12 + test-suite/success/unfold.v | 2 +- test-suite/success/unification.v | 50 ++- test-suite/success/universes-coercion.v | 22 + 51 files changed, 1516 insertions(+), 316 deletions(-) create mode 100644 test-suite/success/PCase.v create mode 100644 test-suite/success/PrintSortedUniverses.v create mode 100644 test-suite/success/Scheme.v create mode 100644 test-suite/success/auto.v create mode 100644 test-suite/success/autorewrite.v delete mode 100644 test-suite/success/autorewritein.v create mode 100644 test-suite/success/bullet.v create mode 100644 test-suite/success/eta.v create mode 100644 test-suite/success/proof_using.v create mode 100644 test-suite/success/remember.v create mode 100644 test-suite/success/searchabout.v create mode 100644 test-suite/success/simpl_tuning.v create mode 100644 test-suite/success/telescope_canonical.v create mode 100644 test-suite/success/universes-coercion.v (limited to 'test-suite/success') 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..745529bf 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -543,7 +543,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 +611,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 @@ -1064,7 +1085,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 +1093,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 diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 29721843..d3b7cf3f 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 *) @@ -506,3 +540,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..47180ef6 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 *) -(* fun H => apply H. (* Checks that local names are accepted *) Section A. Remark Refl : forall (A : Set) (x : A), x = x. - Proof. exact refl_equal. Defined. + Proof. exact @refl_equal. Defined. Definition Sym := sym_equal. Let Trans := trans_equal. 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..df4da431 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 *) -(* 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. 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/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..00a13aed 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. diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index d4e6a82e..2602c7e3 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -55,13 +55,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 +315,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. @@ -543,7 +543,7 @@ Inductive ex_Set (P : Set -> Prop) : Type := 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. @@ -966,37 +966,37 @@ 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), + Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t 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. +> Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n), n= 0 -> v = Vnil A. > ^^^^^^ Error: In environment A : Set n : nat -v : vector A n +v : Vector.t A n e : n = 0 -The term "Vnil A" has type "vector A 0" while it is expected to have type - "vector A n" +The term "Vnil A" 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 +1004,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 +1063,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/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/Tauto.v b/test-suite/success/Tauto.v index 324d340a..c4e67677 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 *) -(* ... 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 *) @@ -326,13 +333,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 +397,21 @@ 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. 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/autorewrite.v b/test-suite/success/autorewrite.v new file mode 100644 index 00000000..5e9064f8 --- /dev/null +++ b/test-suite/success/autorewrite.v @@ -0,0 +1,29 @@ +Variable Ack : nat -> nat -> nat. + +Axiom Ack0 : forall m : nat, Ack 0 m = S m. +Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1. +Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m). + +Hint Rewrite Ack0 Ack1 Ack2 : base0. + +Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. +Proof. + intros. + autorewrite with base0 in H using try (apply H; reflexivity). +Qed. + +Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. +Proof. + intros. + autorewrite with base0 in *. + 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/autorewritein.v b/test-suite/success/autorewritein.v deleted file mode 100644 index 68f2f7ce..00000000 --- a/test-suite/success/autorewritein.v +++ /dev/null @@ -1,23 +0,0 @@ -Variable Ack : nat -> nat -> nat. - -Axiom Ack0 : forall m : nat, Ack 0 m = S m. -Axiom Ack1 : forall n : nat, Ack (S n) 0 = Ack n 1. -Axiom Ack2 : forall n m : nat, Ack (S n) (S m) = Ack n (Ack (S n) m). - -Hint Rewrite Ack0 Ack1 Ack2 : base0. - -Lemma ResAck0 : (Ack 2 2 = 7 -> False) -> False. -Proof. - intros. - autorewrite with base0 in H using try (apply H; reflexivity). -Qed. - -Lemma ResAck1 : forall H:(Ack 2 2 = 7 -> False), True -> False. -Proof. - intros. - autorewrite with base0 in *. - apply H;reflexivity. -Qed. - - - 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..c65cf303 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -30,3 +30,11 @@ change 3 at 1 with (1+2) in H |- *. change 3 at 1 with (1+2) in H, H|-. change 3 in |- * 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..001beae7 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -81,3 +81,11 @@ 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. 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/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..a94d8b1d 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 *) -(* 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..2f1ec757 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -238,3 +238,74 @@ 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). diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 4fec6e7f..3f8a3bc4 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 *) -(* 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..234c4223 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 *) -(* (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..fcadd150 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 *) -(* 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 in |- *. +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..d9ade314 --- /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 Zmult Zplus "distr". +SearchAbout "+"%Z "*"%Z "distr" -positive -Prop. +SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 033b3f48..19693d70 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -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/telescope_canonical.v b/test-suite/success/telescope_canonical.v new file mode 100644 index 00000000..8a607c93 --- /dev/null +++ b/test-suite/success/telescope_canonical.v @@ -0,0 +1,12 @@ +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 foo (n : hidden_nat) : P _ n. +Admitted. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 66c4e080..5649e2f7 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 *) -(* 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/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" +*) -- cgit v1.2.3