diff options
Diffstat (limited to 'test-suite')
46 files changed, 827 insertions, 738 deletions
diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v new file mode 100644 index 0000000000..b2f00ffc65 --- /dev/null +++ b/test-suite/bugs/closed/2417.v @@ -0,0 +1,15 @@ +Parameter x y : nat. +Axiom H : x = y. +Hint Rewrite H : mybase. + +Ltac bar base := autorewrite with base. + +Tactic Notation "foo" ident(base) := autorewrite with base. + +Goal x = 0. + bar mybase. + now_show (y = 0). + Undo 2. + foo mybase. + now_show (y = 0). +Abort. 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/3612.v b/test-suite/bugs/closed/3612.v index a547685070..4b4f81dbce 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. +Declare ML Module "ltac_plugin". Declare ML Module "coretactics". +Set Default Proof Mode "Classic". + Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x)) (xx : @paths (@sigT A (fun x0 : A => B x0)) x x), @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index fc4c171e2c..8687eaab00 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -2,7 +2,9 @@ (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) +Declare ML Module "ltac_plugin". Declare ML Module "coretactics". +Set Default Proof Mode "Classic". Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). Delimit Scope type_scope with type. diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v index d34a2b8b1b..816bc845fd 100644 --- a/test-suite/bugs/closed/4121.v +++ b/test-suite/bugs/closed/4121.v @@ -4,6 +4,8 @@ Unset Strict Universe Declaration. (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *) +Declare ML Module "ltac_plugin". + Set Universe Polymorphism. Class Contr_internal (A : Type) := BuildContr { center : A }. Arguments center A {_}. @@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}. Check @contr_paths_contr0@{i}. Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *) -(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file +(** It should have length 1, just like contr_paths_contr0 *) diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 08628377f0..c6fcc24b6b 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -5,6 +5,7 @@ then from 269 lines to 255 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index ae17fb145d..64c7fd8eb1 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -5,6 +5,7 @@ then from 285 lines to 271 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. @@ -223,4 +224,4 @@ v = _) r, | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good" | [ |- ?G ] => fail 1 "bad" G end. - Fail rewrite concat_p_pp.
\ No newline at end of file + Fail rewrite concat_p_pp. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index da140c9318..64dd8c304f 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -2,6 +2,7 @@ (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. @@ -1004,4 +1005,4 @@ Proof. Fail Timeout 1 Time rewrite !loops_functor_group. (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *) Timeout 1 do 3 rewrite loops_functor_group. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/5277.v b/test-suite/bugs/closed/5277.v new file mode 100644 index 0000000000..7abc38bfce --- /dev/null +++ b/test-suite/bugs/closed/5277.v @@ -0,0 +1,11 @@ +(* Scheme Equality not robust wrt names *) + +Module A1. + Inductive A (T : Type) := C (a : T). + Scheme Equality for A. (* success *) +End A1. + +Module A2. + Inductive A (x : Type) := C (a : x). + Scheme Equality for A. +End A2. 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/Arguments.out b/test-suite/output/Arguments.out index a2ee2d4c8e..979396969a 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -97,8 +97,8 @@ Expands to: Constant Top.f forall w : r, w 3 true = tt : Prop The command has indeed failed with message: -Error: Unknown interpretation for notation "$". +Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -Error: Extra arguments: _, _. +Extra arguments: _, _. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index b084ad4984..4df21ae353 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,5 +1,5 @@ The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +To rename arguments the "rename" flag must be specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: Warning: This command is just asserting the names of arguments of identity. @@ -103,15 +103,15 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -Error: Argument lists should agree on the names they provide. +Argument lists should agree on the names they provide. The command has indeed failed with message: -Error: Sequences of implicit arguments must be of different lengths. +Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Error: Some argument names are duplicated: F +Some argument names are duplicated: F The command has indeed failed with message: -Error: Argument z cannot be declared implicit. +Argument z cannot be declared implicit. The command has indeed failed with message: -Error: Extra arguments: y. +Extra arguments: y. The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/ErrorInModule.out b/test-suite/output/ErrorInModule.out index 851ecd9306..776dfeb550 100644 --- a/test-suite/output/ErrorInModule.out +++ b/test-suite/output/ErrorInModule.out @@ -1,2 +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.out b/test-suite/output/ErrorInSection.out index 851ecd9306..776dfeb550 100644 --- a/test-suite/output/ErrorInSection.out +++ b/test-suite/output/ErrorInSection.out @@ -1,2 +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/Errors.out b/test-suite/output/Errors.out index 06a6b2d157..38d055b28e 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -7,4 +7,4 @@ In nested Ltac calls to "f" and "apply x", last call failed. Unable to unify "nat" with "True". The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. -Error: Instance is not well-typed in the environment of ?x. +Instance is not well-typed in the environment of ?x. diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out new file mode 100644 index 0000000000..8d2a125c1d --- /dev/null +++ b/test-suite/output/FunExt.out @@ -0,0 +1,19 @@ +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Already an intensional equality. +The command has indeed failed with message: +In nested Ltac calls to "extensionality in (var)" and +"clearbody (ne_var_list)", last call failed. +Hypothesis e depends on the body of H' diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v new file mode 100644 index 0000000000..7658ce718e --- /dev/null +++ b/test-suite/output/FunExt.v @@ -0,0 +1,168 @@ +Require Import FunctionalExtensionality. + +(* Basic example *) +Goal (forall x y z, x+y+z = z+y+x) -> (fun x y z => z+y+x) = (fun x y z => x+y+z). +intro H. +extensionality in H. +symmetry in H. +assumption. +Qed. + +(* Test rejection of non-equality *) +Goal forall H:(forall A:Prop, A), H=H -> forall H'':True, H''=H''. +intros H H' H''. +Fail extensionality in H. +clear H'. +Fail extensionality in H. +Fail extensionality in H''. +Abort. + +(* Test success on dependent equality *) +Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1. +intros p H. +extensionality in p. +assumption. +Qed. + +(* Test dependent functional extensionality *) +Goal forall (P:nat->Type) (Q:forall a, P a -> Type) (f g:forall a (b:P a), Q a b), + (forall x y, f x y = g x y) -> f = g. +intros * H. +extensionality in H. +assumption. +Qed. + +(* Other tests, courtesy of Jason Gross *) + +Goal forall A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c), (forall a b c, f a b c = g a b c) -> f = g. +Proof. + intros A B C D f g H. + extensionality in H. + match type of H with f = g => idtac end. + exact H. +Qed. + +Section test_section. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = g a b c). + Goal f = g. + Proof. + extensionality in H. + match type of H with f = g => idtac end. + exact H. + Qed. +End test_section. + +Section test2. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + extensionality in H. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H. + Qed. +End test2. + +Section test3. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a c, (fun b => f a b c) = (fun b => g a b c)). + Goal (fun a c b => f a b c) = (fun a c b => g a b c). + Proof. + extensionality in H. + match type of H with (fun a c b => f a b c) = (fun a' c' b' => g a' b' c') => idtac end. + exact H. + Qed. +End test3. + +Section test4. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c -> Type) + (H : forall b, (forall a c d, f a b c d) = (forall a c d, g a b c d)). + Goal (fun b => forall a c d, f a b c d) = (fun b => forall a c d, g a b c d). + Proof. + extensionality in H. + exact H. + Qed. +End test4. + +Section test5. + Goal nat -> True. + Proof. + intro n. + Fail extensionality in n. + constructor. + Qed. +End test5. + +Section test6. + Goal let f := fun A (x : A) => x in let pf := fun A x => @eq_refl _ (f A x) in f = f. + Proof. + intros f pf. + extensionality in pf. + match type of pf with f = f => idtac end. + exact pf. + Qed. +End test6. + +Section test7. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, True -> f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun a b c (_ : True) => f a b c) = (fun a' b' c' (_ : True) => g a' b' c') => idtac end. + constructor. + Qed. +End test7. + +Section test8. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : True -> forall a b c, f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun (_ : True) => f) = (fun (_ : True) => g) => idtac end. + constructor. + Qed. +End test8. + +Section test9. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + pose H as H'. + extensionality in H. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H'. + Qed. +End test9. + +Section test10. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : f = g). + Goal True. + Proof. + Fail extensionality in H. + constructor. + Qed. +End test10. + +Section test11. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = f a b c). + Goal True. + Proof. + pose H as H'. + pose (eq_refl : H = H') as e. + extensionality in H. + Fail extensionality in H'. + clear e. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + lazymatch type of H with f = f => idtac end. + constructor. + Qed. +End test11. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 26eaca8272..9d106d2dac 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0 -4 : Z The command has indeed failed with message: -Error: x should not be bound in a recursive pattern of the right-hand side. +x should not be bound in a recursive pattern of the right-hand side. The command has indeed failed with message: -Error: in the right-hand side, y and z should appear in +in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: The reference w was not found in the current environment. The command has indeed failed with message: -Error: in the right-hand side, y and z should appear in +in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: -Error: z is expected to occur in binding position in the right-hand side. +z is expected to occur in binding position in the right-hand side. The command has indeed failed with message: -Error: as y is a non-closed binder, no such "," is allowed to occur. +as y is a non-closed binder, no such "," is allowed to occur. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Both ends of the recursive pattern are the same. +Both ends of the recursive pattern are the same. SUM (nat * nat) nat : Set FST (0; 1) 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/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index c012a86b01..95be04c32c 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -37,3 +37,5 @@ fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop forall '(x, y) '(z, t), swap (x, y) = (z, t) : Prop +fun (pat : nat) '(x, y) => x + y = pat + : nat -> nat * nat -> Prop diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v index 6fa357a90c..0bad472f41 100644 --- a/test-suite/output/PatternsInBinders.v +++ b/test-suite/output/PatternsInBinders.v @@ -64,3 +64,6 @@ Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t). Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t). End Suboptimal. + +(** Test risk of collision for internal name *) +Check fun pat => fun '(x,y) => x+y = pat. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index c17b285bc9..81fda176ec 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,108 +1,108 @@ le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m +le_n_S: forall n m : nat, n <= m -> S n <= S m +le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m +le_S_n: forall n m : nat, S n <= S m -> n <= m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n le_ind: forall (n : nat) (P : nat -> Prop), P n -> (forall m : nat, n <= m -> P m -> P (S m)) -> forall n0 : nat, n <= n0 -> P n0 -le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m -le_S_n: forall n m : nat, S n <= S m -> n <= m -le_0_n: forall n : nat, 0 <= n -le_n_S: forall n m : nat, n <= m -> S n <= S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -true: bool false: bool -bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b -bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b -bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b -andb: bool -> bool -> bool -orb: bool -> bool -> bool -implb: bool -> bool -> bool -xorb: bool -> bool -> bool +true: bool +is_true: bool -> Prop negb: bool -> bool -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true -andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true eq_true: bool -> Prop -eq_true_rect: - forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b -eq_true_ind: - forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool +xorb: bool -> bool -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +BoolSpec: Prop -> Prop -> bool -> Prop +Nat.eqb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b +bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b -is_true: bool -> Prop -eq_true_ind_r: - forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true -eq_true_rec_r: - forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rect_r: forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true -BoolSpec: Prop -> Prop -> bool -> Prop +eq_true_rec_r: + forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +eq_true_ind_r: + forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true BoolSpec_ind: forall (P Q : Prop) (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool -Nat.even: nat -> bool -Nat.odd: nat -> bool -Nat.testbit: nat -> nat -> bool -Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -eq_S: forall x y : nat, x = y -> S x = S y -f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 +n_Sn: forall n : nat, n <> S n pred_Sn: forall n : nat, n = Nat.pred (S n) +O_S: forall n : nat, 0 <> S n +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +eq_S: forall x y : nat, x = y -> S x = S y eq_add_S: forall n m : nat, S n = S m -> n = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y not_eq_S: forall n m : nat, n <> m -> S n <> S m -O_S: forall n : nat, 0 <> S n -n_Sn: forall n : nat, n <> S n +mult_n_Sm: forall n m : nat, n * m + n = n * S m f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +f_equal2_mult: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 -plus_n_O: forall n : nat, n = n + 0 -plus_O_n: forall n : nat, 0 + n = n -plus_n_Sm: forall n m : nat, S (n + m) = n + S m -plus_Sn_m: forall n m : nat, S n + m = S (n + m) -f_equal2_mult: - forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -mult_n_O: forall n : nat, 0 = n * 0 -mult_n_Sm: forall n m : nat, n * m + n = n * S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true -h': newdef n <> n +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true h: n <> newdef n h': newdef n <> n h: n <> newdef n +h': newdef n <> n h: n <> newdef n h: n <> newdef n -h': ~ P n h: P n h': ~ P n h: P n h': ~ P n h: P n +h': ~ P n h: P n h: P n diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 0d5924ec61..7038eac22c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -1,39 +1,39 @@ le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m -le_S_n: forall n m : nat, S n <= S m -> n <= m -le_0_n: forall n : nat, 0 <= n le_n_S: forall n m : nat, n <= m -> S n <= S m -true: bool +le_S_n: forall n m : nat, S n <= S m -> n <= m false: bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool +true: bool +negb: bool -> bool implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool xorb: bool -> bool -> bool -negb: bool -> bool -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool -eq_S: forall x y : nat, x = y -> S x = S y -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +Nat.eqb: nat -> nat -> bool +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 pred_Sn: forall n : nat, n = Nat.pred (S n) +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y eq_add_S: forall n m : nat, S n = S m -> n = m -f_equal2_plus: - forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 -plus_n_O: forall n : nat, n = n + 0 -plus_O_n: forall n : nat, 0 + n = n +eq_S: forall x y : nat, x = y -> S x = S y +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n plus_n_Sm: forall n m : nat, S (n + m) = n + S m plus_Sn_m: forall n m : nat, S n + m = S (n + m) +mult_n_Sm: forall n m : nat, n * m + n = n * S m +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -mult_n_O: forall n : nat, 0 = n * 0 -mult_n_Sm: forall n m : nat, n * m + n = n * S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m h: newdef n h: P n diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index f3c12effca..45ff5e73b6 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,77 +1,77 @@ -true: bool false: bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool +true: bool +negb: bool -> bool implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool xorb: bool -> bool -> bool -negb: bool -> bool -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool -O: nat -S: nat -> nat -length: forall A : Type, list A -> nat +Nat.eqb: nat -> nat -> bool +Nat.two: nat Nat.zero: nat Nat.one: nat -Nat.two: nat -Nat.succ: nat -> nat +O: nat +Nat.double: nat -> nat +Nat.sqrt: nat -> nat +Nat.div2: nat -> nat +Nat.log2: nat -> nat Nat.pred: nat -> nat +Nat.square: nat -> nat +S: nat -> nat +Nat.succ: nat -> nat +Nat.ldiff: nat -> nat -> nat Nat.add: nat -> nat -> nat -Nat.double: nat -> nat +Nat.lor: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.land: nat -> nat -> nat Nat.mul: nat -> nat -> nat Nat.sub: nat -> nat -> nat Nat.max: nat -> nat -> nat -Nat.min: nat -> nat -> nat -Nat.pow: nat -> nat -> nat Nat.div: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.min: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.square: nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat -Nat.sqrt: nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -Nat.log2: nat -> nat -Nat.div2: nat -> nat +length: forall A : Type, list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.div2: nat -> nat +Nat.sqrt: nat -> nat +Nat.log2: nat -> nat +Nat.double: nat -> nat +Nat.pred: nat -> nat +Nat.square: nat -> nat +Nat.succ: nat -> nat +S: nat -> nat Nat.ldiff: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat -S: nat -> nat -Nat.succ: nat -> nat -Nat.pred: nat -> nat -Nat.add: nat -> nat -> nat -Nat.double: nat -> nat +Nat.div: nat -> nat -> nat Nat.mul: nat -> nat -> nat -Nat.sub: nat -> nat -> nat -Nat.max: nat -> nat -> nat Nat.min: nat -> nat -> nat -Nat.pow: nat -> nat -> nat -Nat.div: nat -> nat -> nat Nat.modulo: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.square: nat -> nat -Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat -Nat.sqrt: nat -> nat +Nat.max: nat -> nat -> nat +Nat.add: nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -Nat.log2: nat -> nat -Nat.div2: nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat -Nat.ldiff: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat mult_n_Sm: forall n m : nat, n * m + n = n * S m -identity_refl: forall (A : Type) (a : A), identity a a iff_refl: forall A : Prop, A <-> A +le_n: forall n : nat, n <= n +identity_refl: forall (A : Type) (a : A), identity a a eq_refl: forall (A : Type) (x : A), x = x Nat.divmod: nat -> nat -> nat -> nat -> nat * nat -le_n: forall n : nat, n <= n -pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B +pair: forall A B : Type, A -> B -> A * B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat h: n <> newdef n h: n <> newdef n diff --git a/test-suite/output/ShowProof.out b/test-suite/output/ShowProof.out new file mode 100644 index 0000000000..2d4be8bce7 --- /dev/null +++ b/test-suite/output/ShowProof.out @@ -0,0 +1 @@ +(fun x : Type => conj I ?Goal) diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v new file mode 100644 index 0000000000..73ecaf2200 --- /dev/null +++ b/test-suite/output/ShowProof.v @@ -0,0 +1,6 @@ +(* Was #4524 *) +Definition foo (x : Type) : True /\ True. +Proof. +split. +- exact I. + Show Proof. (* Was not finding an evar name at some time *) diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out new file mode 100644 index 0000000000..a5b55a9993 --- /dev/null +++ b/test-suite/output/auto.out @@ -0,0 +1,20 @@ +(* info auto: *) +simple apply or_intror (in core). + intro. + assumption. +Debug: (* debug auto: *) +Debug: * assumption. (*fail*) +Debug: * intro. (*fail*) +Debug: * simple apply or_intror (in core). (*success*) +Debug: ** assumption. (*fail*) +Debug: ** intro. (*success*) +Debug: ** assumption. (*success*) +(* info eauto: *) +simple apply or_intror. + intro. + exact H. +Debug: (* debug eauto: *) +Debug: 1 depth=5 +Debug: 1.1 depth=4 simple apply or_intror +Debug: 1.1.1 depth=4 intro +Debug: 1.1.1.1 depth=4 exact H diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v new file mode 100644 index 0000000000..a77b7b82e6 --- /dev/null +++ b/test-suite/output/auto.v @@ -0,0 +1,11 @@ +(* testing info/debug auto/eauto *) + +Goal False \/ (True -> True). +info_auto. +Undo. +debug auto. +Undo. +info_eauto. +Undo. +debug eauto. +Qed. 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/ltac.out b/test-suite/output/ltac.out index 1ff09e3af6..35c3057d84 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,4 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize @@ -22,11 +21,11 @@ The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -Error: No primitive equality found. +No primitive equality found. The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -Error: No primitive equality found. +No primitive equality found. Hx nat nat diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out new file mode 100644 index 0000000000..172612405f --- /dev/null +++ b/test-suite/output/ltac_missing_args.out @@ -0,0 +1,20 @@ +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing arguments for variables y and _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v new file mode 100644 index 0000000000..8ecd97aa56 --- /dev/null +++ b/test-suite/output/ltac_missing_args.v @@ -0,0 +1,19 @@ +Ltac foo x := idtac x. +Ltac bar x := fun y _ => idtac x y. +Ltac baz := foo. +Ltac qux := bar. +Ltac mydo tac := tac (). +Ltac rec x := rec. + +Goal True. + Fail foo. + Fail bar. + Fail bar True. + Fail baz. + Fail qux. + Fail mydo ltac:(fun _ _ => idtac). + Fail let tac := (fun _ => idtac) in tac. + Fail (fun _ => idtac). + Fail rec True. + Fail let rec tac x := tac in tac True. +Abort.
\ No newline at end of file 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/Discriminate.v b/test-suite/success/Discriminate.v index a759674115..6abfca4c3f 100644 --- a/test-suite/success/Discriminate.v +++ b/test-suite/success/Discriminate.v @@ -38,3 +38,10 @@ Abort. Goal ~ identity 0 1. discriminate. Qed. + +(* 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 -> False. +discriminate. +Qed. diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index da2183841d..78652fb64b 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -150,6 +150,13 @@ match goal with end. Abort. +(* Injection in the presence of local definitions *) +Inductive A := B (T := unit) (x y : bool) (z := x). +Goal forall x y x' y', B x y = B x' y' -> y = y'. +intros * [= H1 H2]. +exact H2. +Qed. + (* Injection does not project at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. 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 58f79d45ec..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. -Qed. - -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/hintdb_in_ltac.v b/test-suite/success/hintdb_in_ltac.v new file mode 100644 index 0000000000..f12b4d1f45 --- /dev/null +++ b/test-suite/success/hintdb_in_ltac.v @@ -0,0 +1,14 @@ +Definition x := 0. + +Hint Unfold x : mybase. + +Ltac autounfoldify base := autounfold with base. + +Tactic Notation "autounfoldify_bis" ident(base) := autounfold with base. + +Goal x = 0. + progress autounfoldify mybase. + Undo. + progress autounfoldify_bis mybase. + trivial. +Qed. diff --git a/test-suite/success/hintdb_in_ltac_bis.v b/test-suite/success/hintdb_in_ltac_bis.v new file mode 100644 index 0000000000..f5c25540ef --- /dev/null +++ b/test-suite/success/hintdb_in_ltac_bis.v @@ -0,0 +1,15 @@ +Parameter Foo : Prop. +Axiom H : Foo. + +Hint Resolve H : mybase. + +Ltac foo base := eauto with base. + +Tactic Notation "bar" ident(base) := + typeclasses eauto with base. + +Goal Foo. + progress foo mybase. + Undo. + progress bar mybase. +Qed.
\ 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/record_syntax.v b/test-suite/success/record_syntax.v index db2bbb0dc7..07a5bc0606 100644 --- a/test-suite/success/record_syntax.v +++ b/test-suite/success/record_syntax.v @@ -45,3 +45,11 @@ Record Foo := { foo : unit; }. Definition foo_ := {| foo := tt; |}. End E. + +Module F. + +Record Foo := { foo : nat * nat -> nat -> nat }. + +Definition foo_ := {| foo '(x,y) n := x+y+n |}. + +End F. 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. |