diff options
| author | Erik Martin-Dorel | 2019-04-03 15:03:02 +0200 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-04-23 20:22:38 +0200 |
| commit | 4bc91ba5654574d156ebf2934a6fb36d31b40ff9 (patch) | |
| tree | b07446667570d47d50478a7d40f304fe4d9617ee /test-suite | |
| parent | e1e5d40a0f351cbf01f7e66d049f9a937d5f8563 (diff) | |
[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations
as suggested by @gares, and:
* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/ssr_under.out | 2 | ||||
| -rw-r--r-- | test-suite/output/ssr_under.v | 15 | ||||
| -rw-r--r-- | test-suite/ssr/over.v | 8 |
3 files changed, 21 insertions, 4 deletions
diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out index 8532b62a54..499d25391e 100644 --- a/test-suite/output/ssr_under.out +++ b/test-suite/output/ssr_under.out @@ -1,2 +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 index b11dd1509c..7335c87e61 100644 --- a/test-suite/output/ssr_under.v +++ b/test-suite/output/ssr_under.v @@ -13,3 +13,18 @@ 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/ssr/over.v b/test-suite/ssr/over.v index cd6b196eeb..8232741b0d 100644 --- a/test-suite/ssr/over.v +++ b/test-suite/ssr/over.v @@ -12,7 +12,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i). unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. over. @@ -27,7 +27,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i). unfold x2 in *; clear x2; unfold R in *; clear R; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. by rewrite over. @@ -45,7 +45,7 @@ assert (H : forall i j, i + 2 * j - i = x2 i j). unfold R in *; clear R; unfold J in *; clear J; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. over. @@ -61,7 +61,7 @@ assert (H : forall i j : nat, i + 2 * j - i = x2 i j). unfold R in *; clear R; unfold J in *; clear J; unfold I in *; clear I. - apply Under_from_eq. + apply Under_eq_from_eq. Fail done. rewrite over. |