diff options
Diffstat (limited to 'test-suite')
45 files changed, 874 insertions, 45 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 207f25ed0b..f333ae63e3 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -391,7 +391,7 @@ misc/deps-order.log: } > "$@" # Sort universes for the whole standard library -EXPECTED_UNIVERSES := 5 +EXPECTED_UNIVERSES := 4 # Prop is not counted universes: misc/universes.log misc/universes.log: misc/universes/all_stdlib.v @echo "TEST misc/universes" diff --git a/test-suite/bugs/opened/2800.v b/test-suite/bugs/closed/2800.v index c559ab0c17..2ee438934e 100644 --- a/test-suite/bugs/opened/2800.v +++ b/test-suite/bugs/closed/2800.v @@ -1,6 +1,6 @@ Goal False. -Fail intuition +intuition match goal with | |- _ => idtac " foo" end. diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 9125ab16dd..25060debe2 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -35,6 +35,9 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (r : p..1 = q..1) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. + +Declare ML Module "coretactics". + Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x)) (xx : @paths (@sigT A (fun x0 : A => B x0)) x x), @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index aad0bb44d5..8dadc2419c 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -65,7 +65,7 @@ Module NonPrim. set (fibermap := fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0)). Set Printing Implicit. - let G := match goal with |- ?G => constr:G end in + let G := match goal with |- ?G => constr:(G) end in first [ match goal with | [ |- (@isconnected_elim n (@hfiber A B f (f a)) (@isconnected_hfiber_conn_map n A B f H (f a)) @@ -142,7 +142,7 @@ Module Prim. set (fibermap := fun a0p : hfiber f (f a) => let (a0, p) := a0p in transport P p (d a0)). Set Printing Implicit. - let G := match goal with |- ?G => constr:G end in + let G := match goal with |- ?G => constr:(G) end in first [ match goal with | [ |- (@isconnected_elim n (@hfiber A B f (f a)) (@isconnected_hfiber_conn_map n A B f H (f a)) diff --git a/test-suite/bugs/opened/3849.v b/test-suite/bugs/closed/3849.v index 5290054a06..a8dc3af9cf 100644 --- a/test-suite/bugs/opened/3849.v +++ b/test-suite/bugs/closed/3849.v @@ -5,4 +5,4 @@ Tactic Notation "bar" hyp_list(hs) := foo hs. Goal True. do 5 pose proof 0 as ?n0. foo n1 n2. -Fail bar n3 n4. +bar n3 n4. diff --git a/test-suite/bugs/closed/3881.v b/test-suite/bugs/closed/3881.v index 070d1e9c71..a327bbf2a9 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -23,7 +23,7 @@ Proof. pose (fun H => @isequiv_homotopic _ _ ((g o f) o f^-1) _ H (fun b => ap g (eisretr f b))) as k. revert k. - let x := match goal with |- let k := ?x in _ => constr:x end in + let x := match goal with |- let k := ?x in _ => constr:(x) end in intro k; clear k; pose (x _). pose (@isequiv_homotopic _ _ ((g o f) o f^-1) g _ diff --git a/test-suite/bugs/closed/3911.v b/test-suite/bugs/closed/3911.v new file mode 100644 index 0000000000..b289eafbf4 --- /dev/null +++ b/test-suite/bugs/closed/3911.v @@ -0,0 +1,26 @@ +(* Tested against coq ee596bc *) + +Set Nonrecursive Elimination Schemes. +Set Primitive Projections. +Set Universe Polymorphism. + +Record setoid := { base : Type }. + +Definition catdata (Obj Arr : Type) : Type := nat. + (* [nat] can be replaced by any other type, it seems, + without changing the error *) + +Record cat : Type := + { + obj : setoid; + arr : Type; + dta : catdata (base obj) arr + }. + +Definition bcwa (C:cat) (B:setoid) :Type := nat. + (* As above, nothing special about [nat] here. *) + +Record temp {C}{B} (e:bcwa C B) := + { fld : base (obj C) }. + +Print temp_rect. diff --git a/test-suite/bugs/closed/3929.v b/test-suite/bugs/closed/3929.v new file mode 100644 index 0000000000..4031dcc45e --- /dev/null +++ b/test-suite/bugs/closed/3929.v @@ -0,0 +1,12 @@ +Goal True. +evar (T:Type). +pose (Z:=nat). +let Tv:=eval cbv [T] in T in +pose (x:=Tv). +revert x. +refine (_ : let x:=Z in True). +let Zv:=eval cbv [Z] in Z in +let Tv:=eval cbv [T] in T in +constr_eq Zv Tv. +Abort. + diff --git a/test-suite/bugs/closed/3957.v b/test-suite/bugs/closed/3957.v new file mode 100644 index 0000000000..e20a6e97f0 --- /dev/null +++ b/test-suite/bugs/closed/3957.v @@ -0,0 +1,6 @@ +Ltac foo tac := tac. + +Goal True. +Proof. +foo subst. +Admitted. diff --git a/test-suite/bugs/opened/4214.v b/test-suite/bugs/closed/4214.v index 3daf452132..d684e8cf4b 100644 --- a/test-suite/bugs/opened/4214.v +++ b/test-suite/bugs/closed/4214.v @@ -2,4 +2,5 @@ Goal forall A (a b c : A), b = a -> b = c -> a = c. intros. subst. -Fail reflexivity. +reflexivity. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4479.v b/test-suite/bugs/closed/4479.v new file mode 100644 index 0000000000..921579d1e1 --- /dev/null +++ b/test-suite/bugs/closed/4479.v @@ -0,0 +1,3 @@ +Goal True. +Fail autorewrite with foo. +try autorewrite with foo. diff --git a/test-suite/bugs/opened/3410.v b/test-suite/bugs/opened/3410.v deleted file mode 100644 index 0d259181aa..0000000000 --- a/test-suite/bugs/opened/3410.v +++ /dev/null @@ -1 +0,0 @@ -Fail repeat match goal with H:_ |- _ => setoid_rewrite X in H end. diff --git a/test-suite/bugs/opened/3889.v b/test-suite/bugs/opened/3889.v new file mode 100644 index 0000000000..6b287324cc --- /dev/null +++ b/test-suite/bugs/opened/3889.v @@ -0,0 +1,11 @@ +Require Import Program. + +Inductive Even : nat -> Prop := +| evenO : Even O +| evenS : forall n, Odd n -> Even (S n) +with Odd : nat -> Prop := +| oddS : forall n, Even n -> Odd (S n). +Axiom admit : forall {T}, T. +Program Fixpoint doubleE {n} (e : Even n) : Even (2 * n) := admit +with doubleO {n} (o : Odd n) : Odd (S (2 * n)) := _. +Next Obligation of doubleE. diff --git a/test-suite/bugs/opened/3890.v b/test-suite/bugs/opened/3890.v new file mode 100644 index 0000000000..f9ac9be2c8 --- /dev/null +++ b/test-suite/bugs/opened/3890.v @@ -0,0 +1,18 @@ +Class Foo. +Class Bar := b : Type. + +Instance foo : Foo := _. +(* 1 subgoals, subgoal 1 (ID 4) + + ============================ + Foo *) + +Instance bar : Bar. +exact Type. +Defined. +(* bar is defined *) + +About foo. +(* foo not a defined object. *) + +Fail Defined. diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v new file mode 100644 index 0000000000..fd95503e6b --- /dev/null +++ b/test-suite/bugs/opened/3916.v @@ -0,0 +1,3 @@ +Require Import List. + +Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *) diff --git a/test-suite/bugs/opened/3919.v-disabled b/test-suite/bugs/opened/3919.v-disabled new file mode 100644 index 0000000000..0d661de9c4 --- /dev/null +++ b/test-suite/bugs/opened/3919.v-disabled @@ -0,0 +1,13 @@ +Require Import MSets. +Require Import Orders. + +Declare Module Signal : OrderedType. + +Module S := MSetAVL.Make(Signal). +Module Sdec := Decide(S). +Export Sdec. + +Hint Extern 0 (Signal.eq ?x ?y) => now symmetry. + +Goal forall o s, Signal.eq o s. +Proof. fsetdec. Qed. diff --git a/test-suite/bugs/opened/3922.v-disabled b/test-suite/bugs/opened/3922.v-disabled new file mode 100644 index 0000000000..ce4f509cad --- /dev/null +++ b/test-suite/bugs/opened/3922.v-disabled @@ -0,0 +1,83 @@ +Set Universe Polymorphism. +Notation Type0 := Set. + +Definition Type1 := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. + +Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x) + := forall x:A, f x = g x. + +Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. + +Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope. +Local Open Scope trunc_scope. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. + +Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := + match n with + | -2 => Contr_internal A + | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y) + end. + +Class IsTrunc (n : trunc_index) (A : Type) : Type := + Trunc_is_trunc : IsTrunc_internal n A. + +Notation Contr := (IsTrunc -2). +Notation IsHProp := (IsTrunc -1). + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Inductive Unit : Type1 := + tt : Unit. + +Record TruncType (n : trunc_index) := BuildTruncType { + trunctype_type : Type ; + istrunc_trunctype_type : IsTrunc n trunctype_type +}. + +Arguments BuildTruncType _ _ {_}. + +Coercion trunctype_type : TruncType >-> Sortclass. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (-1)-Type. + +Notation BuildhProp := (BuildTruncType -1). + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + +Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i}) +: IsTrunc@{j} n (Trunc@{i} n A). +Admitted. + +Definition Trunc_ind {n A} + (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)} + : (forall a, P (tr a)) -> (forall aa, P aa) +:= (fun f aa => match aa with tr a => fun _ => f a end Pt). +Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). +Definition cconst_factors_contr `{Funext} {X Y : Type} (f : X -> Y) + (P : Type) `{Pc : X -> Contr P} + (g : X -> P) (h : P -> Y) (p : h o g == f) +: Unit. +Proof. + assert (merely X -> IsHProp P) by admit. + refine (let g' := Trunc_ind (fun _ => P) g : merely X -> P in _); + [ assumption.. | ]. + Fail pose (g' := Trunc_ind (fun _ => P) g : merely X -> P). diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v new file mode 100644 index 0000000000..cfad763572 --- /dev/null +++ b/test-suite/bugs/opened/3926.v @@ -0,0 +1,30 @@ +Notation compose := (fun g f x => g (f x)). +Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. +Open Scope function_scope. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Arguments idpath {A a} , [A] a. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. +Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. +Local Open Scope equiv_scope. +Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x. +Generalizable Variables A B C f g. +Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000 + := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1). +Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g + := Build_IsEquiv _ _ g (f ^-1). +Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000 + := Build_IsEquiv B A f^-1 f. +Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} + `{IsEquiv A B f} `{IsEquiv A C (g o f)} + : IsEquiv g. +Proof. + Unset Typeclasses Modulo Eta. + exact (isequiv_homotopic (compose (compose g f) f^-1) + (fun b => ap g (eisretr f b))) || fail "too early". + Undo. + Set Typeclasses Modulo Eta. + Set Typeclasses Dependency Order. + Set Typeclasses Debug. + Fail exact (isequiv_homotopic (compose (compose g f) f^-1) + (fun b => ap g (eisretr f b))). diff --git a/test-suite/bugs/opened/3928.v-disabled b/test-suite/bugs/opened/3928.v-disabled new file mode 100644 index 0000000000..b470eb229b --- /dev/null +++ b/test-suite/bugs/opened/3928.v-disabled @@ -0,0 +1,12 @@ +Typeclasses eauto := bfs. + +Class Foo := {}. +Class Bar := {}. + +Instance: Bar. +Instance: Foo -> Bar -> Foo -> Foo | 1. +Instance: Bar -> Foo | 100. +Instance: Foo -> Bar -> Foo -> Foo | 1. + +Set Typeclasses Debug. +Timeout 1 Check (_ : Foo). (* timeout *) diff --git a/test-suite/bugs/opened/3938.v b/test-suite/bugs/opened/3938.v new file mode 100644 index 0000000000..2d0d1930f1 --- /dev/null +++ b/test-suite/bugs/opened/3938.v @@ -0,0 +1,6 @@ +Require Import Coq.Arith.PeanoNat. +Hint Extern 1 => admit : typeclass_instances. +Goal forall a b (f : nat -> Set), Nat.eq a b -> f a = f b. + intros a b f H. + rewrite H. (* Toplevel input, characters 15-25: +Anomaly: Evar ?X11 was not declared. Please report. *) diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/3946.v new file mode 100644 index 0000000000..e77bdbc652 --- /dev/null +++ b/test-suite/bugs/opened/3946.v @@ -0,0 +1,11 @@ +Require Import ZArith. + +Inductive foo := Foo : Z.le 0 1 -> foo. + +Definition bar (f : foo) := let (f) := f in f. + +(* Doesn't work: *) +(* Arguments bar f.*) + +(* Does work *) +Arguments bar f _. diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v new file mode 100644 index 0000000000..165813084d --- /dev/null +++ b/test-suite/bugs/opened/3948.v @@ -0,0 +1,25 @@ +Module Type S. +Parameter t : Type. +End S. + +Module Bar(X : S). +Proof. + Definition elt := X.t. + Axiom fold : elt. +End Bar. + +Module Make (X: S) := Bar(X). + +Declare Module X : S. + +Module Type Interface. + Parameter constant : unit. +End Interface. + +Module DepMap : Interface. + Module Dom := Make(X). + Definition constant : unit := + let _ := @Dom.fold in tt. +End DepMap. + +Print Assumptions DepMap.constant.
\ No newline at end of file diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v index 52dae265bd..04fa59075b 100644 --- a/test-suite/complexity/ring2.v +++ b/test-suite/complexity/ring2.v @@ -39,7 +39,7 @@ Admitted. Ltac Zcst t := match isZcst t with true => t - | _ => constr:NotConstant + | _ => constr:(NotConstant) end. Add Ring Zr : Zth diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v index 91de87332f..8089de2bf0 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -5,5 +5,47 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Fail Inductive t : Set := - c : (t -> nat) -> t. + +(* Negative occurrence *) +Fail Inductive t : Type := + c : (t -> nat) -> t. + +(* Non-strictely positive occurrence *) +Fail Inductive t : Type := + c : ((t -> nat) -> nat) -> t. + +(* Self-nested type (no proof of + soundness yet *) +Fail Inductive t (A:Type) : Type := + c : t (t A) -> t A. + +(* Nested inductive types *) + +Inductive pos (A:Type) := + p : pos A -> pos A. + +Inductive nnpos (A:Type) := + nnp : ((A -> nat) -> nat) -> nnpos A. + +Inductive neg (A:Type) := + n : (A->neg A) -> neg A. + +Inductive arg : Type -> Prop := + a : forall A, arg A -> arg A. + +(* Strictly covariant parameter: accepted. *) +Fail Fail Inductive t := + c : pos t -> t. + +(* Non-strictly covariant parameter: not + strictly positive. *) +Fail Inductive t := + c : nnpos t -> t. + +(* Contravariant parameter: not positive. *) +Fail Inductive t := + c : neg t -> t. + +(* Strict index: not positive. *) +Fail Inductive t := + c : arg t -> t. diff --git a/test-suite/ide/undo013.fake b/test-suite/ide/undo013.fake index f44156aa38..921a9d0f0d 100644 --- a/test-suite/ide/undo013.fake +++ b/test-suite/ide/undo013.fake @@ -23,5 +23,5 @@ ADD { Qed. } ADD { apply H. } # </replay> ADD { Qed. } -QUERY { Fail idtac. } +QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo014.fake b/test-suite/ide/undo014.fake index 6d58b061e6..f5fe774704 100644 --- a/test-suite/ide/undo014.fake +++ b/test-suite/ide/undo014.fake @@ -22,5 +22,5 @@ ADD { destruct H. } ADD { Qed. } ADD { apply H. } ADD { Qed. } -QUERY { Fail idtac. } +QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo015.fake b/test-suite/ide/undo015.fake index ac17985aab..a1e5c947b3 100644 --- a/test-suite/ide/undo015.fake +++ b/test-suite/ide/undo015.fake @@ -25,5 +25,5 @@ ADD { destruct H. } ADD { Qed. } ADD { apply H. } ADD { Qed. } -QUERY { Fail idtac. } +QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } diff --git a/test-suite/ide/undo016.fake b/test-suite/ide/undo016.fake index bdb81ecd95..f9414c1ea7 100644 --- a/test-suite/ide/undo016.fake +++ b/test-suite/ide/undo016.fake @@ -27,5 +27,5 @@ ADD { destruct H. } ADD { Qed. } ADD { apply H. } ADD { Qed. } -QUERY { Fail idtac. } +QUERY { Fail Show. } QUERY { Check (aa,bb,cc). } diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index 8767f6874e..abf8be72ef 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -53,8 +53,7 @@ Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. - unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Z.mul_1_r. - intros HQeq. + unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq. assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 09f032d478..f44465456f 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -48,8 +48,8 @@ f = fun H : B => match H with | AC x => - (let b0 := b in - if b0 as b return (P b -> True) + let b0 := b in + (if b0 as b return (P b -> True) then fun _ : P true => Logic.I else fun _ : P false => Logic.I) x end diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 4116a5ebc2..a4d19d6930 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -72,8 +72,8 @@ Inductive B : Prop := AC : P b -> B. Definition f : B -> True. Proof. -intros []. -destruct b as [|] ; intros _ ; exact Logic.I. +intros [x]. +destruct b as [|] ; exact Logic.I. Defined. Print f. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 4512e2c5ce..576fbd7c0b 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,7 +6,7 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n in ?y ?y0 : T n +fun n : nat => let x := A n : T n in ?y ?y0 : T n : forall n : nat, T n where ?y : [n : nat x := A n : T n |- ?T -> T n] diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v index 0d75d52a31..06357cfc21 100644 --- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v @@ -1902,14 +1902,14 @@ Qed. Lemma Zsgn_15 : forall x y : Z, Zsgn (x * y) = (Zsgn x * Zsgn y)%Z. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; constructor. + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; constructor. Qed. Lemma Zsgn_16 : forall x y : Z, Zsgn (x * y) = 1%Z -> {(0 < x)%Z /\ (0 < y)%Z} + {(x < 0)%Z /\ (y < 0)%Z}. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; try discriminate H; [ left | right ]; repeat split. Qed. @@ -1917,13 +1917,13 @@ Lemma Zsgn_17 : forall x y : Z, Zsgn (x * y) = (-1)%Z -> {(0 < x)%Z /\ (y < 0)%Z} + {(x < 0)%Z /\ (0 < y)%Z}. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; try discriminate H; [ left | right ]; repeat split. Qed. Lemma Zsgn_18 : forall x y : Z, Zsgn (x * y) = 0%Z -> {x = 0%Z} + {y = 0%Z}. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; try discriminate H; [ left | right | right ]; constructor. Qed. @@ -1932,40 +1932,40 @@ Qed. Lemma Zsgn_19 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 < x + y)%Z. Proof. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; discriminate H || (constructor || apply Zsgn_12; assumption). Qed. Lemma Zsgn_20 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x + y < 0)%Z. Proof. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intro H; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H; discriminate H || (constructor || apply Zsgn_11; assumption). Qed. Lemma Zsgn_21 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= x)%Z. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intros H H0; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0; discriminate H || discriminate H0. Qed. Lemma Zsgn_22 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x <= 0)%Z. Proof. Proof. - intros [y| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; intros H H0; + intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0; discriminate H || discriminate H0. Qed. Lemma Zsgn_23 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= y)%Z. Proof. - intros [[| p2| p2]| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; + intros [|p1|p1] [|p2|p2]; simpl in |- *; intros H H0; discriminate H || discriminate H0. Qed. Lemma Zsgn_24 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (y <= 0)%Z. Proof. - intros [[| p2| p2]| p1 [| p2| p2]| p1 [| p2| p2]]; simpl in |- *; + intros [|p1|p1] [|p2|p2]; simpl in |- *; intros H H0; discriminate H || discriminate H0. Qed. diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 25e464d677..56ed89ed86 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -68,6 +68,12 @@ einjection (H O). instantiate (1:=O). Abort. +Goal (forall x y : nat, x = y -> S x = S y) -> True. +intros. +einjection (H O ?[y]) as H0. +instantiate (y:=O). +Abort. + (* Test the injection intropattern *) Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b. diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v index 7069bba430..8462d36272 100644 --- a/test-suite/success/MatchFail.v +++ b/test-suite/success/MatchFail.v @@ -9,14 +9,14 @@ Require Export ZArithRing. Ltac compute_POS := match goal with | |- context [(Zpos (xI ?X1))] => - let v := constr:X1 in - match constr:v with + let v := constr:(X1) in + match constr:(v) with | 1%positive => fail 1 | _ => rewrite (BinInt.Pos2Z.inj_xI v) end | |- context [(Zpos (xO ?X1))] => - let v := constr:X1 in - match constr:v with + let v := constr:(X1) in + match constr:(v) with | 1%positive => fail 1 | _ => rewrite (BinInt.Pos2Z.inj_xO v) end diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v new file mode 100644 index 0000000000..9505a56e3f --- /dev/null +++ b/test-suite/success/Notations2.v @@ -0,0 +1,92 @@ +(* This file is giving some examples about how implicit arguments and + scopes are treated when using abbreviations or notations, in terms + or patterns, or when using @ and parentheses in terms and patterns. + +The convention is: + +Constant foo with implicit arguments and scopes used in a term or a pattern: + + foo do not deactivate further arguments and scopes + @foo deactivates further arguments and scopes + (foo x) deactivates further arguments and scopes + (@foo x) deactivates further arguments and scopes + +Notations binding to foo: + +# := foo do not deactivate further arguments and scopes +# := @foo deactivates further arguments and scopes +# x := foo x deactivates further arguments and scopes +# x := @foo x deactivates further arguments and scopes + +Abbreviations binding to foo: + +f := foo do not deactivate further arguments and scopes +f := @foo deactivates further arguments and scopes +f x := foo x do not deactivate further arguments and scopes +f x := @foo x do not deactivate further arguments and scopes +*) + +(* One checks that abbreviations and notations in patterns now behave like in terms *) + +Inductive prod' A : Type -> Type := +| pair' (a:A) B (b:B) (c:bool) : prod' A B. +Arguments pair' [A] a%bool_scope [B] b%bool_scope c%bool_scope. +Notation "0" := true : bool_scope. + +(* 1. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) +Notation c1 x := (pair' x). +Check pair' 0 0 0 : prod' bool bool. +Check (pair' 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *) +Check c1 0 0 0 : prod' bool bool. +Check fun x : prod' bool bool => match x with c1 0 y 0 => 2 | _ => 1 end. + +(* 2. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) +Notation c2 x := (@pair' _ x). +Check (@pair' _ 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *) +Check c2 0 0 0 : prod' bool bool. +Check fun A (x : prod' bool A) => match x with c2 0 y 0 => 2 | _ => 1 end. +Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ => 1 end. + +(* 3. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) +Notation c3 x := ((@pair') _ x). +Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *) +Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *) +Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *) +Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end. + +(* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *) +(* unless an atomic @ is given *) +Notation c4 := (@pair'). +Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end. +Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end. + +(* 5. Notations stop further implicit arguments to be inserted and scopes to be used *) +Notation "# x" := (pair' x) (at level 0, x at level 1). +Check pair' 0 0 0 : prod' bool bool. +Check # 0 _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end. + +(* 6. Notations stop further implicit arguments to be inserted and scopes to be used *) +Notation "## x" := ((@pair') _ x) (at level 0, x at level 1). +Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. +Check ## 0%bool _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end. + +(* 7. Notations stop further implicit arguments to be inserted and scopes to be used *) +Notation "###" := (@pair') (at level 0). +Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check ### _ 0%bool _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with ### _ 0%bool _ y 0%bool => 2 | _ => 1 end. + +(* 8. Notations w/o @ preserves implicit arguments and scopes *) +Notation "####" := pair' (at level 0). +Check #### 0 0 0 : prod' bool bool. +Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end. + +(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *) +Notation "##### x" := (pair' x) (at level 0, x at level 1). +Check ##### 0 _ 0%bool 0%bool : prod' bool bool. +Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 30a2a7429c..d6e590af30 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -57,4 +57,25 @@ Section sec. let's try to get rid of the intermediate constant foo. Surely we can just expand it inline, right? Wrong!: *) Check U (fun x => e x) _. -End sec.
\ No newline at end of file +End sec. + +Module IterativeDeepening. + + Class A. + Class B. + Class C. + + Instance: B -> A | 0. + Instance: C -> A | 0. + Instance: C -> B -> A | 0. + Instance: A -> A | 0. + + Goal C -> A. + intros. + Set Typeclasses Debug. + Fail Timeout 1 typeclasses eauto. + Set Typeclasses Iterative Deepening. + typeclasses eauto. + Qed. + +End IterativeDeepening. diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index a70d919635..dc0527d826 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -129,5 +129,10 @@ Qed. End bug_2447. +(* congruence was supposed to do discriminate but it was bugged for + types with indices *) - +Inductive I : nat -> Type := C : I 0 | D : I 0. +Goal ~C=D. +congruence. +Qed. diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v new file mode 100644 index 0000000000..46174e4810 --- /dev/null +++ b/test-suite/success/decl_mode2.v @@ -0,0 +1,249 @@ +Theorem this_is_trivial: True. +proof. + thus thesis. +end proof. +Qed. + +Theorem T: (True /\ True) /\ True. + split. split. +proof. (* first subgoal *) + thus thesis. +end proof. +trivial. (* second subgoal *) +proof. (* third subgoal *) + thus thesis. +end proof. +Abort. + +Theorem this_is_not_so_trivial: False. +proof. +end proof. (* here a warning is issued *) +Fail Qed. (* fails: the proof in incomplete *) +Admitted. (* Oops! *) + +Theorem T: True. +proof. +escape. +auto. +return. +Abort. + +Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False). +intros a b. +proof. +assume H:(if a then True else False). +reconsider H as False. +reconsider thesis as True. +Abort. + +Theorem T: forall x, x=2 -> 2+x=4. +proof. +let x be such that H:(x=2). +have H':(2+x=2+2) by H. +Abort. + +Theorem T: forall x, x=2 -> 2+x=4. +proof. +let x be such that H:(x=2). +then (2+x=2+2). +Abort. + +Theorem T: forall x, x=2 -> x + x = x * x. +proof. +let x be such that H:(x=2). +have (4 = 4). + ~= (2 * 2). + ~= (x * x) by H. + =~ (2 + 2). + =~ H':(x + x) by H. +Abort. + +Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2. +proof. +let x be such that H:(x + x = x * x). +claim H':((x - 2) * x = 0). +thus thesis. +end claim. +Abort. + +Theorem T: forall (A B:Prop), A -> B -> A /\ B. +intros A B HA HB. +proof. +hence B. +Abort. + +Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C. +intros A B C HA HB HC. +proof. +thus B by HB. +Abort. + +Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B. +intros A B C HA HB HC. +proof. +Fail hence C. (* fails *) +Abort. + +Theorem T: forall (A B:Prop), B -> A \/ B. +intros A B HB. +proof. +hence B. +Abort. + +Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D). +intros A B C D HC HD. +proof. +thus C by HC. +Abort. + +Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. +intros P HP. +proof. +take 2. +Abort. + +Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. +intros P HP. +proof. +hence (P 2). +Abort. + +Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y. +intros P R HP HR. +proof. +thus (P 2) by HP. +Abort. + +Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B. +intros A B P HP HA. +proof. +suffices to have x such that HP':(P x) to show B by HP,HP'. +Abort. + +Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). +intros A P HP HA. +proof. +(* BUG: the next line fails when it should succeed. +Waiting for someone to investigate the bug. +focus on (forall x, x = 2 -> P x). +let x be such that (x = 2). +hence thesis by HP. +end focus. +*) +Abort. + +Theorem T: forall x, x = 0 -> x + x = x * x. +proof. +let x be such that H:(x = 0). +define sqr x as (x * x). +reconsider thesis as (x + x = sqr x). +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +let x:nat. +assume HP:(P x). +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +Fail let x. (* fails because x's type is not clear *) +let x be such that HP:(P x). (* here x's type is inferred from (P x) *) +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x. +proof. +let P:(nat -> Prop). +let x:nat. +assume (P x). (* temporary name created *) +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +let x be such that (P x). (* temporary name created *) +Abort. + +Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A. +proof. +let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A). +consider x such that HP:(P x) and HA:A from H. +Abort. + +(* Here is an example with pairs: *) + +Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p). +proof. +let p:(nat * nat)%type. +consider x:nat,y:nat from p. +reconsider thesis as (x >= y \/ x < y). +Abort. + +Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> +(exists m, P m) -> P 0. +proof. +let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)). +given m such that Hm:(P m). +Abort. + +Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C. +proof. +let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C). +assume HAB:(A \/ B). +per cases on HAB. +suppose A. + hence thesis by HAC. +suppose HB:B. + thus thesis by HB,HBC. +end cases. +Abort. + +Section Coq. + +Hypothesis EM : forall P:Prop, P \/ ~ P. + +Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. +proof. +let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). +per cases of (A \/ ~A) by EM. +suppose (~A). + hence thesis by HNAC. +suppose A. + hence thesis by HAC. +end cases. +Abort. + +Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. +proof. +let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). +per cases on (EM A). +suppose (~A). +Abort. +End Coq. + +Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B. +proof. +let A:Prop,B:Prop,x:bool. +per cases on x. +suppose it is true. + assume A. + hence A. +suppose it is false. + assume B. + hence B. +end cases. +Abort. + +Theorem T: forall (n:nat), n + 0 = n. +proof. +let n:nat. +per induction on n. +suppose it is 0. + thus (0 + 0 = 0). +suppose it is (S m) and H:thesis for m. + then (S (m + 0) = S m). + thus =~ (S m + 0). +end induction. +Abort.
\ No newline at end of file diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index b8c6bf3ff7..1ed731f50f 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -151,3 +151,46 @@ intros x H1 H. induction H. change (0 = z -> True) in IHrepr''. Abort. + +(* Test double induction *) + +(* This was failing in 8.5 and before because of a bug in the order of + hypotheses *) + +Inductive I2 : Type := + C2 : forall x:nat, x=x -> I2. +Goal forall a b:I2, a = b. +double induction a b. +Abort. + +(* This was leaving useless hypotheses in 8.5 and before because of + the same bug. This is a change of compatibility. *) + +Inductive I3 : Prop := + C3 : forall x:nat, x=x -> I3. +Goal forall a b:I3, a = b. +double induction a b. +Fail clear H. (* H should have been erased *) +Abort. + +(* This one had quantification in reverse order in 8.5 and before *) +(* This is a change of compatibility. *) + +Goal forall m n, le m n -> le n m -> n=m. +intros m n. double induction 1 2. +3:destruct 1. (* Should be "S m0 <= m0" *) +Abort. + +(* Idem *) + +Goal forall m n p q, le m n -> le p q -> n+p=m+q. +intros *. double induction 1 2. +3:clear H2. (* H2 should have been erased *) +Abort. + +(* This is unchanged *) + +Goal forall m n:nat, n=m. +double induction m n. +Abort. + diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 11156aa0ee..ee69df9774 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -84,3 +84,47 @@ Qed. Goal forall x : nat, True. intros y%(fun x => x). Abort. + +(* Fixing a bug in the order of side conditions of a "->" step *) + +Goal (True -> 1=0) -> 1=1. +intros ->. +- reflexivity. +- exact I. +Qed. + +Goal forall x, (True -> x=0) -> 0=x. +intros x ->. +- reflexivity. +- exact I. +Qed. + +(* Fixing a bug when destructing a type with let-ins in the constructor *) + +Inductive I := C : let x:=1 in x=1 -> I. +Goal I -> True. +intros [x H]. (* Was failing in 8.5 *) +Abort. + +(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up + to skipping let-ins *) + +Goal I -> 1=1. +intros (H). (* This skips x *) +exact H. +Qed. + +Goal I -> 1=1. +Fail intros (x,H,H'). +Fail intros [|]. +intros (x,H). +exact H. +Qed. + +Goal Acc le 0 -> True. +Fail induction 1 as (n,H). (* Induction hypothesis is missing *) +induction 1 as (n,H,IH). +exact Logic.I. +Qed. + + diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 6c4d4ae98f..ce90990594 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -15,7 +15,7 @@ Ltac F x := idtac; G x with G y := idtac; F y. (* Check that Match Context keeps a closure *) -Ltac U := let a := constr:I in +Ltac U := let a := constr:(I) in match goal with | |- _ => apply a end. @@ -75,7 +75,7 @@ Qed. (* Check context binding *) Ltac sym t := - match constr:t with + match constr:(t) with | context C[(?X1 = ?X2)] => context C [X1 = X2] end. @@ -143,7 +143,7 @@ Qed. Ltac check_binding y := cut ((fun y => y) = S). Goal True. -check_binding ipattern:H. +check_binding ipattern:(H). Abort. (* Check that variables explicitly parsed as ltac variables are not @@ -151,7 +151,7 @@ Abort. Ltac afi tac := intros; tac. Goal 1 = 2. -afi ltac:auto. +afi ltac:(auto). Abort. (* Tactic Notation avec listes *) @@ -174,7 +174,7 @@ Abort. empty args *) Goal True. -match constr:@None with @None => exact I end. +match constr:(@None) with @None => exact I end. Abort. (* Check second-order pattern unification *) @@ -218,7 +218,7 @@ Ltac Z1 t := set (x:=t). Ltac Z2 t := t. Goal True -> True. Z1 O. -Z2 ltac:O. +Z2 ltac:(O). exact I. Qed. @@ -302,7 +302,7 @@ Abort. (* Check instantiation of binders using ltac names *) Goal True. -let x := ipattern:y in assert (forall x y, x = y + 0). +let x := ipattern:(y) in assert (forall x y, x = y + 0). intro. destruct y. (* Check that the name is y here *) Abort. diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v new file mode 100644 index 0000000000..3f6b9cb39f --- /dev/null +++ b/test-suite/success/shrink_abstract.v @@ -0,0 +1,13 @@ +Set Shrink Abstract. + +Definition foo : forall (n m : nat), bool. +Proof. +pose (p := 0). +intros n. +pose (q := n). +intros m. +pose (r := m). +abstract (destruct m; [left|right]). +Defined. + +Check (foo_subproof : nat -> bool). diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v new file mode 100644 index 0000000000..676b97878f --- /dev/null +++ b/test-suite/success/shrink_obligations.v @@ -0,0 +1,28 @@ +Require Program. + +Obligation Tactic := idtac. + +Set Shrink Obligations. + +Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit := +let bar : {r | n < r} := _ in +let qux : {r | p < r} := _ in +let quz : m = n -> True := _ in +tt. +Next Obligation. +intros m p n q. +exists (S n); constructor. +Qed. +Next Obligation. +intros m p n q. +exists (S (S m)); constructor. +Qed. +Next Obligation. +intros m p n q ? ? H. +destruct H. +constructor. +Qed. + +Check (foo_obligation_1 : forall n, {r | n < r}). +Check (foo_obligation_2 : forall m, {r | (S m) < r}). +Check (foo_obligation_3 : forall m n, m = n -> True). diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v new file mode 100644 index 0000000000..8336f6a806 --- /dev/null +++ b/test-suite/success/subst.v @@ -0,0 +1,25 @@ +(* Test various subtleties of the "subst" tactics *) + +(* Should proceed from left to right (see #4222) *) +Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y. +intros. +subst. +change (3 = 2) in H1. +change (3 = 3). +Abort. + +(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *) +Goal forall x y, x = y -> x = 3 -> x = y. +intros. +subst. +change (3 = 3). +Abort. + +(* Should substitute cycles once, until a recursive equation is obtained *) +(* (failed in 8.4) *) +Goal forall x y, x = S y -> y = S x -> x = y. +intros. +subst. +change (y = S (S y)) in H0. +change (S y = y). +Abort. |