blob: b5e276f2019956d2966a282b871419f75b6865ba (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
|
(** * Machinery for reimplementing some bits of [rewrite_strat] with open pattern databases *)
Require Import Crypto.Util.Notations.
(** We build classes for rewriting in each direction, and pick lemmas
by resolving on tags and the term to be rewritten. *)
(** Base class, for bidirectional rewriting. *)
Class rewrite_eq {tagT} (tag : tagT) {A} (x y : A)
:= by_rewrite : x = y.
Arguments by_rewrite {tagT} tag {A} _ _ {_}.
Infix "<~=~>" := (rewrite_eq _) : type_scope.
Class rewrite_right_to_left_eq {tagT} (tag : tagT) {A} (x y : A)
:= by_rewrite_right_to_left : rewrite_eq tag x y.
Arguments by_rewrite_right_to_left {tagT} tag {A} _ _ {_}.
Global Instance unfold_rewrite_right_to_left_eq {tagT tag A x y} (H : @rewrite_eq tagT tag A x y)
: @rewrite_right_to_left_eq tagT tag A x y := H.
Infix "<~=" := (rewrite_right_to_left_eq _) : type_scope.
Class rewrite_left_to_right_eq {tagT} (tag : tagT) {A} (x y : A)
:= by_rewrite_left_to_right : rewrite_eq tag x y.
Arguments by_rewrite_left_to_right {tagT} tag {A} _ _ {_}.
Global Instance unfold_rewrite_left_to_right_eq {tagT tag A x y} (H : @rewrite_eq tagT tag A x y)
: @rewrite_left_to_right_eq tagT tag A x y := H.
Infix "=~>" := (rewrite_left_to_right_eq _) : type_scope.
Ltac typeclass_do_left_to_right tag from tac :=
let lem := constr:(by_rewrite_left_to_right tag from _ : from = _) in tac lem.
Ltac typeclass_do_right_to_left tag from tac :=
let lem := constr:(by_rewrite_right_to_left tag _ from : _ = from) in tac lem.
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" open_constr(from) "->" :=
typeclass_do_left_to_right tag from ltac:(fun lem => rewrite -> lem).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" open_constr(from) "->" "in" "*" :=
typeclass_do_left_to_right tag from ltac:(fun lem => rewrite -> lem in * ).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" open_constr(from) "->" "in" hyp_list(H) :=
typeclass_do_left_to_right tag from ltac:(fun lem => rewrite -> lem in H).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" open_constr(from) "->" "in" hyp_list(H) "|-" "*" :=
typeclass_do_left_to_right tag from ltac:(fun lem => rewrite -> lem in H |- *).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" open_constr(from) "->" "in" "*" "|-" "*" :=
typeclass_do_left_to_right tag from ltac:(fun lem => rewrite -> lem in * |- * ).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" open_constr(from) "->" "in" "*" "|-" :=
typeclass_do_left_to_right tag from ltac:(fun lem => rewrite -> lem in * |- ).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" "<-" open_constr(from) :=
typeclass_do_right_to_left tag from ltac:(fun lem => rewrite <- lem).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" "<-" open_constr(from) "in" "*" :=
typeclass_do_right_to_left tag from ltac:(fun lem => rewrite <- lem in * ).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" "<-" open_constr(from) "in" hyp_list(H) :=
typeclass_do_right_to_left tag from ltac:(fun lem => rewrite <- lem in H).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" "<-" open_constr(from) "in" hyp_list(H) "|-" "*" :=
typeclass_do_right_to_left tag from ltac:(fun lem => rewrite <- lem in H |- *).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" "<-" open_constr(from) "in" "*" "|-" "*" :=
typeclass_do_right_to_left tag from ltac:(fun lem => rewrite <- lem in * |- * ).
Tactic Notation "tc_rewrite" "(" open_constr(tag) ")" "<-" open_constr(from) "in" "*" "|-" :=
typeclass_do_right_to_left tag from ltac:(fun lem => rewrite <- lem in * |- ).
|
