diff options
| author | Erik Martin-Dorel | 2019-12-27 00:13:52 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-12-27 00:30:26 +0100 |
| commit | ec2d1bc0d0f0447f8824def545697b8c05fcb670 (patch) | |
| tree | f120e755c0c0cf09919874288dfb3335f8de0a24 /test-suite | |
| parent | 4c19baf3a1b0ee9b1e94df4bca29c53125445db8 (diff) | |
fix: Shorten ssrsetoid.v
* This patch is a quick fix that removes part of the features of coq/coq#10022,
namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged
relation R. This just means we'll need to do an extra step [rewrite UnderE.]
which was unnecessary with Coq 8.11+alpha.
* This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient
feature of coq/coq#10022 (generalize under & over to any Reflexive relation).
* Related: coq-community/atbr#23
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ssr/under.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v index c12491138a..0312b9c733 100644 --- a/test-suite/ssr/under.v +++ b/test-suite/ssr/under.v @@ -313,8 +313,7 @@ Qed. End TestGeneric2. Section TestPreOrder. -(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 - but without needing to do [rewrite UnderE] manually. *) +(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 *) Require Import Morphisms. @@ -330,7 +329,7 @@ Parameter leq_mul : Local Notation "+%N" := addn (at level 0, only parsing). -(** Context lemma (could *) +(** Context lemma *) Lemma leq'_big : forall I (F G : I -> nat) (r : seq I), (forall i : I, leq' (F i) (G i)) -> (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)). @@ -370,8 +369,10 @@ have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n). under leq'_big => i. { - (* The "magic" is here: instantiate the evar with the bound "3 + n" *) - rewrite lem ?ltn_ord //. over. + rewrite UnderE. + + (* instantiate the evar with the bound "3 + n" *) + apply: lem; exact: ltn_ord. } cbv beta. |