diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/2640.v | 17 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4957.v | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5359.v | 218 | ||||
| -rw-r--r-- | test-suite/ide/undo.v | 103 | ||||
| -rw-r--r-- | test-suite/ide/undo011.fake | 34 | ||||
| -rw-r--r-- | test-suite/output/ErrorInModule.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorInModule.v | 4 | ||||
| -rw-r--r-- | test-suite/output/ErrorInSection.out | 3 | ||||
| -rw-r--r-- | test-suite/output/ErrorInSection.v | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.out | 6 | ||||
| -rw-r--r-- | test-suite/output/UnivBinders.v | 7 | ||||
| -rw-r--r-- | test-suite/output/inference.out | 12 | ||||
| -rw-r--r-- | test-suite/output/qualification.out | 1 | ||||
| -rw-r--r-- | test-suite/success/abstract_chain.v | 43 | ||||
| -rw-r--r-- | test-suite/success/change_pattern.v | 34 | ||||
| -rw-r--r-- | test-suite/success/decl_mode.v | 182 | ||||
| -rw-r--r-- | test-suite/success/decl_mode2.v | 249 | ||||
| -rw-r--r-- | test-suite/success/old_typeclass.v | 13 | ||||
| -rw-r--r-- | test-suite/success/rewrite_evar.v | 8 | ||||
| -rw-r--r-- | test-suite/success/univnames.v | 13 |
21 files changed, 369 insertions, 593 deletions
diff --git a/test-suite/bugs/closed/2640.v b/test-suite/bugs/closed/2640.v deleted file mode 100644 index da0cc68a4e..0000000000 --- a/test-suite/bugs/closed/2640.v +++ /dev/null @@ -1,17 +0,0 @@ -(* Testing consistency of globalization and interpretation in some - extreme cases *) - -Section sect. - - (* Simplification of the initial example *) - Hypothesis Other: True. - - Lemma C2 : True. - proof. - Fail have True using Other. - Abort. - - (* Variant of the same problem *) - Lemma C2 : True. - Fail clear; Other. - Abort. diff --git a/test-suite/bugs/closed/4957.v b/test-suite/bugs/closed/4957.v new file mode 100644 index 0000000000..0efd87ac0d --- /dev/null +++ b/test-suite/bugs/closed/4957.v @@ -0,0 +1,6 @@ +Ltac get_value H := eval cbv delta [H] in H. + +Goal True. +refine (let X := _ in _). +let e := get_value X in unify e Prop. +Abort. diff --git a/test-suite/bugs/closed/5359.v b/test-suite/bugs/closed/5359.v new file mode 100644 index 0000000000..87e69565e3 --- /dev/null +++ b/test-suite/bugs/closed/5359.v @@ -0,0 +1,218 @@ +Require Import Coq.nsatz.Nsatz. +Goal False. + + (* the first (succeeding) goal was reached by clearing one hypothesis in the second goal which overflows 6GB of stack space *) + let sugar := constr:( 0%Z ) in + let nparams := constr:( (-1)%Z ) in + let reified_goal := constr:( + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) ) in + let power := constr:( N.one ) in + let reified_givens := constr:( + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) + :: Ring_polynom.PEsub + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEX Z 10)) (Ring_polynom.PEc 1%Z) + :: Ring_polynom.PEsub + (Ring_polynom.PEmul + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEX Z 9)) (Ring_polynom.PEc 1%Z) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 7) + (Ring_polynom.PEX Z 7))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) (Ring_polynom.PEX Z 8))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 7) + (Ring_polynom.PEX Z 7))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) + (Ring_polynom.PEX Z 8)))) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 5) + (Ring_polynom.PEX Z 5))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 6) + (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 5) + (Ring_polynom.PEX Z 5))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 6) + (Ring_polynom.PEX Z 6)))) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 2))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 3))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 2))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 3)))) :: nil)%list ) in + Nsatz.nsatz_compute + (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))). + + let sugar := constr:( 0%Z ) in + let nparams := constr:( (-1)%Z ) in + let reified_goal := constr:( + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) ) in + let power := constr:( N.one ) in + let reified_givens := constr:( + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) + :: Ring_polynom.PEadd + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6)))) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 6)) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 5)))) (Ring_polynom.PEX Z 7)) + (Ring_polynom.PEsub + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) (Ring_polynom.PEX Z 6)) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)))) + (Ring_polynom.PEX Z 8)) + :: Ring_polynom.PEsub + (Ring_polynom.PEmul + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) (Ring_polynom.PEX Z 5)) + (Ring_polynom.PEX Z 3)) (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEX Z 10)) (Ring_polynom.PEc 1%Z) + :: Ring_polynom.PEsub + (Ring_polynom.PEmul + (Ring_polynom.PEsub (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEX Z 2)) + (Ring_polynom.PEX Z 5)) (Ring_polynom.PEX Z 3)) + (Ring_polynom.PEX Z 6))) (Ring_polynom.PEX Z 9)) + (Ring_polynom.PEc 1%Z) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 7) + (Ring_polynom.PEX Z 7))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) + (Ring_polynom.PEX Z 8))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 7) + (Ring_polynom.PEX Z 7))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 8) + (Ring_polynom.PEX Z 8)))) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 5) + (Ring_polynom.PEX Z 5))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 6) + (Ring_polynom.PEX Z 6))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 5) + (Ring_polynom.PEX Z 5))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 6) + (Ring_polynom.PEX Z 6)))) + :: Ring_polynom.PEsub + (Ring_polynom.PEadd + (Ring_polynom.PEmul (Ring_polynom.PEX Z 1) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 2))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 3))) + (Ring_polynom.PEadd (Ring_polynom.PEc 1%Z) + (Ring_polynom.PEmul + (Ring_polynom.PEmul (Ring_polynom.PEX Z 4) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 2) + (Ring_polynom.PEX Z 2))) + (Ring_polynom.PEmul (Ring_polynom.PEX Z 3) + (Ring_polynom.PEX Z 3)))) :: nil)%list ) in + Nsatz.nsatz_compute + (@cons _ (@Ring_polynom.PEc _ sugar) (@cons _ (@Ring_polynom.PEc _ nparams) (@cons _ (@Ring_polynom.PEpow _ reified_goal power) reified_givens))). diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v deleted file mode 100644 index ea3920551d..0000000000 --- a/test-suite/ide/undo.v +++ /dev/null @@ -1,103 +0,0 @@ -(* Here are a sequences of scripts to test interactively with undo and - replay in coqide proof sessions *) - -(* Undoing arbitrary commands, as first step *) - -Theorem a : O=O. (* 2 *) -Ltac f x := x. (* 1 * 3 *) -assert True by trivial. -trivial. -Qed. - -(* Undoing arbitrary commands, as non-first step *) - -Theorem b : O=O. -assert True by trivial. -Ltac g x := x. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, as first step *) -(* was bugged in 8.1 *) - -Theorem c : O=O. -Inductive T : Type := I. -trivial. -Qed. - -(* Undoing declarations, as first step *) -(* new in 8.2 *) - -Theorem d : O=O. -Definition e := O. -Definition f := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, as non-first step *) -(* new in 8.2 *) - -Theorem h : O=O. -assert True by trivial. -Definition i := O. -Definition j := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, interleaved with proof steps *) -(* new in 8.2 *) - -Theorem k : O=O. -assert True by trivial. -Definition l := O. -assert True by trivial. -Definition m := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, interleaved with proof steps and commands *) -(* new in 8.2 *) - -Theorem n : O=O. -assert True by trivial. -Definition o := O. -Ltac h x := x. -assert True by trivial. -Focus. -Definition p := O. -assert True by trivial. -trivial. -Qed. - -(* Undoing declarations, not in proof *) - -Definition q := O. -Definition r := O. - -(* Bug 2082 : Follow the numbers *) -(* Broken due to proof engine rewriting *) - -Variable A : Prop. -Variable B : Prop. - -Axiom OR : A \/ B. - -Lemma MyLemma2 : True. -proof. -per cases of (A \/ B) by OR. -suppose A. - then (1 = 1). - then H1 : thesis. (* 4 *) - thus thesis by H1. (* 2 *) -suppose B. (* 1 *) (* 3 *) - then (1 = 1). - then H2 : thesis. - thus thesis by H2. -end cases. -end proof. -Qed. (* 5 if you made it here, there is no regression *) - diff --git a/test-suite/ide/undo011.fake b/test-suite/ide/undo011.fake deleted file mode 100644 index 0be439b272..0000000000 --- a/test-suite/ide/undo011.fake +++ /dev/null @@ -1,34 +0,0 @@ -# Script simulating a dialog between coqide and coqtop -ideslave -# Run it via fake_ide -# -# Bug 2082 -# Broken due to proof engine rewriting -# -ADD { Variable A : Prop. } -ADD { Variable B : Prop. } -ADD { Axiom OR : A \/ B. } -ADD { Lemma MyLemma2 : True. } -ADD { proof. } -ADD { per cases of (A \/ B) by OR. } -ADD { suppose A. } -ADD { then (1 = 1). } -ADD there { then H1 : thesis. } -ADD here { thus thesis by H1. } -ADD { suppose B. } -QUERY { Show. } -EDIT_AT here -# <replay> -ADD { suppose B. } -# </replay> -EDIT_AT there -# <replay> -ADD { thus thesis by H1. } -ADD { suppose B. } -# </replay> -QUERY { Show. } -ADD { then (1 = 1). } -ADD { then H2 : thesis. } -ADD { thus thesis by H2. } -ADD { end cases. } -ADD { end proof. } -ADD { Qed. } diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out new file mode 100644 index 0000000000..776dfeb550 --- /dev/null +++ b/test-suite/output/ErrorInModule.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. + diff --git a/test-suite/output/ErrorInModule.v b/test-suite/output/ErrorInModule.v new file mode 100644 index 0000000000..e69e23276b --- /dev/null +++ b/test-suite/output/ErrorInModule.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +Module M. + Definition foo := nonexistent. +End M. diff --git a/test-suite/output/ErrorInSection.out b/test-suite/output/ErrorInSection.out new file mode 100644 index 0000000000..776dfeb550 --- /dev/null +++ b/test-suite/output/ErrorInSection.out @@ -0,0 +1,3 @@ +File "stdin", line 3, characters 20-31: +Error: The reference nonexistent was not found in the current environment. + diff --git a/test-suite/output/ErrorInSection.v b/test-suite/output/ErrorInSection.v new file mode 100644 index 0000000000..3036f8f05b --- /dev/null +++ b/test-suite/output/ErrorInSection.v @@ -0,0 +1,4 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-quick") -*- *) +Section S. + Definition foo := nonexistent. +End S. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index ad60aeccce..1ec701ae81 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -32,7 +32,7 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d : Type -> Prop λ A : Type, ∀ n p : A, n = p : Type -> Prop -let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 +let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 : bool -> nat λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out new file mode 100644 index 0000000000..128bc77673 --- /dev/null +++ b/test-suite/output/UnivBinders.out @@ -0,0 +1,6 @@ +bar@{u} = nat + : Wrap@{u} Set +(* u |= Set < u + *) + +bar is universe polymorphic diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v new file mode 100644 index 0000000000..d9e89e43c6 --- /dev/null +++ b/test-suite/output/UnivBinders.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Class Wrap A := wrap : A. + +Instance bar@{u} : Wrap@{u} Set. Proof nat. +Print bar. diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index 576fbd7c0b..c70467912f 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -6,13 +6,13 @@ fun e : option L => match e with : option L -> option L fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H : forall m n p : nat, S m <= S n + p -> m <= n + p -fun n : nat => let x := A n : T n in ?y ?y0 : T n +fun n : nat => let x : T n := A n in ?t ?y : T n : forall n : nat, T n where -?y : [n : nat x := A n : T n |- ?T -> T n] -?y0 : [n : nat x := A n : T n |- ?T] -fun n : nat => ?y ?y0 : T n +?t : [n : nat x := A n : T n |- ?T -> T n] +?y : [n : nat x := A n : T n |- ?T] +fun n : nat => ?t ?y : T n : forall n : nat, T n where -?y : [n : nat |- ?T -> T n] -?y0 : [n : nat |- ?T] +?t : [n : nat |- ?T -> T n] +?y : [n : nat |- ?T] diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out index 9300c3f546..e9c70d1efc 100644 --- a/test-suite/output/qualification.out +++ b/test-suite/output/qualification.out @@ -1,3 +1,4 @@ File "stdin", line 19, characters 0-7: Error: Signature components for label test do not match: expected type "Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t". + diff --git a/test-suite/success/abstract_chain.v b/test-suite/success/abstract_chain.v new file mode 100644 index 0000000000..0ff61e87f8 --- /dev/null +++ b/test-suite/success/abstract_chain.v @@ -0,0 +1,43 @@ +Lemma foo1 : nat -> True. +Proof. +intros _. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +exact H'. +Qed. + +Lemma foo2 : True. +Proof. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +assert (H'' : True). +{ abstract (exact (bar qux)) using quz. } +exact H''. +Qed. + +Set Universe Polymorphism. + +Lemma foo3 : nat -> True. +Proof. +intros _. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +exact H'. +Qed. + +Lemma foo4 : True. +Proof. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +assert (H'' : True). +{ abstract (exact (bar qux)) using quz. } +exact H''. +Qed. diff --git a/test-suite/success/change_pattern.v b/test-suite/success/change_pattern.v new file mode 100644 index 0000000000..874abf49f1 --- /dev/null +++ b/test-suite/success/change_pattern.v @@ -0,0 +1,34 @@ +Set Implicit Arguments. +Unset Strict Implicit. + +Axiom vector : Type -> nat -> Type. + +Record KleeneStore i j a := kleeneStore + { dim : nat + ; peek : vector j dim -> a + ; pos : vector i dim + }. + +Definition KSmap i j a b (f : a -> b) (s : KleeneStore i j a) : KleeneStore i j b := + kleeneStore (fun v => f (peek v)) (pos s). + +Record KleeneCoalg (i o : Type -> Type) := kleeneCoalg + { coalg :> forall a b, (o a) -> KleeneStore (i a) (i b) (o b) }. + +Axiom free_b_dim : forall i o (k : KleeneCoalg i o) a b b' (x : o a), dim (coalg k b x) = dim (coalg k b' x). +Axiom t : Type -> Type. +Axiom traverse : KleeneCoalg (fun x => x) t. + +Definition size a (x:t a) : nat := dim (traverse a a x). + +Lemma iso1_iso2_2 a (y : {x : t unit & vector a (size x)}) : False. +Proof. +destruct y. +pose (X := KSmap (traverse a unit) (traverse unit a x)). +set (e :=(eq_sym (free_b_dim traverse (a:=unit) a unit x))). +clearbody e. +(** The pattern generated by change must have holes where there were implicit + arguments in the original user-provided term. This particular example fails + if this is not the case because the inferred argument does not coincide with + the one in the considered term. *) +progress (change (dim (traverse unit a x)) with (dim X) in e). diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v deleted file mode 100644 index e569bcb49f..0000000000 --- a/test-suite/success/decl_mode.v +++ /dev/null @@ -1,182 +0,0 @@ -(* \sqrt 2 is irrationnal, (c) 2006 Pierre Corbineau *) - -Set Firstorder Depth 1. -Require Import ArithRing Wf_nat Peano_dec Div2 Even Lt. - -Lemma double_div2: forall n, div2 (double n) = n. -proof. - assume n:nat. - per induction on n. - suppose it is 0. - suffices (0=0) to show thesis. - thus thesis. - suppose it is (S m) and Hrec:thesis for m. - have (div2 (double (S m))= div2 (S (S (double m)))). - ~= (S (div2 (double m))). - thus ~= (S m) by Hrec. - end induction. -end proof. -Show Script. -Qed. - -Lemma double_inv : forall n m, double n = double m -> n = m . -proof. - let n, m be such that H:(double n = double m). -have (n = div2 (double n)) by double_div2,H. - ~= (div2 (double m)) by H. - thus ~= m by double_div2. -end proof. -Qed. - -Lemma double_mult_l : forall n m, (double (n * m)=n * double m). -proof. - assume n:nat and m:nat. - have (double (n * m) = n*m + n * m). - ~= (n * (m+m)) by * using ring. - thus ~= (n * double m). -end proof. -Qed. - -Lemma double_mult_r : forall n m, (double (n * m)=double n * m). -proof. - assume n:nat and m:nat. - have (double (n * m) = n*m + n * m). - ~= ((n + n) * m) by * using ring. - thus ~= (double n * m). -end proof. -Qed. - -Lemma even_is_even_times_even: forall n, even (n*n) -> even n. -proof. - let n be such that H:(even (n*n)). - per cases of (even n \/ odd n) by even_or_odd. - suppose (odd n). - hence thesis by H,even_mult_inv_r. - end cases. -end proof. -Qed. - -Lemma main_thm_aux: forall n,even n -> -double (double (div2 n *div2 n))=n*n. -proof. - given n such that H:(even n). - *** have (double (double (div2 n * div2 n)) - = double (div2 n) * double (div2 n)) - by double_mult_l,double_mult_r. - thus ~= (n*n) by H,even_double. -end proof. -Qed. - -Require Import Omega. - -Lemma even_double_n: (forall m, even (double m)). -proof. - assume m:nat. - per induction on m. - suppose it is 0. - thus thesis. - suppose it is (S mm) and thesis for mm. - then H:(even (S (S (mm+mm)))). - have (S (S (mm + mm)) = S mm + S mm) using omega. - hence (even (S mm +S mm)) by H. - end induction. -end proof. -Qed. - -Theorem main_theorem: forall n p, n*n=double (p*p) -> p=0. -proof. - assume n0:nat. - define P n as (forall p, n*n=double (p*p) -> p=0). - claim rec_step: (forall n, (forall m,m<n-> P m) -> P n). - let n be such that H:(forall m : nat, m < n -> P m) and p:nat . - per cases of ({n=0}+{n<>0}) by eq_nat_dec. - suppose H1:(n=0). - per cases on p. - suppose it is (S p'). - assume (n * n = double (S p' * S p')). - =~ 0 by H1,mult_n_O. - ~= (S ( p' + p' * S p' + S p'* S p')) - by plus_n_Sm. - hence thesis . - suppose it is 0. - thus thesis. - end cases. - suppose H1:(n<>0). - assume H0:(n*n=double (p*p)). - have (even (double (p*p))) by even_double_n . - then (even (n*n)) by H0. - then H2:(even n) by even_is_even_times_even. - then (double (double (div2 n *div2 n))=n*n) - by main_thm_aux. - ~= (double (p*p)) by H0. - then H':(double (div2 n *div2 n)= p*p) by double_inv. - have (even (double (div2 n *div2 n))) by even_double_n. - then (even (p*p)) by even_double_n,H'. - then H3:(even p) by even_is_even_times_even. - have (double(double (div2 n * div2 n)) = n*n) - by H2,main_thm_aux. - ~= (double (p*p)) by H0. - ~= (double(double (double (div2 p * div2 p)))) - by H3,main_thm_aux. - then H'':(div2 n * div2 n = double (div2 p * div2 p)) - by double_inv. - then (div2 n < n) by lt_div2,neq_O_lt,H1. - then H4:(div2 p=0) by (H (div2 n)),H''. - then (double (div2 p) = double 0). - =~ p by even_double,H3. - thus ~= 0. - end cases. - end claim. - hence thesis by (lt_wf_ind n0 P). -end proof. -Qed. - -Require Import Reals Field. -(*Coercion INR: nat >->R. -Coercion IZR: Z >->R.*) - -Open Scope R_scope. - -Lemma square_abs_square: - forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p). -proof. - assume p:Z. - per cases on p. - suppose it is (0%Z). - thus thesis. - suppose it is (Zpos z). - thus thesis. - suppose it is (Zneg z). - have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) = - (IZR (Zpos z) * IZR (Zpos z))). - ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))). - thus ~= (IZR (Zneg z) * IZR (Zneg z)). - end cases. -end proof. -Admitted. - -Definition irrational (x:R):Prop := - forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q). - -Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)). -proof. - let p:Z,q:nat be such that H:(q<>0%nat) - and H0:(sqrt (INR 2%nat)=(IZR p/INR q)). - have H_in_R:(INR q<>0:>R) by H. - have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field. - have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def. - have (INR (Z.abs_nat p * Z.abs_nat p) - = (INR (Z.abs_nat p) * INR (Z.abs_nat p))) - by mult_INR. - ~= (IZR p* IZR p) by square_abs_square. - ~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *) - ~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring. - ~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0. - ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR. - then (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat. - ~= ((q*q)+(q*q))%nat. - ~= (Div2.double (q*q)). - then (q=0%nat) by main_theorem. - hence thesis by H. -end proof. -Qed. diff --git a/test-suite/success/decl_mode2.v b/test-suite/success/decl_mode2.v deleted file mode 100644 index 46174e4810..0000000000 --- a/test-suite/success/decl_mode2.v +++ /dev/null @@ -1,249 +0,0 @@ -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/old_typeclass.v b/test-suite/success/old_typeclass.v new file mode 100644 index 0000000000..01e35810b0 --- /dev/null +++ b/test-suite/success/old_typeclass.v @@ -0,0 +1,13 @@ +Require Import Setoid Coq.Classes.Morphisms. +Set Typeclasses Legacy Resolution. + +Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and. + +Axiom In : Prop. +Axiom union_spec : In <-> True. + +Lemma foo : In /\ True. +Proof. +progress rewrite union_spec. +repeat constructor. +Qed. diff --git a/test-suite/success/rewrite_evar.v b/test-suite/success/rewrite_evar.v new file mode 100644 index 0000000000..f7ad261cbb --- /dev/null +++ b/test-suite/success/rewrite_evar.v @@ -0,0 +1,8 @@ +Require Import Coq.Setoids.Setoid. + +Goal forall (T2 MT1 MT2 : Type) (x : T2) (M2 m2 : MT2) (M1 m1 : MT1) (F : T2 -> MT1 -> MT2 -> Prop), + (forall (defaultB : T2) (m3 : MT1) (m4 : MT2), F defaultB m3 m4 <-> True) -> F x M1 M2 -> F x m1 m2. + intros ????????? H' H. + rewrite (H' _) in *. + (** The above rewrite should also rewrite in H. *) + Fail progress rewrite H' in H. diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v index 048b53d26c..fe3b8c1d7c 100644 --- a/test-suite/success/univnames.v +++ b/test-suite/success/univnames.v @@ -21,6 +21,17 @@ Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla. Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy. +Class Wrap A := wrap : A. + +Fail Instance bad@{} : Wrap Type := Type. + +Instance bad@{} : Wrap Type. +Fail Proof Type. +Abort. + +Instance bar@{u} : Wrap@{u} Set. Proof nat. + + Monomorphic Universe g. -Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file +Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'. |