diff options
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/Hints.v | 44 | ||||
-rw-r--r-- | test-suite/success/apply.v | 47 | ||||
-rw-r--r-- | test-suite/success/auto.v | 2 | ||||
-rw-r--r-- | test-suite/success/extraction_polyprop.v | 11 | ||||
-rw-r--r-- | test-suite/success/intros.v | 36 | ||||
-rw-r--r-- | test-suite/success/ltac.v | 19 | ||||
-rw-r--r-- | test-suite/success/namedunivs.v | 2 | ||||
-rw-r--r-- | test-suite/success/polymorphism.v | 30 | ||||
-rw-r--r-- | test-suite/success/primitiveproj.v | 7 | ||||
-rw-r--r-- | test-suite/success/proof_using.v | 76 | ||||
-rw-r--r-- | test-suite/success/record_syntax.v | 47 | ||||
-rw-r--r-- | test-suite/success/sideff.v | 12 | ||||
-rw-r--r-- | test-suite/success/simpl.v | 7 | ||||
-rw-r--r-- | test-suite/success/specialize.v | 20 | ||||
-rw-r--r-- | test-suite/success/univnames.v | 26 |
15 files changed, 367 insertions, 19 deletions
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index cc8cec47..f934a5c7 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -62,3 +62,47 @@ Axiom cast_coalesce : ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2). Hint Rewrite cast_coalesce : ltamer. + +Require Import Program. +Module HintCut. +Class A (f : nat -> nat) := a : True. +Class B (f : nat -> nat) := b : True. +Class C (f : nat -> nat) := c : True. +Class D (f : nat -> nat) := d : True. +Class E (f : nat -> nat) := e : True. + +Instance a_is_b f : A f -> B f. +Proof. easy. Qed. +Instance b_is_c f : B f -> C f. +Proof. easy. Qed. +Instance c_is_d f : C f -> D f. +Proof. easy. Qed. +Instance d_is_e f : D f -> E f. +Proof. easy. Qed. + +Instance a_compose f g : A f -> A g -> A (compose f g). +Proof. easy. Qed. +Instance b_compose f g : B f -> B g -> B (compose f g). +Proof. easy. Qed. +Instance c_compose f g : C f -> C g -> C (compose f g). +Proof. easy. Qed. +Instance d_compose f g : D f -> D g -> D (compose f g). +Proof. easy. Qed. +Instance e_compose f g : E f -> E g -> E (compose f g). +Proof. easy. Qed. + +Instance a_id : A id. +Proof. easy. Qed. + +Instance foo f : + E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ + id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id). +Proof. + Fail Timeout 1 apply _. (* 3.7s *) + +Hint Cut [!*; (a_is_b | b_is_c | c_is_d | d_is_e) ; + (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. + + Timeout 1 Fail apply _. (* 0.06s *) +Abort. +End HintCut.
\ No newline at end of file diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index a4ed76c5..55b666b7 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -333,13 +333,10 @@ exact (refl_equal 3). exact (refl_equal 4). Qed. -(* From 12612, descent in conjunctions is more powerful *) +(* From 12612, Dec 2009, descent in conjunctions is more powerful *) (* 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. - - Added Aug 2014: why it fails is now that trivial unification ?x = goal is - rejected by the descent in conjunctions to avoid surprising results. *) + ill-formed elimination from Prop to the domain of ex which is in Type. *) Goal True. Fail eapply ex_intro. @@ -351,28 +348,32 @@ Fail eapply (ex_intro _). exact I. Qed. -(* Note: the following succeed directly (i.e. w/o "exact I") since - Aug 2014 since the descent in conjunction does not use a "cut" - anymore: the iota-redex is contracted and we get rid of the - uninstantiated evars - - Is it good or not? Maybe it does not matter so much. +(* No failure here, because the domain of ex is in Prop *) Goal True. -eapply (ex_intro (fun _ => True) I). -exact I. (* Not needed since Aug 2014 *) +eapply (ex_intro (fun _ => 0=0) I). +reflexivity. Qed. Goal True. -eapply (ex_intro (fun _ => True) I _). -exact I. (* Not needed since Aug 2014 *) +eapply (ex_intro (fun _ => 0=0) I _). +Unshelve. (* In 8.4: Grab Existential Variables. *) +reflexivity. Qed. Goal True. eapply (fun (A:Prop) (x:A) => conj I x). -exact I. (* Not needed since Aug 2014 *) +Unshelve. (* In 8.4: the goal ?A was there *) +exact I. Qed. -*) + +(* Testing compatibility mode with v8.4 *) + +Goal True. +Fail eapply existT. +Set Universal Lemma Under Conjunction. +eapply existT. +Abort. (* The following was not accepted from r12612 to r12657 *) @@ -463,6 +464,7 @@ Abort. Goal forall H:0=0, H = H. intros. Fail apply eq_sym in H. +Abort. (* Check that unresolved evars not originally present in goal prevent apply in to work*) @@ -546,3 +548,14 @@ apply (foo ?y). Grab Existential Variables. exact 0. Qed. + +(* Test position of new hypotheses when using "apply ... in ... as ..." *) +Goal (True -> 0=0 /\ True) -> True -> False -> True/\0=0. +intros H H0 H1. +apply H in H0 as (a,b). +(* clear H1:False *) match goal with H:_ |- _ => clear H end. +split. +- (* use b:True *) match goal with H:_ |- _ => exact H end. +- (* clear b:True *) match goal with H:_ |- _ => clear H end. + (* use a:0=0 *) match goal with H:_ |- _ => exact H end. +Qed. diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index db3b19af..aaa7b3a5 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -1,6 +1,6 @@ (* Wish #2154 by E. van der Weegen *) -(* auto was not using f_equal-style lemmas with metavariables occuring +(* auto was not using f_equal-style lemmas with metavariables occurring only in the type of an evar of the concl, but not directly in the concl itself *) diff --git a/test-suite/success/extraction_polyprop.v b/test-suite/success/extraction_polyprop.v new file mode 100644 index 00000000..7215bd99 --- /dev/null +++ b/test-suite/success/extraction_polyprop.v @@ -0,0 +1,11 @@ +(* The current extraction cannot handle this situation, + and shouldn't try, otherwise it might produce some Ocaml + code that segfaults. See Table.error_singleton_become_prop + or S. Glondu's thesis for more details. *) + +Definition f {X} (p : (nat -> X) * True) : X * nat := + (fst p 0, 0). + +Definition f_prop := f ((fun _ => I),I). + +Fail Extraction f_prop. diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 9443d01e..35ba94fb 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -33,3 +33,39 @@ Goal True -> True -> True. intros _ ?. exact H. Qed. + +(* A short test about introduction pattern pat/c *) +Goal (True -> 0=0) -> True /\ False -> 0=0. +intros H (H1/H,_). +exact H1. +Qed. + +(* A test about bugs in 8.5beta2 *) +Goal (True -> 0=0) -> True /\ False -> False -> 0=0. +intros H H0 H1. +destruct H0 as (a/H,_). +(* Check that H0 is removed (was bugged in 8.5beta2) *) +Fail clear H0. +(* Check position of newly created hypotheses when using pat/c (was + left at top in 8.5beta2) *) +match goal with H:_ |- _ => clear H end. (* clear H1:False *) +match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *) +Qed. + +Goal (True -> 0=0) -> True -> 0=0. +intros H H1/H. +exact H1. +Qed. + +Goal forall n, n = S n -> 0=0. +intros n H/n_Sn. +destruct H. +Qed. + +(* Another check about generated names and cleared hypotheses with + pat/c patterns *) +Goal (True -> 0=0 /\ 1=1) -> True -> 0=0. +intros H (H1,?)/H. +change (1=1) in H0. +exact H1. +Qed. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index badce063..6c4d4ae9 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -298,3 +298,22 @@ 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 instantiation of binders using ltac names *) + +Goal True. +let x := ipattern:y in assert (forall x y, x = y + 0). +intro. +destruct y. (* Check that the name is y here *) +Abort. + +(* An example suggested by Jason (see #4317) showing the intended semantics *) +(* Order of binders is reverted because y is just told to depend on x *) + +Goal 1=1. +let T := constr:(fun a b : nat => a) in + lazymatch T with + | (fun x z => ?y) => pose ((fun x x => y) 2 1) + end. +exact (eq_refl n). +Qed. diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v index 059462fa..f9154ef5 100644 --- a/test-suite/success/namedunivs.v +++ b/test-suite/success/namedunivs.v @@ -4,6 +4,8 @@ (* Fail exact H. *) (* Section . *) +Unset Strict Universe Declaration. + Section lift_strict. Polymorphic Definition liftlt := let t := Type@{i} : Type@{k} in diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 9167c9fc..d6bbfe29 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -1,3 +1,5 @@ +Unset Strict Universe Declaration. + Module withoutpoly. Inductive empty :=. @@ -292,3 +294,31 @@ Section foo2. Context `{forall A B, Funext A B}. Print Universes. End foo2. + +Module eta. +Set Universe Polymorphism. + +Set Printing Universes. + +Axiom admit : forall A, A. +Record R := {O : Type}. + +Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}. +Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl. +Definition RLRL' : forall x : R, RL x = RL (RL x). + intros. apply eq_refl. +Qed. + +End eta. + +Module Hurkens'. + Require Import Hurkens. + +Polymorphic Record box (X : Type) (T := Type) : Type := wrap { unwrap : T }. + +Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw. + +Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _ +Type)) eq_refl. + +End Hurkens'.
\ No newline at end of file diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 068f8ac3..125615c5 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -188,3 +188,10 @@ Set Printing All. Check (@p' nat). Check p'. Unset Printing All. + +Record wrap (A : Type) := { unwrap : A; unwrap2 : A }. + +Definition term (x : wrap nat) := x.(unwrap). +Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x. +Recursive Extraction term term'. +(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index 61e73f85..c83f45e2 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -117,5 +117,81 @@ End T1. Check (bla 7 : 2 = 8). +Section A. +Variable a : nat. +Variable b : nat. +Variable c : nat. +Variable H1 : a = 3. +Variable H2 : a = 3 -> b = 7. +Variable H3 : c = 3. + +Lemma foo : a = a. +Proof using Type*. +pose H1 as e1. +pose H2 as e2. +reflexivity. +Qed. + +Lemma bar : a = 3 -> b = 7. +Proof using b*. +exact H2. +Qed. + +Lemma baz : c=3. +Proof using c*. +exact H3. +Qed. + +Lemma baz2 : c=3. +Proof using c* a. +exact H3. +Qed. + +End A. + +Check (foo 3 7 (refl_equal 3) + (fun _ => refl_equal 7)). +Check (bar 3 7 (refl_equal 3) + (fun _ => refl_equal 7)). +Check (baz2 99 3 (refl_equal 3)). +Check (baz 3 (refl_equal 3)). + +Section Let. + +Variables a b : nat. +Let pa : a = a. Proof. reflexivity. Qed. +Unset Default Proof Using. +Set Suggest Proof Using. +Lemma test_let : a = a. +Proof using a. +exact pa. +Qed. + +Let ppa : pa = pa. Proof. reflexivity. Qed. + +Lemma test_let2 : pa = pa. +Proof using Type. +exact ppa. +Qed. + +End Let. + +Check (test_let 3). + +Section Clear. + +Variable a: nat. +Hypotheses H : a = 4. + +Set Proof Using Clear Unused. + +Lemma test_clear : a = a. +Proof using a. +Fail rewrite H. +trivial. +Qed. + +End Clear. + diff --git a/test-suite/success/record_syntax.v b/test-suite/success/record_syntax.v new file mode 100644 index 00000000..db2bbb0d --- /dev/null +++ b/test-suite/success/record_syntax.v @@ -0,0 +1,47 @@ +Module A. + +Record Foo := { foo : unit; bar : unit }. + +Definition foo_ := {| + foo := tt; + bar := tt +|}. + +Definition foo0 (p : Foo) := match p with {| |} => tt end. +Definition foo1 (p : Foo) := match p with {| foo := f |} => f end. +Definition foo2 (p : Foo) := match p with {| foo := f; |} => f end. +Definition foo3 (p : Foo) := match p with {| foo := f; bar := g |} => (f, g) end. +Definition foo4 (p : Foo) := match p with {| foo := f; bar := g; |} => (f, g) end. + +End A. + +Module B. + +Record Foo := { }. + +End B. + +Module C. + +Record Foo := { foo : unit; bar : unit; }. + +Definition foo_ := {| + foo := tt; + bar := tt; +|}. + +End C. + +Module D. + +Record Foo := { foo : unit }. +Definition foo_ := {| foo := tt |}. + +End D. + +Module E. + +Record Foo := { foo : unit; }. +Definition foo_ := {| foo := tt; |}. + +End E. diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v new file mode 100644 index 00000000..3c0b8156 --- /dev/null +++ b/test-suite/success/sideff.v @@ -0,0 +1,12 @@ +Definition idw (A : Type) := A. +Lemma foobar : unit. +Proof. + Require Import Program. + apply (const tt tt). +Qed. + +Lemma foobar' : unit. + Lemma aux : forall A : Type, A -> unit. + Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed. + apply (@aux unit tt). +Qed. diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index e540ae5f..5b87e877 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -98,3 +98,10 @@ Fail simpl (unbox _ (unbox _ _)) at 3 4. (* Nested and even overlapping *) simpl (unbox _ (unbox _ _)) at 2 4. match goal with |- unbox _ (Box _ True) = unbox _ (Box _ True) => idtac end. Abort. + +(* Check interpretation of ltac variables (was broken in 8.5 beta 1 and 2 *) + +Goal 2=1+1. +match goal with |- (_ = ?c) => simpl c end. +match goal with |- 2 = 2 => idtac end. (* Check that it reduced *) +Abort. diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index c5f032be..3faa1ca4 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -45,4 +45,22 @@ specialize eq_trans with _ a b c. intros _. (* Anomaly: Evar ?88 was not declared. Please report. *) *) -Abort.
\ No newline at end of file +Abort. + +(* Test use of pose proof and assert as a specialize *) + +Goal True -> (True -> 0=0) -> False -> 0=0. +intros H0 H H1. +pose proof (H I) as H. +(* Check that the hypothesis is in 2nd position by removing the top one *) +match goal with H:_ |- _ => clear H end. +match goal with H:_ |- _ => exact H end. +Qed. + +Goal True -> (True -> 0=0) -> False -> 0=0. +intros H0 H H1. +assert (H:=H I). +(* Check that the hypothesis is in 2nd position by removing the top one *) +match goal with H:_ |- _ => clear H end. +match goal with H:_ |- _ => exact H end. +Qed. diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v new file mode 100644 index 00000000..048b53d2 --- /dev/null +++ b/test-suite/success/univnames.v @@ -0,0 +1,26 @@ +Set Universe Polymorphism. + +Definition foo@{i j} (A : Type@{i}) (B : Type@{j}) := A. + +Set Printing Universes. + +Fail Definition bar@{i} (A : Type@{i}) (B : Type) := A. + +Definition baz@{i j} (A : Type@{i}) (B : Type@{j}) := (A * B)%type. + +Fail Definition bad@{i j} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type. + +Fail Definition bad@{i} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type. + +Definition shuffle@{i j} (A : Type@{j}) (B : Type@{i}) := (A * B)%type. + +Definition nothing (A : Type) := A. + +Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla. + +Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy. + + +Monomorphic Universe g. + +Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file |