From bf0d9280ebf806eef8ee3280f7976edb3282ae6e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 25 Aug 2016 11:48:05 -0700 Subject: Integrate suggestions from Andres --- src/Util/AutoRewrite.v | 56 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 src/Util/AutoRewrite.v (limited to 'src/Util/AutoRewrite.v') diff --git a/src/Util/AutoRewrite.v b/src/Util/AutoRewrite.v new file mode 100644 index 000000000..b5e276f20 --- /dev/null +++ b/src/Util/AutoRewrite.v @@ -0,0 +1,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 * |- ). -- cgit v1.2.3