diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-05 02:13:23 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-05 02:13:23 -0400 |
commit | 69c7f94400afa2f373ba213f3acafde44e81bad2 (patch) | |
tree | 8f5b8a911a278d952c2f77b5cd7b44129f6c0539 /src/Util/Tactics/MoveLetIn.v | |
parent | 161b2b1c7e6f018936e998fdba9ef96e3ce330b2 (diff) |
Add Tactics.MoveLetIn
Diffstat (limited to 'src/Util/Tactics/MoveLetIn.v')
-rw-r--r-- | src/Util/Tactics/MoveLetIn.v | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/src/Util/Tactics/MoveLetIn.v b/src/Util/Tactics/MoveLetIn.v new file mode 100644 index 000000000..a0ef910b2 --- /dev/null +++ b/src/Util/Tactics/MoveLetIn.v @@ -0,0 +1,64 @@ +(** * Tactics for moving around [let ... in ...] and [dlet ... in ...] *) +Require Import Crypto.Util.LetIn. +(** The tactic [sig_dlet_in_rhs_to_context] moves to the context any + [dlet x := y in ...] on the rhs of a goal of the form [{ a | lhs = + rhs }]. *) +Ltac sig_dlet_in_rhs_to_context_step v := + lazymatch goal with + | [ |- { a | _ = @Let_In ?A ?B ?x _ } ] + => pose x as v; + replace (@Let_In A B x) with (fun P : forall a : A, B a => P v) + by (clear; abstract (subst v; cbv [Let_In]; reflexivity)); + cbv beta + end. +Ltac sig_dlet_in_rhs_to_context := + repeat let v := fresh "x" in sig_dlet_in_rhs_to_context_step v. +(** The tactic [sig_dlet_in_lhs_to_context] moves to the context any + [dlet x := y in ...] on the lhs of a goal of the form [{ a | lhs = + rhs }]. *) +Ltac sig_dlet_in_lhs_to_context_step v := + lazymatch goal with + | [ |- { a | @Let_In ?A ?B ?x _ = _ } ] + => pose x as v; + replace (@Let_In A B x) with (fun P : forall a : A, B a => P v) + by (clear; abstract (subst v; cbv [Let_In]; reflexivity)); + cbv beta + end. +Ltac sig_dlet_in_lhs_to_context := + repeat let v := fresh "x" in sig_dlet_in_lhs_to_context_step v. +(** The tactic [goal_dlet_to_context] moves to the context any + [dlet x := y in ...] in the goal. *) +Ltac goal_dlet_to_context_step v := + match goal with + | [ |- context[@Let_In ?A ?B ?x] ] + => pose x as v; + replace (@Let_In A B x) with (fun P : forall a : A, B a => P v) + by (clear; abstract (subst v; cbv [Let_In]; reflexivity)); + cbv beta + end. +Ltac goal_dlet_to_context := + repeat let v := fresh "x" in goal_dlet_to_context_step v. +(** Takes in a uconstr [uc], uses [set] to find it in the goal and + passes the constr that it finds to [k] *) +Local Ltac with_uconstr_in_goal uc k := + let f := fresh in + set (f := uc); + let f' := (eval cbv delta [f] in f) in + subst f; k f'. +(** This tactic creates a [dlet x := f in rhs] in the rhs of a goal + of the form [lhs = rhs]. *) +Ltac context_to_dlet_in_rhs f := + lazymatch goal with + | [ |- ?LHS = ?RHS ] + => with_uconstr_in_goal + f + ltac:(fun f + => let RHS' := lazymatch (eval pattern f in RHS) with + | ?RHS _ => RHS + end in + let x := fresh "x" in + transitivity (dlet x := f in RHS' x); + [ | clear; abstract (cbv [Let_In]; reflexivity) ] + ) + end. +Tactic Notation "context_to_dlet_in_rhs" uconstr(f) := context_to_dlet_in_rhs f. |