diff options
Diffstat (limited to 'test-suite')
| -rwxr-xr-x | test-suite/coq-makefile/timing/run.sh | 3 | ||||
| -rw-r--r-- | test-suite/output/Inductive.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations.v | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 1 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 42 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 67 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 26 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 91 | ||||
| -rw-r--r-- | test-suite/output/bug_9180.out | 4 | ||||
| -rw-r--r-- | test-suite/output/bug_9180.v | 11 | ||||
| -rw-r--r-- | test-suite/output/ssr_under.out | 4 | ||||
| -rw-r--r-- | test-suite/output/ssr_under.v | 30 | ||||
| -rw-r--r-- | test-suite/prerequisite/ssr_mini_mathcomp.v | 2 | ||||
| -rw-r--r-- | test-suite/ssr/over.v | 70 | ||||
| -rw-r--r-- | test-suite/ssr/under.v | 234 |
16 files changed, 381 insertions, 214 deletions
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 78a3f7c63a..4ee4aae36c 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -49,16 +49,15 @@ TO_SED_IN_BOTH=( -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it + -e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622 ) TO_SED_IN_PER_FILE=( - -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start -e s'/ */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign ) TO_SED_IN_PER_LINE=( - -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start -e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives ) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index 2ba02924c9..af202ea01c 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -1,6 +1,6 @@ The command has indeed failed with message: Last occurrence of "list'" must have "A" as 1st argument in - "A -> list' A -> list' (A * A)". + "A -> list' A -> list' (A * A)%type". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x For foo: Argument scopes are [type_scope _] diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index bec4fc1579..94b86fc222 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -72,7 +72,7 @@ Nil : forall A : Type, list A NIL : list nat : list nat -(false && I 3)%bool /\ (I 6)%bool +(false && I 3)%bool /\ I 6 : Prop [|1, 2, 3; 4, 5, 6|] : Z * Z * Z * (Z * Z * Z) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 2ffc3b14e2..adab324cf0 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)). Section A. -Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. +Notation "! A" := (forall _:nat, A) (at level 60). Check ! (0=0). Check forall n, n=0. @@ -195,9 +195,9 @@ Open Scope nat_scope. Coercion is_true := fun b => b=true. Coercion of_nat n := match n with 0 => true | _ => false end. -Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). -Check (false && I 3)%bool /\ (I 6)%bool. +Check (false && I 3)%bool /\ I 6. (**********************************************************************) (* Check notations with several recursive patterns *) diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 923caedace..bcb2468792 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -71,7 +71,6 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* Note: does not work for pattern *) Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). -Open Scope nat_scope. Check fun f x => f x + S x. Open Scope list_scope. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 015dac2512..d32cf67e28 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -128,27 +128,25 @@ return (1, 2, 3, 4) : nat *(1.2) : nat -! '{{x, y}}, x + y = 0 +! '{{x, y}}, x.y = 0 : Prop exists x : nat, nat -> exists y : nat, - nat -> - exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x + y = 0 /\ u + t = 0 + nat -> exists '{{u, t}}, forall z1 : nat, z1 = 0 /\ x.y = 0 /\ u.t = 0 : Prop exists x : nat, nat -> exists y : nat, - nat -> - exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x + y = 0 /\ z + t = 0 + nat -> exists '{{z, t}}, forall z2 : nat, z2 = 0 /\ x.y = 0 /\ z.t = 0 : Prop -exists_true '{{x, y}} (u := 0) '{{z, t}}, x + y = 0 /\ z + t = 0 +exists_true '{{x, y}} (u := 0) '{{z, t}}, x.y = 0 /\ z.t = 0 : Prop exists_true (A : Type) (R : A -> A -> Prop) (_ : Reflexive R), (forall x : A, R x x) : Prop exists_true (x : nat) (A : Type) (R : A -> A -> Prop) -(_ : Reflexive R) (y : nat), x + y = 0 -> forall z : A, R z z +(_ : Reflexive R) (y : nat), x.y = 0 -> forall z : A, R z z : Prop {{{{True, nat -> True}}, nat -> True}} : Prop * Prop * Prop @@ -184,22 +182,22 @@ pair (prod nat (prod nat nat))) (prod (prod nat nat) nat) fun x : nat => if x is n .+ 1 then n else 1 : nat -> nat -{'{{x, y}} : nat * nat | x + y = 0} +{'{{x, y}} : nat * nat | x.y = 0} : Set exists2' {{x, y}}, x = 0 & y = 0 : Prop myexists2 x : nat * nat, let '{{y, z}} := x in y > z & let '{{y, z}} := x in z > y : Prop -fun '({{x, y}} as z) => x + y = 0 /\ z = z +fun '({{x, y}} as z) => x.y = 0 /\ z = z : nat * nat -> Prop -myexists ({{x, y}} as z), x + y = 0 /\ z = z +myexists ({{x, y}} as z), x.y = 0 /\ z = z : Prop -exists '({{x, y}} as z), x + y = 0 /\ z = z +exists '({{x, y}} as z), x.y = 0 /\ z = z : Prop -∀ '({{x, y}} as z), x + y = 0 /\ z = z +∀ '({{x, y}} as z), x.y = 0 /\ z = z : Prop -fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x + y +fun '({{{{x, y}}, true}} | {{{{x, y}}, false}}) => x.y : nat * nat * bool -> nat myexists ({{{{x, y}}, true}} | {{{{x, y}}, false}}), x > y : Prop @@ -211,17 +209,17 @@ fun p : nat => if p is S n then n else 0 : nat -> nat fun p : comparison => if p is Lt then 1 else 0 : comparison -> nat -fun S : nat => [S | S + S] +fun S : nat => [S | S.S] : nat -> nat * (nat -> nat) -fun N : nat => [N | N + 0] +fun N : nat => [N | N.0] : nat -> nat * (nat -> nat) -fun S : nat => [[S | S + S]] +fun S : nat => [[S | S.S]] : nat -> nat * (nat -> nat) {I : nat | I = I} : Set {'I : True | I = I} : Prop -{'{{x, y}} : nat * nat | x + y = 0} +{'{{x, y}} : nat * nat | x.y = 0} : Set exists2 '{{y, z}} : nat * nat, y > z & z > y : Prop @@ -254,13 +252,3 @@ myfoo01 tt : nat myfoo01 tt : nat -[{0; 0}] - : list (list nat) -[{1; 2; 3}; - {4; 5; 6}; - {7; 8; 9}] - : list (list nat) -amatch = mmatch 0 (with 0 => 1| 1 => 2 end) - : unit -alist = [0; 1; 2] - : list nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 2caffad1d9..dcc8bd7165 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) -Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -183,13 +183,9 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) -Section S1. -Variable plus : nat -> nat -> nat. -Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. -End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). @@ -197,12 +193,10 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -Section S2. -Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). Check (((id 1) + 2) + 3). Check (id (1 + 2)). -End S2. (* Test contraction of "forall x, let 'pat := x in ..." into "forall 'pat, ..." *) (* for isolated "forall" (was not working already in 8.6) *) @@ -416,58 +410,3 @@ Check myfoo0 1 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] Check myfoo01 tt. (* was printing [myfoo0 1 HI], but should print [myfoo01 HI] *) End Issue8126. - -(* Test printing of notations guided by scope *) - -Module A. - -Declare Scope line_scope. -Delimit Scope line_scope with line. -Declare Scope matx_scope. -Notation "{ }" := nil (format "{ }") : line_scope. -Notation "{ x }" := (cons x nil) : line_scope. -Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. -Notation "[ ]" := nil (format "[ ]") : matx_scope. -Notation "[ l ]" := (cons l%line nil) : matx_scope. -Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) - (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. - -Open Scope matx_scope. -Check [[0;0]]. -Check [[1;2;3];[4;5;6];[7;8;9]]. - -End A. - -(* Example by Beta Ziliani *) - -Require Import Lists.List. - -Module B. - -Import ListNotations. - -Declare Scope pattern_scope. -Delimit Scope pattern_scope with pattern. - -Declare Scope patterns_scope. -Delimit Scope patterns_scope with patterns. - -Notation "a => b" := (a, b) (at level 201) : pattern_scope. -Notation "'with' p1 | .. | pn 'end'" := - ((cons p1%pattern (.. (cons pn%pattern nil) ..))) - (at level 91, p1 at level 210, pn at level 210) : patterns_scope. - -Definition mymatch (n:nat) (l : list (nat * nat)) := tt. -Arguments mymatch _ _%patterns. -Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). - -Close Scope patterns_scope. -Close Scope pattern_scope. - -Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. -Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) - -Definition alist := [0;1;2]. -Print alist. - -End B. diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 5bf4ec7bfb..9d972a68f7 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -21,36 +21,10 @@ Let "x" e1 e2 : expr Let "x" e1 e2 : expr -fun x : nat => (# x)%nat - : nat -> nat -fun x : nat => ## x - : nat -> nat -fun x : nat => # x - : nat -> nat -fun x : nat => ### x - : nat -> nat -fun x : nat => ## x - : nat -> nat -fun x : nat => (x.-1)%pred - : nat -> nat -∀ a : nat, a = 0 - : Prop -((∀ a : nat, a = 0) -> True)%type - : Prop -# - : Prop -# -> True - : Prop -((∀ a : nat, a = 0) -> True)%type - : Prop -## - : Prop myAnd1 True True : Prop r 2 3 : Prop -Notation Cn := Foo.FooCn -Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn let v := 0%test17 in v : myint63 : myint63 fun y : nat => # (x, z) |-> y & y diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index b33ad17ed4..81c64418cb 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -5,8 +5,8 @@ Module A. Declare Custom Entry myconstr. Notation "[ x ]" := x (x custom myconstr at level 6). -Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5) : nat_scope. -Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4) : nat_scope. +Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5). +Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. @@ -95,76 +95,6 @@ Check (Let "x" e1 e2). End D. -(* Check fix of #8551: a delimiter should be inserted because the - lonely notation hides the scope nat_scope, even though the latter - is open *) - -Module E. - -Notation "# x" := (S x) (at level 20) : nat_scope. -Notation "# x" := (Some x). -Check fun x => (# x)%nat. - -End E. - -(* Other tests of precedence *) - -Module F. - -Notation "# x" := (S x) (at level 20) : nat_scope. -Notation "## x" := (S x) (at level 20). -Check fun x => S x. -Open Scope nat_scope. -Check fun x => S x. -Notation "### x" := (S x) (at level 20) : nat_scope. -Check fun x => S x. -Close Scope nat_scope. -Check fun x => S x. - -End F. - -(* Lower priority of generic application rules *) - -Module G. - -Declare Scope predecessor_scope. -Delimit Scope predecessor_scope with pred. -Declare Scope app_scope. -Delimit Scope app_scope with app. -Notation "x .-1" := (Nat.pred x) (at level 10, format "x .-1") : predecessor_scope. -Notation "f ( x )" := (f x) (at level 10, format "f ( x )") : app_scope. -Check fun x => pred x. - -End G. - -(* Checking arbitration between in the presence of a notation in type scope *) - -Module H. - -Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) - (at level 200, x binder, y binder, right associativity, - format "'[ ' '[ ' ∀ x .. y ']' , '/' P ']'") : type_scope. -Check forall a, a = 0. - -Close Scope type_scope. -Check ((forall a, a = 0) -> True)%type. -Open Scope type_scope. - -Notation "#" := (forall a, a = 0). -Check #. -Check # -> True. - -Close Scope type_scope. -Check (# -> True)%type. -Open Scope type_scope. - -Declare Scope my_scope. -Notation "##" := (forall a, a = 0) : my_scope. -Open Scope my_scope. -Check ##. - -End H. - (* Fixing bugs reported by G. Gonthier in #9207 *) Module I. @@ -181,23 +111,6 @@ Check r 2 3. End I. -(* Fixing a bug reported by G. Gonthier in #9207 *) - -Module J. - -Module Import Mfoo. -Module Foo. -Definition FooCn := 2. -Module Bar. -Notation Cn := FooCn. -End Bar. -End Foo. -Export Foo.Bar. -End Mfoo. -About Cn. - -End J. - Require Import Coq.Numbers.Cyclic.Int63.Int63. Module NumeralNotations. Module Test17. diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out new file mode 100644 index 0000000000..ed4892b389 --- /dev/null +++ b/test-suite/output/bug_9180.out @@ -0,0 +1,4 @@ +Notation +"n .+1" := S n : nat_scope (default interpretation) +forall x : nat, x.+1 = x.+1 + : Prop diff --git a/test-suite/output/bug_9180.v b/test-suite/output/bug_9180.v new file mode 100644 index 0000000000..f221a94a50 --- /dev/null +++ b/test-suite/output/bug_9180.v @@ -0,0 +1,11 @@ +Notation succn := (Datatypes.S). + +Notation "n .+1" := (succn n) (at level 2, left associativity, + format "n .+1") : nat_scope. + +Locate ".+1". +(* Notation *) +(* "n .+1" := S n : nat_scope (default interpretation) *) +(** so Coq does not apply succn notation *) + +Check forall x : nat, x.+1 = x.+1. diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out new file mode 100644 index 0000000000..499d25391e --- /dev/null +++ b/test-suite/output/ssr_under.out @@ -0,0 +1,4 @@ +'Under[ m - m ] +(G (fun _ : nat => 0) n >= 0) +'Under[ r = R0 \/ E r ] +(Rbar_le Rbar0 (Lub_Rbar (fun r : R => r = R0 \/ E r))) diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v new file mode 100644 index 0000000000..fb7503d902 --- /dev/null +++ b/test-suite/output/ssr_under.v @@ -0,0 +1,30 @@ +From Coq Require Import ssreflect. + +Axiom subnn : forall n : nat, n - n = 0. +Parameter G : (nat -> nat) -> nat -> nat. +Axiom eq_G : + forall F1 F2 : nat -> nat, + (forall n : nat, F1 n = F2 n) -> + forall n : nat, G F1 n = G F2 n. + +Ltac show := match goal with [|-?g] => idtac g end. + +Lemma example_G (n : nat) : G (fun n => n - n) n >= 0. +under eq_G => m do [show; rewrite subnn]. +show. +Abort. + +Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar). +Parameter Rbar_le : Rbar -> Rbar -> Prop. +Parameter Lub_Rbar : (R -> Prop) -> Rbar. +Parameter Lub_Rbar_eqset : + forall E1 E2 : R -> Prop, + (forall x : R, E1 x <-> E2 x) -> + Lub_Rbar E1 = Lub_Rbar E2. + +Lemma test_Lub_Rbar (E : R -> Prop) : + Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)). +Proof. +under Lub_Rbar_eqset => r do show. +show. +Abort. diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v index cb2c56736c..ca360f65a7 100644 --- a/test-suite/prerequisite/ssr_mini_mathcomp.v +++ b/test-suite/prerequisite/ssr_mini_mathcomp.v @@ -427,6 +427,8 @@ Lemma leqnSn n : n <= n.+1. Proof. by elim: n. Qed. Lemma leq_trans n m p : m <= n -> n <= p -> m <= p. Admitted. +Lemma leq_ltn_trans n m p : m <= n -> n < p -> m < p. +Admitted. Lemma leqW m n : m <= n -> m <= n.+1. Admitted. Hint Resolve leqnSn. diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v new file mode 100644 index 0000000000..8232741b0d --- /dev/null +++ b/test-suite/ssr/over.v @@ -0,0 +1,70 @@ +Require Import ssreflect. + +Axiom daemon : False. Ltac myadmit := case: daemon. + +(** Testing over for the 1-var case *) + +Lemma test_over_1_1 : False. +intros. +evar (I : Type); evar (R : Type); evar (x2 : I -> R). +assert (H : forall i : nat, i + 2 * i - i = x2 i). + intros i. + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold I in *; clear I. + apply Under_eq_from_eq. + Fail done. + + over. + myadmit. +Qed. + +Lemma test_over_1_2 : False. +intros. +evar (I : Type); evar (R : Type); evar (x2 : I -> R). +assert (H : forall i : nat, i + 2 * i - i = x2 i). + intros i. + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold I in *; clear I. + apply Under_eq_from_eq. + Fail done. + + by rewrite over. + myadmit. +Qed. + +(** Testing over for the 2-var case *) + +Lemma test_over_2_1 : False. +intros. +evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). +assert (H : forall i j, i + 2 * j - i = x2 i j). + intros i j. + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold J in *; clear J; + unfold I in *; clear I. + apply Under_eq_from_eq. + Fail done. + + over. + myadmit. +Qed. + +Lemma test_over_2_2 : False. +intros. +evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R). +assert (H : forall i j : nat, i + 2 * j - i = x2 i j). + intros i j. + unfold x2 in *; clear x2; + unfold R in *; clear R; + unfold J in *; clear J; + unfold I in *; clear I. + apply Under_eq_from_eq. + Fail done. + + rewrite over. + done. + myadmit. +Qed. diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v new file mode 100644 index 0000000000..f285ad138b --- /dev/null +++ b/test-suite/ssr/under.v @@ -0,0 +1,234 @@ +Require Import ssreflect. +Require Import ssrbool TestSuite.ssr_mini_mathcomp. +Global Unset SsrOldRewriteGoalsOrder. + +(* under <names>: {occs}[patt]<lemma>. + under <names>: {occs}[patt]<lemma> by tac1. + under <names>: {occs}[patt]<lemma> by [tac1 | ...]. + *) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Axiom daemon : False. Ltac myadmit := case: daemon. + +Module Mocks. + +(* Mock bigop.v definitions to test the behavior of under with bigops + without requiring mathcomp *) + +Definition eqfun := + fun (A B : Type) (f g : forall _ : B, A) => forall x : B, @eq A (f x) (g x). + +Section Defix. +Variables (T : Type) (n : nat) (f : forall _ : T, T) (x : T). +Fixpoint loop (m : nat) : T := + match m return T with + | O => x + | S i => f (loop i) + end. +Definition iter := loop n. +End Defix. + +Parameter eq_bigl : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P1 P2 : pred I) (F : forall _ : I, R) (_ : @eqfun bool I P1 P2), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P1 i) (F i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P2 i) (F i))). + +Parameter eq_big : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P1 P2 : pred I) (F1 F2 : forall _ : I, R) (_ : @eqfun bool I P1 P2) + (_ : forall (i : I) (_ : is_true (P1 i)), @eq R (F1 i) (F2 i)), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P1 i) (F1 i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P2 i) (F2 i))). + +Parameter eq_bigr : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type) + (r : list I) (P : pred I) (F1 F2 : forall _ : I, R) + (_ : forall (i : I) (_ : is_true (P i)), @eq R (F1 i) (F2 i)), + @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P i) (F1 i))) + (@bigop R I idx r (fun i : I => @BigBody R I i op (P i) (F2 i))). + +Parameter big_const_nat : + forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (m n : nat) (x : R), + @eq R (@bigop R nat idx (index_iota m n) (fun i : nat => @BigBody R nat i op true x)) + (@iter R (subn n m) (op x) idx). + +Delimit Scope N_scope with num. +Delimit Scope nat_scope with N. + +Reserved Notation "\sum_ ( m <= i < n | P ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n | P ) '/ ' F ']'"). +Reserved Notation "\sum_ ( m <= i < n ) F" + (at level 41, F at level 41, i, m, n at level 50, + format "'[' \sum_ ( m <= i < n ) '/ ' F ']'"). + +Local Notation "+%N" := addn (at level 0, only parsing). + +Notation "\sum_ ( m <= i < n | P ) F" := + (\big[+%N/0%N]_(m <= i < n | P%B) F%N) : (*nat_scope*) big_scope. +Notation "\sum_ ( m <= i < n ) F" := + (\big[+%N/0%N]_(m <= i < n) F%N) : (*nat_scope*) big_scope. + +Parameter iter_addn_0 : forall m n : nat, @eq nat (@iter nat n (addn m) O) (muln m n). + +End Mocks. + +Import Mocks. + +(*****************************************************************************) + +Lemma test_big_nested_1 (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). +Proof. +(* in interactive mode *) +under eq_bigr => i Hi. + under eq_big => [j|j Hj]. + { rewrite muln1. over. } + { rewrite addnC. over. } + simpl. (* or: cbv beta. *) + over. +by []. +Qed. + +Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). +Proof. +(* in one-liner mode *) +under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1 | rewrite addnC ]. +done. +Qed. + +Lemma test_big_2cond_0intro (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +under eq_big. +{ move=> n; rewrite (addnC n 1); over. } +{ move=> i Hi; rewrite (addnC i 2); over. } +done. +Qed. + +Lemma test_big_2cond_1intro (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +Fail under eq_big => i. +(* as it amounts to [under eq_big => [i]] *) +Abort. + +Lemma test_big_2cond_all (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in interactive mode *) +Fail under eq_big => *. +(* as it amounts to [under eq_big => [*]] *) +Abort. + +Lemma test_big_2cond_all_implied (F : nat -> nat) (m : nat) : + \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0. +Proof. +(* in one-liner mode *) +under eq_big do [rewrite addnC + |rewrite addnC]. +(* amounts to [under eq_big => [*|*] do [...|...]] *) +done. +Qed. + +Lemma test_big_patt1 (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0. +Proof. +under [in RHS]eq_bigr => i Hi. + by rewrite addnC over. +done. +Qed. + +Lemma test_big_patt2 (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (F i + F i) = + \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2). +Proof. +under [X in _ = _ + X]eq_bigr => i Hi do rewrite mulnS muln1. +by rewrite big_const_nat iter_addn_0. +Qed. + +Lemma test_big_occs (F G : nat -> nat) (n : nat) : + \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0). +Proof. +under {2}[in RHS]eq_bigr => i Hi do rewrite muln0. +by rewrite big_const_nat iter_addn_0. +Qed. + +(* Solely used, one such renaming is useless in practice, but it works anyway *) +Lemma test_big_cosmetic (F G : nat -> nat) (m n : nat) : + \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) = + \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i). +Proof. +under [RHS]eq_bigr => a A do under eq_bigr => b B do []. (* renaming bound vars *) +myadmit. +Qed. + +Lemma test_big_andb (F : nat -> nat) (m n : nat) : + \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1. +Proof. +under eq_bigl => i do [rewrite andb_idl; first by move/eqP->]. +under eq_bigr => i do move/eqP=>{1}->. (* the 2nd occ should not be touched *) +myadmit. +Qed. + +Lemma test_foo (f1 f2 : nat -> nat) (f_eq : forall n, f1 n = f2 n) + (G : (nat -> nat) -> nat) + (Lem : forall f1 f2 : nat -> nat, + True -> + (forall n, f1 n = f2 n) -> + False = False -> + G f1 = G f2) : + G f1 = G f2. +Proof. +(* +under x: Lem. +- done. +- rewrite f_eq; over. +- done. + *) +under Lem => [|x|] do [done|rewrite f_eq|done]. +done. +Qed. + + +(* Inspired From Coquelicot.Lub. *) +(* http://coquelicot.saclay.inria.fr/html/Coquelicot.Lub.html#Lub_Rbar_eqset *) + +Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar). +Parameter Rbar_le : Rbar -> Rbar -> Prop. +Parameter Lub_Rbar : (R -> Prop) -> Rbar. +Parameter Lub_Rbar_eqset : + forall E1 E2 : R -> Prop, + (forall x : R, E1 x <-> E2 x) -> + Lub_Rbar E1 = Lub_Rbar E2. + +Lemma test_Lub_Rbar (E : R -> Prop) : + Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)). +Proof. +under Lub_Rbar_eqset => r. +by rewrite over. +Abort. + + +Lemma ex_iff R (P1 P2 : R -> Prop) : + (forall x : R, P1 x <-> P2 x) -> ((exists x, P1 x) <-> (exists x, P2 x)). +Proof. +by move=> H; split; move=> [x Hx]; exists x; apply H. +Qed. + +Arguments ex_iff [R P1] P2 iffP12. + +Require Import Setoid. +Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True. +under ex_iff => n. +by rewrite over. +Abort. |