diff options
Diffstat (limited to 'test-suite/success')
47 files changed, 1849 insertions, 107 deletions
diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f14725a8..8f95484c 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with | _ => 0 end). +(* This one could eventually be solved, the "Fail" is just to ensure *) +(* that it does not fail with an anomaly, as it did at some time *) +Fail Check (fun x : I' 0 => match x return _ x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). + (* Check insertion of coercions around matched subterm *) Parameter A:Set. diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v index 3679eead..6424fe92 100644 --- a/test-suite/success/CaseInClause.v +++ b/test-suite/success/CaseInClause.v @@ -20,3 +20,10 @@ Theorem foo : forall (n m : nat) (pf : n = m), match pf in _ = N with | eq_refl => unit end. + +(* Check redundant clause is removed *) +Inductive I : nat * nat -> Type := C : I (0,0). +Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end. + +(* An example of non-local inference of the type of an impossible case *) +Check (fun y n (x:Vector.t nat (S n)) => match x with a::_ => a | _ => y end) 2. diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v new file mode 100644 index 00000000..db6348fa --- /dev/null +++ b/test-suite/success/Compat84.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) + +Goal True. + solve [ constructor 1 ]. Undo. + solve [ econstructor 1 ]. Undo. + solve [ constructor ]. Undo. + solve [ econstructor ]. Undo. + solve [ constructor (fail) ]. Undo. + solve [ econstructor (fail) ]. Undo. + split. +Qed. + +Goal False \/ True. + solve [ constructor (constructor) ]. Undo. + solve [ econstructor (econstructor) ]. Undo. + solve [ constructor 2; constructor ]. Undo. + solve [ econstructor 2; econstructor ]. Undo. + right; esplit. +Qed. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index f934a5c7..1abe1477 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -1,4 +1,12 @@ (* Checks syntax of Hints commands *) +(* Old-style syntax *) +Hint Resolve eq_refl eq_sym. +Hint Resolve eq_refl eq_sym: foo. +Hint Immediate eq_refl eq_sym. +Hint Immediate eq_refl eq_sym: foo. +Hint Unfold fst eq_sym. +Hint Unfold fst eq_sym: foo. + (* Checks that qualified names are accepted *) (* New-style syntax *) @@ -8,13 +16,76 @@ Hint Unfold eq_sym: core. Hint Constructors eq: foo bar. Hint Extern 3 (_ = _) => apply eq_refl: foo bar. -(* Old-style syntax *) -Hint Resolve eq_refl eq_sym. -Hint Resolve eq_refl eq_sym: foo. -Hint Immediate eq_refl eq_sym. -Hint Immediate eq_refl eq_sym: foo. -Hint Unfold fst eq_sym. -Hint Unfold fst eq_sym: foo. +(* Extended new syntax with patterns *) +Hint Resolve eq_refl | 4 (_ = _) : baz. +Hint Resolve eq_sym eq_trans : baz. +Hint Extern 3 (_ = _) => apply eq_sym : baz. + +Parameter pred : nat -> Prop. +Parameter pred0 : pred 0. +Parameter f : nat -> nat. +Parameter predf : forall n, pred n -> pred (f n). + +(* No conversion on let-bound variables and constants in pred (the default) *) +Hint Resolve pred0 | 1 (pred _) : pred. +Hint Resolve predf | 0 : pred. + +(* Allow full conversion on let-bound variables and constants *) +Create HintDb predconv discriminated. +Hint Resolve pred0 | 1 (pred _) : predconv. +Hint Resolve predf | 0 : predconv. + +Goal exists n, pred n. + eexists. + Fail Timeout 1 typeclasses eauto with pred. + Set Typeclasses Filtered Unification. + Set Typeclasses Debug Verbosity 2. + (* predf is not tried as it doesn't match the goal *) + typeclasses eauto with pred. +Qed. + +Parameter predconv : forall n, pred n -> pred (0 + S n). + +(* The inferred pattern contains 0 + ?n, syntactic match will fail to see convertible + terms *) +Hint Resolve pred0 : pred2. +Hint Resolve predconv : pred2. + +(** In this database we allow predconv to apply to pred (S _) goals, more generally + than the inferred pattern (pred (0 + S _)). *) +Create HintDb pred2conv discriminated. +Hint Resolve pred0 : pred2conv. +Hint Resolve predconv | 1 (pred (S _)) : pred2conv. + +Goal pred 3. + Fail typeclasses eauto with pred2. + typeclasses eauto with pred2conv. +Abort. + +Set Typeclasses Filtered Unification. +Set Typeclasses Debug Verbosity 2. +Hint Resolve predconv | 1 (pred _) : pred. +Hint Resolve predconv | 1 (pred (S _)) : predconv. +Test Typeclasses Limit Intros. +Goal pred 3. + (* predf is not tried as it doesn't match the goal *) + (* predconv is tried but fails as the transparent state doesn't allow + unfolding + *) + Fail typeclasses eauto with pred. + (* Here predconv succeeds as it matches (pred (S _)) and then + full unification is allowed *) + typeclasses eauto with predconv. +Qed. + +(** The other way around: goal contains redexes instead of instances *) +Goal exists n, pred (0 + n). + eexists. + (* predf is applied indefinitely *) + Fail Timeout 1 typeclasses eauto with pred. + (* pred0 (pred _) matches the goal *) + typeclasses eauto with predconv. +Qed. + (* Checks that local names are accepted *) Section A. @@ -100,9 +171,9 @@ Instance foo f : 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. +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 +End HintCut. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 9661b3bf..f746def5 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -162,3 +162,24 @@ Inductive L (A:Type) (T:=A) : Type := C : L nat -> L A. hit the Inductiveops.get_arity bug mentioned above (see #3491) *) Inductive IND6 (A:Type) (T:=A) := CONS6 : IND6 T -> IND6 A. + + +Module TemplateProp. + + (** Check lowering of a template universe polymorphic inductive to Prop *) + + Inductive Foo (A : Type) : Type := foo : A -> Foo A. + + Check Foo True : Prop. + +End TemplateProp. + +Module PolyNoLowerProp. + + (** Check lowering of a general universe polymorphic inductive to Prop is _failing_ *) + + Polymorphic Inductive Foo (A : Type) : Type := foo : A -> Foo A. + + Fail Check Foo True : Prop. + +End PolyNoLowerProp. diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 25e464d6..da218384 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -4,6 +4,7 @@ Require Eqdep_dec. (* Check that Injection tries Intro until *) +Unset Structural Injection. Lemma l1 : forall x : nat, S x = S (S x) -> False. injection 1. apply n_Sn. @@ -37,6 +38,7 @@ intros. injection H. exact (fun H => H). Qed. +Set Structural Injection. (* Test injection as *) @@ -65,7 +67,13 @@ Qed. Goal (forall x y : nat, x = y -> S x = S y) -> True. intros. einjection (H O). -instantiate (1:=O). +2: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 *) @@ -79,12 +87,21 @@ Qed. (* Basic case, using sigT *) Scheme Equality for nat. +Unset Structural Injection. Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, existT P n H1 = existT P n H2 -> H1 = H2. intros. injection H. intro H0. exact H0. Abort. +Set Structural Injection. + +Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n, + existT P n H1 = existT P n H2 -> H1 = H2. +intros. +injection H as H0. +exact H0. +Abort. (* Test injection using K, knowing that an equality is decidable *) (* Basic case, using sigT, with "as" clause *) @@ -118,7 +135,22 @@ intros * [= H]. exact H. Abort. -(* Injection does not projects at positions in Prop... allow it? +(* Test the Keep Proof Equalities option. *) +Set Keep Proof Equalities. +Unset Structural Injection. + +Inductive pbool : Prop := Pbool1 | Pbool2. + +Inductive pbool_shell : Set := Pbsc : pbool -> pbool_shell. + +Goal Pbsc Pbool1 = Pbsc Pbool2 -> True. +injection 1. +match goal with + |- Pbool1 = Pbool2 -> True => idtac | |- True => fail +end. +Abort. + +(* Injection does not project at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. Goal forall p q : True\/True, c _ p = c _ q -> False. diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v index 7069bba4..8462d362 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 b72a0674..07bbb60c 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -58,7 +58,7 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end). (* Check multi-tokens recursive notations *) -Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). +Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). Check [ 0 ]. Check [ 0 # ; 1 ]. @@ -107,3 +107,24 @@ Notation traverse_var f l := (traverse (fun l => f l) l). Notation "'intros' x" := (S x) (at level 0). Goal True -> True. intros H. exact H. Qed. + +(* Check absence of collision on ".." in nested notations with ".." *) +Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). + +(* Check that vector notations do not break Ltac [] (bugs #4785, #4733) *) +Require Import Coq.Vectors.VectorDef. +Import VectorNotations. +Goal True. idtac; []. (* important for test: no space here *) constructor. Qed. + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. +Check |- {{ 0 }} 0. + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v new file mode 100644 index 00000000..9505a56e --- /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/PatternsInBinders.v b/test-suite/success/PatternsInBinders.v new file mode 100644 index 00000000..77710791 --- /dev/null +++ b/test-suite/success/PatternsInBinders.v @@ -0,0 +1,67 @@ +(** The purpose of this file is to test functional properties of the + destructive patterns used in binders ([fun] and [forall]). *) + + +Definition swap {A B} '((x,y) : A*B) := (y,x). + +(** Tests the use of patterns in [fun] and [Definition] *) +Section TestFun. + + Variables A B : Type. + + Goal forall (x:A) (y:B), swap (x,y) = (y,x). + Proof. reflexivity. Qed. + + Goal forall u:A*B, swap (swap u) = u. + Proof. destruct u. reflexivity. Qed. + + Goal @swap A B = fun '(x,y) => (y,x). + Proof. reflexivity. Qed. + +End TestFun. + + +(** Tests the use of patterns in [forall] *) +Section TestForall. + + Variables A B : Type. + + Goal forall '((x,y) : A*B), swap (x,y) = (y,x). + Proof. intros [x y]. reflexivity. Qed. + + Goal forall x0:A, exists '((x,y) : A*A), swap (x,y) = (x,y). + Proof. + intros x0. + exists (x0,x0). + reflexivity. + Qed. + +End TestForall. + + + +(** Tests the use of patterns in dependent definitions. *) + +Section TestDependent. + + Inductive Fin (n:nat) := Z : Fin n. + + Definition F '(n,p) : Type := (Fin n * Fin p)%type. + + Definition both_z '(n,p) : F (n,p) := (Z _,Z _). + +End TestDependent. + + +(** Tests with a few other types just to make sure parsing is + robust. *) +Section TestExtra. + + Definition proj_informative {A P} '(exist _ x _ : { x:A | P x }) : A := x. + + Inductive Foo := Bar : nat -> bool -> unit -> nat -> Foo. + + Definition foo '(Bar n b tt p) := + if b then n+p else n-p. + +End TestExtra. diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 11fbf24d..d8f80424 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -831,7 +831,7 @@ Proof. intro n. apply nat_ind with (P:= fun n => n <> S n). discriminate. - red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial. + red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;auto. Qed. Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}. @@ -1075,8 +1075,8 @@ Proof. apply vector_double_rect. simpl. destruct i; discriminate 1. - destruct i; simpl;auto. - injection 1; injection 2;intros; subst a; subst b; auto. + destruct i; simpl;auto. + injection 1 as ->; injection 1 as ->; auto. Qed. Set Implicit Arguments. diff --git a/test-suite/success/TacticNotation2.v b/test-suite/success/TacticNotation2.v new file mode 100644 index 00000000..cb341b8e --- /dev/null +++ b/test-suite/success/TacticNotation2.v @@ -0,0 +1,12 @@ +Tactic Notation "complete" tactic(tac) := tac; fail. + +Ltac f0 := complete (intuition idtac). +(** FIXME: This is badly printed because of bug #3079. + At least we check that it does not fail anomalously. *) +Print Ltac f0. + +Ltac f1 := complete f1. +Print Ltac f1. + +Ltac f2 := complete intuition. +Print Ltac f2. diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index c8a8b862..023cb5f5 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -53,7 +53,7 @@ Abort. Lemma essai2 : forall x : nat, x = x. -Fail refine (fix f (x : nat) : x = x := _). +refine (fix f (x : nat) : x = x := _). Restart. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index 30a2a742..6b1f0315 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -1,3 +1,117 @@ +Module onlyclasses. + +(* In 8.6 we still allow non-class subgoals *) + Variable Foo : Type. + Variable foo : Foo. + Hint Extern 0 Foo => exact foo : typeclass_instances. + Goal Foo * Foo. + split. shelve. + Set Typeclasses Debug. + typeclasses eauto. + Unshelve. typeclasses eauto. + Qed. + + Module RJung. + Class Foo (x : nat). + + Instance foo x : x = 2 -> Foo x. + Hint Extern 0 (_ = _) => reflexivity : typeclass_instances. + Typeclasses eauto := debug. + Check (_ : Foo 2). + + + Fail Definition foo := (_ : 0 = 0). + + End RJung. +End onlyclasses. + +Module shelve_non_class_subgoals. + Variable Foo : Type. + Variable foo : Foo. + Hint Extern 0 Foo => exact foo : typeclass_instances. + Class Bar := {}. + Instance bar1 (f:Foo) : Bar := {}. + + Typeclasses eauto := debug. + Set Typeclasses Debug Verbosity 2. + Goal Bar. + (* Solution has shelved subgoals (of non typeclass type) *) + typeclasses eauto. + Abort. +End shelve_non_class_subgoals. + +Module RefineVsNoTceauto. + + Class Foo (A : Type) := foo : A. + Instance: Foo nat := { foo := 0 }. + Instance: Foo nat := { foo := 42 }. + Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances. + Goal exists (f : Foo nat), @foo _ f = 0. + Proof. + unshelve (notypeclasses refine (ex_intro _ _ _)). + Set Typeclasses Debug. Set Printing All. + all:once (typeclasses eauto). + Fail idtac. (* Check no subgoals are left *) + Undo 3. + (** In this case, the (_ = _) subgoal is not considered + by typeclass resolution *) + refine (ex_intro _ _ _). Fail reflexivity. + Abort. + +End RefineVsNoTceauto. + +Module Leivantex2PR339. + (** Was a bug preventing to find hints associated with no pattern *) + Class Bar := {}. + Instance bar1 (t:Type) : Bar. + Hint Extern 0 => exact True : typeclass_instances. + Typeclasses eauto := debug. + Goal Bar. + Set Typeclasses Debug Verbosity 2. + typeclasses eauto. (* Relies on resolution of a non-class subgoal *) + Undo 1. + typeclasses eauto with typeclass_instances. + Qed. +End Leivantex2PR339. + +Module bt. +Require Import Equivalence. + +Record Equ (A : Type) (R : A -> A -> Prop). +Definition equiv {A} R (e : Equ A R) := R. +Record Refl (A : Type) (R : A -> A -> Prop). +Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e). +Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo. + +Variable R : nat -> nat -> Prop. +Lemma bas : Equ nat R. +Admitted. +Hint Resolve bas : foo. +Hint Extern 1 => match goal with |- (_ -> _ -> Prop) => shelve end : foo. + +Goal exists R, @Refl nat R. + eexists. + Set Typeclasses Debug. + (* Fail solve [unshelve eauto with foo]. *) + Set Typeclasses Debug Verbosity 1. + Test Typeclasses Depth. + solve [typeclasses eauto with foo]. +Qed. + +Set Typeclasses Compatibility "8.5". +Parameter f : nat -> Prop. +Parameter g : nat -> nat -> Prop. +Parameter h : nat -> nat -> nat -> Prop. +Axiom a : forall x y, g x y -> f x -> f y. +Axiom b : forall x (y : Empty_set), g (fst (x,y)) x. +Axiom c : forall x y z, h x y z -> f x -> f y. +Hint Resolve a b c : mybase. +Goal forall x y z, h x y z -> f x -> f y. + intros. + Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *) + Unshelve. +Abort. +End bt. Generalizable All Variables. Module mon. @@ -23,8 +137,15 @@ Notation "'return' t" := (unit t). Class A `(e: T) := { a := True }. Class B `(e_: T) := { e := e_; sg_ass :> A e }. -Goal forall `{B T}, a. - intros. exact I. +(* Set Typeclasses Debug. *) +(* Set Typeclasses Debug Verbosity 2. *) + +Goal forall `{B T}, Prop. + intros. apply a. +Defined. + +Goal forall `{B T}, Prop. + intros. refine (@a _ _ _). Defined. Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }. @@ -57,4 +178,65 @@ Section sec. let's try to get rid of the intermediate constant foo. Surely we can just expand it inline, right? Wrong!: *) Check U (fun x => e x) _. -End sec.
\ No newline at end of file +End sec. + +Module UniqueSolutions. + Set Typeclasses Unique Solutions. + Class Eq (A : Type) : Set. + Instance eqa : Eq nat := {}. + Instance eqb : Eq nat := {}. + + Goal Eq nat. + try apply _. + Fail exactly_once typeclasses eauto. + Abort. +End UniqueSolutions. + + +Module UniqueInstances. + (** Optimize proof search on this class by never backtracking on (closed) goals + for it. *) + Set Typeclasses Unique Instances. + Class Eq (A : Type) : Set. + Instance eqa : Eq nat := _. constructor. Qed. + Instance eqb : Eq nat := {}. + Class Foo (A : Type) (e : Eq A) : Set. + Instance fooa : Foo _ eqa := {}. + + Tactic Notation "refineu" open_constr(c) := unshelve refine c. + + Set Typeclasses Debug. + Goal { e : Eq nat & Foo nat e }. + unshelve refineu (existT _ _ _). + all:simpl. + (** Does not backtrack on the (wrong) solution eqb *) + Fail all:typeclasses eauto. + Abort. +End UniqueInstances. + +Module IterativeDeepening. + + Class A. + Class B. + Class C. + + Instance: B -> A | 0. + Instance: C -> A | 0. + Instance: C -> B -> A | 0. + Instance: A -> A | 0. + + Goal C -> A. + intros. + Set Typeclasses Debug. + Fail Timeout 1 typeclasses eauto. + Set Typeclasses Iterative Deepening. + Fail typeclasses eauto 1. + typeclasses eauto 2. + Undo. + Unset Typeclasses Iterative Deepening. + Fail Timeout 1 typeclasses eauto. + Set Typeclasses Iterative Deepening. + typeclasses eauto. + Qed. + +End IterativeDeepening. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 55b666b7..02e043bc 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 aaa7b3a5..5477c833 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 00000000..7fd0cf66 --- /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/bteauto.v b/test-suite/success/bteauto.v new file mode 100644 index 00000000..3178c6fc --- /dev/null +++ b/test-suite/success/bteauto.v @@ -0,0 +1,170 @@ +Require Import Program.Tactics. +Module Backtracking. + Class A := { foo : nat }. + + Instance A_1 : A | 2 := { foo := 42 }. + Instance A_0 : A | 1 := { foo := 0 }. + Lemma aeq (a : A) : foo = foo. + reflexivity. + Qed. + + Arguments foo A : clear implicits. + Example find42 : exists n, n = 42. + Proof. + eexists. + eapply eq_trans. + evar (a : A). subst a. + refine (@aeq ?a). + Unshelve. all:cycle 1. + typeclasses eauto. + Fail reflexivity. + Undo 2. + (* Without multiple successes it fails *) + Set Typeclasses Debug Verbosity 2. + Fail all:((once (typeclasses eauto with typeclass_instances)) + + apply eq_refl). + (* Does backtrack if other goals fail *) + all:[> typeclasses eauto + reflexivity .. ]. + Undo 1. + all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *) + Show Proof. + Qed. + + Print find42. + + Hint Extern 0 (_ = _) => reflexivity : equality. + + Goal exists n, n = 42. + eexists. + eapply eq_trans. + evar (a : A). subst a. + refine (@aeq ?a). + Unshelve. all:cycle 1. + typeclasses eauto. + Fail reflexivity. + Undo 2. + + (* Does backtrack between individual goals *) + Set Typeclasses Debug. + all:(typeclasses eauto with typeclass_instances equality). + Qed. + + Unset Typeclasses Debug. + + Module Leivant. + Axiom A : Type. + Existing Class A. + Axioms a b c d e: A. + + Ltac get_value H := eval cbv delta [H] in H. + + Goal True. + Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail. + Admitted. + + Goal exists x:A, x=a. + unshelve evar (t : A). all:cycle 1. + refine (@ex_intro _ _ t _). + all:cycle 1. + all:(typeclasses eauto + reflexivity). + Qed. + End Leivant. +End Backtracking. + + +Hint Resolve 100 eq_sym eq_trans : core. +Hint Cut [(_)* eq_sym eq_sym] : core. +Hint Cut [_* eq_trans eq_trans] : core. +Hint Cut [_* eq_trans eq_sym eq_trans] : core. + + +Goal forall x y z : nat, x = y -> z = y -> x = z. +Proof. + intros. + typeclasses eauto with core. +Qed. + +Module Hierarchies. + Class A := mkA { data : nat }. + Class B := mkB { aofb :> A }. + + Existing Instance mkB. + + Definition makeB (a : A) : B := _. + Definition makeA (a : B) : A := _. + + Fail Timeout 1 Definition makeA' : A := _. + + Hint Cut [_* mkB aofb] : typeclass_instances. + Fail Definition makeA' : A := _. + Fail Definition makeB' : B := _. +End Hierarchies. + +(** Hint modes *) + +Class Equality (A : Type) := { eqp : A -> A -> Prop }. + +Check (eqp 0%nat 0). + +Instance nat_equality : Equality nat := { eqp := eq }. + +Instance default_equality A : Equality A | 1000 := + { eqp := eq }. + +Check (eqp 0%nat 0). + +(* Defaulting *) +Check (fun x y => eqp x y). +(* No more defaulting, reduce "trigger-happiness" *) +Definition ambiguous x y := eqp x y. + +Hint Mode Equality ! : typeclass_instances. +Fail Definition ambiguous' x y := eqp x y. +Definition nonambiguous (x y : nat) := eqp x y. + +(** Typical looping instances with defaulting: *) +Definition flip {A B C} (f : A -> B -> C) := fun x y => f y x. + +Class SomeProp {A : Type} (f : A -> A -> A) := + { prf : forall x y, f x y = f x y }. + +Instance propflip (A : Type) (f : A -> A -> A) : + SomeProp f -> SomeProp (flip f). +Proof. + intros []. constructor. reflexivity. +Qed. + +Fail Timeout 1 Check prf. + +Hint Mode SomeProp + + : typeclass_instances. +Check prf. +Check (fun H : SomeProp plus => _ : SomeProp (flip plus)). + +(** Iterative deepening / breadth-first search *) + +Module IterativeDeepening. + + Class A. + Class B. + Class C. + + Instance: B -> A | 0. + Instance: C -> A | 0. + Instance: C -> B -> A | 0. + Instance: A -> A | 0. + + Goal C -> A. + intros. + Fail Timeout 1 typeclasses eauto. + Set Typeclasses Iterative Deepening. + Fail typeclasses eauto 1. + typeclasses eauto 2. + Undo. + Unset Typeclasses Iterative Deepening. + Fail Timeout 1 typeclasses eauto. + Set Typeclasses Iterative Deepening. + Typeclasses eauto := debug 3. + typeclasses eauto. + Qed. + +End IterativeDeepening. diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index a70d9196..bbfe5ec4 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -129,5 +129,25 @@ 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. + +(* Example by Jonathan Leivant, congruence up to universes *) +Section JLeivant. + Variables S1 S2 : Set. + + Definition T1 : Type := S1. + Definition T2 : Type := S2. + Goal T1 = T1. + congruence. + Undo. + unfold T1. + congruence. + Qed. +End JLeivant. diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v index 976bec73..e25510cf 100644 --- a/test-suite/success/clear.v +++ b/test-suite/success/clear.v @@ -13,3 +13,21 @@ Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True. reflexivity. Qed. +Class A. + +Section Foo. + + Variable a : A. + + Goal A. + solve [typeclasses eauto]. + Undo 1. + clear a. + try typeclasses eauto. + assert(a:=Build_A). + solve [ typeclasses eauto ]. + Undo 2. + assert(b:=Build_A). + solve [ typeclasses eauto ]. + Qed. +End Foo.
\ No newline at end of file diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v index 4e0b7bf5..5b9265b6 100644 --- a/test-suite/success/coindprim.v +++ b/test-suite/success/coindprim.v @@ -1,36 +1,75 @@ +Require Import Program. + Set Primitive Projections. -CoInductive stream A := { hd : A; tl : stream A }. +CoInductive Stream (A : Type) := mkStream { hd : A; tl : Stream A}. -CoFixpoint ticks : stream unit := - {| hd := tt; tl := ticks |}. +Arguments mkStream [A] hd tl. +Arguments hd [A] s. +Arguments tl [A] s. -Arguments hd [ A ] s. -Arguments tl [ A ] s. +Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}. -CoInductive bisim {A} : stream A -> stream A -> Prop := - | bisims s s' : hd s = hd s' -> bisim (tl s) (tl s') -> bisim s s'. +CoFixpoint ones := {| hd := 1; tl := ones |}. +CoFixpoint ticks := {| hd := tt; tl := ticks |}. -Lemma bisim_refl {A} (s : stream A) : bisim s s. -Proof. - revert s. - cofix aux. intros. constructor. reflexivity. apply aux. -Defined. +CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop := + mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }. +Arguments stream_equiv {A} s s'. -Lemma constr : forall (A : Type) (s : stream A), - bisim s (Build_stream _ s.(hd) s.(tl)). -Proof. - intros. constructor. reflexivity. simpl. apply bisim_refl. -Defined. +Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) := + {| hdeq := eq_refl; tleq := ones_eq |}. + +CoFixpoint stream_equiv_refl {A} (s : Stream A) : stream_equiv s s := + {| hdeq := eq_refl; tleq := stream_equiv_refl (tl s) |}. + +CoFixpoint stream_equiv_sym {A} (s s' : Stream A) (H : stream_equiv s s') : stream_equiv s' s := + {| hdeq := eq_sym H.(hdeq); tleq := stream_equiv_sym _ _ H.(tleq) |}. + +CoFixpoint stream_equiv_trans {A} {s s' s'' : Stream A} + (H : stream_equiv s s') (H' : stream_equiv s' s'') : stream_equiv s s'' := + {| hdeq := eq_trans H.(hdeq) H'.(hdeq); + tleq := stream_equiv_trans H.(tleq) H'.(tleq) |}. -Lemma constr' : forall (A : Type) (s : stream A), - s = Build_stream _ s.(hd) s.(tl). +Program Definition eta_eq {A} (s : Stream A) : stream_equiv s (eta s):= + {| hdeq := eq_refl; tleq := stream_equiv_refl (tl (eta s))|}. + +Section Parks. + Variable A : Type. + + Variable R : Stream A -> Stream A -> Prop. + Hypothesis bisim1 : forall s1 s2:Stream A, + R s1 s2 -> hd s1 = hd s2. + Hypothesis bisim2 : forall s1 s2:Stream A, + R s1 s2 -> R (tl s1) (tl s2). + CoFixpoint park_ppl : + forall s1 s2:Stream A, R s1 s2 -> stream_equiv s1 s2 := + fun s1 s2 (p : R s1 s2) => + mkStreamEq _ _ _ (bisim1 s1 s2 p) + (park_ppl (tl s1) + (tl s2) + (bisim2 s1 s2 p)). +End Parks. + +Program CoFixpoint iterate {A} (f : A -> A) (x : A) : Stream A := + {| hd := x; tl := iterate f (f x) |}. + +Program CoFixpoint map {A B} (f : A -> B) (s : Stream A) : Stream B := + {| hd := f s.(hd); tl := map f s.(tl) |}. + +Theorem map_iterate A (f : A -> A) (x : A) : stream_equiv (iterate f (f x)) + (map f (iterate f x)). Proof. - intros. - Fail destruct s. -Abort. +apply park_ppl with +(R:= fun s1 s2 => exists x : A, s1 = iterate f (f x) /\ + s2 = map f (iterate f x)). +now intros s1 s2 (x0,(->,->)). +intros s1 s2 (x0,(->,->)). +now exists (f x0). +now exists x. +Qed. -Eval compute in constr _ ticks. +Fail Check (fun A (s : Stream A) => eq_refl : s = eta s). Notation convertible x y := (eq_refl x : x = y). diff --git a/test-suite/success/contradiction.v b/test-suite/success/contradiction.v new file mode 100644 index 00000000..92a7c6cc --- /dev/null +++ b/test-suite/success/contradiction.v @@ -0,0 +1,32 @@ +(* Some tests for contradiction *) + +Lemma L1 : forall A B : Prop, A -> ~A -> B. +Proof. +intros; contradiction. +Qed. + +Lemma L2 : forall A B : Prop, ~A -> A -> B. +Proof. +intros; contradiction. +Qed. + +Lemma L3 : forall A : Prop, ~True -> A. +Proof. +intros; contradiction. +Qed. + +Lemma L4 : forall A : Prop, forall x : nat, ~x=x -> A. +Proof. +intros; contradiction. +Qed. + +Lemma L5 : forall A : Prop, forall x y : nat, ~x=y -> x=y -> A. +Proof. +intros; contradiction. +Qed. + +Lemma L6 : forall A : Prop, forall x y : nat, x=y -> ~x=y -> A. +Proof. +intros; contradiction. +Qed. + diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v new file mode 100644 index 00000000..46174e48 --- /dev/null +++ b/test-suite/success/decl_mode2.v @@ -0,0 +1,249 @@ +Theorem this_is_trivial: True. +proof. + thus thesis. +end proof. +Qed. + +Theorem T: (True /\ True) /\ True. + split. split. +proof. (* first subgoal *) + thus thesis. +end proof. +trivial. (* second subgoal *) +proof. (* third subgoal *) + thus thesis. +end proof. +Abort. + +Theorem this_is_not_so_trivial: False. +proof. +end proof. (* here a warning is issued *) +Fail Qed. (* fails: the proof in incomplete *) +Admitted. (* Oops! *) + +Theorem T: True. +proof. +escape. +auto. +return. +Abort. + +Theorem T: let a:=false in let b:= true in ( if a then True else False -> if b then True else False). +intros a b. +proof. +assume H:(if a then True else False). +reconsider H as False. +reconsider thesis as True. +Abort. + +Theorem T: forall x, x=2 -> 2+x=4. +proof. +let x be such that H:(x=2). +have H':(2+x=2+2) by H. +Abort. + +Theorem T: forall x, x=2 -> 2+x=4. +proof. +let x be such that H:(x=2). +then (2+x=2+2). +Abort. + +Theorem T: forall x, x=2 -> x + x = x * x. +proof. +let x be such that H:(x=2). +have (4 = 4). + ~= (2 * 2). + ~= (x * x) by H. + =~ (2 + 2). + =~ H':(x + x) by H. +Abort. + +Theorem T: forall x, x + x = x * x -> x = 0 \/ x = 2. +proof. +let x be such that H:(x + x = x * x). +claim H':((x - 2) * x = 0). +thus thesis. +end claim. +Abort. + +Theorem T: forall (A B:Prop), A -> B -> A /\ B. +intros A B HA HB. +proof. +hence B. +Abort. + +Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B /\ C. +intros A B C HA HB HC. +proof. +thus B by HB. +Abort. + +Theorem T: forall (A B C:Prop), A -> B -> C -> A /\ B. +intros A B C HA HB HC. +proof. +Fail hence C. (* fails *) +Abort. + +Theorem T: forall (A B:Prop), B -> A \/ B. +intros A B HB. +proof. +hence B. +Abort. + +Theorem T: forall (A B C D:Prop), C -> D -> (A /\ B) \/ (C /\ D). +intros A B C D HC HD. +proof. +thus C by HC. +Abort. + +Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. +intros P HP. +proof. +take 2. +Abort. + +Theorem T: forall (P:nat -> Prop), P 2 -> exists x,P x. +intros P HP. +proof. +hence (P 2). +Abort. + +Theorem T: forall (P:nat -> Prop) (R:nat -> nat -> Prop), P 2 -> R 0 2 -> exists x, exists y, P y /\ R x y. +intros P R HP HR. +proof. +thus (P 2) by HP. +Abort. + +Theorem T: forall (A B:Prop) (P:nat -> Prop), (forall x, P x -> B) -> A -> A /\ B. +intros A B P HP HA. +proof. +suffices to have x such that HP':(P x) to show B by HP,HP'. +Abort. + +Theorem T: forall (A:Prop) (P:nat -> Prop), P 2 -> A -> A /\ (forall x, x = 2 -> P x). +intros A P HP HA. +proof. +(* BUG: the next line fails when it should succeed. +Waiting for someone to investigate the bug. +focus on (forall x, x = 2 -> P x). +let x be such that (x = 2). +hence thesis by HP. +end focus. +*) +Abort. + +Theorem T: forall x, x = 0 -> x + x = x * x. +proof. +let x be such that H:(x = 0). +define sqr x as (x * x). +reconsider thesis as (x + x = sqr x). +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +let x:nat. +assume HP:(P x). +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +Fail let x. (* fails because x's type is not clear *) +let x be such that HP:(P x). (* here x's type is inferred from (P x) *) +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x -> P x. +proof. +let P:(nat -> Prop). +let x:nat. +assume (P x). (* temporary name created *) +Abort. + +Theorem T: forall (P:nat -> Prop), forall x, P x -> P x. +proof. +let P:(nat -> Prop). +let x be such that (P x). (* temporary name created *) +Abort. + +Theorem T: forall (P:nat -> Prop) (A:Prop), (exists x, (P x /\ A)) -> A. +proof. +let P:(nat -> Prop),A:Prop be such that H:(exists x, P x /\ A). +consider x such that HP:(P x) and HA:A from H. +Abort. + +(* Here is an example with pairs: *) + +Theorem T: forall p:(nat * nat)%type, (fst p >= snd p) \/ (fst p < snd p). +proof. +let p:(nat * nat)%type. +consider x:nat,y:nat from p. +reconsider thesis as (x >= y \/ x < y). +Abort. + +Theorem T: forall P:(nat -> Prop), (forall n, P n -> P (n - 1)) -> +(exists m, P m) -> P 0. +proof. +let P:(nat -> Prop) be such that HP:(forall n, P n -> P (n - 1)). +given m such that Hm:(P m). +Abort. + +Theorem T: forall (A B C:Prop), (A -> C) -> (B -> C) -> (A \/ B) -> C. +proof. +let A:Prop,B:Prop,C:Prop be such that HAC:(A -> C) and HBC:(B -> C). +assume HAB:(A \/ B). +per cases on HAB. +suppose A. + hence thesis by HAC. +suppose HB:B. + thus thesis by HB,HBC. +end cases. +Abort. + +Section Coq. + +Hypothesis EM : forall P:Prop, P \/ ~ P. + +Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. +proof. +let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). +per cases of (A \/ ~A) by EM. +suppose (~A). + hence thesis by HNAC. +suppose A. + hence thesis by HAC. +end cases. +Abort. + +Theorem T: forall (A C:Prop), (A -> C) -> (~A -> C) -> C. +proof. +let A:Prop,C:Prop be such that HAC:(A -> C) and HNAC:(~A -> C). +per cases on (EM A). +suppose (~A). +Abort. +End Coq. + +Theorem T: forall (A B:Prop) (x:bool), (if x then A else B) -> A \/ B. +proof. +let A:Prop,B:Prop,x:bool. +per cases on x. +suppose it is true. + assume A. + hence A. +suppose it is false. + assume B. + hence B. +end cases. +Abort. + +Theorem T: forall (n:nat), n + 0 = n. +proof. +let n:nat. +per induction on n. +suppose it is 0. + thus (0 + 0 = 0). +suppose it is (S m) and H:thesis for m. + then (S (m + 0) = S m). + thus =~ (S m + 0). +end induction. +Abort.
\ No newline at end of file diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 9f091e39..90a60daa 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -96,21 +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. @@ -426,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 773dd321..160f2d9d 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -5,6 +5,184 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) + +Class A (A : Type). + Instance an: A nat. + +Class B (A : Type) (a : A). +Instance bn0: B nat 0. +Instance bn1: B nat 1. + +Goal A nat. +Proof. + typeclasses eauto. +Qed. + +Goal B nat 2. +Proof. + Fail typeclasses eauto. +Abort. + +Goal exists T : Type, A T. +Proof. + eexists. typeclasses eauto. +Defined. + +Hint Extern 0 (_ /\ _) => constructor : typeclass_instances. + +Existing Class and. + +Goal exists (T : Type) (t : T), A T /\ B T t. +Proof. + eexists. eexists. typeclasses eauto. +Defined. + +Instance ab: A bool. (* Backtrack on A instance *) +Goal exists (T : Type) (t : T), A T /\ B T t. +Proof. + eexists. eexists. typeclasses eauto. +Defined. + +Class C {T} `(a : A T) (t : T). +Require Import Classes.Init. +Hint Extern 0 { x : ?A & _ } => + unshelve class_apply @existT : typeclass_instances. +Existing Class sigT. +Set Typeclasses Debug. +Instance can: C an 0. +(* Backtrack on instance implementation *) +Goal exists (T : Type) (t : T), { x : A T & C x t }. +Proof. + eexists. eexists. typeclasses eauto. +Defined. + +Class D T `(a: A T). + Instance: D _ an. +Goal exists (T : Type), { x : A T & D T x }. +Proof. + eexists. typeclasses eauto. +Defined. + + +(* Example from Nicolas Magaud on coq-club - Jul 2000 *) + +Definition Nat : Set := nat. +Parameter S' : Nat -> Nat. +Parameter plus' : Nat -> Nat -> Nat. + +Lemma simpl_plus_l_rr1 : + (forall n0 : Nat, + (forall m p : Nat, plus' n0 m = plus' n0 p -> m = p) -> + forall m p : Nat, S' (plus' n0 m) = S' (plus' n0 p) -> m = p) -> + forall n : Nat, + (forall m p : Nat, plus' n m = plus' n p -> m = p) -> + forall m p : Nat, S' (plus' n m) = S' (plus' n p) -> m = p. + intros. + apply H0. apply f_equal_nat. + Time info_eauto. + Undo. + Set Typeclasses Debug. + Set Typeclasses Iterative Deepening. + Time typeclasses eauto 6 with nocore. Show Proof. + Undo. + Time eauto. (* does EApply H *) +Qed. + +(* Example from Nicolas Tabareau on coq-club - Feb 2016. + Full backtracking on dependent subgoals. + *) +Require Import Coq.Classes.Init. + +Module NTabareau. + +Set Typeclasses Dependency Order. +Unset Typeclasses Iterative Deepening. +Notation "x .1" := (projT1 x) (at level 3). +Notation "x .2" := (projT2 x) (at level 3). + +Parameter myType: Type. + +Class Foo (a:myType) := {}. + +Class Bar (a:myType) := {}. + +Class Qux (a:myType) := {}. + +Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}. + +Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}. + +Hint Extern 5 (Bar ?D.1) => + destruct D; simpl : typeclass_instances. + +Hint Extern 5 (Qux ?D.1) => + destruct D; simpl : typeclass_instances. + +Hint Extern 1 myType => + unshelve refine (fooTobar _ _).1 : typeclass_instances. + +Hint Extern 1 myType => unshelve refine (barToqux _ _).1 : typeclass_instances. + +Hint Extern 0 { x : _ & _ } => simple refine (existT _ _ _) : typeclass_instances. + +Unset Typeclasses Debug. +Definition trivial a (H : Foo a) : {b : myType & Qux b}. +Proof. + Time typeclasses eauto 10 with typeclass_instances. + Undo. Set Typeclasses Iterative Deepening. + Time typeclasses eauto with typeclass_instances. +Defined. + +End NTabareau. + +Module NTabareauClasses. + +Set Typeclasses Dependency Order. +Unset Typeclasses Iterative Deepening. +Notation "x .1" := (projT1 x) (at level 3). +Notation "x .2" := (projT2 x) (at level 3). + +Parameter myType: Type. +Existing Class myType. + +Class Foo (a:myType) := {}. + +Class Bar (a:myType) := {}. + +Class Qux (a:myType) := {}. + +Parameter fooTobar : forall a (H : Foo a), {b: myType & Bar b}. + +Parameter barToqux : forall a (H : Bar a), {b: myType & Qux b}. + +Hint Extern 5 (Bar ?D.1) => + destruct D; simpl : typeclass_instances. + +Hint Extern 5 (Qux ?D.1) => + destruct D; simpl : typeclass_instances. + +Hint Extern 1 myType => + unshelve notypeclasses refine (fooTobar _ _).1 : typeclass_instances. + +Hint Extern 1 myType => + unshelve notypeclasses refine (barToqux _ _).1 : typeclass_instances. + +Hint Extern 0 { x : _ & _ } => + unshelve notypeclasses refine (existT _ _ _) : typeclass_instances. + +Unset Typeclasses Debug. + +Definition trivial a (H : Foo a) : {b : myType & Qux b}. +Proof. + Time typeclasses eauto 10 with typeclass_instances. + Undo. Set Typeclasses Iterative Deepening. + (* Much faster in iteratove deepening mode *) + Time typeclasses eauto with typeclass_instances. +Defined. + +End NTabareauClasses. + + Require Import List. Parameter in_list : list (nat * nat) -> nat -> Prop. @@ -38,23 +216,6 @@ Hint Resolve lem1 lem2 lem3 lem4: essai. Goal forall (l : list (nat * nat)) (n p q : nat), not_in_list ((p, q) :: l) n -> not_in_list l n. -intros. - eauto with essai. -Qed. - -(* Example from Nicolas Magaud on coq-club - Jul 2000 *) - -Definition Nat : Set := nat. -Parameter S' : Nat -> Nat. -Parameter plus' : Nat -> Nat -> Nat. - -Lemma simpl_plus_l_rr1 : - (forall n0 : Nat, - (forall m p : Nat, plus' n0 m = plus' n0 p -> m = p) -> - forall m p : Nat, S' (plus' n0 m) = S' (plus' n0 p) -> m = p) -> - forall n : Nat, - (forall m p : Nat, plus' n m = plus' n p -> m = p) -> - forall m p : Nat, S' (plus' n m) = S' (plus' n p) -> m = p. -intros. - eauto. (* does EApply H *) + intros. + eauto with essai. Qed. diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 1f6af0dc..724e2998 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -14,6 +14,18 @@ Lemma lem1 : forall x y : T, {x = y} + {x <> y}. decide equality. Qed. +Lemma lem1' : forall x y : T, x = y \/ x <> y. + decide equality. +Qed. + +Lemma lem1'' : forall x y : T, {x <> y} + {x = y}. + decide equality. +Qed. + +Lemma lem1''' : forall x y : T, x <> y \/ x = y. + decide equality. +Qed. + Lemma lem2 : forall x y : T, {x = y} + {x <> y}. intros x y. decide equality. diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v new file mode 100644 index 00000000..86814051 --- /dev/null +++ b/test-suite/success/goal_selector.v @@ -0,0 +1,55 @@ +Inductive two : bool -> Prop := +| Zero : two false +| One : two true. + +Ltac dup := + let H := fresh in assert (forall (P : Prop), P -> P -> P) as H by (intros; trivial); + apply H; clear H. + +Lemma transform : two false <-> two true. +Proof. split; intros _; constructor. Qed. + +Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true. +Proof. + do 2 dup. + - repeat split. + 2, 4-99, 100-3:idtac. + 2-5:exact One. + par:exact Zero. + - repeat split. + 3-6:swap 1 4. + 1-5:swap 1 5. + 0-4:exact One. + all:exact Zero. + - repeat split. + 1, 3:exact Zero. + 1, 2, 3, 4: exact One. + - repeat split. + all:apply transform. + 2, 4, 6:apply transform. + all:apply transform. + 1-5:apply transform. + 1-6:exact One. +Qed. + +Goal True -> True. +Proof. + intros y; only 1-2 : repeat idtac. + 1-1:match goal with y : _ |- _ => let x := y in idtac x end. + Fail 1-1:let x := y in idtac x. + 1:let x := y in idtac x. + exact I. +Qed. + +Goal True /\ (True /\ True). +Proof. + dup. + - split; only 2: (split; exact I). + exact I. + - split; only 2: split; exact I. +Qed. + +Goal True -> exists (x : Prop), x. +Proof. + intro H; eexists ?[x]; only [x]: exact True. 1: assumption. +Qed. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index b8c6bf3f..1ed731f5 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -151,3 +151,46 @@ intros x H1 H. induction H. change (0 = z -> True) in IHrepr''. Abort. + +(* Test double induction *) + +(* This was failing in 8.5 and before because of a bug in the order of + hypotheses *) + +Inductive I2 : Type := + C2 : forall x:nat, x=x -> I2. +Goal forall a b:I2, a = b. +double induction a b. +Abort. + +(* This was leaving useless hypotheses in 8.5 and before because of + the same bug. This is a change of compatibility. *) + +Inductive I3 : Prop := + C3 : forall x:nat, x=x -> I3. +Goal forall a b:I3, a = b. +double induction a b. +Fail clear H. (* H should have been erased *) +Abort. + +(* This one had quantification in reverse order in 8.5 and before *) +(* This is a change of compatibility. *) + +Goal forall m n, le m n -> le n m -> n=m. +intros m n. double induction 1 2. +3:destruct 1. (* Should be "S m0 <= m0" *) +Abort. + +(* Idem *) + +Goal forall m n p q, le m n -> le p q -> n+p=m+q. +intros *. double induction 1 2. +3:clear H2. (* H2 should have been erased *) +Abort. + +(* This is unchanged *) + +Goal forall m n:nat, n=m. +double induction m n. +Abort. + diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 11156aa0..ee69df97 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -84,3 +84,47 @@ Qed. Goal forall x : nat, True. intros y%(fun x => x). Abort. + +(* Fixing a bug in the order of side conditions of a "->" step *) + +Goal (True -> 1=0) -> 1=1. +intros ->. +- reflexivity. +- exact I. +Qed. + +Goal forall x, (True -> x=0) -> 0=x. +intros x ->. +- reflexivity. +- exact I. +Qed. + +(* Fixing a bug when destructing a type with let-ins in the constructor *) + +Inductive I := C : let x:=1 in x=1 -> I. +Goal I -> True. +intros [x H]. (* Was failing in 8.5 *) +Abort. + +(* Ensuring that the (pat1,...,patn) intropatterns has the expected size, up + to skipping let-ins *) + +Goal I -> 1=1. +intros (H). (* This skips x *) +exact H. +Qed. + +Goal I -> 1=1. +Fail intros (x,H,H'). +Fail intros [|]. +intros (x,H). +exact H. +Qed. + +Goal Acc le 0 -> True. +Fail induction 1 as (n,H). (* Induction hypothesis is missing *) +induction 1 as (n,H,IH). +exact Logic.I. +Qed. + + diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index 5b0502cf..b88c142b 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -58,4 +58,5 @@ Qed. Lemma test b : b && true = b. Fail rewrite andb_true_l. - Admitted.
\ No newline at end of file + Admitted. +
\ No newline at end of file diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 6c4d4ae9..ce909905 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -15,7 +15,7 @@ Ltac F x := idtac; G x with G y := idtac; F y. (* Check that Match Context keeps a closure *) -Ltac U := let a := constr:I in +Ltac U := let a := constr:(I) in match goal with | |- _ => apply a end. @@ -75,7 +75,7 @@ Qed. (* Check context binding *) Ltac sym t := - match constr:t with + match constr:(t) with | context C[(?X1 = ?X2)] => context C [X1 = X2] end. @@ -143,7 +143,7 @@ Qed. Ltac check_binding y := cut ((fun y => y) = S). Goal True. -check_binding ipattern:H. +check_binding ipattern:(H). Abort. (* Check that variables explicitly parsed as ltac variables are not @@ -151,7 +151,7 @@ Abort. Ltac afi tac := intros; tac. Goal 1 = 2. -afi ltac:auto. +afi ltac:(auto). Abort. (* Tactic Notation avec listes *) @@ -174,7 +174,7 @@ Abort. empty args *) Goal True. -match constr:@None with @None => exact I end. +match constr:(@None) with @None => exact I end. Abort. (* Check second-order pattern unification *) @@ -218,7 +218,7 @@ Ltac Z1 t := set (x:=t). Ltac Z2 t := t. Goal True -> True. Z1 O. -Z2 ltac:O. +Z2 ltac:(O). exact I. Qed. @@ -302,7 +302,7 @@ Abort. (* Check instantiation of binders using ltac names *) Goal True. -let x := ipattern:y in assert (forall x y, x = y + 0). +let x := ipattern:(y) in assert (forall x y, x = y + 0). intro. destruct y. (* Check that the name is y here *) Abort. diff --git a/test-suite/success/ltacprof.v b/test-suite/success/ltacprof.v new file mode 100644 index 00000000..d5552695 --- /dev/null +++ b/test-suite/success/ltacprof.v @@ -0,0 +1,8 @@ +(** Some LtacProf tests *) + +Set Ltac Profiling. +Ltac multi := (idtac + idtac). +Goal True. + try (multi; fail). (* Used to result in: Anomaly: Uncaught exception Failure("hd"). Please report. *) +Admitted. +Show Ltac Profile. diff --git a/test-suite/success/onlyprinting.v b/test-suite/success/onlyprinting.v new file mode 100644 index 00000000..91a628d7 --- /dev/null +++ b/test-suite/success/onlyprinting.v @@ -0,0 +1,7 @@ +Notation "x ++ y" := (plus x y) (only printing). + +Fail Check 0 ++ 0. + +Notation "x + y" := (max x y) (only printing). + +Check (eq_refl : 42 + 18 = 60). diff --git a/test-suite/success/par_abstract.v b/test-suite/success/par_abstract.v new file mode 100644 index 00000000..7f6f9d62 --- /dev/null +++ b/test-suite/success/par_abstract.v @@ -0,0 +1,25 @@ +Axiom T : Type. + +Lemma foo : True * Type. +Proof. + split. + par: abstract (exact I || exact T). +Defined. + +(* Yes, these names are generated hence + the test is fragile. I want to assert + that abstract was correctly handled + by par: *) +Check foo_subproof. +Check foo_subproof0. +Check (refl_equal _ : + foo = + pair foo_subproof foo_subproof0). + +Lemma bar : True * Type. +Proof. + split. + par: (exact I || exact T). +Defined. +Check (refl_equal _ : + bar = pair I T). diff --git a/test-suite/success/paralleltac.v b/test-suite/success/paralleltac.v index 94ff96ef..d25fd32a 100644 --- a/test-suite/success/paralleltac.v +++ b/test-suite/success/paralleltac.v @@ -1,3 +1,17 @@ +Lemma test_nofail_like_all1 : + True /\ False. +Proof. +split. +all: trivial. +Admitted. + +Lemma test_nofail_like_all2 : + True /\ False. +Proof. +split. +par: trivial. +Admitted. + Fixpoint fib n := match n with | O => 1 | S m => match m with @@ -19,28 +33,28 @@ Lemma test_old x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x). Proof. repeat split. idtac "T1: linear". -Time all: solve_P. +Time all: solve [solve_P]. Qed. Lemma test_ok x : P (S x) /\ P (S x) /\ P (S x) /\ P (S x). Proof. repeat split. idtac "T2: parallel". -Time par: solve_P. +Time par: solve [solve_P]. Qed. Lemma test_fail x : P (S x) /\ P x /\ P (S x) /\ P (S x). Proof. repeat split. idtac "T3: linear failure". -Fail Time all: solve_P. -all: apply (P_triv Type). +Fail Time all: solve solve_P. +all: solve [apply (P_triv Type)]. Qed. Lemma test_fail2 x : P (S x) /\ P x /\ P (S x) /\ P (S x). Proof. repeat split. idtac "T4: parallel failure". -Fail Time par: solve_P. -all: apply (P_triv Type). +Fail Time par: solve [solve_P]. +all: solve [apply (P_triv Type)]. Qed. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 281d707c..2fa77049 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,19 +45,11 @@ 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. - -Fixpoint yn (n : nat) (y : Y) : Y := - match n with - | 0 => t - | S n => {| next := Some (yn n y) |} - end. +Proof. Fail reflexivity. Abort. -Lemma eta_ind' (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}. -Proof. reflexivity. Defined. +Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }. +Fail Scheme Fdef_rec := Induction for Fdef Sort Prop. (* Rules for parsing and printing of primitive projections and their eta expansions. diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v new file mode 100644 index 00000000..414c572f --- /dev/null +++ b/test-suite/success/programequality.v @@ -0,0 +1,13 @@ +Require Import Program. + +Axiom t : nat -> Set. + +Goal forall (x y : nat) (e : x = y) (e' : x = y) (P : t y -> x = y -> Type) + (a : t x), + P (eq_rect _ _ a _ e) e'. +Proof. + intros. + pi_eq_proofs. clear e. + destruct e'. simpl. + change (P a eq_refl). +Abort.
\ No newline at end of file diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v index 0befe054..b26a9ff1 100644 --- a/test-suite/success/remember.v +++ b/test-suite/success/remember.v @@ -14,3 +14,16 @@ let name := fresh "fresh" in remember (1 + 2) as x eqn:name. rewrite fresh. Abort. + +(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *) + +Module A. +Axiom N : nat. +End A. +Module B. +Include A. +End B. +Goal id A.N = B.N. +reflexivity. +Qed. + diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 0465c4b3..1f24ef2a 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -166,3 +166,16 @@ Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort. Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort. +(* This should not raise an anomaly as it did for some time in early 2016 *) + +Definition t := nat -> bool. +Definition h (a b : t) := forall n, a n = b n. + +Instance subrelh : subrelation h (Morphisms.pointwise_relation nat eq). +Proof. intros x y H; assumption. Qed. + +Goal forall a b, h a b -> a 0 = b 0. +intros. +setoid_rewrite H. (* Fallback on ordinary rewrite without anomaly *) +reflexivity. +Qed. diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v new file mode 100644 index 00000000..3f6b9cb3 --- /dev/null +++ b/test-suite/success/shrink_abstract.v @@ -0,0 +1,13 @@ +Set Shrink Abstract. + +Definition foo : forall (n m : nat), bool. +Proof. +pose (p := 0). +intros n. +pose (q := n). +intros m. +pose (r := m). +abstract (destruct m; [left|right]). +Defined. + +Check (foo_subproof : nat -> bool). diff --git a/test-suite/success/shrink_obligations.v b/test-suite/success/shrink_obligations.v new file mode 100644 index 00000000..676b9787 --- /dev/null +++ b/test-suite/success/shrink_obligations.v @@ -0,0 +1,28 @@ +Require Program. + +Obligation Tactic := idtac. + +Set Shrink Obligations. + +Program Definition foo (m : nat) (p := S m) (n : nat) (q := S n) : unit := +let bar : {r | n < r} := _ in +let qux : {r | p < r} := _ in +let quz : m = n -> True := _ in +tt. +Next Obligation. +intros m p n q. +exists (S n); constructor. +Qed. +Next Obligation. +intros m p n q. +exists (S (S m)); constructor. +Qed. +Next Obligation. +intros m p n q ? ? H. +destruct H. +constructor. +Qed. + +Check (foo_obligation_1 : forall n, {r | n < r}). +Check (foo_obligation_2 : forall m, {r | (S m) < r}). +Check (foo_obligation_3 : forall m n, m = n -> True). diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v index d4191b93..2728672f 100644 --- a/test-suite/success/simpl_tuning.v +++ b/test-suite/success/simpl_tuning.v @@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end. Abort. Definition volatile := fun x : nat => x. -Arguments volatile /. +Arguments volatile / _. Lemma foo : volatile = volatile. simpl. diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 3faa1ca4..fba05cd9 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -64,3 +64,11 @@ assert (H:=H I). match goal with H:_ |- _ => clear H end. match goal with H:_ |- _ => exact H end. Qed. + +(* Test specialize as *) + +Goal (forall x, x=0) -> 1=0. +intros. +specialize (H 1) as ->. +reflexivity. +Qed. diff --git a/test-suite/success/ssrpattern.v b/test-suite/success/ssrpattern.v new file mode 100644 index 00000000..96f0bbac --- /dev/null +++ b/test-suite/success/ssrpattern.v @@ -0,0 +1,22 @@ +Require Import ssrmatching. + +(*Set Debug SsrMatching.*) + +Tactic Notation "at" "[" ssrpatternarg(pat) "]" tactic(t) := + let name := fresh in + let def_name := fresh in + ssrpattern pat; + intro name; + pose proof (refl_equal name) as def_name; + unfold name at 1 in def_name; + t def_name; + [ rewrite <- def_name | idtac.. ]; + clear name def_name. + +Lemma test (H : True -> True -> 3 = 7) : 28 = 3 * 4. +Proof. +at [ X in X * 4 ] ltac:(fun place => rewrite -> H in place). +- reflexivity. +- trivial. +- trivial. +Qed. diff --git a/test-suite/success/subst.v b/test-suite/success/subst.v new file mode 100644 index 00000000..25ee81b5 --- /dev/null +++ b/test-suite/success/subst.v @@ -0,0 +1,42 @@ +(* Test various subtleties of the "subst" tactics *) + +(* Should proceed from left to right (see #4222) *) +Goal forall x y, x = y -> x = 3 -> y = 2 -> x = y. +intros. +subst. +change (3 = 2) in H1. +change (3 = 3). +Abort. + +(* Should work with "x = y" and "x = t" equations (see #4214, failed in 8.4) *) +Goal forall x y, x = y -> x = 3 -> x = y. +intros. +subst. +change (3 = 3). +Abort. + +(* Should substitute cycles once, until a recursive equation is obtained *) +(* (failed in 8.4) *) +Goal forall x y, x = S y -> y = S x -> x = y. +intros. +subst. +change (y = S (S y)) in H0. +change (S y = y). +Abort. + +(* A bug revealed by OCaml 4.03 warnings *) +(* fixes in 4e3d464 and 89ec88f for v8.5, 4e3d4646 and 89ec88f1e for v8.6 *) +Goal forall y, let x:=0 in y=x -> y=y. +intros * H; +(* This worked as expected *) +subst. +Fail clear H. +Abort. + +Goal forall y, let x:=0 in x=y -> y=y. +intros * H; +(* Before the fix, this unfolded x instead of + substituting y and erasing H *) +subst. +Fail clear H. +Abort. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index e00701fb..269359ae 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/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v index 58fa3974..62df96c0 100644 --- a/test-suite/success/vm_univ_poly.v +++ b/test-suite/success/vm_univ_poly.v @@ -38,8 +38,8 @@ Definition _4 : 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. +| PSome : T -> poption T +| PNone : poption T. Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T := match p with @@ -49,7 +49,7 @@ Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} := | pnil -| pcons : T -> plist@{i} T -> plist@{i} T. +| pcons : T -> plist T -> plist T. Arguments pnil {_}. Arguments pcons {_} _ _. @@ -59,7 +59,7 @@ Polymorphic Definition pmap@{i j} 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) + | @pcons _ l ls => @pcons@{j} U (f l) (pmap ls) end. Universe Ubool. @@ -75,7 +75,7 @@ Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) p Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} := | Empty -| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T. +| Branch : plist@{i} (Tree T) -> Tree T. Polymorphic Definition pfold@{i u} {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) := @@ -111,7 +111,7 @@ Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i} 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')) + | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree n')) end. Eval compute in height (big_tree (S (S (S O)))). |