diff options
Diffstat (limited to 'test-suite/success')
24 files changed, 346 insertions, 23 deletions
diff --git a/test-suite/success/BidirectionalityHints.v b/test-suite/success/BidirectionalityHints.v new file mode 100644 index 0000000000..284cdc871b --- /dev/null +++ b/test-suite/success/BidirectionalityHints.v @@ -0,0 +1,114 @@ +From Coq Require Import Utf8. +Set Default Proof Using "Type". + +Module SimpleExamples. + +Axiom c : bool -> nat. +Coercion c : bool >-> nat. +Inductive Boxed A := Box (a : A). +Arguments Box {A} & a. +Check Box true : Boxed nat. + +(* Here we check that there is no regression due e.g. to refining arguments + in the wrong order *) +Axiom f : forall b : bool, (if b then bool else nat) -> Type. +Check f true true : Type. +Arguments f & _ _. +Check f true true : Type. + +End SimpleExamples. + +Module Issue7910. + +Local Set Universe Polymorphism. + +(** Telescopes *) +Inductive tele : Type := + | TeleO : tele + | TeleS {X} (binder : X → tele) : tele. + +Arguments TeleS {_} _. + +(** The telescope version of Coq's function type *) +Fixpoint tele_fun (TT : tele) (T : Type) : Type := + match TT with + | TeleO => T + | TeleS b => ∀ x, tele_fun (b x) T + end. + +Notation "TT -t> A" := + (tele_fun TT A) (at level 99, A at level 200, right associativity). + +(** An eliminator for elements of [tele_fun]. + We use a [fix] because, for some reason, that makes stuff print nicer + in the proofs in iris:bi/lib/telescopes.v *) +Definition tele_fold {X Y} {TT : tele} (step : ∀ {A : Type}, (A → Y) → Y) (base : X → Y) + : (TT -t> X) → Y := + (fix rec {TT} : (TT -t> X) → Y := + match TT as TT return (TT -t> X) → Y with + | TeleO => λ x : X, base x + | TeleS b => λ f, step (λ x, rec (f x)) + end) TT. +Arguments tele_fold {_ _ !_} _ _ _ /. + +(** A sigma-like type for an "element" of a telescope, i.e. the data it + takes to get a [T] from a [TT -t> T]. *) +Inductive tele_arg : tele → Type := +| TargO : tele_arg TeleO +(* the [x] is the only relevant data here *) +| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder). + +Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T := + λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T := + match a in tele_arg TT return (TT -t> T) → T with + | TargO => λ t : T, t + | TargS x a => λ f, rec a (f x) + end) TT a f. +Arguments tele_app {!_ _} & _ !_ /. + +Coercion tele_arg : tele >-> Sortclass. +Coercion tele_app : tele_fun >-> Funclass. + +(** Operate below [tele_fun]s with argument telescope [TT]. *) +Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U := + match TT as TT return (TT → U) → TT -t> U with + | TeleO => λ F, F TargO + | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *) + tele_bind (λ a, F (TargS x a)) + end. +Arguments tele_bind {_ !_} _ /. + +(** Telescopic quantifiers *) +Definition tforall {TT : tele} (Ψ : TT → Prop) : Prop := + tele_fold (λ (T : Type) (b : T → Prop), ∀ x : T, b x) (λ x, x) (tele_bind Ψ). +Arguments tforall {!_} _ /. +Definition texist {TT : tele} (Ψ : TT → Prop) : Prop := + tele_fold ex (λ x, x) (tele_bind Ψ). +Arguments texist {!_} _ /. + +Notation "'∀..' x .. y , P" := (tforall (λ x, .. (tforall (λ y, P)) .. )) + (at level 200, x binder, y binder, right associativity, + format "∀.. x .. y , P"). +Notation "'∃..' x .. y , P" := (texist (λ x, .. (texist (λ y, P)) .. )) + (at level 200, x binder, y binder, right associativity, + format "∃.. x .. y , P"). + +(** The actual test case *) +Definition test {TT : tele} (t : TT → Prop) : Prop := + ∀.. x, t x ∧ t x. + +Notation "'[TEST' x .. z , P ']'" := + (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (tele_app (λ x, .. (λ z, P) ..))) + (x binder, z binder). +Notation "'[TEST2' x .. z , P ']'" := + (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (tele_app (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..))) + (λ x, .. (λ z, P) ..))) + (x binder, z binder). + +Check [TEST (x y : nat), x = y]. + +Check [TEST2 (x y : nat), x = y]. + +End Issue7910. diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v index 69fca48e24..ba6bf3bba2 100644 --- a/test-suite/success/Case15.v +++ b/test-suite/success/Case15.v @@ -20,7 +20,7 @@ Definition test (B : Boite) := | boite false (n, m) => n + m end. -(* Check lazyness of compilation ... future work +(* Check laziness of compilation ... future work Inductive I : Set := c : (b:bool)(if b then bool else nat)->I. Check [x] diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v index be9ca8d41b..6bea435090 100644 --- a/test-suite/success/Case18.v +++ b/test-suite/success/Case18.v @@ -1,7 +1,10 @@ (* Check or-patterns *) +(* Non-interference with Numbers divisibility. *) +Reserved Notation "( p | q )" (at level 0). + Definition g x := - match x with ((((1 as x),_) | (_,x)), (_,(2 as y))|(y,_)) => (x,y) end. + match x with ((((1 as x),_) | (_,x)), ((_,(2 as y)) | (y,_))) => (x,y) end. Check (refl_equal _ : g ((1,2),(3,4)) = (1,3)). diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 8d9edbd62d..02e15b8ee2 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -62,7 +62,7 @@ Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option n (* -------------------------------------------------------------------- *) (* Example to test patterns matching on dependent families *) -(* This exemple extracted from the developement done by Nacira Chabane *) +(* This exemple extracted from the development done by Nacira Chabane *) (* (equipe Paris 6) *) (* -------------------------------------------------------------------- *) @@ -298,7 +298,7 @@ End Version1. (* ------------------------------------------------------------------*) -(* Initial exemple (without patterns) *) +(* Initial example (without patterns) *) (*-------------------------------------------------------------------*) Module Version2. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 36fecf7204..56a4fa0aad 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/Discriminate_HoTT.v b/test-suite/success/Discriminate_HoTT.v new file mode 100644 index 0000000000..2a5e083d56 --- /dev/null +++ b/test-suite/success/Discriminate_HoTT.v @@ -0,0 +1,89 @@ +(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter") -*- *) + +(* This file tests the discriminate tactic compatibility with HoTT. + The first part of the file will setup a mini HoTT environment. + Afterwards a number of tests are performed. The tests are basically + copied from the Discriminate.v test file. *) + +Unset Elimination Schemes. + +Set Universe Polymorphism. + +Declare ML Module "ltac_plugin". + +Global Set Default Proof Mode "Classic". + +Notation "x -> y" := (forall (_:x), y) (at level 99, right associativity, y at level 200). + +Cumulative Variant paths {A} (a:A) : A -> Type + := idpath : paths a a. + +Arguments idpath {A a} , [A] a. + +Scheme paths_ind := Induction for paths Sort Type. +Arguments paths_ind [A] a P f y p. + +Notation "x = y :> A" := (@paths A x y) (at level 70, y at next level, no associativity). +Notation "x = y" := (x = y :>_) (at level 70, no associativity). + +Register paths as core.identity.type. +Register idpath as core.identity.refl. +Register paths_ind as core.identity.ind. + +Definition inverse {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. +Arguments inverse {A x y} p : simpl nomatch. +Register inverse as core.identity.sym. + +Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z := + match p, q with idpath, idpath => idpath end. +Arguments concat {A x y z} p q : simpl nomatch. +Register concat as core.identity.trans. + +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. +Arguments ap {A B} f {x y} p. +Register ap as core.identity.congr. + +Variant Empty : Type :=. + +Register Empty as core.False.type. + +Variant Unit : Type := tt. + +Register Unit as core.True.type. +Register tt as core.True.I. + +Variant Bool : Type := true | false. + +Inductive nat : Type := O | S (n:nat). + +(*********** Test discriminate tactic below. ***************) + +Goal O = S O -> Empty. + discriminate 1. +Qed. + +Goal forall H : O = S O, H = H. + discriminate H. +Qed. + +Goal O = S O -> Unit. +intros. discriminate H. Qed. +Goal O = S O -> Unit. +intros. Ltac g x := discriminate x. g H. Qed. + +Goal (forall x y : nat, x = y -> x = S y) -> Unit. +intros. +try discriminate (H O) || exact tt. +Qed. + +Goal (forall x y : nat, x = y -> x = S y) -> Unit. +intros. ediscriminate (H O). instantiate (1:=O). Abort. + +(* Check discriminate on types with local definitions *) + +Inductive A := B (T := Unit) (x y : Bool) (z := x). +Goal forall x y, B x true = B y false -> Empty. +discriminate. +Qed. diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index fdf7797d4b..31e442549b 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 2f13b7c225..e96a5f9048 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -175,7 +175,7 @@ End HintCut. (* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *) -(* e.g. those tactics when considering a goal with existential varibles *) +(* e.g. those tactics when considering a goal with existential variables *) (* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *) (* See this Coq club post for more detail: *) (* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index ee540d7109..1dbeaf3e1f 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -179,7 +179,7 @@ exact Logic.I. Qed. (* Up to September 2014, H0 below was renamed called H1 because of a collision - with the automaticallly generated names for equations. + with the automatically generated names for equations. (example taken from CoLoR) *) Inductive term := Var | Fun : term -> term -> term. diff --git a/test-suite/success/LocalDefinition.v b/test-suite/success/LocalDefinition.v new file mode 100644 index 0000000000..22fb09526d --- /dev/null +++ b/test-suite/success/LocalDefinition.v @@ -0,0 +1,53 @@ +(* Test consistent behavior of Local Definition (#8722) *) + +(* Test consistent behavior of Local Definition wrt Admitted *) + +Module TestAdmittedVisibility. + Module A. + Let a1 : nat. Admitted. (* Suppose to behave like a "Local Definition" *) + Local Definition b1 : nat. Admitted. (* Told to be a "Local Definition" *) + Local Definition c1 := 0. + Local Parameter d1 : nat. + Section S. + Let a2 : nat. Admitted. (* Told to be turned into a toplevel assumption *) + Local Definition b2 : nat. Admitted. (* Told to be a "Local Definition" *) + Local Definition c2 := 0. + Local Parameter d2 : nat. + End S. + End A. + Import A. + Fail Check a1. (* used to be accepted *) + Fail Check b1. (* used to be accepted *) + Fail Check c1. + Fail Check d1. + Fail Check a2. (* used to be accepted *) + Fail Check b2. (* used to be accepted *) + Fail Check c2. + Fail Check d2. +End TestAdmittedVisibility. + +(* Test consistent behavior of Local Definition wrt automatic declaration of instances *) + +Module TestVariableAsInstances. + Module Test1. + Set Typeclasses Axioms Are Instances. + Class U. + Local Parameter b : U. + Definition testU := _ : U. (* _ resolved *) + + Class T. + Variable a : T. (* warned to be the same as "Local Parameter" *) + Definition testT := _ : T. (* _ resolved *) + End Test1. + + Module Test2. + Unset Typeclasses Axioms Are Instances. + Class U. + Local Parameter b : U. + Fail Definition testU := _ : U. (* _ unresolved *) + + Class T. + Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *) + Fail Definition testT := _ : T. (* used to succeed *) + End Test2. +End TestVariableAsInstances. diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v new file mode 100644 index 0000000000..d313ba0aa4 --- /dev/null +++ b/test-suite/success/NotationDeprecation.v @@ -0,0 +1,62 @@ +Module Syndefs. + +#[deprecated(since = "8.8", note = "Do not use.")] +Notation foo := Prop. + +Notation bar := Prop (compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Notation zar := Prop (compat "8.8"). + +Check foo. +Check bar. + +Set Warnings "+deprecated". + +Fail Check foo. +Fail Check bar. + +End Syndefs. + +Module Notations. + +#[deprecated(since = "8.8", note = "Do not use.")] +Notation "!!" := Prop. + +Notation "##" := Prop (compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Notation "**" := Prop (compat "8.8"). + +Check !!. +Check ##. + +Set Warnings "+deprecated". + +Fail Check !!. +Fail Check ##. + +End Notations. + +Module Infix. + +#[deprecated(since = "8.8", note = "Do not use.")] +Infix "!!" := plus (at level 1). + +Infix "##" := plus (at level 1, compat "8.8"). + +Fail +#[deprecated(since = "8.8", note = "Do not use.")] +Infix "**" := plus (at level 1, compat "8.8"). + +Check (_ !! _). +Check (_ ## _). + +Set Warnings "+deprecated". + +Fail Check (_ !! _). +Fail Check (_ ## _). + +End Infix. diff --git a/test-suite/success/Reordering.v b/test-suite/success/Reordering.v index de9b997590..98759264e5 100644 --- a/test-suite/success/Reordering.v +++ b/test-suite/success/Reordering.v @@ -1,7 +1,7 @@ (* Testing the reordering of hypothesis required by pattern, fold and change. *) Goal forall (A:Set) (x:A) (A':=A), True. intros. -fold A' in x. (* suceeds: x is moved after A' *) +fold A' in x. (* succeeds: x is moved after A' *) Undo. pattern A' in x. Undo. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index 7d01d3b07b..ea0cf43451 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index f1683078cb..287c77c866 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 5b616ccc33..28200f8783 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 9b3fb3c5c7..17c6a93d21 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 95ae070940..54c82ff6f1 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v index fb0adabae9..c566a6db9f 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -34,7 +34,7 @@ Definition testAbis := Abis.u + Abis.y. Recursive Extraction testAbis. (* without: A B v w x *) Extraction TestCompile testAbis. -(** 2) With signature, we only keep elements mentionned in signature. *) +(** 2) With signature, we only keep elements mentioned in signature. *) Module Type SIG. Parameter u : nat. diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index 0951c5c8d4..ae834e7696 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -13,13 +13,15 @@ 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. + Fail 7:idtac. + Fail 2-1:idtac. + 1,2,4-6:idtac. 2-5:exact One. par:exact Zero. - repeat split. 3-6:swap 1 4. 1-5:swap 1 5. - 0-4:exact One. + 1-4:exact One. all:exact Zero. - repeat split. 1, 3:exact Zero. @@ -34,7 +36,7 @@ Qed. Goal True -> True. Proof. - intros y; only 1-2 : repeat idtac. + intros y. 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. diff --git a/test-suite/success/if.v b/test-suite/success/if.v index c81d2b9bf1..68d26ac8df 100644 --- a/test-suite/success/if.v +++ b/test-suite/success/if.v @@ -1,4 +1,4 @@ -(* The synthesis of the elimination predicate may fail if algebric *) +(* The synthesis of the elimination predicate may fail if algebraic *) (* universes are not cautiously treated *) Check (fun b : bool => if b then Type else nat). diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index 92fd6cb17d..ed781b3a40 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index da7df69e62..c8e5be93e9 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 2c76a13597..ac734de9df 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 72f0d94dea..b7ab75349e 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) |