1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
From stdpp Require Import strings.
Lemma tc_simpl_test_lemma (P : nat → Prop) x y :
TCSimpl x y →
P x → P y.
Proof. by intros ->%TCSimpl_eq. Qed.
Check "tc_simpl_test".
Lemma tc_simpl_test (P : nat → Prop) y : P (5 + S y).
Proof.
apply (tc_simpl_test_lemma _ _ _ _). (* would be nicer with ssr [apply:] *)
Show.
Abort.
(** Check that [@Reflexive Prop ?r] picks the instance setoid_rewrite needs.
Really, we want to set [Hint Mode Reflexive] in a way that this fails, but
we cannot [1]. So at least we try to make sure the first solution found
is the right one, to not pay performance in the success case [2].
[1] https://github.com/coq/coq/issues/7916
[2] https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/merge_requests/38
*)
Lemma test_setoid_rewrite :
∃ R, @Reflexive Prop R ∧ R = iff.
Proof.
eexists. split.
- apply _.
- reflexivity.
Qed.
|
