diff options
Diffstat (limited to 'test-suite')
158 files changed, 4118 insertions, 204 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 31b2129001..f333ae63e3 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -154,6 +154,9 @@ summary.log: $(SHOW) SUMMARY $(HIDE)$(MAKE) --quiet summary > "$@" +report: summary.log + $(HIDE)if grep -F 'Error!' summary.log ; then false; fi + ####################################################################### # Regression (and progression) tests ####################################################################### @@ -349,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v fi; \ } > "$@" -# Additionnal dependencies for module tests +# Additional dependencies for module tests $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo modules/%.vo: modules/%.v $(HIDE)$(coqtop) -R modules Mods -compile $< @@ -388,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/bench/lists-100.v b/test-suite/bench/lists-100.v index 352c7cea74..5c64716c72 100644 --- a/test-suite/bench/lists-100.v +++ b/test-suite/bench/lists-100.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v index 352c7cea74..5c64716c72 100644 --- a/test-suite/bench/lists_100.v +++ b/test-suite/bench/lists_100.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/bugs/4623.v b/test-suite/bugs/4623.v new file mode 100644 index 0000000000..405d09809c --- /dev/null +++ b/test-suite/bugs/4623.v @@ -0,0 +1,5 @@ +Goal Type -> Type. +set (T := Type). +clearbody T. +refine (@id _). +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/4624.v b/test-suite/bugs/4624.v new file mode 100644 index 0000000000..a737afcdab --- /dev/null +++ b/test-suite/bugs/4624.v @@ -0,0 +1,7 @@ +Record foo := mkfoo { type : Type }. + +Canonical Structure fooA (T : Type) := mkfoo (T -> T). + +Definition id (t : foo) (x : type t) := x. + +Definition bar := id _ ((fun x : nat => x) : _).
\ No newline at end of file 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/3068.v b/test-suite/bugs/closed/3068.v index ced6d95949..79671ce930 100644 --- a/test-suite/bugs/closed/3068.v +++ b/test-suite/bugs/closed/3068.v @@ -56,7 +56,7 @@ Section Finite_nat_set. subst fs1. apply iff_refl. intros H. - eapply counted_list_equal_nth_char. + eapply (counted_list_equal_nth_char _ _ _ _ ?[def]). intros i. destruct (counted_def_nth fs1 i _ ) eqn:H0. (* This was not part of the initial bug report; this is to check that diff --git a/test-suite/bugs/closed/3249.v b/test-suite/bugs/closed/3249.v index d41d231739..71d457b002 100644 --- a/test-suite/bugs/closed/3249.v +++ b/test-suite/bugs/closed/3249.v @@ -5,7 +5,7 @@ Ltac ret_and_left T := lazymatch eval hnf in t with | ?a /\ ?b => constr:(proj1 T) | forall x : ?T', @?f x => - constr:(fun x : T' => $(let fx := constr:(T x) in + constr:(fun x : T' => ltac:(let fx := constr:(T x) in let t := ret_and_left fx in - exact t)$) + exact t)) end. diff --git a/test-suite/bugs/closed/3257.v b/test-suite/bugs/closed/3257.v new file mode 100644 index 0000000000..d8aa6a0479 --- /dev/null +++ b/test-suite/bugs/closed/3257.v @@ -0,0 +1,5 @@ +Require Import Setoid Morphisms Basics. +Lemma foo A B (P : B -> Prop) : + pointwise_relation _ impl (fun z => A -> P z) P. +Proof. + Fail reflexivity. diff --git a/test-suite/bugs/closed/3267.v b/test-suite/bugs/closed/3267.v index 5ce1ddf0c4..8175d66ac7 100644 --- a/test-suite/bugs/closed/3267.v +++ b/test-suite/bugs/closed/3267.v @@ -34,3 +34,14 @@ Module d. debug eauto. Defined. End d. + +(* An other variant which was still failing in 8.5 beta2 *) + +Parameter A B : Prop. +Axiom a:B. + +Hint Extern 1 => match goal with H:_ -> id _ |- _ => try (unfold id in H) end. +Goal (B -> id A) -> A. +intros. +eauto using a. +Abort. diff --git a/test-suite/bugs/closed/3285.v b/test-suite/bugs/closed/3285.v index 25162329ef..68e6b7386f 100644 --- a/test-suite/bugs/closed/3285.v +++ b/test-suite/bugs/closed/3285.v @@ -1,7 +1,7 @@ Goal True. Proof. match goal with - | _ => let x := constr:($(fail)$) in idtac + | _ => let x := constr:(ltac:(fail)) in idtac | _ => idtac end. Abort. diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v index b08b7ab3cc..701480fc83 100644 --- a/test-suite/bugs/closed/3286.v +++ b/test-suite/bugs/closed/3286.v @@ -6,20 +6,20 @@ Ltac make_apply_under_binders_in lem H := | forall x : ?T, @?P x => let ret := constr:(fun x' : T => let Hx := H x' in - $(let ret' := tac lem Hx in - exact ret')$) in + ltac:(let ret' := tac lem Hx in + exact ret')) in match eval cbv zeta in ret with | fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in constr:(Some P') end - | _ => let ret := constr:($(match goal with + | _ => let ret := constr:(ltac:(match goal with | _ => (let H' := fresh in pose H as H'; apply lem in H'; exact (Some H')) | _ => exact (@None nat) end - )$) in + )) in let ret' := (eval cbv beta zeta in ret) in constr:(ret') | _ => constr:(@None nat) diff --git a/test-suite/bugs/closed/3314.v b/test-suite/bugs/closed/3314.v index fb3791af55..a5782298c3 100644 --- a/test-suite/bugs/closed/3314.v +++ b/test-suite/bugs/closed/3314.v @@ -1,9 +1,9 @@ Require Import TestSuite.admit. Set Universe Polymorphism. Definition Lift -: $(let U1 := constr:(Type) in +: ltac:(let U1 := constr:(Type) in let U0 := constr:(Type : U1) in - exact (U0 -> U1))$ + exact (U0 -> U1)) := fun T => T. Fail Check nat:Prop. (* The command has indeed failed with message: diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v index e6a50449da..e3b5e94356 100644 --- a/test-suite/bugs/closed/3330.v +++ b/test-suite/bugs/closed/3330.v @@ -8,7 +8,7 @@ Inductive foo : Type@{l} := bar : foo . Section MakeEq. Variables (a : foo@{i}) (b : foo@{j}). - Let t := $(let ty := type of b in exact ty)$. + Let t := ltac:(let ty := type of b in exact ty). Definition make_eq (x:=b) := a : t. End MakeEq. diff --git a/test-suite/bugs/closed/3347.v b/test-suite/bugs/closed/3347.v index 63d5c7a57b..dcf5394eaf 100644 --- a/test-suite/bugs/closed/3347.v +++ b/test-suite/bugs/closed/3347.v @@ -1,7 +1,7 @@ Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 12653 lines to 12453 lines, then from 11673 lines to 681 lines, then from 693 lines to 469 lines, then from 375 lines to 56 lines *) Set Universe Polymorphism. -Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). +Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing). Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. Inductive Unit : Type1 := tt : Unit. Fail Check Unit : Set. (* [Check Unit : Set] should fail if [Type1] is defined correctly *) diff --git a/test-suite/bugs/closed/3354.v b/test-suite/bugs/closed/3354.v index 14b66db362..a635285f2c 100644 --- a/test-suite/bugs/closed/3354.v +++ b/test-suite/bugs/closed/3354.v @@ -1,5 +1,5 @@ Set Universe Polymorphism. -Notation Type1 := $(let U := constr:(Type) in let gt := constr:(Set : U) in exact U)$ (only parsing). +Notation Type1 := ltac:(let U := constr:(Type) in let gt := constr:(Set : U) in exact U) (only parsing). Inductive Empty : Type1 := . Fail Check Empty : Set. (* Toplevel input, characters 15-116: diff --git a/test-suite/bugs/closed/3467.v b/test-suite/bugs/closed/3467.v index 7e37116249..88ae030578 100644 --- a/test-suite/bugs/closed/3467.v +++ b/test-suite/bugs/closed/3467.v @@ -1,5 +1,5 @@ Module foo. - Notation x := $(exact I)$. + Notation x := ltac:(exact I). End foo. Module bar. Include foo. diff --git a/test-suite/bugs/closed/3487.v b/test-suite/bugs/closed/3487.v index 03c60a8baa..1321a8598c 100644 --- a/test-suite/bugs/closed/3487.v +++ b/test-suite/bugs/closed/3487.v @@ -1,4 +1,4 @@ -Notation bar := $(exact I)$. +Notation bar := ltac:(exact I). Notation foo := bar (only parsing). Class baz := { x : False }. Instance: baz. diff --git a/test-suite/bugs/closed/3554.v b/test-suite/bugs/closed/3554.v new file mode 100644 index 0000000000..13a79cc840 --- /dev/null +++ b/test-suite/bugs/closed/3554.v @@ -0,0 +1 @@ +Example foo (f : forall {_ : Type}, Type) : Type. 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/3682.v b/test-suite/bugs/closed/3682.v index 2a282d221f..9d37d1a2d0 100644 --- a/test-suite/bugs/closed/3682.v +++ b/test-suite/bugs/closed/3682.v @@ -3,4 +3,4 @@ Class Foo. Definition bar `{Foo} (x : Set) := Set. Instance: Foo. Definition bar1 := bar nat. -Definition bar2 := bar $(admit)$. +Definition bar2 := bar ltac:(admit). diff --git a/test-suite/bugs/closed/3684.v b/test-suite/bugs/closed/3684.v index f7b137386b..130d57779d 100644 --- a/test-suite/bugs/closed/3684.v +++ b/test-suite/bugs/closed/3684.v @@ -1,5 +1,5 @@ Require Import TestSuite.admit. Definition foo : Set. Proof. - refine ($(abstract admit)$). + refine (ltac:(abstract admit)). Qed. diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v index a5bea34a98..7a0c3e6f1d 100644 --- a/test-suite/bugs/closed/3685.v +++ b/test-suite/bugs/closed/3685.v @@ -39,11 +39,11 @@ Module Export PointwiseCore. (G : Functor D D') : Functor (C -> D) (C' -> D'). Proof. - refine (Build_Functor + unshelve (refine (Build_Functor (C -> D) (C' -> D') _ _ - _); + _)); abstract admit. Defined. End PointwiseCore. diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v index b650920b26..df5f667480 100644 --- a/test-suite/bugs/closed/3686.v +++ b/test-suite/bugs/closed/3686.v @@ -33,11 +33,11 @@ Module Export PointwiseCore. (G : Functor D D') : Functor (C -> D) (C' -> D'). Proof. - refine (Build_Functor + unshelve (refine (Build_Functor (C -> D) (C' -> D') _ _ - _); + _)); abstract admit. Defined. End PointwiseCore. diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index df9f5f4761..c24173abf1 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -18,7 +18,7 @@ Top.8} Top.6 Top.7 Top.8 |= *) *) -Definition bar := $(let t := eval compute in foo in exact t)$. +Definition bar := ltac:(let t := eval compute in foo in exact t). Check @bar. (* bar@{Top.13 Top.14 Top.15 Top.16} : Type@{Top.16+1} diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 62137f0c06..8dadc2419c 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,8 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +47,8 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intros [a p]. exact (transport P p (d a)). Defined. @@ -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)) @@ -111,8 +111,8 @@ Module Prim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +124,8 @@ Module Prim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intros [a p]. exact (transport P p (d a)). Defined. @@ -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/closed/3735.v b/test-suite/bugs/closed/3735.v new file mode 100644 index 0000000000..a50572ace0 --- /dev/null +++ b/test-suite/bugs/closed/3735.v @@ -0,0 +1,4 @@ +Require Import Coq.Program.Tactics. +Class Foo := { bar : Type }. +Fail Lemma foo : Foo -> bar. (* 'Command has indeed failed.' in both 8.4 and trunk *) +Fail Program Lemma foo : Foo -> bar.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3743.v b/test-suite/bugs/closed/3743.v index 4dfb3380a8..c799d4393f 100644 --- a/test-suite/bugs/closed/3743.v +++ b/test-suite/bugs/closed/3743.v @@ -3,7 +3,7 @@ coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *) Require Export Coq.Setoids.Setoid. -Fail Add Parametric Relation A +Add Parametric Relation A : A (@eq A) transitivity proved by transitivity as refine_rel. diff --git a/test-suite/bugs/closed/3746.v b/test-suite/bugs/closed/3746.v new file mode 100644 index 0000000000..a9463f94bb --- /dev/null +++ b/test-suite/bugs/closed/3746.v @@ -0,0 +1,92 @@ + +(* Bug report #3746 : Include and restricted signature *) + +Module Type MT. Parameter p : nat. End MT. +Module Type EMPTY. End EMPTY. +Module Empty. End Empty. + +(* Include of an applied functor with restricted sig : + Used to create axioms (bug report #3746), now forbidden. *) + +Module F (X:EMPTY) : MT. + Definition p := 0. +End F. + +Module InclFunctRestr. + Fail Include F(Empty). +End InclFunctRestr. + +(* A few variants (indirect restricted signature), also forbidden. *) + +Module F1 := F. +Module F2 (X:EMPTY) := F X. + +Module F3a (X:EMPTY). Definition p := 0. End F3a. +Module F3 (X:EMPTY) : MT := F3a X. + +Module InclFunctRestrBis. + Fail Include F1(Empty). + Fail Include F2(Empty). + Fail Include F3(Empty). +End InclFunctRestrBis. + +(* Recommended workaround: manual instance before the include. *) + +Module InclWorkaround. + Module Temp := F(Empty). + Include Temp. +End InclWorkaround. + +Compute InclWorkaround.p. +Print InclWorkaround.p. +Print Assumptions InclWorkaround.p. (* Closed under the global context *) + + + +(* Related situations which are ok, just to check *) + +(* A) Include of non-functor with restricted signature : + creates a proxy to initial stuff *) + +Module M : MT. + Definition p := 0. +End M. + +Module InclNonFunct. + Include M. +End InclNonFunct. + +Definition check : InclNonFunct.p = M.p := eq_refl. +Print Assumptions InclNonFunct.p. (* Closed *) + + +(* B) Include of a module type with opaque content: + The opaque content is "copy-pasted". *) + +Module Type SigOpaque. + Definition p : nat. Proof. exact 0. Qed. +End SigOpaque. + +Module InclSigOpaque. + Include SigOpaque. +End InclSigOpaque. + +Compute InclSigOpaque.p. +Print InclSigOpaque.p. +Print Assumptions InclSigOpaque.p. (* Closed *) + + +(* C) Include of an applied functor with opaque proofs : + opaque proof "copy-pasted" (and substituted). *) + +Module F' (X:EMPTY). + Definition p : nat. Proof. exact 0. Qed. +End F'. + +Module InclFunctOpa. + Include F'(Empty). +End InclFunctOpa. + +Compute InclFunctOpa.p. +Print InclFunctOpa.p. +Print Assumptions InclFunctOpa.p. (* Closed *) diff --git a/test-suite/bugs/closed/3807.v b/test-suite/bugs/closed/3807.v new file mode 100644 index 0000000000..108ebf592b --- /dev/null +++ b/test-suite/bugs/closed/3807.v @@ -0,0 +1,33 @@ +Set Universe Polymorphism. +Set Printing Universes. +Unset Universe Minimization ToSet. + + +Definition foo : Type := nat. +About foo. +(* foo@{Top.1} : Type@{Top.1}*) +(* Top.1 |= *) + +Definition bar : foo -> nat. +Admitted. +About bar. +(* bar@{Top.2} : foo@{Top.2} -> nat *) +(* Top.2 |= *) + +Lemma baz@{i} : foo@{i} -> nat. +Proof. + exact bar. +Defined. + +Definition bar'@{i} : foo@{i} -> nat. + intros f. exact 0. +Admitted. +About bar'. +(* bar'@{i} : foo@{i} -> nat *) +(* i |= *) + +Axiom f@{i} : Type@{i}. +(* +*** [ f@{i} : Type@{i} ] +(* i |= *) +*)
\ No newline at end of file diff --git a/test-suite/bugs/opened/3848.v b/test-suite/bugs/closed/3848.v index a03e8ffdab..c0ef02f1e8 100644 --- a/test-suite/bugs/opened/3848.v +++ b/test-suite/bugs/closed/3848.v @@ -19,4 +19,4 @@ Proof. refine (functor_forall (f^-1) (fun (x:A) (y:Q (f^-1 x)) => eisretr f x # (g (f^-1 x))^-1 y)). -Fail Defined. (* Error: Attempt to save an incomplete proof *) +Defined. (* was: Error: Attempt to save an incomplete proof *) 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 4408ab885d..a327bbf2a9 100644 --- a/test-suite/bugs/closed/3881.v +++ b/test-suite/bugs/closed/3881.v @@ -8,7 +8,7 @@ Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Notation "A -> B" := (forall (_ : A), B) : type_scope. Axiom admit : forall {T}, T. Notation "g 'o' f" := (fun x => g (f x)) (at level 40, left associativity). -Notation "g 'o' f" := $(let g' := g in let f' := f in exact (fun x => g' (f' x)))$ (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *) +Notation "g 'o' f" := ltac:(let g' := g in let f' := f in exact (fun x => g' (f' x))) (at level 40, left associativity). (* Ensure that x is not captured in [g] or [f] in case they contain holes *) Inductive eq {A} (x:A) : A -> Prop := eq_refl : x = x where "x = y" := (@eq _ x y) : type_scope. Arguments eq_refl {_ _}. Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with eq_refl => eq_refl end. @@ -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/opened/3923.v b/test-suite/bugs/closed/3923.v index 6aa6b4932e..0aa029e73d 100644 --- a/test-suite/bugs/opened/3923.v +++ b/test-suite/bugs/closed/3923.v @@ -30,4 +30,4 @@ Axiom empty_fieldstore : cert_fieldstore. End MkCertRuntimeTypes. -Fail Extraction MkCertRuntimeTypes. +Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *) diff --git a/test-suite/bugs/closed/3974.v b/test-suite/bugs/closed/3974.v new file mode 100644 index 0000000000..b6be159595 --- /dev/null +++ b/test-suite/bugs/closed/3974.v @@ -0,0 +1,7 @@ +Module Type S. +End S. + +Module Type M (X : S). + Fail Module P (X : S). + (* Used to say: Anomaly: X already exists. Please report. *) + (* Should rather say now: Error: X already exists. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3975.v b/test-suite/bugs/closed/3975.v new file mode 100644 index 0000000000..95851c8137 --- /dev/null +++ b/test-suite/bugs/closed/3975.v @@ -0,0 +1,8 @@ +Module Type S. End S. + +Module M (X:S). End M. + +Module Type P (X : S). + Print M. + (* Used to say: Anomaly: X already exists. Please report. *) + (* Should rather : print something :-) *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3998.v b/test-suite/bugs/closed/3998.v new file mode 100644 index 0000000000..ced13839dd --- /dev/null +++ b/test-suite/bugs/closed/3998.v @@ -0,0 +1,24 @@ +Class FieldType (F : Set) := mkFieldType { fldTy: F -> Set }. +Hint Mode FieldType + : typeclass_instances. (* The F parameter is an input *) + +Inductive I1 := C. +Inductive I2 := . + +Instance I1FieldType : FieldType I1 := { fldTy := I1_rect _ bool }. +Instance I2FieldType : FieldType I2 := { fldTy := I2_rect _ }. + +Definition RecordOf F (FT: FieldType F) := forall f:F, fldTy f. + +Class MapOps (M K : Set) := { + tgtTy: K -> Set; + update: M -> forall k:K, tgtTy k -> M +}. + +Instance RecordMapOps F (FT: FieldType F) : MapOps (RecordOf F FT) F := +{ tgtTy := fldTy; update := fun r (f: F) (x: fldTy f) z => r z }. + +Axiom ex : RecordOf _ I1FieldType. + +Definition works := (fun ex' => update ex' C true) (update ex C false). +Set Typeclasses Debug. +Definition doesnt := update (update ex C false) C true.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4116.v b/test-suite/bugs/closed/4116.v index f808cb45e9..5932c9c56e 100644 --- a/test-suite/bugs/closed/4116.v +++ b/test-suite/bugs/closed/4116.v @@ -110,7 +110,7 @@ Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. Tactic Notation "transparent" "assert" "(" ident(name) ":" constr(type) ")" := - refine (let __transparent_assert_hypothesis := (_ : type) in _); + unshelve refine (let __transparent_assert_hypothesis := (_ : type) in _); [ | ( let H := match goal with H := _ |- _ => constr:(H) end in @@ -321,7 +321,7 @@ Section Grothendieck. Definition Gcategory : PreCategory. Proof. - refine (@Build_PreCategory + unshelve refine (@Build_PreCategory Pair (fun s d => Gmorphism s d) Gidentity @@ -346,7 +346,7 @@ Section Grothendieck2. Instance iscategory_grothendieck_toset : IsCategory (Gcategory F). Proof. intros s d. - refine (isequiv_adjointify _ _ _ _). + unshelve refine (isequiv_adjointify _ _ _ _). { intro m. transparent assert (H' : (s.(c) = d.(c))). diff --git a/test-suite/bugs/closed/4149.v b/test-suite/bugs/closed/4149.v new file mode 100644 index 0000000000..b81c680cd7 --- /dev/null +++ b/test-suite/bugs/closed/4149.v @@ -0,0 +1,4 @@ +Goal forall A, A -> Type. +Proof. + intros; eauto. +Qed. diff --git a/test-suite/bugs/closed/4151.v b/test-suite/bugs/closed/4151.v new file mode 100644 index 0000000000..fec64555f4 --- /dev/null +++ b/test-suite/bugs/closed/4151.v @@ -0,0 +1,403 @@ +Lemma foo (H : forall A, A) : forall A, A. + Show Universes. + eexact H. +Qed. + +(* File reduced by coq-bug-finder from original input, then from 6390 lines to 397 lines *) +(* coqc version 8.5beta1 (March 2015) compiled on Mar 17 2015 12:34:25 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (1b3759e78f227eb85a128c58b8ce8c11509dd8c3) *) +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.SetoidList. +Require Export Coq.Program.Program. + +Global Set Implicit Arguments. +Global Set Asymmetric Patterns. + +Fixpoint combine_sig_helper {T} {P : T -> Prop} (ls : list T) : (forall x, In x ls -> P x) -> list (sig P). + admit. +Defined. + +Lemma Forall_forall1_transparent_helper_1 {A P} {x : A} {xs : list A} {l : list A} + (H : Forall P l) (H' : x::xs = l) +: P x. + admit. +Defined. +Lemma Forall_forall1_transparent_helper_2 {A P} {x : A} {xs : list A} {l : list A} + (H : Forall P l) (H' : x::xs = l) +: Forall P xs. + admit. +Defined. + +Fixpoint Forall_forall1_transparent {A} (P : A -> Prop) (l : list A) {struct l} +: Forall P l -> forall x, In x l -> P x + := match l as l return Forall P l -> forall x, In x l -> P x with + | nil => fun _ _ f => match f : False with end + | x::xs => fun H x' H' => + match H' with + | or_introl H'' => eq_rect x + P + (Forall_forall1_transparent_helper_1 H eq_refl) + _ + H'' + | or_intror H'' => @Forall_forall1_transparent A P xs (Forall_forall1_transparent_helper_2 H eq_refl) _ H'' + end + end. + +Definition combine_sig {T P ls} (H : List.Forall P ls) : list (@sig T P) + := combine_sig_helper ls (@Forall_forall1_transparent T P ls H). +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Record string_like (CharType : Type) := + { + String :> Type; + Singleton : CharType -> String where "[ x ]" := (Singleton x); + Empty : String; + Concat : String -> String -> String where "x ++ y" := (Concat x y); + bool_eq : String -> String -> bool; + bool_eq_correct : forall x y : String, bool_eq x y = true <-> x = y; + Length : String -> nat; + Associativity : forall x y z, (x ++ y) ++ z = x ++ (y ++ z); + LeftId : forall x, Empty ++ x = x; + RightId : forall x, x ++ Empty = x; + Singleton_Length : forall x, Length (Singleton x) = 1; + Length_correct : forall s1 s2, Length s1 + Length s2 = Length (s1 ++ s2); + Length_Empty : Length Empty = 0; + Empty_Length : forall s1, Length s1 = 0 -> s1 = Empty; + Not_Singleton_Empty : forall x, Singleton x <> Empty; + SplitAt : nat -> String -> String * String; + SplitAt_correct : forall n s, fst (SplitAt n s) ++ snd (SplitAt n s) = s; + SplitAt_concat_correct : forall s1 s2, SplitAt (Length s1) (s1 ++ s2) = (s1, s2); + SplitAtLength_correct : forall n s, Length (fst (SplitAt n s)) = min (Length s) n + }. + +Delimit Scope string_like_scope with string_like. +Bind Scope string_like_scope with String. +Arguments Length {_%type_scope _} _%string_like. +Notation "[[ x ]]" := (@Singleton _ _ x) : string_like_scope. +Infix "++" := (@Concat _ _) : string_like_scope. +Infix "=s" := (@bool_eq _ _) (at level 70, right associativity) : string_like_scope. + +Definition str_le {CharType} {String : string_like CharType} (s1 s2 : String) + := Length s1 < Length s2 \/ s1 = s2. +Infix "≤s" := str_le (at level 70, right associativity). + +Record StringWithSplitState {CharType} (String : string_like CharType) (split_stateT : String -> Type) := + { string_val :> String; + state_val : split_stateT string_val }. + +Module Export ContextFreeGrammar. + Require Import Coq.Strings.String. + + Section cfg. + Variable CharType : Type. + + Section definitions. + + Inductive item := + | Terminal (_ : CharType) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + End cfg. + +End ContextFreeGrammar. +Module Export BaseTypes. + Import Coq.Strings.String. + + Local Open Scope string_like_scope. + + Inductive any_grammar CharType := + | include_item (_ : item CharType) + | include_production (_ : production CharType) + | include_productions (_ : productions CharType) + | include_nonterminal (_ : string). + Global Coercion include_item : item >-> any_grammar. + Global Coercion include_production : production >-> any_grammar. + + Section recursive_descent_parser. + Context {CharType : Type} + {String : string_like CharType} + {G : grammar CharType}. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> string -> bool; + remove_nonterminal : nonterminals_listT -> string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal = true + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_computational_types_dataT := + { predata :> parser_computational_predataT; + split_stateT : String -> nonterminals_listT -> any_grammar CharType -> String -> Type }. + + Class parser_computational_dataT' `{parser_computational_types_dataT} := + { split_string_for_production + : forall (str0 : String) (valid : nonterminals_listT) (it : item CharType) (its : production CharType) (str : StringWithSplitState String (split_stateT str0 valid (it::its : production CharType))), + list (StringWithSplitState String (split_stateT str0 valid it) + * StringWithSplitState String (split_stateT str0 valid its)); + split_string_for_production_correct + : forall str0 valid it its str, + let P f := List.Forall f (@split_string_for_production str0 valid it its str) in + P (fun s1s2 => (fst s1s2 ++ snd s1s2 =s str) = true) }. + End recursive_descent_parser. + +End BaseTypes. +Import Coq.Strings.String. + +Section cfg. + Context CharType (String : string_like CharType) (G : grammar CharType). + Context (names_listT : Type) + (initial_names_data : names_listT) + (is_valid_name : names_listT -> string -> bool) + (remove_name : names_listT -> string -> names_listT) + (names_listT_R : names_listT -> names_listT -> Prop) + (remove_name_dec : forall ls name, + is_valid_name ls name = true + -> names_listT_R (remove_name ls name) ls) + (remove_name_1 + : forall ls ps ps', + is_valid_name (remove_name ls ps) ps' = true + -> is_valid_name ls ps' = true) + (remove_name_2 + : forall ls ps ps', + is_valid_name (remove_name ls ps) ps' = false + <-> is_valid_name ls ps' = false \/ ps = ps') + (ntl_wf : well_founded names_listT_R). + + Inductive minimal_parse_of + : forall (str0 : String) (valid : names_listT) + (str : String), + productions CharType -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : names_listT) + (str : String), + production CharType -> Type := + | MinParseProductionNil : forall str0 valid, + @minimal_parse_of_production str0 valid (Empty _) nil + | MinParseProductionCons : forall str0 valid str strs pat pats, + str ++ strs ≤s str0 + -> @minimal_parse_of_item str0 valid str pat + -> @minimal_parse_of_production str0 valid strs pats + -> @minimal_parse_of_production str0 valid (str ++ strs) (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : names_listT) + (str : String), + item CharType -> Type := + | MinParseTerminal : forall str0 valid x, + @minimal_parse_of_item str0 valid [[ x ]]%string_like (Terminal x) + | MinParseNonTerminal + : forall str0 valid str name, + @minimal_parse_of_name str0 valid str name + -> @minimal_parse_of_item str0 valid str (NonTerminal CharType name) + with minimal_parse_of_name + : forall (str0 : String) (valid : names_listT) + (str : String), + string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid name str, + Length str < Length str0 + -> is_valid_name initial_names_data name = true + -> @minimal_parse_of str initial_names_data str (Lookup G name) + -> @minimal_parse_of_name str0 valid str name + | MinParseNonTerminalStrEq + : forall str valid name, + is_valid_name initial_names_data name = true + -> is_valid_name valid name = true + -> @minimal_parse_of str (remove_name valid name) str (Lookup G name) + -> @minimal_parse_of_name str valid str name. +End cfg. + +Local Coercion is_true : bool >-> Sortclass. + +Local Open Scope string_like_scope. + +Section general. + Context {CharType} {String : string_like CharType} {G : grammar CharType}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_stateT : String -> Type; + data' :> _ := {| BaseTypes.predata := predata ; BaseTypes.split_stateT := fun _ _ _ => split_stateT |}; + split_string_for_production + : forall it its, + StringWithSplitState String split_stateT + -> list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT); + split_string_for_production_correct + : forall it its (str : StringWithSplitState String split_stateT), + let P f := List.Forall f (split_string_for_production it its str) in + P (fun s1s2 => + (fst s1s2 ++ snd s1s2 =s str) = true); + premethods :> parser_computational_dataT' + := @Build_parser_computational_dataT' + _ String data' + (fun _ _ => split_string_for_production) + (fun _ _ => split_string_for_production_correct) }. + + Definition split_list_completeT `{data : boolean_parser_dataT} + {str0 valid} + (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) + (split_list : list (StringWithSplitState String split_stateT * StringWithSplitState String split_stateT)) + (it : item CharType) (its : production CharType) + := ({ s1s2 : String * String + & (fst s1s2 ++ snd s1s2 =s str) + * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it) + * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type) + -> ({ s1s2 : StringWithSplitState String split_stateT * StringWithSplitState String split_stateT + & (In s1s2 split_list) + * (minimal_parse_of_item _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (fst s1s2) it) + * (minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid (snd s1s2) its) }%type). +End general. + +Section recursive_descent_parser. + Context {CharType} + {String : string_like CharType} + {G : grammar CharType}. + Context `{data : @boolean_parser_dataT _ String}. + + Section bool. + Section parts. + Definition parse_item + (str_matches_nonterminal : string -> bool) + (str : StringWithSplitState String split_stateT) + (it : item CharType) + : bool + := match it with + | Terminal ch => [[ ch ]] =s str + | NonTerminal nt => str_matches_nonterminal nt + end. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Fixpoint parse_production + (str : StringWithSplitState String split_stateT) + (pf : str ≤s str0) + (prod : production CharType) + : bool. + Proof. + refine + match prod with + | nil => + + str =s Empty _ + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (let mapF f := map f (combine_sig (split_string_for_production_correct it its str)) in + mapF (fun s1s2p => + (parse_item + (parse_nonterminal (fst (proj1_sig s1s2p)) _) + (fst (proj1_sig s1s2p)) + it) + && parse_production' (snd (proj1_sig s1s2p)) _)%bool) + end; + revert pf; clear; intros; admit. + Defined. + End production. + + End parts. + End bool. +End recursive_descent_parser. + +Section sound. + Context CharType (String : string_like CharType) (G : grammar CharType). + Context `{data : @boolean_parser_dataT CharType String}. + + Section production. + Context (str0 : String) + (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Definition parse_nonterminal_completeT P + := forall valid (str : StringWithSplitState String split_stateT) pf nonterminal (H_sub : P str0 valid nonterminal), + minimal_parse_of_name _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal + -> @parse_nonterminal str pf nonterminal = true. + + Lemma parse_production_complete + valid Pv + (parse_nonterminal_complete : parse_nonterminal_completeT Pv) + (Hinit : forall str (pf : str ≤s str0) nonterminal, + minimal_parse_of_name String G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str nonterminal + -> Pv str0 valid nonterminal) + (str : StringWithSplitState String split_stateT) (pf : str ≤s str0) + (prod : production CharType) + (split_string_for_production_complete' + : forall str0 valid str pf, + Forall_tails + (fun prod' => + match prod' return Type with + | nil => True + | it::its => split_list_completeT (G := G) (valid := valid) (str0 := str0) str pf (split_string_for_production it its str) it its + end) + prod) + : minimal_parse_of_production _ G initial_nonterminals_data is_valid_nonterminal remove_nonterminal str0 valid str prod + -> parse_production parse_nonterminal str pf prod = true. + admit. + Defined. + End production. + Context (str0 : String) + (parse_nonterminal : forall (str : StringWithSplitState String split_stateT), + str ≤s str0 + -> string + -> bool). + + Goal forall (a : production CharType), + (forall (str1 : String) (valid : nonterminals_listT) + (str : StringWithSplitState String split_stateT) + (pf : str ≤s str1), + Forall_tails + (fun prod' : list (item CharType) => + match prod' with + | [] => True + | it :: its => + split_list_completeT (G := G) (valid := valid) str pf + (split_string_for_production it its str) it its + end) a) -> + forall (str : String) (pf : str ≤s str0) (st : split_stateT str), + parse_production parse_nonterminal + {| string_val := str; state_val := st |} pf a = true. + Proof. + intros a X **. + eapply parse_production_complete. + Focus 3. + exact X. + Undo. + assumption. + Undo. + eassumption. (* no applicable tactic *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4256.v b/test-suite/bugs/closed/4256.v new file mode 100644 index 0000000000..3cdc4ada02 --- /dev/null +++ b/test-suite/bugs/closed/4256.v @@ -0,0 +1,43 @@ +(* Testing 8.5 regression with type classes not solving evars + redefined while trying to solve them with the type class mechanism *) + +Global Set Universe Polymorphism. +Monomorphic Universe i. +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Inductive trunc_index : Type := +| minus_two : trunc_index +| trunc_S : trunc_index -> trunc_index. +Notation "-1" := (trunc_S minus_two) (at level 0). + +Class IsPointed (A : Type) := point : A. +Arguments point A {_}. + +Record pType := + { pointed_type : Type ; + ispointed_type : IsPointed pointed_type }. +Coercion pointed_type : pType >-> Sortclass. +Existing Instance ispointed_type. + +Private Inductive Trunc (n : trunc_index) (A :Type) : Type := + tr : A -> Trunc n A. +Arguments tr {n A} a. + + + +Record ooGroup := + { classifying_space : pType@{i} }. + +Definition group_loops (X : pType) +: ooGroup. +Proof. + (** This works: *) + pose (x0 := point X). + pose (H := existT (fun x:X => Trunc -1 (x = point X)) x0 (tr idpath)). + clear H x0. + (** But this doesn't: *) + pose (existT (fun x:X => Trunc -1 (x = point X)) (point X) (tr idpath)). diff --git a/test-suite/bugs/closed/4273.v b/test-suite/bugs/closed/4273.v new file mode 100644 index 0000000000..591ea4b5b2 --- /dev/null +++ b/test-suite/bugs/closed/4273.v @@ -0,0 +1,9 @@ + + +Set Primitive Projections. +Record total2 (P : nat -> Prop) := tpair { pr1 : nat; pr2 : P pr1 }. +Theorem onefiber' (q : total2 (fun y => y = 0)) : True. +Proof. assert (foo:=pr2 _ q). simpl in foo. + destruct foo. (* Error: q is used in conclusion. *) exact I. Qed. + +Print onefiber'.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4284.v b/test-suite/bugs/closed/4284.v new file mode 100644 index 0000000000..0fff3026ff --- /dev/null +++ b/test-suite/bugs/closed/4284.v @@ -0,0 +1,6 @@ +Set Primitive Projections. +Record total2 { T: Type } ( P: T -> Type ) := tpair { pr1 : T; pr2 : P pr1 }. +Theorem onefiber' {X : Type} (P : X -> Type) (x : X) : True. +Proof. +set (Q1 := total2 (fun f => pr1 P f = x)). +set (f1:=fun q1 : Q1 => pr2 _ (pr1 _ q1)). diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v index 0623cf5b84..43c9b51295 100644 --- a/test-suite/bugs/closed/4287.v +++ b/test-suite/bugs/closed/4287.v @@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) := let foo (A : Type@{j}) := A in foo B. Fail Check @setlt@{j Prop}. -Check @setlt@{Prop j}. -Check @setle@{Prop j}. - Fail Definition foo := @setle@{j Prop}. -Definition foo := @setle@{Prop j}. +Check setlt@{Set i}. +Check setlt@{Set j}.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4293.v b/test-suite/bugs/closed/4293.v new file mode 100644 index 0000000000..3671c931b7 --- /dev/null +++ b/test-suite/bugs/closed/4293.v @@ -0,0 +1,7 @@ +Module Type Foo. +Definition T := let X := Type in Type. +End Foo. + +Module M : Foo. +Definition T := let X := Type in Type. +End M.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4363.v b/test-suite/bugs/closed/4363.v new file mode 100644 index 0000000000..9895548c1d --- /dev/null +++ b/test-suite/bugs/closed/4363.v @@ -0,0 +1,9 @@ +Set Printing Universes. +Definition foo : Type. +Proof. + assert (H : Set) by abstract (assert Type by abstract exact Type using bar; exact nat). + exact bar. +Defined. (* Toplevel input, characters 0-8: +Error: +The term "(fun _ : Set => bar) foo_subproof" has type +"Type@{Top.2}" while it is expected to have type "Type@{Top.1}". *) diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v new file mode 100644 index 0000000000..03af16535b --- /dev/null +++ b/test-suite/bugs/closed/4375.v @@ -0,0 +1,106 @@ + + +Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + + +Module A. +Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => foo t n + end. +End A. + +Module B. +Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => foo t n + end. +End B. + +Module C. +Fail Polymorphic Fixpoint foo@{i} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{j} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End C. + +Module D. +Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{i j} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End D. + +Module E. +Fail Polymorphic Fixpoint foo@{i j} (t : Type@{i}) (n : nat) : Type@{i} := + match n with + | 0 => t + | S n => bar t n + end + +with bar@{j i} (t : Type@{j}) (n : nat) : Type@{j} := + match n with + | 0 => t + | S n => foo t n + end. +End E. + +(* +Polymorphic Fixpoint g@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + +Print g. + +Polymorphic Fixpoint a@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t +with b@{i} (t : Type@{i}) (n : nat) : Type@{i} := + t. + +Print a. +Print b. +*) + +Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} := +| A : foo T -> foo T. + +Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (cg@{i} t). + +Print cg. + +Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (@cb@{i} t) +with cb@{i} (t : Type@{i}) : foo@{i} t := + @A@{i} t (@ca@{i} t). + +Print ca. +Print cb.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4378.v b/test-suite/bugs/closed/4378.v new file mode 100644 index 0000000000..9d59165562 --- /dev/null +++ b/test-suite/bugs/closed/4378.v @@ -0,0 +1,9 @@ +Tactic Notation "epose" open_constr(a) := + let a' := fresh in + pose a as a'. +Tactic Notation "epose2" open_constr(a) tactic3(tac) := + let a' := fresh in + pose a as a'. +Goal True. + epose _. Undo. + epose2 _ idtac. diff --git a/test-suite/bugs/closed/4390.v b/test-suite/bugs/closed/4390.v new file mode 100644 index 0000000000..a96a137001 --- /dev/null +++ b/test-suite/bugs/closed/4390.v @@ -0,0 +1,37 @@ +Module A. +Set Printing All. +Set Printing Universes. + +Module M. +Section foo. +Universe i. +End foo. +End M. + +Check Type@{i}. +(* Succeeds *) + +Fail Check Type@{j}. +(* Error: Undeclared universe: j *) + +Definition foo@{j} : Type@{i} := Type@{j}. +(* ok *) +End A. + +Set Universe Polymorphism. +Fail Universes j. +Monomorphic Universe j. +Section foo. + Universes i. + Constraint i < j. + Definition foo : Type@{j} := Type@{i}. + Definition foo' : Type@{j} := Type@{i}. +End foo. + +Check eq_refl : foo@{i} = foo'@{i}. + +Definition bar := foo. +Monomorphic Definition bar'@{k} := foo@{k}. + +Fail Constraint j = j. +Monomorphic Constraint i = i. diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v new file mode 100644 index 0000000000..60c9354597 --- /dev/null +++ b/test-suite/bugs/closed/4394.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) + +Require Import Equality List. +Inductive Foo (I : Type -> Type) (A : Type) : Type := +| foo (B : Type) : A -> I B -> Foo I A. +Definition Family := Type -> Type. +Definition FooToo : Family -> Family := Foo. +Definition optionize (I : Type -> Type) (A : Type) := option (I A). +Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A. +Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. +Definition barRec : Rec (optionize id) := {| rec := bar id |}. +Inductive Empty {T} : T -> Prop := . +Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) : + Empty (a, b) -> False. +Proof. + intro e. + dependent induction e. +Qed. + diff --git a/test-suite/bugs/closed/4397.v b/test-suite/bugs/closed/4397.v new file mode 100644 index 0000000000..3566353d84 --- /dev/null +++ b/test-suite/bugs/closed/4397.v @@ -0,0 +1,3 @@ +Require Import Equality. +Theorem foo (u : unit) (H : u = u) : True. +dependent destruction H. diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v new file mode 100644 index 0000000000..5c23f8404b --- /dev/null +++ b/test-suite/bugs/closed/4400.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-emacs" "-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *) +Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality. +Set Printing Universes. +Inductive Foo (I : Type -> Type) (A : Type) : Type := +| foo (B : Type) : A -> I B -> Foo I A. +Definition Family := Type -> Type. +Definition FooToo : Family -> Family := Foo. +Definition optionize (I : Type -> Type) (A : Type) := option (I A). +Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A. +Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }. +Definition barRec : Rec (optionize id) := {| rec := bar id |}. +Inductive Empty {T} : T -> Prop := . +Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) +nil)) (b : unit) : + Empty (a, b) -> False. +Proof. + intro e. + dependent induction e. +Qed. diff --git a/test-suite/bugs/closed/4404.v b/test-suite/bugs/closed/4404.v new file mode 100644 index 0000000000..27b43a61d4 --- /dev/null +++ b/test-suite/bugs/closed/4404.v @@ -0,0 +1,4 @@ +Inductive Foo : Type -> Type := foo A : Foo A. +Goal True. + remember Foo. + diff --git a/test-suite/bugs/closed/4412.v b/test-suite/bugs/closed/4412.v new file mode 100644 index 0000000000..4b2aae0c7b --- /dev/null +++ b/test-suite/bugs/closed/4412.v @@ -0,0 +1,4 @@ +Require Import Coq.Bool.Bool Coq.Setoids.Setoid. +Goal forall (P : forall b : bool, b = true -> Type) (x y : bool) (H : andb x y = true) (H' : P _ H), True. + intros. + Fail rewrite Bool.andb_true_iff in H. diff --git a/test-suite/bugs/closed/4420.v b/test-suite/bugs/closed/4420.v new file mode 100644 index 0000000000..0e16cb2399 --- /dev/null +++ b/test-suite/bugs/closed/4420.v @@ -0,0 +1,19 @@ +Module foo. + Context (Char : Type). + Axiom foo : Type -> Type. + Goal foo Char = foo Char. + change foo with (fun x => foo x). + cbv beta. + reflexivity. + Defined. +End foo. + +Inductive foo (A : Type) : Prop := I. (*Top.1*) +Lemma bar : foo Type. (*Top.3*) +Proof. + Set Printing Universes. +change foo with (fun x : Type => foo x). (*Top.4*) +cbv beta. +apply I. (* I Type@{Top.3} : (fun x : Type@{Top.4} => foo x) Type@{Top.3} *) +Defined. + diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v new file mode 100644 index 0000000000..bf0e570ab8 --- /dev/null +++ b/test-suite/bugs/closed/4429.v @@ -0,0 +1,31 @@ +Require Import Arith.Compare_dec. +Require Import Unicode.Utf8. + +Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A := + match n with + | O => x + | S n' => f (my_nat_iter n' f x) + end. + +Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat := + match mn with + | (0, 0) => 0 + | (0, S n') => S n' + | (S m', 0) => S m' + | (S m', S n') => + match le_gt_dec (S m') (S n') with + | left _ => f (S m', S n' - S m') + | right _ => f (S m' - S n', S n') + end + end. + +Axiom max_correct_l : ∀ m n : nat, m <= max m n. +Axiom max_correct_r : ∀ m n : nat, n <= max m n. + +Hint Resolve max_correct_l max_correct_r : arith. + +Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')). +Proof. + intros. + Timeout 3 eauto with arith. +Qed. diff --git a/test-suite/bugs/closed/4433.v b/test-suite/bugs/closed/4433.v new file mode 100644 index 0000000000..9eeb864689 --- /dev/null +++ b/test-suite/bugs/closed/4433.v @@ -0,0 +1,29 @@ +Require Import Coq.Arith.Arith Coq.Init.Wf. +Axiom proof_admitted : False. +Goal exists x y z : nat, Fix + Wf_nat.lt_wf + (fun _ => nat -> nat) + (fun x' f => match x' as x'0 + return match x'0 with + | 0 => True + | S x'' => x'' < x' + end + -> nat -> nat + with + | 0 => fun _ _ => 0 + | S x'' => f x'' + end + (match x' with + | 0 => I + | S x'' => (Nat.lt_succ_diag_r _) + end)) + z + y + = 0. +Proof. + do 3 (eexists; [ shelve.. | ]). + match goal with |- ?G => let G' := (eval lazy in G) in change G with G' end. + case proof_admitted. + Unshelve. + all:constructor. +Defined.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v new file mode 100644 index 0000000000..66dfa0e685 --- /dev/null +++ b/test-suite/bugs/closed/4443.v @@ -0,0 +1,31 @@ +Set Universe Polymorphism. + +Record TYPE@{i} := cType { + type : Type@{i}; +}. + +Definition PROD@{i j k} + (A : Type@{i}) + (B : A -> Type@{j}) + : TYPE@{k}. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + +Local Unset Strict Universe Declaration. +Definition PRODinj + (A : Type@{i}) + (B : A -> Type) + : TYPE. +Proof. + refine (cType@{i} _). ++ refine (forall x : A, B x). +Defined. + + Monomorphic Universe i j. + Monomorphic Constraint j < i. +Set Printing Universes. +Check PROD@{i i i}. +Check PRODinj@{i j}. +Fail Check PRODinj@{j i}.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4453.v b/test-suite/bugs/closed/4453.v new file mode 100644 index 0000000000..009dd5e3ca --- /dev/null +++ b/test-suite/bugs/closed/4453.v @@ -0,0 +1,8 @@ + +Section Foo. +Variable A : Type. +Lemma foo : A -> True. now intros _. Qed. +Goal Type -> True. +rename A into B. +intros A. +Fail apply foo. diff --git a/test-suite/bugs/closed/4456.v b/test-suite/bugs/closed/4456.v new file mode 100644 index 0000000000..a32acf789c --- /dev/null +++ b/test-suite/bugs/closed/4456.v @@ -0,0 +1,647 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fiat" "-top" "BooleanRecognizerMin" "-R" "." "Top") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2475 lines to 729 lines, then from 746 lines to 658 lines, then from 675 lines to 658 lines *) +(* coqc version 8.5beta3 (November 2015) compiled on Nov 11 2015 18:23:0 with OCaml 4.01.0 + coqtop version 8.5beta3 (November 2015) *) +(* Variable P : forall n m : nat, n = m -> Prop. *) +(* Axiom Prefl : forall n : nat, P n n eq_refl. *) +Axiom proof_admitted : False. + +Tactic Notation "admit" := case proof_admitted. + +Require Coq.Program.Program. +Require Coq.Strings.String. +Require Coq.omega.Omega. +Module Export Fiat_DOT_Common. +Module Export Fiat. +Module Common. +Import Coq.Lists.List. +Export Coq.Program.Program. + +Global Set Implicit Arguments. + +Global Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sum {A B} (b : sum A B) : bool := if b then true else false. + +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +End Common. + +End Fiat. + +End Fiat_DOT_Common. +Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export Fiat. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Relations.Relation_Definitions. +Import Coq.Classes.Morphisms. + +Local Coercion is_true : bool >-> Sortclass. + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + get : nat -> String -> option Char; + unsafe_get : nat -> String -> Char; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + singleton_exists : forall s, length s = 1 -> exists ch, s ~= [ ch ]; + get_0 : forall s ch, take 1 s ~= [ ch ] <-> get 0 s = Some ch; + get_S : forall n s, get (S n) s = get n (drop 1 s); + unsafe_get_correct : forall n s ch, get n s = Some ch -> unsafe_get n s = ch; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str); + bool_eq_from_get : forall str str', (forall n, get n str = get n str') -> str =s str' + }. +Global Arguments StringLikeProperties _ {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core. +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Core. +Import Coq.Strings.String. +Import Coq.Lists.List. +Export Fiat.Parsers.StringLike.Core. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End Core. + +End ContextFreeGrammar. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Core. + +Module Export Fiat_DOT_Parsers_DOT_BaseTypes. +Module Export Fiat. +Module Export Parsers. +Module Export BaseTypes. +Import Coq.Arith.Wf_nat. + +Local Coercion is_true : bool >-> Sortclass. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + nonterminal_carrierT : Type; + of_nonterminal : String.string -> nonterminal_carrierT; + to_nonterminal : nonterminal_carrierT -> String.string; + initial_nonterminals_data : nonterminals_listT; + nonterminals_length : nonterminals_listT -> nat; + is_valid_nonterminal : nonterminals_listT -> nonterminal_carrierT -> bool; + remove_nonterminal : nonterminals_listT -> nonterminal_carrierT -> nonterminals_listT }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop + := ltof _ nonterminals_length; + nonterminals_length_zero : forall ls, + nonterminals_length ls = 0 + -> forall nt, is_valid_nonterminal ls nt = false; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + remove_nonterminal_noninc : forall ls nonterminal, + ~nonterminals_listT_R ls (remove_nonterminal ls nonterminal); + initial_nonterminals_correct : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) <-> List.In nonterminal (Valid_nonterminals G); + initial_nonterminals_correct' : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data nonterminal <-> List.In (to_nonterminal nonterminal) (Valid_nonterminals G); + to_of_nonterminal : forall nonterminal, + List.In nonterminal (Valid_nonterminals G) + -> to_nonterminal (of_nonterminal nonterminal) = nonterminal; + of_to_nonterminal : forall nonterminal, + is_valid_nonterminal initial_nonterminals_data nonterminal + -> of_nonterminal (to_nonterminal nonterminal) = nonterminal; + ntl_wf : well_founded nonterminals_listT_R + := well_founded_ltof _ _; + remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. + + Class split_dataT := + { split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_data :> split_dataT }. +End recursive_descent_parser. + +End BaseTypes. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_BaseTypes. + +Module Export Fiat_DOT_Common_DOT_List_DOT_Operations. +Module Export Fiat. +Module Export Common. +Module Export List. +Module Export Operations. + +Import Coq.Lists.List. + +Module Export List. + Section InT. + Context {A : Type} (a : A). + + Fixpoint InT (ls : list A) : Set + := match ls return Set with + | nil => False + | b :: m => (b = a) + InT m + end%type. + End InT. + + End List. + +End Operations. + +End List. + +End Common. + +End Fiat. + +End Fiat_DOT_Common_DOT_List_DOT_Operations. + +Module Export Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties. +Module Export Fiat. +Module Export Parsers. +Module Export StringLike. +Module Export Properties. + +Section String. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char}. + + Lemma take_length {str n} + : length (take n str) = min n (length str). +admit. +Defined. + + End String. + +End Properties. + +End StringLike. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_StringLike_DOT_Properties. + +Module Export Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties. +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Properties. + +Local Open Scope list_scope. +Definition production_is_reachableT {Char} (G : grammar Char) (p : production Char) + := { nt : _ + & { prefix : _ + & List.In nt (Valid_nonterminals G) + * List.InT + (prefix ++ p) + (Lookup G nt) } }%type. + +End Properties. + +End ContextFreeGrammar. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_ContextFreeGrammar_DOT_Properties. + +Module Export Fiat_DOT_Parsers_DOT_MinimalParse. +Module Export Fiat. +Module Export Parsers. +Module Export MinimalParse. +Import Coq.Lists.List. +Import Fiat.Parsers.ContextFreeGrammar.Core. + +Local Coercion is_true : bool >-> Sortclass. +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' _ G predata}. + + Inductive minimal_parse_of + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall len0 valid str pat pats, + @minimal_parse_of_production len0 valid str pat + -> @minimal_parse_of len0 valid str (pat::pats) + | MinParseTail : forall len0 valid str pat pats, + @minimal_parse_of len0 valid str pats + -> @minimal_parse_of len0 valid str (pat::pats) + with minimal_parse_of_production + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall len0 valid str, + length str = 0 + -> @minimal_parse_of_production len0 valid str nil + | MinParseProductionCons : forall len0 valid str n pat pats, + length str <= len0 + -> @minimal_parse_of_item len0 valid (take n str) pat + -> @minimal_parse_of_production len0 valid (drop n str) pats + -> @minimal_parse_of_production len0 valid str (pat::pats) + with minimal_parse_of_item + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall len0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item len0 valid str (Terminal ch) + | MinParseNonTerminal + : forall len0 valid str (nt : String.string), + @minimal_parse_of_nonterminal len0 valid str nt + -> @minimal_parse_of_item len0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (len0 : nat) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall len0 valid (nt : String.string) str, + length str < len0 + -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) + -> @minimal_parse_of (length str) initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal len0 valid str nt + | MinParseNonTerminalStrEq + : forall len0 str valid nonterminal, + length str = len0 + -> is_valid_nonterminal initial_nonterminals_data (of_nonterminal nonterminal) + -> is_valid_nonterminal valid (of_nonterminal nonterminal) + -> @minimal_parse_of len0 (remove_nonterminal valid (of_nonterminal nonterminal)) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal len0 valid str nonterminal. + +End cfg. + +End MinimalParse. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_MinimalParse. + +Module Export Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes. +Module Export Fiat. +Module Export Parsers. +Module Export CorrectnessBaseTypes. +Import Coq.Lists.List. +Import Fiat.Parsers.ContextFreeGrammar.Core. +Import Fiat_DOT_Common.Fiat.Common. +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Definition split_list_completeT_for {data : @parser_computational_predataT} + {len0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : length str <= len0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) len0 valid (take n str) it) + * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In (min (length str) n) (map (min (length str)) split_list)) + * (minimal_parse_of_item (G := G) len0 valid (take n str) it) + * (minimal_parse_of_production (G := G) len0 valid (drop n str) its) }%type). + + Definition split_list_completeT {data : @parser_computational_predataT} + (splits : item Char -> production Char -> String -> list nat) + := forall len0 valid str (pf : length str <= len0) nt, + is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt) + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT_for data len0 valid it its str pf (splits it its str) + end)) + (Lookup G nt). + + Class boolean_parser_completeness_dataT' {data : boolean_parser_dataT} := + { split_string_for_production_complete + : split_list_completeT split_string_for_production }. +End general. + +End CorrectnessBaseTypes. + +End Parsers. + +End Fiat. + +End Fiat_DOT_Parsers_DOT_CorrectnessBaseTypes. + +Module Export Fiat. +Module Export Parsers. +Module Export ContextFreeGrammar. +Module Export Valid. +Export Fiat.Parsers.StringLike.Core. + +Section cfg. + Context {Char : Type} {HSL : StringLike Char} (G : grammar Char) + {predata : parser_computational_predataT}. + + Definition item_valid (it : item Char) + := match it with + | Terminal _ => True + | NonTerminal nt' => is_true (is_valid_nonterminal initial_nonterminals_data (of_nonterminal nt')) + end. + + Definition production_valid pat + := List.Forall item_valid pat. + + Definition productions_valid pats + := List.Forall production_valid pats. + + Definition grammar_valid + := forall nt, + List.In nt (Valid_nonterminals G) + -> productions_valid (Lookup G nt). +End cfg. + +End Valid. + +Section app. + Context {Char : Type} {HSL : StringLike Char} (G : grammar Char) + {predata : parser_computational_predataT}. + + Lemma hd_production_valid + (it : item Char) + (its : production Char) + (H : production_valid (it :: its)) + : item_valid it. +admit. +Defined. + + Lemma production_valid_cons + (it : item Char) + (its : production Char) + (H : production_valid (it :: its)) + : production_valid its. +admit. +Defined. + + End app. + +Import Coq.Lists.List. +Import Coq.omega.Omega. +Import Fiat_DOT_Common.Fiat.Common. +Import Fiat.Parsers.ContextFreeGrammar.Valid. +Local Open Scope string_like_scope. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' _ G _} + {gvalid : grammar_valid G}. + + Local Notation dec T := (T + (T -> False))%type (only parsing). + + Local Notation iffT x y := ((x -> y) * (y -> x))%type (only parsing). + + Lemma dec_prod {A B} (HA : dec A) (HB : dec B) : dec (A * B). +admit. +Defined. + + Lemma dec_In {A} {P : A -> Type} (HA : forall a, dec (P a)) ls + : dec { a : _ & (In a ls * P a) }. +admit. +Defined. + + Section item. + Context {len0 valid} + (str : String) + (str_matches_nonterminal' + : nonterminal_carrierT -> bool) + (str_matches_nonterminal + : forall nt : nonterminal_carrierT, + dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))). + + Section valid. + Context (Hmatches + : forall nt, + is_valid_nonterminal initial_nonterminals_data nt + -> str_matches_nonterminal nt = str_matches_nonterminal' nt :> bool) + (it : item Char) + (Hvalid : item_valid it). + + Definition parse_item' + : dec (minimal_parse_of_item (G := G) len0 valid str it). + Proof. + clear Hvalid. + refine (match it return dec (minimal_parse_of_item len0 valid str it) with + | Terminal ch => if Sumbool.sumbool_of_bool (str ~= [ ch ]) + then inl (MinParseTerminal _ _ _ _ _) + else inr (fun _ => !) + | NonTerminal nt => if str_matches_nonterminal (of_nonterminal nt) + then inl (MinParseNonTerminal _) + else inr (fun _ => !) + end); + clear str_matches_nonterminal Hmatches; + admit. + Defined. + End valid. + + End item. + Context {len0 valid} + (parse_nonterminal + : forall (str : String) (len : nat) (Hlen : length str = len) (pf : len <= len0) (nt : nonterminal_carrierT), + dec (minimal_parse_of_nonterminal (G := G) len0 valid str (to_nonterminal nt))). + + Lemma dec_in_helper {ls it its str} + : iffT {n0 : nat & + (In (min (length str) n0) (map (min (length str)) ls) * + minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type} + {n0 : nat & + (In n0 ls * + (minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its))%type}. +admit. +Defined. + + Lemma parse_production'_helper {str it its} (pf : length str <= len0) + : dec {n0 : nat & + (minimal_parse_of_item (G := G) len0 valid (take n0 str) it * + minimal_parse_of_production (G := G) len0 valid (drop n0 str) its)%type} + -> dec (minimal_parse_of_production (G := G) len0 valid str (it :: its)). +admit. +Defined. + Local Ltac t_parse_production_for := repeat + match goal with + | [ H : (beq_nat _ _) = true |- _ ] => apply EqNat.beq_nat_true in H + | _ => progress subst + | _ => solve [ constructor; assumption ] + | [ H : minimal_parse_of_production _ _ _ nil |- _ ] => (inversion H; clear H) + | [ H : minimal_parse_of_production _ _ _ (_::_) |- _ ] => (inversion H; clear H) + | [ H : ?x = 0, H' : context[?x] |- _ ] => rewrite H in H' + | _ => progress simpl in * + | _ => discriminate + | [ H : forall x, (_ * _)%type -> _ |- _ ] => specialize (fun x y z => H x (y, z)) + | _ => solve [ eauto with nocore ] + | _ => solve [ apply Min.min_case_strong; omega ] + | _ => omega + | [ H : production_valid (_::_) |- _ ] + => let H' := fresh in + pose proof H as H'; + apply production_valid_cons in H; + apply hd_production_valid in H' + end. + + Definition parse_production'_for + (splits : item Char -> production Char -> String -> list nat) + (Hsplits : forall str it its (Hreachable : production_is_reachableT G (it::its)) pf', split_list_completeT_for (len0 := len0) (G := G) (valid := valid) it its str pf' (splits it its str)) + (str : String) + (len : nat) + (Hlen : length str = len) + (pf : len <= len0) + (prod : production Char) + (Hreachable : production_is_reachableT G prod) + : dec (minimal_parse_of_production (G := G) len0 valid str prod). + Proof. + revert prod Hreachable str len Hlen pf. + refine + ((fun pf_helper => + list_rect + (fun prod => + forall (Hreachable : production_is_reachableT G prod) + (str : String) + (len : nat) + (Hlen : length str = len) + (pf : len <= len0), + dec (minimal_parse_of_production (G := G) len0 valid str prod)) + ( + fun Hreachable str len Hlen pf + => match Utils.dec (beq_nat len 0) with + | left H => inl _ + | right H => inr (fun p => _) + end) + (fun it its parse_production' Hreachable str len Hlen pf + => parse_production'_helper + _ + (let parse_item := (fun n pf => parse_item' (parse_nonterminal (take n str) (len := min n len) (eq_trans take_length (f_equal (min _) Hlen)) pf) it) in + let parse_item := (fun n => parse_item n (Min.min_case_strong n len (fun k => k <= len0) (fun Hlen => (Nat.le_trans _ _ _ Hlen pf)) (fun Hlen => pf))) in + let parse_production := (fun n => parse_production' (pf_helper it its Hreachable) (drop n str) (len - n) (eq_trans (drop_length _ _) (f_equal (fun x => x - _) Hlen)) (Nat.le_trans _ _ _ (Nat.le_sub_l _ _) pf)) in + match dec_In + (fun n => dec_prod (parse_item n) (parse_production n)) + (splits it its str) + with + | inl p => inl (existT _ (projT1 p) (snd (projT2 p))) + | inr p + => let pf' := (Nat.le_trans _ _ _ (Nat.eq_le_incl _ _ Hlen) pf) in + let H := (_ : split_list_completeT_for (G := G) (len0 := len0) (valid := valid) it its str pf' (splits it its str)) in + inr (fun p' => p (fst dec_in_helper (H p'))) + end) + )) _); + [ clear parse_nonterminal Hsplits splits rdata cdata + | clear parse_nonterminal Hsplits splits rdata cdata + | .. + | admit ]. + abstract t_parse_production_for. + abstract t_parse_production_for. + abstract t_parse_production_for. + abstract t_parse_production_for. + Defined. diff --git a/test-suite/bugs/closed/4462.v b/test-suite/bugs/closed/4462.v new file mode 100644 index 0000000000..c680518c6a --- /dev/null +++ b/test-suite/bugs/closed/4462.v @@ -0,0 +1,7 @@ +Variables P Q : Prop. +Axiom pqrw : P <-> Q. + +Require Setoid. + +Goal P -> Q. +unshelve (rewrite pqrw). diff --git a/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v new file mode 100644 index 0000000000..6f8631d458 --- /dev/null +++ b/test-suite/bugs/closed/4467.v @@ -0,0 +1,15 @@ +(* Fixing missing test for variable shadowing *) + +Definition test (x y:bool*bool) := + match x with + | (e as e1, (true) as e2) + | ((true) as e1, e as e2) => + let '(e, b) := y in + e + | _ => true + end. + +Goal test (true,false) (true,true) = true. +(* used to evaluate to "false = true" in 8.4 *) +reflexivity. +Qed. 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/closed/4480.v b/test-suite/bugs/closed/4480.v new file mode 100644 index 0000000000..08a86330f2 --- /dev/null +++ b/test-suite/bugs/closed/4480.v @@ -0,0 +1,12 @@ +Require Import Setoid. + +Definition proj (P Q : Prop) := P. + +Lemma foo (P : Prop) : proj P P = P. +Admitted. +Lemma trueI : True <-> True. +Admitted. +Goal True. + Fail setoid_rewrite foo. + Fail setoid_rewrite trueI. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/4484.v b/test-suite/bugs/closed/4484.v new file mode 100644 index 0000000000..f988539d62 --- /dev/null +++ b/test-suite/bugs/closed/4484.v @@ -0,0 +1,10 @@ +(* Testing 8.5 regression with type classes not solving evars + redefined while trying to solve them with the type class mechanism *) + +Class A := {}. +Axiom foo : forall {ac : A}, bool. +Lemma bar (ac : A) : True. +Check (match foo as k return foo = k -> True with + | true => _ + | false => _ + end eq_refl). diff --git a/test-suite/bugs/closed/4495.v b/test-suite/bugs/closed/4495.v new file mode 100644 index 0000000000..8b032db5f5 --- /dev/null +++ b/test-suite/bugs/closed/4495.v @@ -0,0 +1 @@ +Fail Notation "'forall' x .. y ',' P " := (forall x, .. (forall y, P) ..) (at level 200, x binder, y binder). diff --git a/test-suite/bugs/closed/4503.v b/test-suite/bugs/closed/4503.v new file mode 100644 index 0000000000..f54d6433d8 --- /dev/null +++ b/test-suite/bugs/closed/4503.v @@ -0,0 +1,37 @@ +Require Coq.Classes.RelationClasses. + +Class PreOrder (A : Type) (r : A -> A -> Type) : Type := +{ refl : forall x, r x x }. + +(* FAILURE 1 *) + +Section foo. + Polymorphic Universes A. + Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + + Fail Definition foo := PO. +End foo. + + +Module ILogic. + +Set Universe Polymorphism. + +(* Logical connectives *) +Class ILogic@{L} (A : Type@{L}) : Type := mkILogic +{ + lentails: A -> A -> Prop; + lentailsPre:> RelationClasses.PreOrder lentails +}. + + +End ILogic. + +Set Printing Universes. + +(* There is stil a problem if the class is universe polymorphic *) +Section Embed_ILogic_Pre. + Polymorphic Universes A T. + Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. + +End Embed_ILogic_Pre.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4511.v b/test-suite/bugs/closed/4511.v new file mode 100644 index 0000000000..0cdb3aee4f --- /dev/null +++ b/test-suite/bugs/closed/4511.v @@ -0,0 +1,3 @@ +Goal True. +Fail evar I. + diff --git a/test-suite/bugs/closed/4519.v b/test-suite/bugs/closed/4519.v new file mode 100644 index 0000000000..ccbc47d20f --- /dev/null +++ b/test-suite/bugs/closed/4519.v @@ -0,0 +1,21 @@ +Set Universe Polymorphism. +Section foo. + Universe i. + Context (foo : Type@{i}) (bar : Type@{i}). + Definition qux@{i} (baz : Type@{i}) := foo -> bar. +End foo. +Set Printing Universes. +Print qux. (* qux@{Top.42 Top.43} = +fun foo bar _ : Type@{Top.42} => foo -> bar + : Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} -> Type@{Top.42} +(* Top.42 Top.43 |= *) +(* This is wrong; the first two types are equal, but the last one is not *) + +qux is universe polymorphic +Argument scopes are [type_scope type_scope type_scope] + *) +Check qux nat nat nat : Set. +Check qux nat nat Set : Set. (* Error: +The term "qux@{Top.50 Top.51} ?T ?T0 Set" has type "Type@{Top.50}" while it is +expected to have type "Set" +(universe inconsistency: Cannot enforce Top.50 = Set because Set < Top.50). *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v new file mode 100644 index 0000000000..ae17fb145d --- /dev/null +++ b/test-suite/bugs/closed/4533.v @@ -0,0 +1,226 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *) +(* File reduced by coq-bug-finder from original input, then from 1125 lines to +346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, +then from 285 lines to 271 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml +4.01.0 + coqtop version 8.5 (January 2016) *) +Inductive False := . +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Init.Datatypes. +Import Coq.Init.Notations. +Global Set Universe Polymorphism. +Global Set Primitive Projections. +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Module Export Datatypes. + Set Implicit Arguments. + Notation nat := Coq.Init.Datatypes.nat. + Notation S := Coq.Init.Datatypes.S. + Record prod (A B : Type) := pair { fst : A ; snd : B }. + Notation "x * y" := (prod x y) : type_scope. + Delimit Scope nat_scope with nat. + Open Scope nat_scope. +End Datatypes. +Module Export Specif. + Set Implicit Arguments. + Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P +proj1_sig }. + Notation sigT := sig (only parsing). + Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. + Notation projT1 := proj1_sig (only parsing). + Notation projT2 := proj2_sig (only parsing). +End Specif. +Global Set Keyed Unification. +Global Unset Strict Universe Declaration. +Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. +Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in +Type@{i}. +Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in + let ge := ((fun x => x) : Type1@{j} -> +Type@{i}) in Type@{i}. +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Open Scope fibration_scope. +Open Scope function_scope. +Notation pr1 := projT1. +Notation pr2 := projT2. +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. +Notation compose := (fun g f x => g (f x)). +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left +associativity) : function_scope. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. +Notation "1" := idpath : path_scope. +Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope. +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +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. +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr +(f x) = ap f (eissect x) + }. +Arguments eissect {A B}%type_scope f%function_scope {_} _. +Inductive Unit : Type1 := tt : Unit. +Local Open Scope path_scope. +Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z += t) : + p @ (q @ r) = (p @ q) @ r := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. +Section Adjointify. + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). + admit. + Defined. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. +End Adjointify. +Definition ExtensionAlong {A B : Type} (f : A -> B) + (P : B -> Type) (d : forall x:A, P (f x)) + := { s : forall y:B, P y & forall x:A, s (f x) = d x }. +Fixpoint ExtendableAlong@{i j k l} + (n : nat) {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := match n with + | 0 => Unit@{l} + | S n => (forall (g : forall a, C (f a)), + ExtensionAlong@{i j k l l} f C g) * + forall (h k : forall b, C b), + ExtendableAlong n f (fun b => h b = k b) + end. + +Definition ooExtendableAlong@{i j k l} + {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := forall n, ExtendableAlong@{i j k l} n f C. + +Module Type ReflectiveSubuniverses. + + Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : +Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : +Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). + +End ReflectiveSubuniverses. + +Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). + Export Os. + Existing Class In. + Module Export Coercions. + Coercion O_reflector : ReflectiveSubuniverse >-> Funclass. + End Coercions. + Global Existing Instance O_inO. + + Section ORecursion. + Context {O : ReflectiveSubuniverse}. + + Definition O_rec {P Q : Type} {Q_inO : In O Q} + (f : P -> Q) + : O P -> Q + := (fst (extendable_to_O O 1%nat) f).1. + + Definition O_rec_beta {P Q : Type} {Q_inO : In O Q} + (f : P -> Q) (x : P) + : O_rec f (to O P x) = f x + := (fst (extendable_to_O O 1%nat) f).2 x. + + Definition O_indpaths {P Q : Type} {Q_inO : In O Q} + (g h : O P -> Q) (p : g o to O P == h o to O P) + : g == h + := (fst (snd (extendable_to_O O 2) g h) p).1. + + End ORecursion. + + + Section Reflective_Subuniverse. + Context (O : ReflectiveSubuniverse@{Ou Oa}). + + Definition isequiv_to_O_inO@{u a i} (T : Type@{i}) `{In@{u a i} O T} : +IsEquiv@{i i} (to O T). + Proof. + + pose (g := O_rec@{u a i i i i i} idmap). + refine (isequiv_adjointify (to O T) g _ _). + - + refine (O_indpaths@{u a i i i i i} (to O T o g) idmap _). + intros x. + apply ap. + apply O_rec_beta. + - + intros x. + apply O_rec_beta. + Defined. + Global Existing Instance isequiv_to_O_inO. + + End Reflective_Subuniverse. + +End ReflectiveSubuniverses_Theory. + +Module Type Preserves_Fibers (Os : ReflectiveSubuniverses). + Module Export Os_Theory := ReflectiveSubuniverses_Theory Os. +End Preserves_Fibers. + +Opaque eissect. +Module Lex_Reflective_Subuniverses + (Os : ReflectiveSubuniverses) (Opf : Preserves_Fibers Os). + Import Opf. + Goal forall (O : ReflectiveSubuniverse) (A : Type) (B : A -> Type) (A_inO : +In O A), + + forall g, + forall (x : O {x : A & B x}) v v' v'' (p2 : v'' = v') (p0 : v' = v) (p1 : +v = _) r, + (p2 + @ (p0 + @ p1)) + @ eissect (to O A) (g x) = r. + intros. + cbv zeta. + rewrite concat_p_pp. + match goal with + | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good" + | [ |- ?G ] => fail 1 "bad" G + end. + Fail rewrite concat_p_pp.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v new file mode 100644 index 0000000000..d14cc86fc7 --- /dev/null +++ b/test-suite/bugs/closed/4544.v @@ -0,0 +1,1007 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *) +(* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 + coqtop version 8.5 (January 2016) *) +Inductive False := . +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Coq.Init.Datatypes. + +Import Coq.Init.Notations. + +Global Set Universe Polymorphism. + +Notation "A -> B" := (forall (_ : A), B) : type_scope. +Global Set Primitive Projections. + +Inductive sum (A B : Type) : Type := + | inl : A -> sum A B + | inr : B -> sum A B. +Notation nat := Coq.Init.Datatypes.nat. +Notation S := Coq.Init.Datatypes.S. +Notation "x + y" := (sum x y) : type_scope. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. + +Notation "x * y" := (prod x y) : type_scope. +Module Export Specif. + +Set Implicit Arguments. + +Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }. +Arguments proj1_sig {A P} _ / . + +Notation sigT := sig (only parsing). +Notation existT := exist (only parsing). + +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. + +Notation projT1 := proj1_sig (only parsing). +Notation projT2 := proj2_sig (only parsing). + +End Specif. +Module Export HoTT_DOT_Basics_DOT_Overture. +Module Export HoTT. +Module Export Basics. +Module Export Overture. + +Global Set Keyed Unification. + +Global Unset Strict Universe Declaration. + +Notation Type0 := Set. + +Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}. + +Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in Type@{i}. + +Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in + let ge := ((fun x => x) : Type1@{j} -> Type@{i}) in Type@{i}. + +Notation idmap := (fun x => x). +Delimit Scope function_scope with function. +Delimit Scope path_scope with path. +Delimit Scope fibration_scope with fibration. +Delimit Scope trunc_scope with trunc. + +Open Scope trunc_scope. +Open Scope path_scope. +Open Scope fibration_scope. +Open Scope nat_scope. +Open Scope function_scope. + +Notation "( x ; y )" := (existT _ x y) : fibration_scope. + +Notation pr1 := projT1. +Notation pr2 := projT2. + +Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope. +Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope. + +Notation compose := (fun g f x => g (f x)). + +Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope. + +Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Notation "x = y :> A" := (@paths A x y) : type_scope. +Notation "x = y" := (x = y :>_) : type_scope. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. + +Notation "1" := idpath : path_scope. + +Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope. + +Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope. + +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := + match p with idpath => u end. + +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + +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. + +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := + forall x : A, r (s x) = x. + +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) +}. + +Arguments eisretr {A B}%type_scope f%function_scope {_} _. + +Record Equiv A B := BuildEquiv { + equiv_fun : A -> B ; + equiv_isequiv : IsEquiv equiv_fun +}. + +Coercion equiv_fun : Equiv >-> Funclass. + +Global Existing Instance equiv_isequiv. + +Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope. + +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope. + +Class Contr_internal (A : Type) := BuildContr { + center : A ; + contr : (forall y : A, center = y) +}. + +Arguments center A {_}. + +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. +Notation "-2" := minus_two (at level 0) : trunc_scope. +Notation "-1" := (-2.+1) (at level 0) : trunc_scope. +Notation "0" := (-1.+1) : 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. + +Global Instance istrunc_paths (A : Type) n `{H : IsTrunc n.+1 A} (x y : A) +: IsTrunc n (x = y) + := H x y. + +Notation Contr := (IsTrunc -2). +Notation IsHProp := (IsTrunc -1). + +Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances. + +Monomorphic Axiom dummy_funext_type : Type0. +Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }. + +Inductive Unit : Type1 := + tt : Unit. + +Class IsPointed (A : Type) := point : A. + +Arguments point A {_}. + +Record pType := + { pointed_type : Type ; + ispointed_type : IsPointed pointed_type }. + +Coercion pointed_type : pType >-> Sortclass. + +Global Existing Instance ispointed_type. + +Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }. + +Ltac revert_opaque x := + revert x; + match goal with + | [ |- forall _, _ ] => idtac + | _ => fail 1 "Reverted constant is not an opaque variable" + end. + +End Overture. + +End Basics. + +End HoTT. + +End HoTT_DOT_Basics_DOT_Overture. +Module Export HoTT_DOT_Basics_DOT_PathGroupoids. +Module Export HoTT. +Module Export Basics. +Module Export PathGroupoids. + +Local Open Scope path_scope. + +Definition concat_p1 {A : Type} {x y : A} (p : x = y) : + p @ 1 = p + := + match p with idpath => 1 end. + +Definition concat_1p {A : Type} {x y : A} (p : x = y) : + 1 @ p = p + := + match p with idpath => 1 end. + +Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : + p @ (q @ r) = (p @ q) @ r := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. + +Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) : + (p @ q) @ r = p @ (q @ r) := + match r with idpath => + match q with idpath => + match p with idpath => 1 + end end end. + +Definition concat_pV {A : Type} {x y : A} (p : x = y) : + p @ p^ = 1 + := + match p with idpath => 1 end. + +Definition moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) : + p = r @ q -> r^ @ p = q. +admit. +Defined. + +Definition moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) : + r @ q = p -> q = r^ @ p. +admit. +Defined. + +Definition moveR_M1 {A : Type} {x y : A} (p q : x = y) : + 1 = p^ @ q -> p = q. +admit. +Defined. + +Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) : + ap f (p @ q) = (ap f p) @ (ap f q) + := + match q with + idpath => + match p with idpath => 1 end + end. + +Definition ap_V {A B : Type} (f : A -> B) {x y : A} (p : x = y) : + ap f (p^) = (ap f p)^ + := + match p with idpath => 1 end. + +Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) : + ap (g o f) p = ap g (ap f p) + := + match p with idpath => 1 end. + +Definition concat_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A} (q : x = y) : + (p x) @ (ap f q) = q @ (p y) + := + match q as i in (_ = y) return (p x @ ap f i = i @ p y) with + | idpath => concat_p1 _ @ (concat_1p _)^ + end. + +End PathGroupoids. + +End Basics. + +End HoTT. + +End HoTT_DOT_Basics_DOT_PathGroupoids. +Module Export HoTT_DOT_Basics_DOT_Equivalences. +Module Export HoTT. +Module Export Basics. +Module Export Equivalences. + +Definition isequiv_commsq {A B C D} + (f : A -> B) (g : C -> D) (h : A -> C) (k : B -> D) + (p : k o f == g o h) + `{IsEquiv _ _ f} `{IsEquiv _ _ h} `{IsEquiv _ _ k} +: IsEquiv g. +admit. +Defined. + +Section Adjointify. + + Context {A B : Type} (f : A -> B) (g : B -> A). + Context (isretr : Sect g f) (issect : Sect f g). + + Let issect' := fun x => + ap g (ap f (issect x)^) @ ap g (isretr (f x)) @ issect x. + + Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a). + Proof. + unfold issect'. + apply moveR_M1. + repeat rewrite ap_pp, concat_p_pp; rewrite <- ap_compose. + rewrite (concat_pA1 (fun b => (isretr b)^) (ap f (issect a)^)). + repeat rewrite concat_pp_p; rewrite ap_V; apply moveL_Vp; rewrite concat_p1. + rewrite concat_p_pp, <- ap_compose. + rewrite (concat_pA1 (fun b => (isretr b)^) (isretr (f a))). + rewrite concat_pV, concat_1p; reflexivity. + Qed. + + Definition isequiv_adjointify : IsEquiv f + := BuildIsEquiv A B f g isretr issect' is_adjoint'. + +End Adjointify. + +End Equivalences. + +End Basics. + +End HoTT. + +End HoTT_DOT_Basics_DOT_Equivalences. +Module Export HoTT_DOT_Basics_DOT_Trunc. +Module Export HoTT. +Module Export Basics. +Module Export Trunc. +Generalizable Variables A B m n f. + +Definition trunc_equiv A {B} (f : A -> B) + `{IsTrunc n A} `{IsEquiv A B f} + : IsTrunc n B. +admit. +Defined. + +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). + +End Trunc. + +End Basics. + +End HoTT. + +End HoTT_DOT_Basics_DOT_Trunc. +Module Export HoTT_DOT_Types_DOT_Unit. +Module Export HoTT. +Module Export Types. +Module Export Unit. + +Notation unit_name x := (fun (_ : Unit) => x). + +End Unit. + +End Types. + +End HoTT. + +End HoTT_DOT_Types_DOT_Unit. +Module Export HoTT_DOT_Types_DOT_Sigma. +Module Export HoTT. +Module Export Types. +Module Export Sigma. +Local Open Scope path_scope. + +Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P) + (pq : {p : u.1 = v.1 & p # u.2 = v.2}) +: u = v + := match pq.2 in (_ = v2) return u = (v.1; v2) with + | 1 => match pq.1 as p in (_ = v1) return u = (v1; p # u.2) with + | 1 => 1 + end + end. + +Definition path_sigma {A : Type} (P : A -> Type) (u v : sigT P) + (p : u.1 = v.1) (q : p # u.2 = v.2) +: u = v + := path_sigma_uncurried P u v (p;q). + +Definition path_sigma' {A : Type} (P : A -> Type) {x x' : A} {y : P x} {y' : P x'} + (p : x = x') (q : p # y = y') +: (x;y) = (x';y') + := path_sigma P (x;y) (x';y') p q. + +Global Instance isequiv_pr1_contr {A} {P : A -> Type} + `{forall a, Contr (P a)} +: IsEquiv (@pr1 A P) | 100. +Proof. + refine (isequiv_adjointify (@pr1 A P) + (fun a => (a ; center (P a))) _ _). + - + intros a; reflexivity. + - + intros [a p]. + refine (path_sigma' P 1 (contr _)). +Defined. + +Definition path_sigma_hprop {A : Type} {P : A -> Type} + `{forall x, IsHProp (P x)} + (u v : sigT P) +: u.1 = v.1 -> u = v + := path_sigma_uncurried P u v o pr1^-1. + +End Sigma. + +End Types. + +End HoTT. + +End HoTT_DOT_Types_DOT_Sigma. +Module Export HoTT_DOT_Extensions. +Module Export HoTT. +Module Export Extensions. + +Section Extensions. + + Definition ExtensionAlong {A B : Type} (f : A -> B) + (P : B -> Type) (d : forall x:A, P (f x)) + := { s : forall y:B, P y & forall x:A, s (f x) = d x }. + + Fixpoint ExtendableAlong@{i j k l} + (n : nat) {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := match n with + | 0 => Unit@{l} + | S n => (forall (g : forall a, C (f a)), + ExtensionAlong@{i j k l l} f C g) * + forall (h k : forall b, C b), + ExtendableAlong n f (fun b => h b = k b) + end. + + Definition ooExtendableAlong@{i j k l} + {A : Type@{i}} {B : Type@{j}} + (f : A -> B) (C : B -> Type@{k}) : Type@{l} + := forall n, ExtendableAlong@{i j k l} n f C. + +End Extensions. + +End Extensions. + +End HoTT. + +End HoTT_DOT_Extensions. +Module Export HoTT. +Module Export Modalities. +Module Export ReflectiveSubuniverse. + +Module Type ReflectiveSubuniverses. + + Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + + let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In@{u a j} O U. + + Parameter hprop_inO@{u a i} + : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + IsHProp (In@{u a i} O T). + + Parameter extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). + +End ReflectiveSubuniverses. + +Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses). +Export Os. + +Module Export Coercions. + + Coercion O_reflector : ReflectiveSubuniverse >-> Funclass. + +End Coercions. + +End ReflectiveSubuniverses_Theory. + +Module Type ReflectiveSubuniverses_Restriction_Data (Os : ReflectiveSubuniverses). + + Parameter New_ReflectiveSubuniverse@{u a} : Type2@{u a}. + + Parameter ReflectiveSubuniverses_restriction@{u a} + : New_ReflectiveSubuniverse@{u a} -> Os.ReflectiveSubuniverse@{u a}. + +End ReflectiveSubuniverses_Restriction_Data. + +Module ReflectiveSubuniverses_Restriction + (Os : ReflectiveSubuniverses) + (Res : ReflectiveSubuniverses_Restriction_Data Os) +<: ReflectiveSubuniverses. + + Definition ReflectiveSubuniverse := Res.New_ReflectiveSubuniverse. + + Definition O_reflector@{u a i} (O : ReflectiveSubuniverse@{u a}) + := Os.O_reflector@{u a i} (Res.ReflectiveSubuniverses_restriction O). + Definition In@{u a i} (O : ReflectiveSubuniverse@{u a}) + := Os.In@{u a i} (Res.ReflectiveSubuniverses_restriction O). + Definition O_inO@{u a i} (O : ReflectiveSubuniverse@{u a}) + := Os.O_inO@{u a i} (Res.ReflectiveSubuniverses_restriction O). + Definition to@{u a i} (O : ReflectiveSubuniverse@{u a}) + := Os.to@{u a i} (Res.ReflectiveSubuniverses_restriction O). + Definition inO_equiv_inO@{u a i j k} (O : ReflectiveSubuniverse@{u a}) + := Os.inO_equiv_inO@{u a i j k} (Res.ReflectiveSubuniverses_restriction O). + Definition hprop_inO@{u a i} (H : Funext) (O : ReflectiveSubuniverse@{u a}) + := Os.hprop_inO@{u a i} H (Res.ReflectiveSubuniverses_restriction O). + Definition extendable_to_O@{u a i j k} (O : ReflectiveSubuniverse@{u a}) + := @Os.extendable_to_O@{u a i j k} (Res.ReflectiveSubuniverses_restriction@{u a} O). + +End ReflectiveSubuniverses_Restriction. + +Module ReflectiveSubuniverses_FamUnion + (Os1 Os2 : ReflectiveSubuniverses) +<: ReflectiveSubuniverses. + + Definition ReflectiveSubuniverse@{u a} : Type2@{u a} + := Os1.ReflectiveSubuniverse@{u a} + Os2.ReflectiveSubuniverse@{u a}. + + Definition O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. +admit. +Defined. + + Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a}. + Proof. + intros [O|O]; [ exact (Os1.In@{u a i} O) + | exact (Os2.In@{u a i} O) ]. + Defined. + + Definition O_inO@{u a i} + : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). +admit. +Defined. + + Definition to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + T -> O_reflector@{u a i} O T. +admit. +Defined. + + Definition inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + In@{u a j} O U. + Proof. + intros [O|O]; [ exact (Os1.inO_equiv_inO@{u a i j k} O) + | exact (Os2.inO_equiv_inO@{u a i j k} O) ]. + Defined. + + Definition hprop_inO@{u a i} + : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + IsHProp (In@{u a i} O T). +admit. +Defined. + + Definition extendable_to_O@{u a i j k} + : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q}, + ooExtendableAlong@{i i j k} (to O P) (fun _ => Q). +admit. +Defined. + +End ReflectiveSubuniverses_FamUnion. + +End ReflectiveSubuniverse. + +End Modalities. + +End HoTT. + +Module Type Modalities. + + Parameter Modality@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : Modality@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter In@{u a i} : forall (O : Modality@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter O_inO@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T). + + Parameter to@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter inO_equiv_inO@{u a i j k} : + forall (O : Modality@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + + let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In@{u a j} O U. + + Parameter hprop_inO@{u a i} + : Funext -> forall (O : Modality@{u a}) (T : Type@{i}), + IsHProp (In@{u a i} O T). + +End Modalities. + +Module Modalities_to_ReflectiveSubuniverses + (Os : Modalities) <: ReflectiveSubuniverses. + + Import Os. + + Fixpoint O_extendable@{u a i j k} (O : Modality@{u a}) + (A : Type@{i}) (B : O_reflector O A -> Type@{j}) + (B_inO : forall a, In@{u a j} O (B a)) (n : nat) + : ExtendableAlong@{i i j k} n (to O A) B. +admit. +Defined. + + Definition ReflectiveSubuniverse := Modality. + + Definition O_reflector := O_reflector. + + Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), + Type2le@{i a} -> Type2le@{i a} + := In@{u a i}. + Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + In@{u a i} O (O_reflector@{u a i} O T) + := O_inO@{u a i}. + Definition to := to. + Definition inO_equiv_inO@{u a i j k} : + forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) + (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), + In@{u a j} O U + := inO_equiv_inO@{u a i j k}. + Definition hprop_inO@{u a i} + : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), + IsHProp (In@{u a i} O T) + := hprop_inO@{u a i}. + + Definition extendable_to_O@{u a i j k} (O : ReflectiveSubuniverse@{u a}) + {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q} + : ooExtendableAlong@{i i j k} (to O P) (fun _ => Q) + := fun n => O_extendable O P (fun _ => Q) (fun _ => Q_inO) n. + +End Modalities_to_ReflectiveSubuniverses. + +Module Type EasyModalities. + + Parameter Modality@{u a} : Type2@{u a}. + + Parameter O_reflector@{u a i} : forall (O : Modality@{u a}), + Type2le@{i a} -> Type2le@{i a}. + + Parameter to@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}), + T -> O_reflector@{u a i} O T. + + Parameter minO_pathsO@{u a i} + : forall (O : Modality@{u a}) (A : Type@{i}) + (z z' : O_reflector@{u a i} O A), + IsEquiv (to@{u a i} O (z = z')). + +End EasyModalities. + +Module EasyModalities_to_Modalities (Os : EasyModalities) +<: Modalities. + + Import Os. + + Definition Modality := Modality. + + Definition O_reflector@{u a i} := O_reflector@{u a i}. + Definition to@{u a i} := to@{u a i}. + + Definition In@{u a i} + : forall (O : Modality@{u a}), Type@{i} -> Type@{i} + := fun O A => IsEquiv@{i i} (to O A). + + Definition hprop_inO@{u a i} `{Funext} (O : Modality@{u a}) + (T : Type@{i}) + : IsHProp (In@{u a i} O T). +admit. +Defined. + + Definition O_ind_internal@{u a i j k} (O : Modality@{u a}) + (A : Type@{i}) (B : O_reflector@{u a i} O A -> Type@{j}) + (B_inO : forall oa, In@{u a j} O (B oa)) + : let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + (forall a, B (to O A a)) -> forall oa, B oa. +admit. +Defined. + + Definition O_ind_beta_internal@{u a i j k} (O : Modality@{u a}) + (A : Type@{i}) (B : O_reflector@{u a i} O A -> Type@{j}) + (B_inO : forall oa, In@{u a j} O (B oa)) + (f : forall a : A, B (to O A a)) (a:A) + : O_ind_internal@{u a i j k} O A B B_inO f (to O A a) = f a. +admit. +Defined. + + Definition O_inO@{u a i} (O : Modality@{u a}) (A : Type@{i}) + : In@{u a i} O (O_reflector@{u a i} O A). +admit. +Defined. + + Definition inO_equiv_inO@{u a i j k} (O : Modality@{u a}) (A : Type@{i}) (B : Type@{j}) + (A_inO : In@{u a i} O A) (f : A -> B) (feq : IsEquiv f) + : In@{u a j} O B. + Proof. + simple refine (isequiv_commsq (to O A) (to O B) f + (O_ind_internal O A (fun _ => O_reflector O B) _ (fun a => to O B (f a))) _). + - + intros; apply O_inO. + - + intros a; refine (O_ind_beta_internal@{u a i j k} O A (fun _ => O_reflector O B) _ _ a). + - + apply A_inO. + - + simple refine (isequiv_adjointify _ + (O_ind_internal O B (fun _ => O_reflector O A) _ (fun b => to O A (f^-1 b))) _ _); + intros x. + + + apply O_inO. + + + pattern x; refine (O_ind_internal O B _ _ _ x); intros. + * + apply minO_pathsO. + * + simpl; admit. + + + pattern x; refine (O_ind_internal O A _ _ _ x); intros. + * + apply minO_pathsO. + * + simpl; admit. + Defined. + +End EasyModalities_to_Modalities. + +Module Modalities_Theory (Os : Modalities). + +Export Os. +Module Export Os_ReflectiveSubuniverses + := Modalities_to_ReflectiveSubuniverses Os. +Module Export RSU + := ReflectiveSubuniverses_Theory Os_ReflectiveSubuniverses. + +Module Export Coercions. + Coercion modality_to_reflective_subuniverse + := idmap : Modality -> ReflectiveSubuniverse. +End Coercions. + +Class IsConnected (O : Modality@{u a}) (A : Type@{i}) + + := isconnected_contr_O : IsTrunc@{i} -2 (O A). + +Class IsConnMap (O : Modality@{u a}) + {A : Type@{i}} {B : Type@{j}} (f : A -> B) + := isconnected_hfiber_conn_map + + : forall b:B, IsConnected@{u a k} O (hfiber@{i j} f b). + +End Modalities_Theory. + +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 Truncation_Modality := trunc_index. + +Module Truncation_Modalities <: Modalities. + + Definition Modality : Type2@{u a} := Truncation_Modality. + + Definition O_reflector (n : Modality@{u u'}) A := Trunc n A. + + Definition In (n : Modality@{u u'}) A := IsTrunc n A. + + Definition O_inO (n : Modality@{u u'}) A : In n (O_reflector n A). +admit. +Defined. + + Definition to (n : Modality@{u u'}) A := @tr n A. + + Definition inO_equiv_inO (n : Modality@{u u'}) + (A : Type@{i}) (B : Type@{j}) Atr f feq + : let gei := ((fun x => x) : Type@{i} -> Type@{k}) in + let gej := ((fun x => x) : Type@{j} -> Type@{k}) in + In n B + := @trunc_equiv A B f n Atr feq. + + Definition hprop_inO `{Funext} (n : Modality@{u u'}) A + : IsHProp (In n A). +admit. +Defined. + +End Truncation_Modalities. + +Module Import TrM := Modalities_Theory Truncation_Modalities. + +Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A). + +Notation IsSurjection := (IsConnMap -1). + +Definition BuildIsSurjection {A B} (f : A -> B) : + (forall b, merely (hfiber f b)) -> IsSurjection f. +admit. +Defined. + +Ltac strip_truncations := + + progress repeat match goal with + | [ T : _ |- _ ] + => revert_opaque T; + refine (@Trunc_ind _ _ _ _ _); + + []; + intro T + end. +Local Open Scope trunc_scope. + +Global Instance conn_pointed_type {n : trunc_index} {A : Type} (a0:A) + `{IsConnMap n _ _ (unit_name a0)} : IsConnected n.+1 A | 1000. +admit. +Defined. + +Definition loops (A : pType) : pType := + Build_pType (point A = point A) idpath. + +Record pMap (A B : pType) := + { pointed_fun : A -> B ; + point_eq : pointed_fun (point A) = point B }. + +Arguments point_eq {A B} f : rename. +Coercion pointed_fun : pMap >-> Funclass. + +Infix "->*" := pMap (at level 99) : pointed_scope. +Local Open Scope pointed_scope. + +Definition pmap_compose {A B C : pType} + (g : B ->* C) (f : A ->* B) +: A ->* C + := Build_pMap A C (g o f) + (ap g (point_eq f) @ point_eq g). + +Record pHomotopy {A B : pType} (f g : pMap A B) := + { pointed_htpy : f == g ; + point_htpy : pointed_htpy (point A) @ point_eq g = point_eq f }. +Arguments pointed_htpy {A B f g} p x. + +Infix "==*" := pHomotopy (at level 70, no associativity) : pointed_scope. + +Definition loops_functor {A B : pType} (f : A ->* B) +: (loops A) ->* (loops B). +Proof. + refine (Build_pMap (loops A) (loops B) + (fun p => (point_eq f)^ @ (ap f p @ point_eq f)) _). + apply moveR_Vp; simpl. + refine (concat_1p _ @ (concat_p1 _)^). +Defined. + +Definition loops_functor_compose {A B C : pType} + (g : B ->* C) (f : A ->* B) +: (loops_functor (pmap_compose g f)) + ==* (pmap_compose (loops_functor g) (loops_functor f)). +admit. +Defined. + +Local Open Scope path_scope. + +Record ooGroup := + { classifying_space : pType@{i} ; + isconn_classifying_space : IsConnected@{u a i} 0 classifying_space + }. + +Local Notation B := classifying_space. + +Definition group_type (G : ooGroup) : Type + := point (B G) = point (B G). + +Coercion group_type : ooGroup >-> Sortclass. + +Definition group_loops (X : pType) +: ooGroup. +Proof. + + pose (x0 := point X); + pose (BG := (Build_pType + { x:X & merely (x = point X) } + (existT (fun x:X => merely (x = point X)) x0 (tr 1)))). + + cut (IsConnected 0 BG). + { + exact (Build_ooGroup BG). +} + cut (IsSurjection (unit_name (point BG))). + { + intros; refine (conn_pointed_type (point _)). +} + apply BuildIsSurjection; simpl; intros [x p]. + strip_truncations; apply tr; exists tt. + apply path_sigma_hprop; simpl. + exact (p^). +Defined. + +Definition loops_group (X : pType) +: loops X <~> group_loops X. +admit. +Defined. + +Definition ooGroupHom (G H : ooGroup) + := pMap (B G) (B H). + +Definition grouphom_fun {G H} (phi : ooGroupHom G H) : G -> H + := loops_functor phi. + +Coercion grouphom_fun : ooGroupHom >-> Funclass. + +Definition group_loops_functor + {X Y : pType} (f : pMap X Y) +: ooGroupHom (group_loops X) (group_loops Y). +Proof. + simple refine (Build_pMap _ _ _ _); simpl. + - + intros [x p]. + exists (f x). + strip_truncations; apply tr. + exact (ap f p @ point_eq f). + - + apply path_sigma_hprop; simpl. + apply point_eq. +Defined. + +Definition loops_functor_group + {X Y : pType} (f : pMap X Y) +: loops_functor (group_loops_functor f) o loops_group X + == loops_group Y o loops_functor f. +admit. +Defined. + +Definition grouphom_compose {G H K : ooGroup} + (psi : ooGroupHom H K) (phi : ooGroupHom G H) +: ooGroupHom G K + := pmap_compose psi phi. + +Definition group_loops_functor_compose + {X Y Z : pType} + (psi : pMap Y Z) (phi : pMap X Y) +: grouphom_compose (group_loops_functor psi) (group_loops_functor phi) + == group_loops_functor (pmap_compose psi phi). +Proof. + intros g. + unfold grouphom_fun, grouphom_compose. + refine (pointed_htpy (loops_functor_compose _ _) g @ _). + pose (p := eisretr (loops_group X) g). + change (loops_functor (group_loops_functor psi) + (loops_functor (group_loops_functor phi) g) + = loops_functor (group_loops_functor + (pmap_compose psi phi)) g). + rewrite <- p. + Fail Timeout 1 Time rewrite !loops_functor_group. + (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *) + Timeout 1 do 3 rewrite loops_functor_group. +Abort.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4574.v b/test-suite/bugs/closed/4574.v new file mode 100644 index 0000000000..39ba190369 --- /dev/null +++ b/test-suite/bugs/closed/4574.v @@ -0,0 +1,8 @@ +Require Import Setoid. + +Definition block A (a : A) := a. + +Goal forall A (a : A), block Type nat. +Proof. +Fail reflexivity. + diff --git a/test-suite/bugs/closed/4580.v b/test-suite/bugs/closed/4580.v new file mode 100644 index 0000000000..4ffd5f0f4b --- /dev/null +++ b/test-suite/bugs/closed/4580.v @@ -0,0 +1,6 @@ +Require Import Program. + +Class Foo (A : Type) := foo : A. + +Unset Refine Instance Mode. +Program Instance f1 : Foo nat := S _. diff --git a/test-suite/bugs/closed/4582.v b/test-suite/bugs/closed/4582.v new file mode 100644 index 0000000000..0842fb8fa7 --- /dev/null +++ b/test-suite/bugs/closed/4582.v @@ -0,0 +1,10 @@ +Require List. +Import List.ListNotations. + +Variable Foo : nat -> nat. + +Delimit Scope Foo_scope with F. + +Notation " [ x ] " := (Foo x) : Foo_scope. + +Check ([1] : nat)%F. diff --git a/test-suite/bugs/closed/4588.v b/test-suite/bugs/closed/4588.v new file mode 100644 index 0000000000..ff66277e03 --- /dev/null +++ b/test-suite/bugs/closed/4588.v @@ -0,0 +1,10 @@ +Set Primitive Projections. + +(* This proof was accepted in Coq 8.5 because the subterm specs were not +projected correctly *) +Inductive foo : Prop := mkfoo { proj1 : False -> foo; proj2 : (forall P : Prop, P -> P) }. + +Fail Fixpoint loop (x : foo) : False := + loop (proj2 x _ x). + +Fail Definition bad : False := loop (mkfoo (fun x => match x with end) (fun _ x => x)). diff --git a/test-suite/bugs/closed/4596.v b/test-suite/bugs/closed/4596.v new file mode 100644 index 0000000000..592fdb6580 --- /dev/null +++ b/test-suite/bugs/closed/4596.v @@ -0,0 +1,14 @@ +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. + +Definition T (x : bool) := x = true. + +Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat) + (s : forall n : nat, bool) + (s0 s1 : nat -> S -> S), + (forall (str0 : S) (n m : nat), + (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) -> + T (b str0 m)) -> + T (b str p). +Proof. +intros ???????? H0. +rewrite H0. diff --git a/test-suite/bugs/closed/4627.v b/test-suite/bugs/closed/4627.v new file mode 100644 index 0000000000..e1206bb37a --- /dev/null +++ b/test-suite/bugs/closed/4627.v @@ -0,0 +1,49 @@ +Class sa (A:Type) := { }. + +Record predicate A (sa:sa A) := + { pred_fun: A->Prop }. +Record ABC : Type := + { abc: Type }. +Record T := + { T_abc: ABC }. + + +(* +sa: forall _ : Type@{Top.179}, Prop +predicate: forall (A : Type@{Top.205}) (_ : sa A), Type@{max(Set+1, Top.205)} +T: Type@{Top.208+1} +ABC: Type@{Top.208+1} +abc: forall _ : ABC, Type@{Top.208} + +Top.205 <= Top.179 predicate <= sa.A +Set < Top.208 Set < abc +Set < Top.205 Set < predicate +*) + +Definition foo : predicate T (Build_sa T) := + {| pred_fun:= fun w => True |}. +(* *) +(* Top.208 < Top.205 <--- added by foo *) +(* *) + +Check predicate nat (Build_sa nat). +(* + +The issue is that the template polymorphic universe of [predicate], Top.205, does not get replaced with the universe of [nat] in the above line. + -Jason Gross + +8.5 -- predicate nat (Build_sa nat): Type@{max(Set+1, Top.205)} +8.5 EXPECTED -- predicate nat (Build_sa nat): Type@{Set+1} +8.4pl4 -- predicate nat {| |}: Type (* max(Set, (Set)+1) *) +*) + +(* This works in 8.4pl4 and SHOULD work in 8.5 *) +Definition bar : ABC := + {| abc:= predicate nat (Build_sa nat) |}. +(* +The term "predicate nat (Build_sa nat)" has type + "Type@{max(Set+1, Top.205)}" +while it is expected to have type "Type@{Top.208}" +(universe inconsistency: Cannot enforce Top.205 <= +Top.208 because Top.208 < Top.205). +*)
\ No newline at end of file diff --git a/test-suite/bugs/closed/931.v b/test-suite/bugs/closed/931.v index e86b3be64e..ea3347a851 100644 --- a/test-suite/bugs/closed/931.v +++ b/test-suite/bugs/closed/931.v @@ -2,6 +2,6 @@ Parameter P : forall n : nat, n=n -> Prop. Goal Prop. refine (P _ _). - 2:instantiate (1:=0). + instantiate (1:=0). trivial. Qed. diff --git a/test-suite/bugs/closed/HoTT_coq_002.v b/test-suite/bugs/closed/HoTT_coq_002.v index ba69f6b158..dba4d5998f 100644 --- a/test-suite/bugs/closed/HoTT_coq_002.v +++ b/test-suite/bugs/closed/HoTT_coq_002.v @@ -9,7 +9,7 @@ Section SpecializedFunctor. (* Variable objC : Type. *) Context `(C : SpecializedCategory objC). - Polymorphic Record SpecializedFunctor := { + Record SpecializedFunctor := { ObjectOf' : objC -> Type; ObjectC : Object C }. diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v index ae3e50d7ee..223a98de1c 100644 --- a/test-suite/bugs/closed/HoTT_coq_014.v +++ b/test-suite/bugs/closed/HoTT_coq_014.v @@ -3,9 +3,9 @@ Set Implicit Arguments. Generalizable All Variables. Set Universe Polymorphism. -Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' { - Object :> _ := obj; - Morphism' : obj -> obj -> Type; +Polymorphic Record SpecializedCategory@{l k} (obj : Type@{l}) := Build_SpecializedCategory' { + Object :> Type@{l} := obj; + Morphism' : obj -> obj -> Type@{k}; Identity' : forall o, Morphism' o o; Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d' diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v index 4938b80f9b..008fb72c4e 100644 --- a/test-suite/bugs/closed/HoTT_coq_020.v +++ b/test-suite/bugs/closed/HoTT_coq_020.v @@ -59,8 +59,8 @@ Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C := Build_Functor Cat0 C (fun x => match x with end). Section Law0. - Variable objC : Type. - Variable C : Category objC. + Polymorphic Variable objC : Type. + Polymorphic Variable C : Category objC. Set Printing All. Set Printing Universes. diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index db3b60edae..017780c1f3 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -30,7 +30,7 @@ Definition prod_rect' A B (P : prod A B -> Type) (u : forall (fst : A) (snd : B) (p : prod A B) : P p := u (fst p) (snd p). -Notation typeof x := ($(let T := type of x in exact T)$) (only parsing). +Notation typeof x := (ltac:(let T := type of x in exact T)) (only parsing). (* Check for eta *) Check eq_refl : typeof (@prod_rect) = typeof (@prod_rect'). diff --git a/test-suite/bugs/closed/HoTT_coq_090.v b/test-suite/bugs/closed/HoTT_coq_090.v index 5fa167038d..d77b9b63a2 100644 --- a/test-suite/bugs/closed/HoTT_coq_090.v +++ b/test-suite/bugs/closed/HoTT_coq_090.v @@ -84,7 +84,7 @@ Arguments transport {A} P {x y} p%path_scope u : simpl nomatch. Instance isequiv_path {A B : Type} (p : A = B) : IsEquiv (transport (fun X:Type => X) p) | 0. Proof. - refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _); + unshelve refine (@BuildIsEquiv _ _ _ (transport (fun X:Type => X) p^) _ _ _); admit. Defined. diff --git a/test-suite/bugs/closed/HoTT_coq_114.v b/test-suite/bugs/closed/HoTT_coq_114.v index 341128338e..3535e6c41f 100644 --- a/test-suite/bugs/closed/HoTT_coq_114.v +++ b/test-suite/bugs/closed/HoTT_coq_114.v @@ -1 +1 @@ -Inductive test : $(let U := type of Type in exact U)$ := t. +Inductive test : ltac:(let U := type of Type in exact U) := t. diff --git a/test-suite/bugs/opened/3248.v b/test-suite/bugs/opened/3248.v index 9e7d1eb5dd..33c408a28c 100644 --- a/test-suite/bugs/opened/3248.v +++ b/test-suite/bugs/opened/3248.v @@ -3,7 +3,7 @@ Ltac ret_and_left f := let T := type of f in lazymatch eval hnf in T with | ?T' -> _ => - let ret := constr:(fun x' : T' => $(tac (f x'))$) in + let ret := constr:(fun x' : T' => ltac:(tac (f x'))) in exact ret | ?T' => exact f end. @@ -12,6 +12,6 @@ Goal forall A B : Prop, forall x y : A, True. Proof. intros A B x y. pose (f := fun (x y : A) => conj x y). - pose (a := $(ret_and_left f)$). + pose (a := ltac:(ret_and_left f)). Fail unify (a x y) (conj x y). Abort. diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v index 19ed787d1e..5f4231363a 100644 --- a/test-suite/bugs/opened/3277.v +++ b/test-suite/bugs/opened/3277.v @@ -4,4 +4,4 @@ Goal True. evarr _. Admitted. Goal True. - Fail exact $(evarr _)$. (* Error: Cannot infer this placeholder. *) + Fail exact ltac:(evarr _). (* Error: Cannot infer this placeholder. *) diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v index ced535afd5..1c6deae94b 100644 --- a/test-suite/bugs/opened/3278.v +++ b/test-suite/bugs/opened/3278.v @@ -1,8 +1,8 @@ Module a. Check let x' := _ in - $(exact x')$. + ltac:(exact x'). - Notation foo x := (let x' := x in $(exact x')$). + Notation foo x := (let x' := x in ltac:(exact x')). Fail Check foo _. (* Error: Cannot infer an internal placeholder of type "Type" in environment: @@ -12,10 +12,10 @@ x' := ?42 : ?41 End a. Module b. - Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I). + Notation foo x := (let x' := x in let y := (ltac:(exact I) : True) in I). Notation bar x := (let x' := x in let y := (I : True) in I). - Check let x' := _ in $(exact I)$. (* let x' := ?5 in I *) + Check let x' := _ in ltac:(exact I). (* let x' := ?5 in I *) Check bar _. (* let x' := ?9 in let y := I in I *) Fail Check foo _. (* Error: Cannot infer an internal placeholder of type "Type" in environment: diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v index 529cc737df..66668930c7 100644 --- a/test-suite/bugs/opened/3304.v +++ b/test-suite/bugs/opened/3304.v @@ -1,3 +1,3 @@ -Fail Notation "( x , y , .. , z )" := $(let r := constr:(prod .. (prod x y) .. z) in r)$. +Fail Notation "( x , y , .. , z )" := ltac:(let r := constr:(prod .. (prod x y) .. z) in r). (* The command has indeed failed with message: => Error: Special token .. is for use in the Notation command. *) 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/3459.v b/test-suite/bugs/opened/3459.v index 9e6107b30a..762611f751 100644 --- a/test-suite/bugs/opened/3459.v +++ b/test-suite/bugs/opened/3459.v @@ -7,9 +7,9 @@ Proof. (* This line used to fail with a Not_found up to some point, and then to produce an ill-typed term *) match goal with - | [ |- context G[2] ] => let y := constr:(fun x => $(let r := constr:(@eq Set x x) in + | [ |- context G[2] ] => let y := constr:(fun x => ltac:(let r := constr:(@eq Set x x) in clear x; - exact r)$) in + exact r)) in pose y end. (* Add extra test for typability (should not fail when bug closed) *) diff --git a/test-suite/bugs/opened/3554.v b/test-suite/bugs/opened/3554.v deleted file mode 100644 index 422c5770ea..0000000000 --- a/test-suite/bugs/opened/3554.v +++ /dev/null @@ -1 +0,0 @@ -Fail Example foo (f : forall {_ : Type}, Type) : Type. diff --git a/test-suite/complexity/f_equal.v b/test-suite/complexity/f_equal.v new file mode 100644 index 0000000000..86698fa872 --- /dev/null +++ b/test-suite/complexity/f_equal.v @@ -0,0 +1,14 @@ +(* Checks that f_equal does not reduce the term uselessly *) +(* Expected time < 1.00s *) + +Fixpoint stupid (n : nat) : unit := +match n with +| 0 => tt +| S n => + let () := stupid n in + let () := stupid n in + tt +end. + +Goal stupid 23 = stupid 23. +Timeout 5 Time f_equal. 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/Tauto.v b/test-suite/failure/Tauto.v index 749db00027..d91d159d9c 100644 --- a/test-suite/failure/Tauto.v +++ b/test-suite/failure/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v index 8e34ffbdab..b3fbff680b 100644 --- a/test-suite/failure/clash_cons.v +++ b/test-suite/failure/clash_cons.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v index 7b52316ed1..c2b521c214 100644 --- a/test-suite/failure/fixpoint1.v +++ b/test-suite/failure/fixpoint1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index b3a0a33562..8db2785837 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v index 7e4c5ac57b..8ed3af1ce4 100644 --- a/test-suite/failure/illtype1.v +++ b/test-suite/failure/illtype1.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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 30762a77f3..8089de2bf0 100644 --- a/test-suite/failure/positivity.v +++ b/test-suite/failure/positivity.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v index e5db81768a..c8dc6303f7 100644 --- a/test-suite/failure/redef.v +++ b/test-suite/failure/redef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v index a6e6bc4891..648ab0820c 100644 --- a/test-suite/failure/search.v +++ b/test-suite/failure/search.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v index ed46eb2298..c8e9af216e 100644 --- a/test-suite/ideal-features/Apply.v +++ b/test-suite/ideal-features/Apply.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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/misc/berardi_test.v b/test-suite/misc/berardi_test.v index 219686b959..a64db4dab7 100644 --- a/test-suite/misc/berardi_test.v +++ b/test-suite/misc/berardi_test.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) 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/Existentials.out b/test-suite/output/Existentials.out index 483a9ea792..9680d2bbff 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,5 +1,4 @@ -Existential 1 = -?Goal0 : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] Existential 2 = ?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) -Existential 3 = ?e : [q : nat n : nat m : nat |- n = ?y] +Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out index 848abd0096..f738b0d091 100644 --- a/test-suite/output/Extraction_matchs_2413.out +++ b/test-suite/output/Extraction_matchs_2413.out @@ -4,7 +4,7 @@ let test1 b = b (** val test2 : bool -> bool **) -let test2 b = +let test2 _ = False (** val wrong_id : 'a1 hole -> 'a2 hole **) diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index b1558dab1c..26eaca8272 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -111,14 +111,14 @@ fun x : option Z => match x with | NONE2 => 0 end : option Z -> Z -fun x : list ?T1 => match x with - | NIL => NONE2 - | (_ :') t => SOME2 t - end - : list ?T1 -> option (list ?T1) +fun x : list ?T => match x with + | NIL => NONE2 + | (_ :') t => SOME2 t + end + : list ?T -> option (list ?T) where -?T1 : [x : list ?T1 x1 : list ?T1 x0 := x1 : list ?T1 |- Type] (x, x1, - x0 cannot be used) +?T : [x : list ?T x1 : list ?T x0 := x1 : list ?T |- Type] (x, x1, + x0 cannot be used) s : s 10 diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index f2d1447785..576fbd7c0b 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,13 +6,13 @@ 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 |- ?T0 -> T n] -?y0 : [n : nat x := A n : T n |- ?T0] +?y : [n : nat x := A n : T n |- ?T -> T n] +?y0 : [n : nat x := A n : T n |- ?T] fun n : nat => ?y ?y0 : T n : forall n : nat, T n where -?y : [n : nat |- ?T0 -> T n] -?y0 : [n : nat |- ?T0] +?y : [n : nat |- ?T -> T n] +?y0 : [n : nat |- ?T] 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/Case22.v b/test-suite/success/Case22.v index ce9050d421..3c696502cd 100644 --- a/test-suite/success/Case22.v +++ b/test-suite/success/Case22.v @@ -17,3 +17,47 @@ Definition foo (x : I') : bool := match x with C' => true end. + +(* Bug found in november 2015: was wrongly failing in 8.5beta2 and 8.5beta3 *) + +Inductive I2 (A:Type) : let B:=A in forall C, let D:=(C*B)%type in Type := + E2 : I2 A nat. + +Check fun x:I2 nat nat => match x in I2 _ X Y Z return X*Y*Z with + E2 _ => (0,0,(0,0)) + end. + +(* This used to succeed in 8.3, 8.4 and 8.5beta1 *) + +Inductive IND : forall X:Type, let Y:=X in Type := + CONSTR : IND True. + +Definition F (x:IND True) (A:Type) := + (* This failed in 8.5beta2 though it should have been accepted *) + match x in IND X Y return Y with + CONSTR => Logic.I + end. + +Theorem paradox : False. + (* This succeeded in 8.3, 8.4 and 8.5beta1 because F had wrong type *) +Fail Proof (F C False). + +(* Another bug found in November 2015 (a substitution was wrongly + reversed at pretyping level) *) + +Inductive Ind (A:Type) : + let X:=A in forall Y:Type, let Z:=(X*Y)%type in Type := + Constr : Ind A nat. + +Check fun x:Ind bool nat => + match x in Ind _ X Y Z return Z with + | Constr _ => (true,0) + end. + +(* A vm_compute bug (the type of constructors was not supposed to + contain local definitions before proper parameters) *) + +Inductive Ind2 (b:=1) (c:nat) : Type := + Constr2 : Ind2 c. + +Eval vm_compute in Constr2 2. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index e42663505d..49c465b6c6 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1861,3 +1861,10 @@ Type (fun n => match n with Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y := match p with eq_refl => u end. + +(* Check in-pattern clauses with constant constructors, which were + previously interpreted as variables (before 8.5) *) + +Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end. + +Check match niln in listn O return O=O with niln => eq_refl end. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 87c38cfa06..e4ee351c3a 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 8db08b6d78..438e461357 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index cc8cec4707..f934a5c74a 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -62,3 +62,47 @@ Axiom cast_coalesce : ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2). Hint Rewrite cast_coalesce : ltamer. + +Require Import Program. +Module HintCut. +Class A (f : nat -> nat) := a : True. +Class B (f : nat -> nat) := b : True. +Class C (f : nat -> nat) := c : True. +Class D (f : nat -> nat) := d : True. +Class E (f : nat -> nat) := e : True. + +Instance a_is_b f : A f -> B f. +Proof. easy. Qed. +Instance b_is_c f : B f -> C f. +Proof. easy. Qed. +Instance c_is_d f : C f -> D f. +Proof. easy. Qed. +Instance d_is_e f : D f -> E f. +Proof. easy. Qed. + +Instance a_compose f g : A f -> A g -> A (compose f g). +Proof. easy. Qed. +Instance b_compose f g : B f -> B g -> B (compose f g). +Proof. easy. Qed. +Instance c_compose f g : C f -> C g -> C (compose f g). +Proof. easy. Qed. +Instance d_compose f g : D f -> D g -> D (compose f g). +Proof. easy. Qed. +Instance e_compose f g : E f -> E g -> E (compose f g). +Proof. easy. Qed. + +Instance a_id : A id. +Proof. easy. Qed. + +Instance foo f : + E (id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ + id ∘ id ∘ id ∘ id ∘ id ∘ f ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id ∘ id). +Proof. + Fail Timeout 1 apply _. (* 3.7s *) + +Hint Cut [!*; (a_is_b | b_is_c | c_is_d | d_is_e) ; + (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. + + Timeout 1 Fail apply _. (* 0.06s *) +Abort. +End HintCut.
\ No newline at end of file diff --git a/test-suite/success/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/Notations.v b/test-suite/success/Notations.v index 2371d32cda..b72a067407 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -101,3 +101,9 @@ Fail Check fun x => match x with S (FORALL x, _) => 0 end. Parameter traverse : (nat -> unit) -> (nat -> unit). Notation traverse_var f l := (traverse (fun l => f l) l). + +(* Check that when an ident become a keyword, it does not break + previous rules relying on the string to be classified as an ident *) + +Notation "'intros' x" := (S x) (at level 0). +Goal True -> True. intros H. exact H. Qed. 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/Tauto.v b/test-suite/success/Tauto.v index 01d9afb426..767f15be72 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 3090f40cde..c8a8b862fa 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 55b666b723..02e043bc36 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -543,7 +543,7 @@ Qed. Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a): exists x, exists y, X x y. Proof. -intros; eexists; eexists; case H. +intros; eexists; eexists ?[y]; case H. apply (foo ?y). Grab Existential Variables. exact 0. diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v index aaa7b3a514..5477c83316 100644 --- a/test-suite/success/auto.v +++ b/test-suite/success/auto.v @@ -45,3 +45,92 @@ Proof. eexists. Fail progress debug eauto with test2. progress eauto with test. Qed. + +(** Patterns of Extern have a "matching" semantics. + It is not so for apply/exact hints *) + +Class B (A : Type). +Class I. +Instance i : I. + +Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y. +Class D (f : nat -> nat -> nat). +Definition ftest (x y : nat) := x + y. +Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f). + Admitted. +Module Instnopat. + Local Instance: B nat. + (* pattern_of_constr -> B nat *) + (* exact hint *) + Check (_ : B nat). + (* map_eauto -> B_instance0 *) + (* NO Constr_matching.matches !!! *) + Check (_ : B _). + + Goal exists T, B T. + eexists. + eauto with typeclass_instances. + Qed. + + Local Instance: D ftest. + Local Hint Resolve flipD | 0 : typeclass_instances. + (* pattern: D (flip _) *) + Fail Timeout 1 Check (_ : D _). (* loops applying flipD *) + +End Instnopat. + +Module InstnopatApply. + Local Instance: I -> B nat. + (* pattern_of_constr -> B nat *) + (* apply hint *) + Check (_ : B nat). + (* map_eauto -> B_instance0 *) + (* NO Constr_matching.matches !!! *) + Check (_ : B _). + + Goal exists T, B T. + eexists. + eauto with typeclass_instances. + Qed. +End InstnopatApply. + +Module InstPat. + Hint Extern 3 (B nat) => split : typeclass_instances. + (* map_eauto -> Extern hint *) + (* Constr_matching.matches -> true *) + Check (_ : B nat). + (* map_eauto -> Extern hint *) + (* Constr_matching.matches -> false: + Because an inductive in the pattern does not match an evar in the goal *) + Check (_ : B _). + + Goal exists T, B T. + eexists. + (* map_existential -> Extern hint *) + (* Constr_matching.matches -> false *) + Fail progress eauto with typeclass_instances. + (* map_eauto -> Extern hint *) + (* Constr_matching.matches -> false *) + Fail typeclasses eauto. + Abort. + + Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances. + Module withftest. + Local Instance: D ftest. + + Check (_ : D _). + (* D_instance_0 : D ftest *) + Check (_ : D (flip _)). + (* ... : D (flip ftest) *) + End withftest. + Module withoutftest. + Hint Extern 0 (D ftest) => split : typeclass_instances. + Check (_ : D _). + (* ? : D ?, _not_ looping *) + Check (_ : D (flip _)). + (* ? : D (flip ?), _not_ looping *) + + Check (_ : D (flip ftest)). + (* flipD ftest {| |} : D (flip ftest) *) + End withoutftest. +End InstPat. 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/destruct.v b/test-suite/success/destruct.v index 83a33f75dc..90a60daa66 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -96,19 +96,21 @@ Abort. (* Check that subterm selection does not solve existing evars *) Goal exists x, S x = S 0. -eexists. +eexists ?[x]. +Show x. (* Incidentally test Show on a named goal *) destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S 0). Abort. Goal exists x, S 0 = S x. -eexists. +eexists ?[x]. destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S ?x). +[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *) Abort. Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. -do 2 eexists. +eexists ?[n]; eexists ?[p]. destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *) change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n). Abort. @@ -387,7 +389,7 @@ Abort. Goal forall b:bool, True. intro b. -destruct !b. +destruct (b). clear b. (* b has to be here *) Abort. @@ -424,7 +426,7 @@ destruct b eqn:H. (* Check natural instantiation behavior when the goal has already an evar *) Goal exists x, S x = x. -eexists. +eexists ?[x]. destruct (S _). change (0 = ?x). Abort. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 9e57801e06..773dd321eb 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 1b5c7f183e..1f6af0dc44 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 57f3775d7e..0086e090bd 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v new file mode 100644 index 0000000000..dfdeff82ff --- /dev/null +++ b/test-suite/success/extraction_impl.v @@ -0,0 +1,82 @@ + +(** Examples of extraction with manually-declared implicit arguments *) + +(** NB: we should someday check the produced code instead of + simply running the commands. *) + +(** Bug #4243, part 1 *) + +Inductive dnat : nat -> Type := +| d0 : dnat 0 +| ds : forall n m, n = m -> dnat n -> dnat (S n). + +Extraction Implicit ds [m]. + +Lemma dnat_nat: forall n, dnat n -> nat. +Proof. + intros n d. + induction d as [| n m Heq d IHn]. + exact 0. exact (S IHn). +Defined. + +Recursive Extraction dnat_nat. + +Extraction Implicit dnat_nat [n]. +Recursive Extraction dnat_nat. + +(** Same, with a Fixpoint *) + +Fixpoint dnat_nat' n (d:dnat n) := + match d with + | d0 => 0 + | ds n m _ d => S (dnat_nat' n d) + end. + +Recursive Extraction dnat_nat'. + +Extraction Implicit dnat_nat' [n]. +Recursive Extraction dnat_nat'. + +(** Bug #4243, part 2 *) + +Inductive enat: nat -> Type := + e0: enat 0 +| es: forall n, enat n -> enat (S n). + +Lemma enat_nat: forall n, enat n -> nat. +Proof. + intros n e. + induction e as [| n e IHe]. + exact (O). + exact (S IHe). +Defined. + +Extraction Implicit es [n]. +Extraction Implicit enat_nat [n]. +Recursive Extraction enat_nat. + +(** Same, with a Fixpoint *) + +Fixpoint enat_nat' n (e:enat n) : nat := + match e with + | e0 => 0 + | es n e => S (enat_nat' n e) + end. + +Extraction Implicit enat_nat' [n]. +Recursive Extraction enat_nat'. + +(** Bug #4228 *) + +Module Food. +Inductive Course := +| main: nat -> Course +| dessert: nat -> Course. + +Inductive Meal : Course -> Type := +| one_course : forall n:nat, Meal (main n) +| two_course : forall n m, Meal (main n) -> Meal (dessert m). +Extraction Implicit two_course [n]. +End Food. + +Recursive Extraction Food.Meal. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index b733aef6db..c729b23ce7 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 7ae60d9892..1ed731f50f 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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 35ba94fb67..ee69df9774 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -34,38 +34,97 @@ intros _ ?. exact H. Qed. -(* A short test about introduction pattern pat/c *) +(* A short test about introduction pattern pat%c *) Goal (True -> 0=0) -> True /\ False -> 0=0. -intros H (H1/H,_). +intros H (H1%H,_). exact H1. Qed. (* A test about bugs in 8.5beta2 *) Goal (True -> 0=0) -> True /\ False -> False -> 0=0. intros H H0 H1. -destruct H0 as (a/H,_). +destruct H0 as (a%H,_). (* Check that H0 is removed (was bugged in 8.5beta2) *) Fail clear H0. -(* Check position of newly created hypotheses when using pat/c (was +(* Check position of newly created hypotheses when using pat%c (was left at top in 8.5beta2) *) match goal with H:_ |- _ => clear H end. (* clear H1:False *) match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *) Qed. Goal (True -> 0=0) -> True -> 0=0. -intros H H1/H. +intros H H1%H. exact H1. Qed. Goal forall n, n = S n -> 0=0. -intros n H/n_Sn. +intros n H%n_Sn. destruct H. Qed. (* Another check about generated names and cleared hypotheses with - pat/c patterns *) + pat%c patterns *) Goal (True -> 0=0 /\ 1=1) -> True -> 0=0. -intros H (H1,?)/H. +intros H (H1,?)%H. change (1=1) in H0. exact H1. Qed. + +(* Checking iterated pat%c1...%cn introduction patterns and side conditions *) + +Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D. +intros * H H0 H1. +intros H2%H%H0. +- exact H2. +- exact H1. +Qed. + +(* Bug found by Enrico *) + +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/keyedrewrite.v b/test-suite/success/keyedrewrite.v index bbe9d4bfff..b88c142be1 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -22,3 +22,41 @@ Qed. Print Equivalent Keys. End foo. + +Require Import Arith List Omega. + +Definition G {A} (f : A -> A -> A) (x : A) := f x x. + +Lemma list_foo A (l : list A) : G (@app A) (l ++ nil) = G (@app A) l. +Proof. unfold G; rewrite app_nil_r; reflexivity. Qed. + +(* Bundled version of a magma *) +Structure magma := Magma { b_car :> Type; op : b_car -> b_car -> b_car }. +Arguments op {_} _ _. + +(* Instance for lists *) +Canonical Structure list_magma A := Magma (list A) (@app A). + +(* Basically like list_foo, but now uses the op projection instead of app for +the argument of G *) +Lemma test1 A (l : list A) : G op (l ++ nil) = G op l. + +(* Ensure that conversion of terms with evars is allowed once a keyed candidate unifier is found *) +rewrite -> list_foo. +reflexivity. +Qed. + +(* Basically like list_foo, but now uses the op projection for everything *) +Lemma test2 A (l : list A) : G op (op l nil) = G op l. +Proof. +rewrite ->list_foo. +reflexivity. +Qed. + + Require Import Bool. + Set Keyed Unification. + + Lemma test b : b && true = b. + Fail rewrite andb_true_l. + Admitted. +
\ No newline at end of file diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 5bef2e512a..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. @@ -317,29 +317,3 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. - -(* Check that matching "match" does not look into the invisible - canonically generated binders of the return clause and of the branches *) - -Goal forall n, match n with 0 => true | S _ => false end = true. -intros. unfold nat_rect. -Fail match goal with |- context [nat] => idtac end. -Abort. - -(* Check that branches of automatically generated elimination - principle are correctly eta-expanded and hence matchable as seen - from the user point of view *) - -Goal forall a f n, nat_rect (fun _ => nat) a f n = 0. -intros. unfold nat_rect. -match goal with |- context [f _] => idtac end. -Abort. - -(* Check that branches of automatically generated elimination - principle are in correct form also in the presence of let-ins *) - -Inductive a (b:=0) : let b':=1 in Type := c : let d:=0 in a. -Goal forall x, match x with c => 0 end = 1. -intros. -match goal with |- context [0] => idtac end. -Abort. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 54cfa658c8..45c1a5e584 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index d6bbfe29ac..878875bd92 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -242,7 +242,7 @@ Fail Check (Prop : Set). Fail Check (Set : Set). Check (Set : Type). Check (Prop : Type). -Definition setType := $(let t := type of Set in exact t)$. +Definition setType := ltac:(let t := type of Set in exact t). Definition foo (A : Prop) := A. @@ -303,7 +303,7 @@ Set Printing Universes. Axiom admit : forall A, A. Record R := {O : Type}. -Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}. +Definition RL (x : R@{i}) : ltac:(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) ) := {|O := @O x|}. Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl. Definition RLRL' : forall x : R, RL x = RL (RL x). intros. apply eq_refl. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 125615c535..b5e6ccd618 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -35,10 +35,6 @@ Set Implicit Arguments. Check nat. -(* Inductive X (U:Type) := Foo (k : nat) (x : X U). *) -(* Parameter x : X nat. *) -(* Check x.(k). *) - Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }. Parameter x:X nat. @@ -49,18 +45,8 @@ Inductive Y := { next : option Y }. Check _.(next) : option Y. Lemma eta_ind (y : Y) : y = Build_Y y.(next). -Proof. reflexivity. Defined. - -Variable t : Y. +Proof. Fail reflexivity. Abort. -Fixpoint yn (n : nat) (y : Y) : Y := - match n with - | 0 => t - | S n => {| next := Some (yn n y) |} - end. - -Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}. -Proof. reflexivity. Defined. (* @@ -194,4 +180,17 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }. Definition term (x : wrap nat) := x.(unwrap). Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x. Recursive Extraction term term'. -(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file +(*Unset Printing Primitive Projection Parameters.*) + +(* Primitive projections in the presence of let-ins (was not failing in beta3)*) + +Set Primitive Projections. +Record s (x:nat) (y:=S x) := {c:=x; d:x=c}. +Lemma f : 0=1. +Proof. +Fail apply d. +(* +split. +reflexivity. +Qed. +*) diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index c83f45e2a4..adaa05ad06 100644 --- a/test-suite/success/proof_using.v +++ b/test-suite/success/proof_using.v @@ -178,6 +178,7 @@ End Let. Check (test_let 3). +(* Disabled Section Clear. Variable a: nat. @@ -192,6 +193,6 @@ trivial. Qed. End Clear. - +*) diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 1e667884b8..352abb2af5 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -62,7 +62,7 @@ Abort. Goal (forall n : nat, n = 0 -> Prop) -> Prop. intro P. refine (P _ _). -2:reflexivity. +reflexivity. Abort. (* Submitted by Jacek Chrzaszcz (bug #1102) *) diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 0465c4b3fb..4c173a3cd5 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -166,3 +166,11 @@ 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. +Goal forall a b, h a b -> a 0 = true. +intros. +rewrite H. (* Fallback on ordinary rewrite without anomaly *) +Abort. diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v new file mode 100644 index 0000000000..3c0b81568a --- /dev/null +++ b/test-suite/success/sideff.v @@ -0,0 +1,12 @@ +Definition idw (A : Type) := A. +Lemma foobar : unit. +Proof. + Require Import Program. + apply (const tt tt). +Qed. + +Lemma foobar' : unit. + Lemma aux : forall A : Type, A -> unit. + Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed. + apply (@aux unit tt). +Qed. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 2954e25562..d595cbc2b8 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index e00701fb68..269359ae62 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -60,3 +60,20 @@ Qed. (* Submitted by Danko Ilik (bug report #1507); related to LetIn *) Record U : Type := { A:=Type; a:A }. + +(** Check assignement of sorts to inductives and records. *) + +Variable sh : list nat. + +Definition is_box_in_shape (b :nat * nat) := True. +Definition myType := Type. + +Module Ind. +Inductive box_in : myType := + myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in. +End Ind. + +Module Rec. +Record box_in : myType := + BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }. +End Rec.
\ No newline at end of file diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v index 31d264f645..048b53d26c 100644 --- a/test-suite/success/univnames.v +++ b/test-suite/success/univnames.v @@ -21,6 +21,6 @@ Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla. Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy. -Universe g. +Monomorphic Universe g. Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v new file mode 100644 index 0000000000..672222bdd6 --- /dev/null +++ b/test-suite/success/unshelve.v @@ -0,0 +1,11 @@ +Axiom F : forall (b : bool), b = true -> + forall (i : unit), i = i -> True. + +Goal True. +Proof. +unshelve (refine (F _ _ _ _)). ++ exact true. ++ exact tt. ++ exact (@eq_refl bool true). ++ exact (@eq_refl unit tt). +Qed. diff --git a/test-suite/success/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v new file mode 100644 index 0000000000..58fa39743d --- /dev/null +++ b/test-suite/success/vm_univ_poly.v @@ -0,0 +1,141 @@ +(* Basic tests *) +Polymorphic Definition pid {T : Type} (x : T) : T := x. +(* +Definition _1 : pid true = true := + @eq_refl _ true <: pid true = true. + +Polymorphic Definition a_type := Type. + +Definition _2 : a_type@{i} = Type@{i} := + @eq_refl _ Type@{i} <: a_type@{i} = Type@{i}. + +Polymorphic Definition FORALL (T : Type) (P : T -> Prop) : Prop := + forall x : T, P x. + +Polymorphic Axiom todo : forall {T:Type}, T -> T. + +Polymorphic Definition todo' (T : Type) := @todo T. + +Definition _3 : @todo'@{Set} = @todo@{Set} := + @eq_refl _ (@todo@{Set}) <: @todo'@{Set} = @todo@{Set}. +*) + +(* Inductive Types *) +Inductive sumbool (A B : Prop) : Set := +| left : A -> sumbool A B +| right : B -> sumbool A B. + +Definition x : sumbool True False := left _ _ I. + +Definition sumbool_copy {A B : Prop} (H : sumbool A B) : sumbool A B := + match H with + | left _ _ x => left _ _ x + | right _ _ x => right _ _ x + end. + +Definition _4 : sumbool_copy x = x := + @eq_refl _ x <: sumbool_copy x = x. + +(* Polymorphic Inductive Types *) +Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} := +| PSome : T -> poption@{i} T +| PNone : poption@{i} T. + +Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T := + match p with + | @PSome _ y => y + | @PNone _ => x + end. + +Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} := +| pnil +| pcons : T -> plist@{i} T -> plist@{i} T. + +Arguments pnil {_}. +Arguments pcons {_} _ _. + +Polymorphic Definition pmap@{i j} + {T : Type@{i}} {U : Type@{j}} (f : T -> U) := + fix pmap (ls : plist@{i} T) : plist@{j} U := + match ls with + | @pnil _ => @pnil _ + | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls) + end. + +Universe Ubool. +Inductive tbool : Type@{Ubool} := ttrue | tfalse. + + +Eval vm_compute in pmap pid (pcons true (pcons false pnil)). +Eval vm_compute in pmap (fun x => match x with + | pnil => true + | pcons _ _ => false + end) (pcons pnil (pcons (pcons false pnil) pnil)). +Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) pnil)). + +Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} := +| Empty +| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T. + +Polymorphic Definition pfold@{i u} + {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) := + fix pfold (acc : U) (ls : plist@{i} T) : U := + match ls with + | pnil => acc + | pcons a b => pfold (f a acc) b + end. + +Polymorphic Inductive nat@{i} : Type@{i} := +| O +| S : nat -> nat. + +Polymorphic Fixpoint nat_max@{i} (a b : nat@{i}) : nat@{i} := + match a , b with + | O , b => b + | a , O => a + | S a , S b => S (nat_max a b) + end. + +Polymorphic Fixpoint height@{i} {T : Type@{i}} (t : Tree@{i} T) : nat@{i} := + match t return nat@{i} with + | Empty _ => O + | Branch _ ls => S@{i} (pfold@{i i} nat_max O (pmap height ls)) + end. + +Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i} T := + match n return plist@{i} T with + | O => pnil + | S n => pcons@{i} v (repeat n v) + end. + +Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} := + match n with + | O => @Empty nat@{i} + | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n')) + end. + +Eval compute in height (big_tree (S (S (S O)))). + +Let big := S (S (S (S (S O)))). +Polymorphic Definition really_big@{i} := (S@{i} (S (S (S (S (S (S (S (S (S O)))))))))). + +Time Definition _5 : height (@Empty nat) = O := + @eq_refl nat O <: height (@Empty nat) = O. + +Time Definition _6 : height@{Set} (@Branch nat pnil) = S O := + @eq_refl nat@{Set} (S@{Set} O@{Set}) <: @eq nat@{Set} (height@{Set} (@Branch@{Set} nat@{Set} (@pnil@{Set} (Tree@{Set} nat@{Set})))) (S@{Set} O@{Set}). + +Time Definition _7 : height (big_tree big) = big := + @eq_refl nat big <: height (big_tree big) = big. + +Time Definition _8 : height (big_tree really_big) = really_big := + @eq_refl nat@{Set} (S@{Set} + (S@{Set} + (S@{Set} + (S@{Set} + (S@{Set} + (S@{Set} (S@{Set} (S@{Set} (S@{Set} (S@{Set} O@{Set})))))))))) + <: + @eq nat@{Set} + (@height nat@{Set} (big_tree really_big@{Set})) + really_big@{Set}. diff --git a/test-suite/success/vm_univ_poly_match.v b/test-suite/success/vm_univ_poly_match.v new file mode 100644 index 0000000000..abe6d0fe07 --- /dev/null +++ b/test-suite/success/vm_univ_poly_match.v @@ -0,0 +1,28 @@ +Set Dump Bytecode. +Set Printing Universes. +Set Printing All. + +Polymorphic Class Applicative@{d c} (T : Type@{d} -> Type@{c}) := +{ pure : forall {A : Type@{d}}, A -> T A + ; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B +}. + +Universes Uo Ua. + +Eval compute in @pure@{Uo Ua}. + +Global Instance Applicative_option : Applicative@{Uo Ua} option := +{| pure := @Some + ; ap := fun _ _ f x => + match f , x with + | Some f , Some x => Some (f x) + | _ , _ => None + end +|}. + +Definition foo := ap (ap (pure plus) (pure 1)) (pure 1). + +Print foo. + + +Eval vm_compute in foo. diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v index 6f37de6583..49f20a23f5 100644 --- a/test-suite/typeclasses/NewSetoid.v +++ b/test-suite/typeclasses/NewSetoid.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/test-suite/typeclasses/open_constr.v b/test-suite/typeclasses/open_constr.v new file mode 100644 index 0000000000..5f1785c706 --- /dev/null +++ b/test-suite/typeclasses/open_constr.v @@ -0,0 +1,12 @@ +Tactic Notation "opose" open_constr(foo) := pose foo. +Class Foo := Build_Foo : Set. +Axiom f : forall `{Foo}, Set. +Set Printing Implicit. +Goal forall `{Foo}, True. +Proof. + intro H. + pose f. + opose f. + Fail let x := (eval hnf in P) in has_evar x. + let x := (eval hnf in P0) in has_evar x. + diff --git a/test-suite/vio/print.v b/test-suite/vio/print.v new file mode 100644 index 0000000000..9c36a463c9 --- /dev/null +++ b/test-suite/vio/print.v @@ -0,0 +1,10 @@ +Lemma a : True. +Proof. +idtac. +exact I. +Qed. + +Print a. + +Lemma b : False. +Admitted. |