diff options
Diffstat (limited to 'test-suite/success')
42 files changed, 712 insertions, 587 deletions
diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v index b4efa7ed..d0aa5c85 100644 --- a/test-suite/success/AdvancedTypeClasses.v +++ b/test-suite/success/AdvancedTypeClasses.v @@ -28,8 +28,8 @@ Class interp_pair (abs : Type) := { repr : term; link: abs = interp repr }. -Implicit Arguments repr [[interp_pair]]. -Implicit Arguments link [[interp_pair]]. +Arguments repr _ {interp_pair}. +Arguments link _ {interp_pair}. Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)). simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity. diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v index ed035f52..2f7425bc 100644 --- a/test-suite/success/BracketsWithGoalSelector.v +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -14,3 +14,12 @@ Proof. Fail Qed. } Qed. + +Lemma foo (n: nat) (P : nat -> Prop): + P n. +Proof. + intros. + refine (nat_ind _ ?[Base] ?[Step] _). + [Base]: { admit. } + [Step]: { admit. } +Abort. diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v index 445ffac8..fbe909ec 100644 --- a/test-suite/success/Case11.v +++ b/test-suite/success/Case11.v @@ -5,9 +5,9 @@ Section A. Variables (Alpha : Set) (Beta : Set). -Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) : +Definition nodep_prod_of_dep (c : sigT (fun a : Alpha => Beta)) : Alpha * Beta := match c with - | existS _ a b => (a, b) + | existT _ a b => (a, b) end. End A. diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v index 861d0466..a4efcca9 100644 --- a/test-suite/success/Case17.v +++ b/test-suite/success/Case17.v @@ -1,5 +1,5 @@ (* Check the synthesis of predicate from a cast in case of matching of - the first component (here [list bool]) of a dependent type (here [sigS]) + the first component (here [list bool]) of a dependent type (here [sigT]) (Simplification of an example from file parsing2.v of the Coq'Art exercises) *) @@ -19,10 +19,10 @@ Axiom HHH : forall A : Prop, A. Check (match rec l0 (HHH _) with - | inleft (existS _ (false :: l1) _) => inright _ (HHH _) - | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) => + | inleft (existT _ (false :: l1) _) => inright _ (HHH _) + | inleft (existT _ (true :: l1) (exist _ t1 (conj Hp Hl))) => inright _ (HHH _) - | inleft (existS _ _ _) => inright _ (HHH _) + | inleft (existT _ _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end :{l'' : list bool & @@ -39,10 +39,10 @@ Check {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) => match rec l0 (HHH _) with - | inleft (existS _ (false :: l1) _) => inright _ (HHH _) - | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) => + | inleft (existT _ (false :: l1) _) => inright _ (HHH _) + | inleft (existT _ (true :: l1) (exist _ t1 (conj Hp Hl))) => inright _ (HHH _) - | inleft (existS _ _ _) => inright _ (HHH _) + | inleft (existT _ _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end :{l'' : list bool & diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v new file mode 100644 index 00000000..e2045900 --- /dev/null +++ b/test-suite/success/Compat88.v @@ -0,0 +1,18 @@ +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(** Check that various syntax usage is available without importing + relevant files. *) +Require Coq.Strings.Ascii Coq.Strings.String. +Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. +Require Coq.Reals.Rdefinitions. +Require Coq.Numbers.Cyclic.Int31.Cyclic31. + +Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *) + +Check String.String "a" String.EmptyString. +Check String.eqb "a" "a". +Check Nat.eqb 1 1. +Check BinNat.N.eqb 1 1. +Check BinInt.Z.eqb 1 1. +Check BinPos.Pos.eqb 1 1. +Check Rdefinitions.Rplus 1 1. +Check Int31.iszero 1. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 288c9d1d..5650dba2 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(* -*- coq-prog-args: ("-compat" "8.9") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq88. +Import Coq.Compat.Coq89. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index b7bbc505..37d50ee6 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.6") -*- *) +(* -*- coq-prog-args: ("-compat" "8.7") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq89. Import Coq.Compat.Coq88. Import Coq.Compat.Coq87. -Import Coq.Compat.Coq86. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 9cfe6039..99813883 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.7") -*- *) +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq89. Import Coq.Compat.Coq88. -Import Coq.Compat.Coq87. diff --git a/test-suite/success/FunindExtraction_compat86.v b/test-suite/success/FunindExtraction_compat86.v deleted file mode 100644 index 8912197d..00000000 --- a/test-suite/success/FunindExtraction_compat86.v +++ /dev/null @@ -1,506 +0,0 @@ -(* -*- coq-prog-args: ("-compat" "8.6") -*- *) - -Definition iszero (n : nat) : bool := - match n with - | O => true - | _ => false - end. - -Functional Scheme iszero_ind := Induction for iszero Sort Prop. - -Lemma toto : forall n : nat, n = 0 -> iszero n = true. -intros x eg. - functional induction iszero x; simpl. -trivial. -inversion eg. -Qed. - - -Function ftest (n m : nat) : nat := - match n with - | O => match m with - | O => 0 - | _ => 1 - end - | S p => 0 - end. -(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *) - -Lemma test1 : forall n m : nat, ftest n m <= 2. -intros n m. - functional induction ftest n m; auto. -Qed. - -Lemma test2 : forall m n, ~ 2 = ftest n m. -Proof. -intros n m;intro H. -functional inversion H ftest. -Qed. - -Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0) \/ n <> 0. -Proof. -functional inversion 1 ftest;auto. -Qed. - - -Require Import Arith. -Lemma test11 : forall m : nat, ftest 0 m <= 2. -intros m. - functional induction ftest 0 m. -auto. -auto. -auto with *. -Qed. - -Function lamfix (m n : nat) {struct n } : nat := - match n with - | O => m - | S p => lamfix m p - end. - -(* Parameter v1 v2 : nat. *) - -Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1. -intros v1 v2. - functional induction lamfix v1 v2. -trivial. -assumption. -Defined. - - - -(* polymorphic function *) -Require Import List. - -Functional Scheme app_ind := Induction for app Sort Prop. - -Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'. -intros A l l'. - functional induction app A l l'; intuition. - rewrite <- H0; trivial. -Qed. - - - - - -Require Export Arith. - - -Function trivfun (n : nat) : nat := - match n with - | O => 0 - | S m => trivfun m - end. - - -(* essaie de parametre variables non locaux:*) - -Parameter varessai : nat. - -Lemma first_try : trivfun varessai = 0. - functional induction trivfun varessai. -trivial. -assumption. -Defined. - - - Functional Scheme triv_ind := Induction for trivfun Sort Prop. - -Lemma bisrepetita : forall n' : nat, trivfun n' = 0. -intros n'. - functional induction trivfun n'. -trivial. -assumption. -Qed. - - - - - - - -Function iseven (n : nat) : bool := - match n with - | O => true - | S (S m) => iseven m - | _ => false - end. - - -Function funex (n : nat) : nat := - match iseven n with - | true => n - | false => match n with - | O => 0 - | S r => funex r - end - end. - - -Function nat_equal_bool (n m : nat) {struct n} : bool := - match n with - | O => match m with - | O => true - | _ => false - end - | S p => match m with - | O => false - | S q => nat_equal_bool p q - end - end. - - -Require Export Div2. -Require Import Nat. -Functional Scheme div2_ind := Induction for div2 Sort Prop. -Lemma div2_inf : forall n : nat, div2 n <= n. -intros n. - functional induction div2 n. -auto. -auto. - -apply le_S. -apply le_n_S. -exact IHn0. -Qed. - -(* reuse this lemma as a scheme:*) - -Function nested_lam (n : nat) : nat -> nat := - match n with - | O => fun m : nat => 0 - | S n' => fun m : nat => m + nested_lam n' m - end. - - -Lemma nest : forall n m : nat, nested_lam n m = n * m. -intros n m. - functional induction nested_lam n m; simpl;auto. -Qed. - - -Function essai (x : nat) (p : nat * nat) {struct x} : nat := - let (n, m) := (p: nat*nat) in - match n with - | O => 0 - | S q => match x with - | O => 1 - | S r => S (essai r (q, m)) - end - end. - -Lemma essai_essai : - forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p. -intros x p. - functional induction essai x p; intros. -inversion H. -auto with arith. - auto with arith. -Qed. - -Function plus_x_not_five'' (n m : nat) {struct n} : nat := - let x := nat_equal_bool m 5 in - let y := 0 in - match n with - | O => y - | S q => - let recapp := plus_x_not_five'' q m in - match x with - | true => S recapp - | false => S recapp - end - end. - -Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. -intros a b. - functional induction plus_x_not_five'' a b; intros hyp; simpl; auto. -Qed. - -Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. -intros n m. - functional induction nat_equal_bool n m; simpl; intros hyp; auto. -rewrite <- hyp in y; simpl in y;tauto. -inversion hyp. -Qed. - -Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. -intros n m. - functional induction nat_equal_bool n m; simpl; intros eg; auto. -inversion eg. -inversion eg. -Qed. - - -Inductive istrue : bool -> Prop := - istrue0 : istrue true. - -Functional Scheme add_ind := Induction for add Sort Prop. - -Lemma inf_x_plusxy' : forall x y : nat, x <= x + y. -intros n m. - functional induction add n m; intros. -auto with arith. -auto with arith. -Qed. - - -Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. -intros n. -unfold plus. - functional induction plus n 0; intros. -auto with arith. -apply le_n_S. -assumption. -Qed. - -Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x. -intros n. - functional induction plus 0 n; intros; auto with arith. -Qed. - -Function mod2 (n : nat) : nat := - match n with - | O => 0 - | S (S m) => S (mod2 m) - | _ => 0 - end. - -Lemma princ_mod2 : forall n : nat, mod2 n <= n. -intros n. - functional induction mod2 n; simpl; auto with arith. -Qed. - -Function isfour (n : nat) : bool := - match n with - | S (S (S (S O))) => true - | _ => false - end. - -Function isononeorfour (n : nat) : bool := - match n with - | S O => true - | S (S (S (S O))) => true - | _ => false - end. - -Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). -intros n. - functional induction isononeorfour n; intros istr; simpl; - inversion istr. -apply istrue0. -destruct n. inversion istr. -destruct n. tauto. -destruct n. inversion istr. -destruct n. inversion istr. -destruct n. tauto. -simpl in *. inversion H0. -Qed. - -Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n). -intros n. - functional induction isononeorfour n; intros m istr; inversion istr. -apply istrue0. -rewrite H in y; simpl in y;tauto. -Qed. - -Function ftest4 (n m : nat) : nat := - match n with - | O => match m with - | O => 0 - | S q => 1 - end - | S p => match m with - | O => 0 - | S r => 1 - end - end. - -Lemma test4 : forall n m : nat, ftest n m <= 2. -intros n m. - functional induction ftest n m; auto with arith. -Qed. - -Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2. -intros n m. -assert ({n0 | n0 = S n}). -exists (S n);reflexivity. -destruct H as [n0 H1]. -rewrite <- H1;revert H1. - functional induction ftest4 n0 m. -inversion 1. -inversion 1. - -auto with arith. -auto with arith. -Qed. - -Function ftest44 (x : nat * nat) (n m : nat) : nat := - let (p, q) := (x: nat*nat) in - match n with - | O => match m with - | O => 0 - | S q => 1 - end - | S p => match m with - | O => 0 - | S r => 1 - end - end. - -Lemma test44 : - forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2. -intros pq n m o r s. - functional induction ftest44 pq n (S m). -auto with arith. -auto with arith. -auto with arith. -auto with arith. -Qed. - -Function ftest2 (n m : nat) {struct n} : nat := - match n with - | O => match m with - | O => 0 - | S q => 0 - end - | S p => ftest2 p m - end. - -Lemma test2' : forall n m : nat, ftest2 n m <= 2. -intros n m. - functional induction ftest2 n m; simpl; intros; auto. -Qed. - -Function ftest3 (n m : nat) {struct n} : nat := - match n with - | O => 0 - | S p => match m with - | O => ftest3 p 0 - | S r => 0 - end - end. - -Lemma test3' : forall n m : nat, ftest3 n m <= 2. -intros n m. - functional induction ftest3 n m. -intros. -auto. -intros. -auto. -intros. -simpl. -auto. -Qed. - -Function ftest5 (n m : nat) {struct n} : nat := - match n with - | O => 0 - | S p => match m with - | O => ftest5 p 0 - | S r => ftest5 p r - end - end. - -Lemma test5 : forall n m : nat, ftest5 n m <= 2. -intros n m. - functional induction ftest5 n m. -intros. -auto. -intros. -auto. -intros. -simpl. -auto. -Qed. - -Function ftest7 (n : nat) : nat := - match ftest5 n 0 with - | O => 0 - | S r => 0 - end. - -Lemma essai7 : - forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2) - (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) - (n : nat), ftest7 n <= 2. -intros hyp1 hyp2 n. - functional induction ftest7 n; auto. -Qed. - -Function ftest6 (n m : nat) {struct n} : nat := - match n with - | O => 0 - | S p => match ftest5 p 0 with - | O => ftest6 p 0 - | S r => ftest6 p r - end - end. - - -Lemma princ6 : - (forall n m : nat, n = 0 -> ftest6 0 m <= 2) -> - (forall n m p : nat, - ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) -> - (forall n m p r : nat, - ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) -> - forall x y : nat, ftest6 x y <= 2. -intros hyp1 hyp2 hyp3 n m. -generalize hyp1 hyp2 hyp3. -clear hyp1 hyp2 hyp3. - functional induction ftest6 n m; auto. -Qed. - -Lemma essai6 : forall n m : nat, ftest6 n m <= 2. -intros n m. - functional induction ftest6 n m; simpl; auto. -Qed. - -(* Some tests with modules *) -Module M. -Function test_m (n:nat) : nat := - match n with - | 0 => 0 - | S n => S (S (test_m n)) - end. - -Lemma test_m_is_double : forall n, div2 (test_m n) = n. -Proof. -intros n. -functional induction (test_m n). -reflexivity. -simpl;rewrite IHn0;reflexivity. -Qed. -End M. -(* We redefine a new Function with the same name *) -Function test_m (n:nat) : nat := - pred n. - -Lemma test_m_is_pred : forall n, test_m n = pred n. -Proof. -intro n. -functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*) -reflexivity. -Qed. - -(* Checks if the dot notation are correctly treated in infos *) -Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n. -intro n. -(* here we should apply M.test_m_ind *) -functional induction (M.test_m n). -reflexivity. -simpl;rewrite IHn0;reflexivity. -Qed. - -Import M. -(* Now test_m is the one which defines double *) - -Lemma test_m_is_double : forall n, div2 (M.test_m n) = n. -intro n. -(* here we should apply M.test_m_ind *) -functional induction (test_m n). -reflexivity. -simpl;rewrite IHn0;reflexivity. -Qed. - -Extraction iszero. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 8d08f597..2f13b7c2 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -183,3 +183,33 @@ End HintCut. Goal forall (m : nat), exists n, m = n /\ m = n. intros m; eexists; split; [trivial | reflexivity]. Qed. + +Section HintTransparent. + + Definition fn (x : nat) := S x. + + Create HintDb trans. + + Hint Resolve eq_refl | (_ = _) : trans. + + (* No reduction *) + Hint Variables Opaque : trans. Hint Constants Opaque : trans. + + Goal forall x : nat, fn x = S x. + Proof. + intros. + Fail typeclasses eauto with trans. + unfold fn. + typeclasses eauto with trans. + Qed. + + (** Now allow unfolding fn *) + Hint Constants Transparent : trans. + + Goal forall x : nat, fn x = S x. + Proof. + intros. + typeclasses eauto with trans. + Qed. + +End HintTransparent. diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v index 921433ca..9a19b595 100644 --- a/test-suite/success/ImplicitArguments.v +++ b/test-suite/success/ImplicitArguments.v @@ -2,7 +2,7 @@ Inductive vector {A : Type} : nat -> Type := | vnil : vector 0 | vcons : A -> forall {n'}, vector n' -> vector (S n'). -Implicit Arguments vector []. +Arguments vector A : clear implicits. Require Import Coq.Program.Program. diff --git a/test-suite/success/ImplicitTactic.v b/test-suite/success/ImplicitTactic.v deleted file mode 100644 index d8fa3043..00000000 --- a/test-suite/success/ImplicitTactic.v +++ /dev/null @@ -1,16 +0,0 @@ -(* A Wiedijk-Cruz-Filipe style tactic for solving implicit arguments *) - -(* Declare a term expression with a hole *) -Parameter quo : nat -> forall n:nat, n<>0 -> nat. -Notation "x / y" := (quo x y _) : nat_scope. - -(* Declare the tactic for resolving implicit arguments still - unresolved after type-checking; it must complete the subgoal to - succeed *) -Declare Implicit Tactic assumption. - -Goal forall n d, d<>0 -> { q:nat & { r:nat | d * q + r = n }}. -intros. -(* Here, assumption is used to solve the implicit argument of quo *) -exists (n / d). - diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 5b1482fd..c2130995 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -1,7 +1,5 @@ (* Test des definitions inductives imbriquees *) -Require Import List. - Inductive X : Set := cons1 : list X -> X. @@ -73,7 +71,7 @@ CoInductive LList (A : Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. -Implicit Arguments LNil [A]. +Arguments LNil [A]. Inductive Finite (A : Set) : LList A -> Prop := | Finite_LNil : Finite LNil diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 78652fb6..7ee471ba 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -19,8 +19,8 @@ Qed. (* Check that no tuple needs to be built *) Lemma l3 : forall x y : nat, - existS (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) = - existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) -> + existT (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) = + existT (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) -> x = y. intros x y H. injection H. @@ -30,10 +30,10 @@ Qed. (* Check that a tuple is built (actually the same as the initial one) *) Lemma l4 : forall p1 p2 : {0 = 0} + {0 = 0}, - existS (fun n : nat => {n = n} + {n = n}) 0 p1 = - existS (fun n : nat => {n = n} + {n = n}) 0 p2 -> - existS (fun n : nat => {n = n} + {n = n}) 0 p1 = - existS (fun n : nat => {n = n} + {n = n}) 0 p2. + existT (fun n : nat => {n = n} + {n = n}) 0 p1 = + existT (fun n : nat => {n = n} + {n = n}) 0 p2 -> + existT (fun n : nat => {n = n} + {n = n}) 0 p1 = + existT (fun n : nat => {n = n} + {n = n}) 0 p2. intros. injection H. exact (fun H => H). diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 45c71615..ee540d71 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := | in_first : forall e, in_extension r (add_rule r e) | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Implicit Arguments NL [I]. +Arguments NL [I]. Inductive super_extension (I : Set) (e : extension I) : extension I -> Type := @@ -107,6 +107,7 @@ Goal forall o, foo2 o -> 0 = 1. intros. eapply trans_eq. inversion H. +Abort. (* Check that the part of "injection" that is called by "inversion" does the same number of intros as the number of equations @@ -136,6 +137,7 @@ Goal True -> True. intro. Fail inversion H using False. Fail inversion foo using True_ind. +Abort. (* Was failing at some time between 7 and 10 September 2014 *) (* even though, it is not clear that the resulting context is interesting *) diff --git a/test-suite/success/Fourier.v b/test-suite/success/LraTest.v index b63bead4..bf3a87da 100644 --- a/test-suite/success/Fourier.v +++ b/test-suite/success/LraTest.v @@ -1,12 +1,14 @@ -Require Import Rfunctions. -Require Import Fourier. +Require Import Reals. +Require Import Lra. + +Open Scope R_scope. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). -intros; split_Rabs; fourier. +intros; split_Rabs; lra. Qed. Lemma l2 : forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1. intros. -split_Rabs; fourier. +split_Rabs; lra. Qed. diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v new file mode 100644 index 00000000..633a5e47 --- /dev/null +++ b/test-suite/success/LtacDeprecation.v @@ -0,0 +1,32 @@ +Set Warnings "+deprecated". + +#[deprecated(since = "8.8", note = "Use idtac instead")] +Ltac foo x := idtac. + +Goal True. +Fail (foo true). +Abort. + +Fail Ltac bar := foo. +Fail Tactic Notation "bar" := foo. + +#[deprecated(since = "8.8", note = "Use idtac instead")] +Tactic Notation "bar" := idtac. + +Goal True. +Fail bar. +Abort. + +Fail Ltac zar := bar. + +Set Warnings "-deprecated". + +Ltac zar := foo. +Ltac zarzar := bar. + +Set Warnings "+deprecated". + +Goal True. +zar x. +zarzar. +Abort. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 7c2cf3ee..1b33863e 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -126,3 +126,31 @@ Notation "'myexists' x , p" := (ex (fun x => p)) (at level 200, x ident, p at level 200, right associativity) : type_scope. Check myexists I, I = 0. (* Should not be seen as a constructor *) End M14. + +(* 15. Testing different ways to give the same levels without failing *) + +Module M15. + Local Notation "###### x" := (S x) (right associativity, at level 79, x at next level). + Fail Local Notation "###### x" := (S x) (right associativity, at level 79). + Local Notation "###### x" := (S x) (at level 79). +End M15. + +(* 16. Some test about custom entries *) +Module M16. + (* Test locality *) + Local Declare Custom Entry foo. + Fail Notation "#" := 0 (in custom foo). (* Should be local *) + Local Notation "#" := 0 (in custom foo). + + (* Test import *) + Module A. + Declare Custom Entry foo2. + End A. + Fail Notation "##" := 0 (in custom foo2). + Import A. + Local Notation "##" := 0 (in custom foo2). + + (* Test Print Grammar *) + Print Grammar foo. + Print Grammar foo2. +End M16. diff --git a/test-suite/success/NumeralNotations.v b/test-suite/success/NumeralNotations.v new file mode 100644 index 00000000..47ef3812 --- /dev/null +++ b/test-suite/success/NumeralNotations.v @@ -0,0 +1,302 @@ +(* Test that we fail, rather than raising anomalies, on opaque terms during interpretation *) + +(* https://github.com/coq/coq/pull/8064#discussion_r202497516 *) +Module Test1. + Axiom hold : forall {A B C}, A -> B -> C. + Definition opaque3 (x : Decimal.int) : Decimal.int := hold x (fix f (x : nat) : nat := match x with O => O | S n => S (f n) end). + Numeral Notation Decimal.int opaque3 opaque3 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Fail Check 1%opaque. +End Test1. + +(* https://github.com/coq/coq/pull/8064#discussion_r202497990 *) +Module Test2. + Axiom opaque4 : option Decimal.int. + Definition opaque6 (x : Decimal.int) : option Decimal.int := opaque4. + Numeral Notation Decimal.int opaque6 opaque6 : opaque_scope. + Delimit Scope opaque_scope with opaque. + Open Scope opaque_scope. + Fail Check 1%opaque. +End Test2. + +Module Test3. + Inductive silly := SILLY (v : Decimal.uint) (f : forall A, A -> A). + Definition to_silly (v : Decimal.uint) := SILLY v (fun _ x => x). + Definition of_silly (v : silly) := match v with SILLY v _ => v end. + Numeral Notation silly to_silly of_silly : silly_scope. + Delimit Scope silly_scope with silly. + Fail Check 1%silly. +End Test3. + + +Module Test4. + Polymorphic NonCumulative Inductive punit := ptt. + Polymorphic Definition pto_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Polymorphic Definition pto_punit_all (v : Decimal.uint) : punit := ptt. + Polymorphic Definition pof_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Definition to_punit (v : Decimal.uint) : option punit := match Nat.of_uint v with O => Some ptt | _ => None end. + Definition of_punit (v : punit) : Decimal.uint := Nat.to_uint 0. + Polymorphic Definition pto_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Polymorphic Definition pof_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Definition to_unit (v : Decimal.uint) : option unit := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_unit (v : unit) : Decimal.uint := Nat.to_uint 0. + Numeral Notation punit to_punit of_punit : pto. + Numeral Notation punit pto_punit of_punit : ppo. + Numeral Notation punit to_punit pof_punit : ptp. + Numeral Notation punit pto_punit pof_punit : ppp. + Numeral Notation unit to_unit of_unit : uto. + Delimit Scope pto with pto. + Delimit Scope ppo with ppo. + Delimit Scope ptp with ptp. + Delimit Scope ppp with ppp. + Delimit Scope uto with uto. + Check let v := 0%pto in v : punit. + Check let v := 0%ppo in v : punit. + Check let v := 0%ptp in v : punit. + Check let v := 0%ppp in v : punit. + Check let v := 0%uto in v : unit. + Fail Check 1%uto. + Fail Check (-1)%uto. + Numeral Notation unit pto_unit of_unit : upo. + Numeral Notation unit to_unit pof_unit : utp. + Numeral Notation unit pto_unit pof_unit : upp. + Delimit Scope upo with upo. + Delimit Scope utp with utp. + Delimit Scope upp with upp. + Check let v := 0%upo in v : unit. + Check let v := 0%utp in v : unit. + Check let v := 0%upp in v : unit. + + Polymorphic Definition pto_punits := pto_punit_all@{Set}. + Polymorphic Definition pof_punits := pof_punit@{Set}. + Numeral Notation punit pto_punits pof_punits : ppps (abstract after 1). + Delimit Scope ppps with ppps. + Universe u. + Constraint Set < u. + Check let v := 0%ppps in v : punit@{u}. (* Check that universes are refreshed *) + Fail Check let v := 1%ppps in v : punit@{u}. (* Note that universes are not refreshed here *) +End Test4. + +Module Test5. + Check S. (* At one point gave Error: Anomaly "Uncaught exception Pretype_errors.PretypeError(_, _, _)." Please report at http://coq.inria.fr/bugs/. *) +End Test5. + +Module Test6. + (* Check that numeral notations on enormous terms don't take forever to print/parse *) + (* Ackerman definition from https://stackoverflow.com/a/10303475/377022 *) + Fixpoint ack (n m : nat) : nat := + match n with + | O => S m + | S p => let fix ackn (m : nat) := + match m with + | O => ack p 1 + | S q => ack p (ackn q) + end + in ackn m + end. + + Timeout 1 Check (S (ack 4 4)). (* should be instantaneous *) + + Local Set Primitive Projections. + Record > wnat := wrap { unwrap :> nat }. + Definition to_uint (x : wnat) : Decimal.uint := Nat.to_uint x. + Definition of_uint (x : Decimal.uint) : wnat := Nat.of_uint x. + Module Export Scopes. + Delimit Scope wnat_scope with wnat. + End Scopes. + Module Export Notations. + Export Scopes. + Numeral Notation wnat of_uint to_uint : wnat_scope (abstract after 5000). + End Notations. + Check let v := 0%wnat in v : wnat. + Check wrap O. + Timeout 1 Check wrap (ack 4 4). (* should be instantaneous *) +End Test6. + +Module Test6_2. + Import Test6.Scopes. + Check Test6.wrap 0. + Import Test6.Notations. + Check let v := 0%wnat in v : Test6.wnat. +End Test6_2. + +Module Test7. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint_scope with wuint. + Numeral Notation wuint wrap unwrap : wuint_scope. + Check let v := 0%wuint in v : wuint. + Check let v := 1%wuint in v : wuint. +End Test7. + +Module Test8. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Delimit Scope wuint8_scope with wuint8. + Delimit Scope wuint8'_scope with wuint8'. + Section with_var. + Context (dummy : unit). + Definition wrap' := let __ := dummy in wrap. + Definition unwrap' := let __ := dummy in unwrap. + Numeral Notation wuint wrap' unwrap' : wuint8_scope. + Check let v := 0%wuint8 in v : wuint. + End with_var. + Check let v := 0%wuint8 in v : nat. + Fail Check let v := 0%wuint8 in v : wuint. + Compute wrap (Nat.to_uint 0). + + Notation wrap'' := wrap. + Notation unwrap'' := unwrap. + Numeral Notation wuint wrap'' unwrap'' : wuint8'_scope. + Check let v := 0%wuint8' in v : wuint. +End Test8. + +Module Test9. + Delimit Scope wuint9_scope with wuint9. + Delimit Scope wuint9'_scope with wuint9'. + Section with_let. + Local Set Primitive Projections. + Record wuint := wrap { unwrap : Decimal.uint }. + Let wrap' := wrap. + Let unwrap' := unwrap. + Local Notation wrap'' := wrap. + Local Notation unwrap'' := unwrap. + Numeral Notation wuint wrap' unwrap' : wuint9_scope. + Check let v := 0%wuint9 in v : wuint. + Numeral Notation wuint wrap'' unwrap'' : wuint9'_scope. + Check let v := 0%wuint9' in v : wuint. + End with_let. + Check let v := 0%wuint9 in v : nat. + Fail Check let v := 0%wuint9 in v : wuint. +End Test9. + +Module Test10. + (* Test that it is only a warning to add abstract after to an optional parsing function *) + Definition to_uint (v : unit) := Nat.to_uint 0. + Definition of_uint (v : Decimal.uint) := match Nat.of_uint v with O => Some tt | _ => None end. + Definition of_any_uint (v : Decimal.uint) := tt. + Delimit Scope unit_scope with unit. + Delimit Scope unit2_scope with unit2. + Numeral Notation unit of_uint to_uint : unit_scope (abstract after 1). + Local Set Warnings Append "+abstract-large-number-no-op". + (* Check that there is actually a warning here *) + Fail Numeral Notation unit of_uint to_uint : unit2_scope (abstract after 1). + (* Check that there is no warning here *) + Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1). +End Test10. + +Module Test11. + (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *) + Inductive unit11 := tt11. + Delimit Scope unit11_scope with unit11. + Goal True. + evar (to_uint : unit11 -> Decimal.uint). + evar (of_uint : Decimal.uint -> unit11). + Fail Numeral Notation unit11 of_uint to_uint : uint11_scope. + exact I. + Unshelve. + all: solve [ constructor ]. + Qed. +End Test11. + +Module Test12. + (* Test for numeral notations on context variables *) + Delimit Scope test12_scope with test12. + Section test12. + Context (to_uint : unit -> Decimal.uint) (of_uint : Decimal.uint -> unit). + + Numeral Notation unit of_uint to_uint : test12_scope. + Check let v := 1%test12 in v : unit. + End test12. +End Test12. + +Module Test13. + (* Test for numeral notations on notations which do not denote references *) + Delimit Scope test13_scope with test13. + Delimit Scope test13'_scope with test13'. + Delimit Scope test13''_scope with test13''. + Definition to_uint (x y : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Definition to_uint_good := to_uint tt. + Notation to_uint' := (to_uint tt). + Notation to_uint'' := (to_uint _). + Numeral Notation unit of_uint to_uint_good : test13_scope. + Check let v := 0%test13 in v : unit. + Fail Numeral Notation unit of_uint to_uint' : test13'_scope. + Fail Check let v := 0%test13' in v : unit. + Fail Numeral Notation unit of_uint to_uint'' : test13''_scope. + Fail Check let v := 0%test13'' in v : unit. +End Test13. + +Module Test14. + (* Test that numeral notations follow [Import], not [Require], and + also test that [Local Numeral Notation]s do not escape modules + nor sections. *) + Delimit Scope test14_scope with test14. + Delimit Scope test14'_scope with test14'. + Delimit Scope test14''_scope with test14''. + Delimit Scope test14'''_scope with test14'''. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14_scope. + Global Numeral Notation unit of_uint to_uint : test14'_scope. + Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + End Inner. + Fail Check let v := 0%test14 in v : unit. + Fail Check let v := 0%test14' in v : unit. + Import Inner. + Fail Check let v := 0%test14 in v : unit. + Check let v := 0%test14' in v : unit. + Section InnerSection. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Local Numeral Notation unit of_uint to_uint : test14''_scope. + Fail Global Numeral Notation unit of_uint to_uint : test14'''_scope. + Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. + End InnerSection. + Fail Check let v := 0%test14'' in v : unit. + Fail Check let v := 0%test14''' in v : unit. +End Test14. + +Module Test15. + (** Test module include *) + Delimit Scope test15_scope with test15. + Module Inner. + Definition to_uint (x : unit) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : unit := tt. + Numeral Notation unit of_uint to_uint : test15_scope. + Check let v := 0%test15 in v : unit. + End Inner. + Module Inner2. + Include Inner. + Check let v := 0%test15 in v : unit. + End Inner2. + Import Inner Inner2. + Check let v := 0%test15 in v : unit. +End Test15. + +Module Test16. + (** Test functors *) + Delimit Scope test16_scope with test16. + Module Type A. + Axiom T : Set. + Axiom t : T. + End A. + Module F (a : A). + Inductive Foo := foo (_ : a.T). + Definition to_uint (x : Foo) : Decimal.uint := Nat.to_uint O. + Definition of_uint (x : Decimal.uint) : Foo := foo a.t. + Global Numeral Notation Foo of_uint to_uint : test16_scope. + Check let v := 0%test16 in v : Foo. + End F. + Module a <: A. + Definition T : Set := unit. + Definition t : T := tt. + End a. + Module Import f := F a. + (** Ideally this should work, but it should definitely not anomaly *) + Fail Check let v := 0%test16 in v : Foo. +End Test16. diff --git a/test-suite/success/ROmega4.v b/test-suite/success/ROmega4.v index 58ae5b8f..a7245927 100644 --- a/test-suite/success/ROmega4.v +++ b/test-suite/success/ROmega4.v @@ -3,12 +3,12 @@ See also #148 for the corresponding improvement in Omega. *) -Require Import ZArith ROmega. +Require Import ZArith Lia. Open Scope Z. Goal let x := 3 in x = 3. intros. -romega. +lia. Qed. (** Example seen in #4132 @@ -22,5 +22,5 @@ Lemma foo (H : - zxy' <= zxy) (H' : zxy' <= x') : - b <= zxy. Proof. -romega. +lia. Qed. diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 84194049..6370cab6 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -589,6 +589,8 @@ Close Scope Z_scope. Theorem S_is_not_O : forall n, S n <> 0. +Set Nested Proofs Allowed. + Definition Is_zero (x:nat):= match x with | 0 => True | _ => False @@ -991,10 +993,10 @@ Proof. Qed. -Implicit Arguments Vector.cons [A n]. -Implicit Arguments Vector.nil [A]. -Implicit Arguments Vector.hd [A n]. -Implicit Arguments Vector.tl [A n]. +Arguments Vector.cons [A] _ [n]. +Arguments Vector.nil [A]. +Arguments Vector.hd [A n]. +Arguments Vector.tl [A n]. Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n. Proof. @@ -1064,7 +1066,7 @@ Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v} | S n', Vector.cons _ v' => vector_nth A n' _ v' end. -Implicit Arguments vector_nth [A p]. +Arguments vector_nth [A] _ [p]. Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i a b, @@ -1159,7 +1161,7 @@ infiniteproof map_iterate'. Qed. -Implicit Arguments LNil [A]. +Arguments LNil [A]. Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A), LNil <> (LCons a l). diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 6f27c1d3..18ebcd63 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -5,7 +5,7 @@ Require Import Program. Require Import List. Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }. -Implicit Arguments vector []. +Arguments vector : clear implicits. Coercion vec_list : vector >-> list. diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v index ca374671..2da63063 100644 --- a/test-suite/success/Scopes.v +++ b/test-suite/success/Scopes.v @@ -11,7 +11,7 @@ Check (A.opp 3). Record B := { f :> Z -> Z }. Variable a:B. -Arguments Scope a [Z_scope]. +Arguments a _%Z_scope : extra scopes. Check a 0. (* Check that casts activate scopes if ever possible *) diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v index cd6eac35..400479ae 100644 --- a/test-suite/success/Typeclasses.v +++ b/test-suite/success/Typeclasses.v @@ -128,8 +128,8 @@ Record Monad {m : Type -> Type} := { Print Visibility. Print unit. -Implicit Arguments unit [[m] [m0] [α]]. -Implicit Arguments Monad []. +Arguments unit {m m0 α}. +Arguments Monad : clear implicits. Notation "'return' t" := (unit t). (* Test correct handling of existentials and defined fields. *) diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 02e043bc..e1df9ba8 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -39,7 +39,7 @@ Qed. (* Check apply/eapply distinction in presence of open terms *) Parameter h : forall x y z : nat, x = z -> x = y. -Implicit Arguments h [[x] [y]]. +Arguments h {x y}. Goal 1 = 0 -> True. intro H. apply h in H || exact I. @@ -559,3 +559,26 @@ split. - (* clear b:True *) match goal with H:_ |- _ => clear H end. (* use a:0=0 *) match goal with H:_ |- _ => exact H end. Qed. + +(* Test choice of most dependent solution *) +Goal forall n, n = 0 -> exists p, p = n /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. (* Compatibility tells [?p:=n] rather than [?p:=0] *) +exact H. (* this checks that the goal is [n=0], not [0=0] *) +Qed. + +(* Check insensitivity to alphabetic order of names*) +(* In both cases, the last name is conventionally chosen *) +(* Before 8.9, the name coming first in alphabetic order *) +(* was chosen. *) +Goal forall m n, m = n -> n = 0 -> exists p, p = n /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. +exact H0. +Qed. + +Goal forall n m, n = m -> m = 0 -> exists p, p = m /\ p = 0. +intros. eexists ?[p]. split. rewrite H. +reflexivity. +exact H0. +Qed. diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v new file mode 100644 index 00000000..83fb3d0c --- /dev/null +++ b/test-suite/success/attribute-syntax.v @@ -0,0 +1,23 @@ +From Coq Require Program. + +Section Scope. + +#[local] Coercion nat_of_bool (b: bool) : nat := + if b then 0 else 1. + +Check (refl_equal : true = 0 :> nat). + +End Scope. + +Fail Check 0 = true :> nat. + +#[polymorphic] +Definition ι T (x: T) := x. + +Check ι _ ι. + +#[program] +Fixpoint f (n: nat) {wf lt n} : nat := _. + +#[deprecated(since="8.9.0")] +Ltac foo := foo. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index f5bb884d..55ae54ca 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -42,7 +42,7 @@ Inductive ctx : Type := Bind Scope context_scope with ctx. Delimit Scope context_scope with ctx. -Arguments Scope snoc [context_scope]. +Arguments snoc _%context_scope. Notation " Γ , τ " := (snoc Γ τ) (at level 25, τ at next level, left associativity) : context_scope. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 6fbe61a9..d1d38465 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -422,6 +422,7 @@ Abort. Goal forall b:bool, b = b. intros. destruct b eqn:H. +Abort. (* Check natural instantiation behavior when the goal has already an evar *) diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 0f9fb745..253b48e4 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -386,7 +386,7 @@ Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c }. -Implicit Arguments mkTri [R S T]. +Arguments mkTri [R S T]. Definition tri_iffT : tri iffT iffT iffT := (mkTri (fun X0 X1 X2 E01 E02 => diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 86814051..0951c5c8 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -53,3 +53,17 @@ Goal True -> exists (x : Prop), x. Proof. intro H; eexists ?[x]; only [x]: exact True. 1: assumption. Qed. + +(* Strict focusing! *) +Set Default Goal Selector "!". + +Goal True -> True /\ True /\ True. +Proof. + intro. + split;only 2:split. + Fail exact I. + Fail !:exact I. + 1:exact I. + - !:exact H. + - exact I. +Qed. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index a0981311..23853890 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -33,11 +33,11 @@ Definition eq1 := fun (A:Type) (x y:A) => x=y. Definition eq2 := fun (A:Type) (x y:A) => x=y. Definition eq3 := fun (A:Type) (x y:A) => x=y. -Implicit Arguments op' []. -Global Implicit Arguments op'' []. +Arguments op' : clear implicits. +Global Arguments op'' : clear implicits. -Implicit Arguments eq2 []. -Global Implicit Arguments eq3 []. +Arguments eq2 : clear implicits. +Global Arguments eq3 : clear implicits. Check (op 0 0). Check (op' nat 0 0). @@ -89,14 +89,14 @@ Fixpoint plus n m {struct n} := (* Check multiple implicit arguments signatures *) -Implicit Arguments eq_refl [[A] [x]] [[A]]. +Arguments eq_refl {A x}, {A}. Check eq_refl : 0 = 0. (* Check that notations preserve implicit (since 8.3) *) Parameter p : forall A, A -> forall n, n = 0 -> True. -Implicit Arguments p [A n]. +Arguments p [A] _ [n]. Notation Q := (p 0). Check Q eq_refl. diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index a329894a..d37ad9f5 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -127,4 +127,28 @@ induction 1 as (n,H,IH). exact Logic.I. Qed. +(* Make "intro"/"intros" progress on existential variables *) +Module Evar. + +Goal exists (A:Prop), A. +eexists. +unshelve (intro x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Goal exists (A:Prop), A. +eexists. +unshelve (intros x). +- exact nat. +- exact (x=x). +- auto. +Qed. + +Definition d := ltac:(intro x; exact (x*x)). + +Definition d' : nat -> _ := ltac:(intros;exact 0). + +End Evar. diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v index de2857b4..2f0d8bf8 100644 --- a/test-suite/success/letproj.v +++ b/test-suite/success/letproj.v @@ -7,3 +7,5 @@ Definition test (A : Type) (f : Foo A) := Scheme foo_case := Case for Foo Sort Type. +Definition test' (A : Type) (f : Foo A) := + let 'Build_Foo _ x y := f in x. diff --git a/test-suite/success/mutual_record.v b/test-suite/success/mutual_record.v new file mode 100644 index 00000000..77529733 --- /dev/null +++ b/test-suite/success/mutual_record.v @@ -0,0 +1,57 @@ +Module M0. + +Inductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M0. + +Module M1. + +Set Primitive Projections. + +Inductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M1. + +Module M2. + +Set Primitive Projections. + +CoInductive foo (A : Type) := Foo { + foo0 : option (bar A); + foo1 : nat; + foo2 := foo1 = 0; + foo3 : foo2; +} + +with bar (A : Type) := Bar { + bar0 : A; + bar1 := 0; + bar2 : bar1 = 0; + bar3 : nat -> foo A; +}. + +End M2. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 31a1608c..299b08bd 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -193,9 +193,37 @@ Set Primitive Projections. Record s (x:nat) (y:=S x) := {c:=x; d:x=c}. Lemma f : 0=1. Proof. -Fail apply d. + Fail apply d. (* split. reflexivity. Qed. *) +Abort. + +(* Primitive projection match compilation *) +Require Import List. +Set Primitive Projections. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Arguments pair {_ _} _ _. + +Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) := + match n with + | 0 => pair nil l + | S n => + match l with + | nil => pair nil nil + | x :: l => let 'pair l1 l2 := split_at l n in pair (x :: l1) l2 + end + end. + +Time Eval vm_compute in split_at (repeat 0 20) 10. (* Takes 0s *) +Time Eval vm_compute in split_at (repeat 0 40) 20. (* Takes 0.001s *) +Timeout 1 Time Eval vm_compute in split_at (repeat 0 60) 30. (* Used to take 60s, now takes 0.001s *) + +Check (@eq_refl _ 0 <: 0 = fst (pair 0 1)). +Fail Check (@eq_refl _ 0 <: 0 = snd (pair 0 1)). + +Check (@eq_refl _ 0 <<: 0 = fst (pair 0 1)). +Fail Check (@eq_refl _ 0 <<: 0 = snd (pair 0 1)). diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 22fb4d75..40986e57 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -121,14 +121,16 @@ Abort. (* Wish 1988: that fun forces unfold in refine *) Goal (forall A : Prop, A -> ~~A). -Proof. refine(fun A a f => _). +Proof. refine(fun A a f => _). Abort. (* Checking beta-iota normalization of hypotheses in created evars *) Goal {x|x=0} -> True. refine (fun y => let (x,a) := y in _). match goal with a:_=0 |- _ => idtac end. +Abort. Goal (forall P, {P 0}+{P 1}) -> True. refine (fun H => if H (fun x => x=x) then _ else _). match goal with _:0=0 |- _ => idtac end. +Abort. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 448d0082..baf08979 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -7,7 +7,7 @@ Inductive listn : nat -> Set := Axiom ax : forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)), - existS _ (n + n') l = existS _ (n' + n) l'. + existT _ (n + n') l = existT _ (n' + n) l'. Lemma lem : forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)), @@ -72,7 +72,7 @@ Qed. Require Import JMeq. -Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True. +Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True. inversion 1; (* Goal is now [JMeq a a -> True] *) dependent rewrite H3. Undo. intros; inversion H; dependent rewrite H4 in H0. @@ -135,7 +135,7 @@ Abort. Goal forall x y, x=y+0 -> let z := x+1 in x+1=y -> z=z -> z=x. intros. subst x. (* was failing *) -subst z. +subst z. rewrite H0. auto with arith. Qed. diff --git a/test-suite/success/sideff.v b/test-suite/success/sideff.v index 3c0b8156..b9a1273b 100644 --- a/test-suite/success/sideff.v +++ b/test-suite/success/sideff.v @@ -5,6 +5,8 @@ Proof. apply (const tt tt). Qed. +Set Nested Proofs Allowed. + Lemma foobar' : unit. Lemma aux : forall A : Type, A -> unit. Proof. intros. pose (foo := idw A). exact tt. Show Universes. Qed. diff --git a/test-suite/success/ssr_delayed_clear_rename.v b/test-suite/success/ssr_delayed_clear_rename.v deleted file mode 100644 index 951e5aff..00000000 --- a/test-suite/success/ssr_delayed_clear_rename.v +++ /dev/null @@ -1,5 +0,0 @@ -Require Import ssreflect. -Example foo (t t1 t2 : True) : True /\ True -> True -> True. -Proof. -move=>[{t1 t2 t} t1 t2] t. -Abort. diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v new file mode 100644 index 00000000..42236a53 --- /dev/null +++ b/test-suite/success/uniform_inductive_parameters.v @@ -0,0 +1,13 @@ +Set Uniform Inductive Parameters. + +Inductive list (A : Type) := + | nil : list + | cons : A -> list -> list. +Check (list : Type -> Type). +Check (cons : forall A, A -> list A -> list A). + +Inductive list2 (A : Type) (A' := prod A A) := + | nil2 : list2 + | cons2 : A' -> list2 -> list2. +Check (list2 : Type -> Type). +Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A). diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 28634045..28426b57 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -60,7 +60,7 @@ Qed. Record U : Type := { A:=Type; a:A }. -(** Check assignement of sorts to inductives and records. *) +(** Check assignment of sorts to inductives and records. *) Variable sh : list nat. diff --git a/test-suite/success/vm_records.v b/test-suite/success/vm_records.v new file mode 100644 index 00000000..8a1544c8 --- /dev/null +++ b/test-suite/success/vm_records.v @@ -0,0 +1,40 @@ +Set Primitive Projections. + +Module M. + +CoInductive foo := Foo { + foo0 : foo; + foo1 : bar; +} +with bar := Bar { + bar0 : foo; + bar1 : bar; +}. + +CoFixpoint f : foo := Foo f g +with g : bar := Bar f g. + +Check (@eq_refl _ g.(bar0) <: f.(foo0).(foo0) = g.(bar0)). +Check (@eq_refl _ g <: g.(bar1).(bar0).(foo1) = g). + +End M. + +Module N. + +Inductive foo := Foo { + foo0 : option foo; + foo1 : list bar; +} +with bar := Bar { + bar0 : option bar; + bar1 : list foo; +}. + +Definition f_0 := Foo None nil. +Definition g_0 := Bar None nil. + +Definition f := Foo (Some f_0) (cons g_0 nil). + +Check (@eq_refl _ f.(foo1) <: f.(foo1) = cons g_0 nil). + +End N. |