blob: 4ccf910ed2d95162f6eba96e6b7976d26945d1c7 (
plain)
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
30
31
32
33
34
35
|
Require Import Crypto.Util.Tactics.Contains.
Ltac setoid_subst'' R x :=
is_var x;
match goal with
| [ H : R x ?y |- _ ]
=> free_in x y; rewrite ?H in *; clear x H
| [ H : R ?y x |- _ ]
=> free_in x y; rewrite <- ?H in *; clear x H
end.
Ltac setoid_subst' x :=
is_var x;
match goal with
| [ H : ?R x _ |- _ ] => setoid_subst'' R x
| [ H : ?R _ x |- _ ] => setoid_subst'' R x
end.
Ltac setoid_subst_rel' R :=
idtac;
match goal with
| [ H : R ?x _ |- _ ] => setoid_subst'' R x
| [ H : R _ ?x |- _ ] => setoid_subst'' R x
end.
Ltac setoid_subst_rel R := repeat setoid_subst_rel' R.
Ltac setoid_subst_all :=
repeat match goal with
| [ H : ?R ?x ?y |- _ ] => is_var x; setoid_subst'' R x
| [ H : ?R ?x ?y |- _ ] => is_var y; setoid_subst'' R y
end.
Tactic Notation "setoid_subst" ident(x) := setoid_subst' x.
Tactic Notation "setoid_subst" := setoid_subst_all.
|
