diff options
Diffstat (limited to 'test-suite')
| -rwxr-xr-x | test-suite/coq-makefile/timing/run.sh | 3 | ||||
| -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 |
6 files changed, 341 insertions, 2 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/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. |