diff options
Diffstat (limited to 'test-suite')
57 files changed, 1036 insertions, 54 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 207f25ed0b..91b8a4ed08 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -92,7 +92,7 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk .PHONY: all run clean $(SUBSYSTEMS) all: run - $(MAKE) --quiet summary.log + $(MAKE) report run: $(SUBSYSTEMS) bugs: $(BUGS) @@ -151,11 +151,11 @@ summary: } summary.log: - $(SHOW) SUMMARY + $(SHOW) BUILDING SUMMARY FILE $(HIDE)$(MAKE) --quiet summary > "$@" report: summary.log - $(HIDE)if grep -F 'Error!' summary.log ; then false; fi + $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi ####################################################################### # Regression (and progression) tests @@ -242,7 +242,6 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v $(HIDE){ \ echo $(call log_intro,$<); \ $(coqc) "$<" $(call get_coq_prog_args,"$<") -async-proofs on \ - -async-proofs-private-flags fallback-to-lazy-if-marshal-error=no,fallback-to-lazy-if-slave-dies=no \ $$opts 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ @@ -391,7 +390,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/closed/1850.v b/test-suite/bugs/closed/1850.v new file mode 100644 index 0000000000..26b48093b7 --- /dev/null +++ b/test-suite/bugs/closed/1850.v @@ -0,0 +1,4 @@ +Parameter P : Type -> Type -> Type. +Notation "e |= t --> v" := (P e t v) (at level 100, t at level 54). +Fail Check (nat |= nat --> nat). + 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/3080.v b/test-suite/bugs/closed/3080.v new file mode 100644 index 0000000000..7d0dc090e1 --- /dev/null +++ b/test-suite/bugs/closed/3080.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-emacs" "-nois") -*- *) +Delimit Scope type_scope with type. +Delimit Scope function_scope with function. + +Bind Scope type_scope with Sortclass. +Bind Scope function_scope with Funclass. + +Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). +Notation "A -> B" := (forall (_ : A), B) : type_scope. + +Definition compose {A B C} (g : B -> C) (f : A -> B) := + fun x : A => g (f x). + +Notation " g ∘ f " := (compose g f) + (at level 40, left associativity) : function_scope. + +Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *) +Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *) diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 9125ab16dd..a547685070 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -6,6 +6,8 @@ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y :> T" (at level 70, y at next level, no associativity). Reserved Notation "x = y" (at level 70, no associativity). +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. Open Scope type_scope. Global Set Universe Polymorphism. Notation "A -> B" := (forall (_ : A), B) : type_scope. @@ -35,6 +37,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/3649.v b/test-suite/bugs/closed/3649.v index 06188e7b1b..fc60897d21 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -4,6 +4,8 @@ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. Open Scope type_scope. Axiom admit : forall {T}, T. Notation "A -> B" := (forall (_ : A), B) : type_scope. @@ -54,4 +56,4 @@ Goal forall (C D : PreCategory) (G G' : Functor C D) (** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *) let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in - progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
\ No newline at end of file + progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)). 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/int31.v b/test-suite/failure/int31.v new file mode 100644 index 0000000000..b1d112247f --- /dev/null +++ b/test-suite/failure/int31.v @@ -0,0 +1,17 @@ +Require Import Int31 BigN. + +Open Scope int31_scope. + +(* This used to go through because of an unbalanced stack bug in the bytecode +interpreter *) + +Lemma bad : False. +assert (1 = 2). +change 1 with (add31 (addmuldiv31 65 (add31 1 1) 2) 1). +Fail vm_compute; reflexivity. +(* +discriminate. +Qed. +*) +Abort. + 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..2b828d382a 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -6,6 +6,8 @@ fix F (t : t) : P t := end : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t + +Argument scopes are [function_scope function_scope _] = fun d : TT => match d with | @CTT _ _ b => b end @@ -24,7 +26,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -Argument scopes are [nat_scope nat_scope _ _ _] +Argument scopes are [nat_scope nat_scope function_scope _ _] foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with @@ -48,8 +50,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/InitSyntax.out b/test-suite/output/InitSyntax.out index bbfd3405af..c17c63e724 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -4,7 +4,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := For sig2: Argument A is implicit For exist2: Argument A is implicit For sig2: Argument scopes are [type_scope type_scope type_scope] -For exist2: Argument scopes are [type_scope _ _ _ _ _] +For exist2: Argument scopes are [type_scope function_scope function_scope _ _ + _] exists x : nat, x = x : Prop fun b : bool => if b then b else b diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index ba076f050a..98420409e8 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -2,7 +2,7 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic Argument A is implicit -Argument scopes are [type_scope _ _ _] +Argument scopes are [type_scope function_scope _ _] Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} @@ -10,7 +10,7 @@ Inductive sigT (A : Type) (P : A -> Type) : Type := For sigT: Argument A is implicit For existT: Argument A is implicit For sigT: Argument scopes are [type_scope type_scope] -For existT: Argument scopes are [type_scope _ _ _] +For existT: Argument scopes are [type_scope function_scope _ _] existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit 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/output/ltac.out b/test-suite/output/ltac.out index d003c70df9..20e274e254 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,2 +1,5 @@ The command has indeed failed with message: Error: Ltac variable y depends on pattern variable name z which is not bound in current context. +Ltac f x y z := + symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize + dependent z diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index 7e2610c7d7..373b870b9f 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -15,3 +15,13 @@ lazymatch goal with | H1 : HT |- _ => idtac end. Abort. + +Ltac f x y z := + symmetry in x, y; + auto with z; + auto; + intros; + clearbody x; + generalize dependent z. + +Print Ltac f. 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/CaseInClause.v b/test-suite/success/CaseInClause.v index 3679eead70..599b9566cb 100644 --- a/test-suite/success/CaseInClause.v +++ b/test-suite/success/CaseInClause.v @@ -20,3 +20,7 @@ Theorem foo : forall (n m : nat) (pf : n = m), match pf in _ = N with | eq_refl => unit end. + +(* Check redundant clause is removed *) +Inductive I : nat * nat -> Type := C : I (0,0). +Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end. 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/TacticNotation2.v b/test-suite/success/TacticNotation2.v new file mode 100644 index 0000000000..cb341b8e10 --- /dev/null +++ b/test-suite/success/TacticNotation2.v @@ -0,0 +1,12 @@ +Tactic Notation "complete" tactic(tac) := tac; fail. + +Ltac f0 := complete (intuition idtac). +(** FIXME: This is badly printed because of bug #3079. + At least we check that it does not fail anomalously. *) +Print Ltac f0. + +Ltac f1 := complete f1. +Print Ltac f1. + +Ltac f2 := complete intuition. +Print Ltac f2. 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/bigQ.v b/test-suite/success/bigQ.v new file mode 100644 index 0000000000..7fd0cf669d --- /dev/null +++ b/test-suite/success/bigQ.v @@ -0,0 +1,66 @@ +Require Import BigQ. +Import List. + +Definition pi_4_approx_low' := +(5066193963420194617885108698600649932059391557720145469382602092416947640628637390992675949693715109726079394291478795603894419483819297806310615866892414925850691415582239745615128821983865262221858109336884967754871321668348027076234335167119885298878199925731495390387858629042311908406056230882123787019283378509712244687397013657159455607193734144010901984756727174636853404278421831024545476850410085042498464474261035780891759930905778986584183710930670670301831474144997069400304290351567959717683444430666444319233768399342338059169002790777424962570605618705584660815518973602995097110557181643034682308210782171804373210646804613922337450953858508244032293753591878060539465788294318856859293281629951093130167801471787011911886414492513677892193100809508943832528344473873460853362957387889412799458784754514139679847887887544849825173792522272708046699681079289358082661375778523609867456540595586031625044964543428047238934233579184772793670436643502740076366994465457847106782560289782615794595755672643440040123002018908935362541166831619056664637901929131328502017686713274283777724453661234225382109584471950444925886358166551424008707439387934109226545596919797083495958300914344992836193126080289565652575543234385558967555959267746932292860747199382633363026440008828134867747920263181610216905129926037611247017868033961426567047355301676870662406173724238530061264149506666345040372864118731705584795947926329181826992456072045382170981478151356381437136818835196834068650217794381425547036331194595892801393225038235274901050364737353586927051766717037643833477566087835266968086513005761986678747515870298138062157791066648217784877968385924845017637219384732843791052551854695220023477365706464590594542001161575677402761543188277502092362285265847964496740584911576627239093631932307473445797386335961743298553548881544486940399236133577915988716682746485564575640818803540680574730591500432326858763829791848612343662539095316357052823005419355719381626599487868023399182174939253393897549026675976384326749445831606130546375395770778462506203752920470130305293966478109733954117063941901686840180727195741528561335809865193566993349413786715403053579411364371500063193205131503024022217701373077790337150298315820556080596579100618643147698304927957576213733526923182742441048553793831725592624850721293495085399785588171300815789795594858916409701139277050529011775828846362873246196866089783324522718656445008090114701320562608474099248873638488023114015981013142490827777895317580810590743940417298263300561876701828404744082864248409230009391001735746615476377303707782123483770118391136826609366946585715225248587168403619476143657107412319421501162805102723455593551478028055839072686207007765300258935153546418515706362733656094770289090398825190320430416955807878686642673124733998295439657633866090085982598765253268688814792672416195730086607425842181518560588819896560847103627615434844684536463752986969865794019299978956052589825441828842338163389851892617560591840546654410705167593310272272965900821031821380595084783691324416454359888103920904935692840264474003367023256964191100139001239923263691779167792867186165635514824889759796850863175082506408142175595463676408992027105356481220754473245821534527625758942093801142305560662681150069082553674495761075895588095760081401141419460482860852822686860785424514171214889677926763812031823537071721974799922995763666175738785000806081164280471363125324839717808977470218218571800106898347366938927189989988149888641129263448064762730769285877330997355234347773807099829665997515649429224335217107760728789764718885665291038706425454675746218345291274054088843647602239258308472486102933167465443294268551209015027897159307743987020521392788721231001835675584104894174434637260464035122611721657641428625505184886116917149318963070896162119215386541876236027342810162765609201440423207771441367926085768438143507025739041041240810056881304230519058117534418374553879198061289605354335880794397478047346975609179199801003098836622253165101961484972165230151495472006888128587168049198312469715081555662345452800468933420359802645393289853553618279788400476187713990872203669487294118461245455333004125835663010526985716431187034663870796866708678078952110615910196519835267441831874676895301527286826106517027821074816850326548617513767142627360001181210946100011774672126943957522004190414960909074050454565964857276407084991922274068961845339154089866785707764290964299529444616711194034827611771558783466230353209661849406004241580029437779784290315347968833708422223285859451369907260780956405036020581705441364379616715041818815829810906212826084485200785283123265202151252852134381195424724503189247411069117189489985791487434549080447866370484866697404176437230771558469231403088139693477706784802801265075586678597768511791952562627345622499328 + # 100788726492580594349650258277496659410917619472657560321971265983799894639441017438166498752997098978003489632843381325240982516059309714013145358125224597827602157516585886911710102182473475545864474089191789296685473601331678556438310133356793199956062857423397512495293688453655805536015029176541424005214818033707522950635262669828538132795615008381824067071229426026518897202246241637377064076189277685257166926338187911595052586669184297526234794666364657344206795357967279911782849686515024121916258300642000317525374433525235296287037535618423661645124459323811792936193272341688261801253469089129439519903538495370298752436267926761998785090092411372633429302950606054074205533246665546979112178855223925266166034953000200646676762301817000435641690517142795144469005596172113586738287118865058604922865654348297975054956781513943444060257230946224520058527667925776273088622386666860662470481606622952298649177217986593047495967209669116410592230626047083795555559776477430548946990993890380787911273437967786556742804566652408275798339221179283430482118140020742719695900657696142739101628984271513292954605191778803974738871043737934546460016184719168074062912083778327025499841998124431899131874519812228674255796948879306477894924710085384116453080236862135706628989104070747737689294987000148388110561753028594988959655591699155508380909698460304884908709246116411180876105681720036833487450945730831039969246996849503525429840196651386469599438064049723005123629385485140945945416764414133189625489032807860400751723995946290581976152580477047961138617997133510128194027510895265424780627975864980749945631413855375897945293107842908479797077570371447220506451229526132919408351287454305932886749170523056147842439813407002950370505941417426433452282518739345666494683448699945734453214481915512562995906034771246088038719298959180199052759295868161570318718927430655393250250811804905393113074074574608255523847592006804881016594060188745212933427473833239777228852952217878690668413947367586040297784502192683200664398064682201012931468052982448022330449955215606614483165425935154496289535573901139223034819824408001205784146243892228030383941863746839845526558421740316887532141893650230936137269356278754487130882868595412163277284772124736531380334814212708066069618080153747333573454834500999083737284449542481264971030785043701582134343596645346132964567391370300568578875509971483039720438955919863275044932311289587494336123538202079503922025306586828117649623642521324286648529829664567232756108169459356549144779085080036654897525078792273443307070502103724611233768453196294899770515940520895908289018412144327894912660060761908970811602375085884115384049610753387776858733798341463052471017393165656926510611173543365663267563198760597092606598728110197523695339144204179424646442294307593146446562536865057987897899655645968129515654148044008249646703504419478535298270862753806142083172190778193001810574370442181909146645889199829207284871551220439225371051511970054965951914399901815408791418836185742573331879114400013259342896515702942707292473805188905427717363630137869116872433627556880809120353079342030725196065815470427569172350436988386579444534375353968759750750178342190349607711313840613843718547859929387259163285524671855725511880656411741012446023392964655239624520090988149679656514996202498334816938716757663800773997302639681907686195671083505910700098597156238624351157219093280177066146218516478636356056420098245995113668018177690728654922707281126889313941750547830163078886329630807850633273613622550216189245162735650139455042125252043274668279981753287687674520319519360593091620297805736177366738063651905396783336064579717230286821545930579779462534206093794040878198825916141099864730374109311705285661056855668930671948265232862757146615431791375559792290479316263924560826544387396762768331402198937951439504767950821089741987629257538953417586416459087855138539304027013800937360598578194413362672871055543854633921502486683911956250444582746421552178164852341035733290405311280719066037175324627429434912416361334254696649419037348733709488576582107382055914938194078813926926742828297826939120316120573453588052056773875836843924877773978390546387248009519202370375478981843515393806263037580338009594022254079586380520797699651840576286033587273591899639699077044271208886940540056794360292760863657703246410020854088849880453524038877935317875884698324859548991680533307680053872403383516589028793015681082435908524045497475001609824047204954932626536311826911363867426654549346914317405110707189532251727848751560224936842128628673253616256326013555922159336370177663785738170802777550686079119049748734352584409583136667752555307842739679930698964098088960000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%bigQ +. + +Definition pi_4_approx_high' := +(5066193963420194617885108698600649932059391557720145469382602092416947640628637390992675949693715109726079394291478795603894419483819297806310615866892414925850691415582239745615128821983865262221858109336884967754871321668348027076234335167119885298878199925731495390387858629042311908406056230882123787019283378509712244687397013657159455607193734144010901984756727174636853404278421831024545476850410085042498464474261035780891759930905778986584183710930670670301831474144997069400304290351567959717683444430666444319233768399342338059169002790777424962570605618705584660815518973602995097110557181643034682308210788409308322071457087096445676662503017187903223859814905546579050729173916234740628466315449085686468204847296426235788544874405450791749423436215032927889914519102361378633666267941326393265376660400091389373564825046526561381561278586121772300141564909333667988204680492088607706214346458601842899721615765319505314310192693665547163360402786722105590252780194994950097926184146718893770363322073641336811404180286358079915338791029818581497746089864894356686643882883410392601500048021013346713450539807687779704798018559373507951388092945938366448668853081682176581336156031434604604833692503597621519809826880683536141897075567053733515342478008373282599947520770191238802249392773327261328133194484586433840861730959791563023761306622956165536481335792721379318928171897265310054788931201902441066997927781894934061720760080768154565282051604447333036111267534150649674590201404453202347064545359869105856798745664471694795576801148562495225166002814304124970965817043547048503388910163287916513427409193998045119986267987892522931703487420953769290650229176116308194977201080691718825944370436642709192983358059711255925052564016519597530235976618244111239816418652282585432539731271068892992142956810775762851238126881225206289553948196520384709574383566733478326330112084307565420647201107231840508040019131253750047046446929758911912155202166566751947087545292626353331520202690130850009389387290465497377022080531269511355734944672010542204118978272180881335465227900174033380001851066811103401787656367819132934758616060307366679580043123632565656840669377840733018248707250548277181001911990237151790533341326223932843775840498222236867608395855700891719880219904948672458645420169533565809609056209006342663841718949396996175294237942265325043426430990062217643279654512512640557763489491751115437780462208361129433667449740743123546232162409802316714286708788831227582498585478334315076725145986771341647015244092760289407649044493584479944044779273447198382196766547779885914425854375158084417582279211000449529495605127376707776277159376010648950025135061284601443461110447113346277147728593420397807946636800365109579479211273476195727270004743568492888900356505584731622538401071221591141889158461271000051210318027818802379539544396973228585821742794928813630781709195703717312953337431290682263448669168179857644544116657440168099166467471736180072984407514757289757495435699300593165669101965987430482600019222913485092771346963058673132443387835726110205958057187517487684058179749952286341120230051432903482992282688283815697442898155194928723360957436110770317998431272108100149791425689283090777721270428030993332057319821685391144252815655146410678839177846108260765981523812232294638190350688210999605869296307711846463311346627138400477211801219366400312514793356564308532012682051019030257269068628100171220662165246389309014292764479226570049772046255291379151017129899157296574099437276707879597755725339406865738613810979022640265737120949077721294633786520294559343155148383011293584240192753971366644780434237846862975993387453786681995831719537733846579480995517357440575781962659282856696638992709756358478461648462532279323701121386551383509193782388241965285971965887701816406255233933761008649762854363984142178331798953040874526844255758512982810004271235810681505829473926495256537353108899526434200682024946218302499640511518360332022463196599199779172637638655415918976955930735312156870786600023896830267884391447789311101069654521354446521135407720085038662159974712373018912537116964809382149581004863115431780452188813210275393919111435118030412595133958954313836191108258769640843644195537185904547405641078708492098917460393911427237155683288565433183738513871595286090814836422982384810033331519971102974091067660369548406192526284519976668985518575216481570167748402860759832933071281814538397923687510782620605409323050353840034866296214149657376249634795555007199540807313397329050410326609108411299737760271566308288500400587417017113933243099961248847368789383209110747378488312550109911605079801570534271874115018095746872468910162721975463388518648962869080447866370484866697404176437230771558469231403088139693477706784802801265075586678597768511791952562627345622499328 + # 100788726492580594349650258277496659410917619472657560321971265983799894639441017438166498752997098978003489632843381325240982516059309714013145358125224597827602157516585886911710102182473475545864474089191789296685473601331678556438310133356793199956062857423397512495293688453655805536015029176541424005214818033707522950635262669828538132795615008381824067071229426026518897202246241637377064076189277685257166926338187911595052586669184297526234794666364657344206795357967279911782849686515024121916258300642000317525374433525235296287037535618423661645124459323811792936193272341688261801253469089129439519903538495370298752436267926761998785090092411372633429302950606054074205533246665546979112178855223925266166034953000200646676762301817000435641690517142795144469005596172113586738287118865058604922865654348297975054956781513943444060257230946224520058527667925776273088622386666860662470481606622952298649177217986593047495967209669116410592230626047083795555559776477430548946990993890380787911273437967786556742804566652408275798339221179283430482118140020742719695900657696142739101628984271513292954605191778803974738871043737934546460016184719168074062912083778327025499841998124431899131874519812228674255796948879306477894924710085384116453080236862135706628989104070747737689294987000148388110561753028594988959655591699155508380909698460304884908709246116411180876105681720036833487450945730831039969246996849503525429840196651386469599438064049723005123629385485140945945416764414133189625489032807860400751723995946290581976152580477047961138617997133510128194027510895265424780627975864980749945631413855375897945293107842908479797077570371447220506451229526132919408351287454305932886749170523056147842439813407002950370505941417426433452282518739345666494683448699945734453214481915512562995906034771246088038719298959180199052759295868161570318718927430655393250250811804905393113074074574608255523847592006804881016594060188745212933427473833239777228852952217878690668413947367586040297784502192683200664398064682201012931468052982448022330449955215606614483165425935154496289535573901139223034819824408001205784146243892228030383941863746839845526558421740316887532141893650230936137269356278754487130882868595412163277284772124736531380334814212708066069618080153747333573454834500999083737284449542481264971030785043701582134343596645346132964567391370300568578875509971483039720438955919863275044932311289587494336123538202079503922025306586828117649623642521324286648529829664567232756108169459356549144779085080036654897525078792273443307070502103724611233768453196294899770515940520895908289018412144327894912660060761908970811602375085884115384049610753387776858733798341463052471017393165656926510611173543365663267563198760597092606598728110197523695339144204179424646442294307593146446562536865057987897899655645968129515654148044008249646703504419478535298270862753806142083172190778193001810574370442181909146645889199829207284871551220439225371051511970054965951914399901815408791418836185742573331879114400013259342896515702942707292473805188905427717363630137869116872433627556880809120353079342030725196065815470427569172350436988386579444534375353968759750750178342190349607711313840613843718547859929387259163285524671855725511880656411741012446023392964655239624520090988149679656514996202498334816938716757663800773997302639681907686195671083505910700098597156238624351157219093280177066146218516478636356056420098245995113668018177690728654922707281126889313941750547830163078886329630807850633273613622550216189245162735650139455042125252043274668279981753287687674520319519360593091620297805736177366738063651905396783336064579717230286821545930579779462534206093794040878198825916141099864730374109311705285661056855668930671948265232862757146615431791375559792290479316263924560826544387396762768331402198937951439504767950821089741987629257538953417586416459087855138539304027013800937360598578194413362672871055543854633921502486683911956250444582746421552178164852341035733290405311280719066037175324627429434912416361334254696649419037348733709488576582107382055914938194078813926926742828297826939120316120573453588052056773875836843924877773978390546387248009519202370375478981843515393806263037580338009594022254079586380520797699651840576286033587273591899639699077044271208886940540056794360292760863657703246410020854088849880453524038877935317875884698324859548991680533307680053872403383516589028793015681082435908524045497475001609824047204954932626536311826911363867426654549346914317405110707189532251727848751560224936842128628673253616256326013555922159336370177663785738170802777550686079119049748734352584409583136667752555307842739679930698964098088960000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)%bigQ +. + +Fixpoint numden_Rcontfrac_tailrecB (accu: list bigZ) (n1 d1: bigZ) (n2 d2: bigZ) (fuel: nat) {struct fuel}: + (list bigZ * bigQ * bigQ) := + let default := (rev_append accu nil, BigQ.div (BigQ.Qz n1) (BigQ.Qz d1), BigQ.div (BigQ.Qz n2) (BigQ.Qz d2)) in + match fuel with + | O => default + | S fuel' => + let '(q1, r1) := BigZ.div_eucl n1 d1 in + let '(q2, r2) := BigZ.div_eucl n2 d2 in + match BigZ.eqb q1 q2 with + | false => default + | true => + let r1_is_zero := BigZ.eqb r1 0 in + let r2_is_zero := BigZ.eqb r2 0 in + match Bool.eqb r1_is_zero r2_is_zero with + | false => default + | true => + match r1_is_zero with + | true => + match BigZ.eqb q1 1 with + | true => (rev_append accu nil, 1%bigQ, 1%bigQ) + | false => (rev_append ((q1 - 1)%bigZ :: accu) nil, 1%bigQ, 1%bigQ) + end + | false => numden_Rcontfrac_tailrecB (q1 :: accu) d1 r1 d2 r2 fuel' + end + end + end + end. + +Definition Bnum b := + match b with + | BigQ.Qz t => t + | BigQ.Qq n d => + if (d =? BigN.zero)%bigN then 0%bigZ else n + end. + +Definition Bden b := + match b with + | BigQ.Qz _ => 1%bigN + | BigQ.Qq _ d => if (d =? BigN.zero)%bigN then 1%bigN else d + end. + +Definition rat_Rcontfrac_tailrecB q1 q2 := + numden_Rcontfrac_tailrecB nil (Bnum q1) (BigZ.Pos (Bden q1)) (Bnum q2) (BigZ.Pos (Bden q2)). + +Definition pi_4_contfrac := + rat_Rcontfrac_tailrecB pi_4_approx_low' pi_4_approx_high' 3000. + +(* The following used to fail because of a non canonical representation of 0 in +the bytecode interpreter. Bug reported privately by Tahina Ramananandro. *) +Goal pi_4_contfrac = pi_4_contfrac. +vm_compute. +reflexivity. +Qed. 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/setoid_test.v b/test-suite/success/setoid_test.v index 0465c4b3fb..1f24ef2a6b 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -166,3 +166,16 @@ 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. +(* This should not raise an anomaly as it did for some time in early 2016 *) + +Definition t := nat -> bool. +Definition h (a b : t) := forall n, a n = b n. + +Instance subrelh : subrelation h (Morphisms.pointwise_relation nat eq). +Proof. intros x y H; assumption. Qed. + +Goal forall a b, h a b -> a 0 = b 0. +intros. +setoid_rewrite H. (* Fallback on ordinary rewrite without anomaly *) +reflexivity. +Qed. 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. |