aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--_CoqProject1
-rw-r--r--src/Util/Tactics.v1
-rw-r--r--src/Util/Tactics/MoveLetIn.v64
3 files changed, 66 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject
index 5553993a0..e0ff28b24 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -301,6 +301,7 @@ src/Util/Tactics/EvarExists.v
src/Util/Tactics/Forward.v
src/Util/Tactics/GetGoal.v
src/Util/Tactics/Head.v
+src/Util/Tactics/MoveLetIn.v
src/Util/Tactics/Not.v
src/Util/Tactics/OnSubterms.v
src/Util/Tactics/PrintContext.v
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 60c93df2f..a4ae3dac7 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -15,6 +15,7 @@ Require Export Crypto.Util.Tactics.ETransitivity.
Require Export Crypto.Util.Tactics.EvarExists.
Require Export Crypto.Util.Tactics.Forward.
Require Export Crypto.Util.Tactics.GetGoal.
+Require Export Crypto.Util.Tactics.MoveLetIn.
Require Export Crypto.Util.Tactics.OnSubterms.
Require Export Crypto.Util.Tactics.Not.
Require Export Crypto.Util.Tactics.PrintContext.
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.