Clean up let-binding infrastructure

theories/lithium/interpreter.v

@@ -7,12 +7,15 @@ Notation "'HIDDEN'" := (Envs _ _ _) (only printing).
 Definition LET_ID {A} (x : A) : A := x.
 Arguments LET_ID : simpl never.
 Notation "'HIDDEN'" := (LET_ID _) (only printing).
+Strategy expand [LET_ID].
 
 Definition EVAR_ID {A} (x : A) : A := x.
 Arguments EVAR_ID : simpl never.
+Strategy expand [EVAR_ID].
 
 Definition SHELVED_SIDECOND (P : Prop) : Prop := P.
 Arguments SHELVED_SIDECOND : simpl never.
+Strategy expand [SHELVED_SIDECOND].
 
 (** * Lemmas used by tactics *)
 Section coq_tactics.
@@ -276,6 +279,7 @@ Ltac liEnforceInvariant :=
                 )
   end.
 
+(*
 Ltac liFresh :=
   lazymatch goal with
   | [ H := Envs _ _ ?n |- _ ] =>
@@ -292,18 +296,41 @@ Ltac liFresh :=
   end in
     constr:(IAnon n)
   end.
+ *)
+
+Tactic Notation "li_let_bind" constr(T) tactic3(tac) :=
+  try (assert_fails (is_var T);
+       let H := fresh "GOAL" in
+       pose H := (LET_ID T);
+       let G := tac H in
+       change_no_check G).
 
+(* unfold_let_goal_tac lets users unfold custom definitions. *)
+Ltac unfold_let_goal_tac H := idtac.
 Ltac liUnfoldLetGoal :=
-  match goal with
-  | |- envs_entails _ ?P =>
-    let rec go P tac :=
-        match P with
-        | ?Q ?R => go Q tac
-        | _ => is_var P; tac P
-        end in
-    go P ltac:(fun P => unfold LET_ID in P; unfold P; try clear P)
+  let do_unfold P :=
+    let H := get_head P in
+    is_var H;
+    unfold LET_ID in H;
+    unfold_let_goal_tac H;
+    (* This unfold inserts a cast but that is not too bad for
+       performance since the goal is small at this point. *)
+    unfold H;
+    try clear H
+  in
+  lazymatch goal with
+  | |- envs_entails _ (?P ∗ _) => do_unfold P
+  | |- envs_entails _ ?P => do_unfold P
   end.
 
+Ltac liUnfoldLetsContaining H :=
+  repeat match goal with
+       | Hx := context [ H ] |- _ =>
+                unfold LET_ID in Hx;
+                unfold Hx in *;
+                clear Hx
+       end.
+
 Ltac liUnfoldLetsInContext :=
   repeat match goal with
   | H := LET_ID _ |- _ => unfold LET_ID in H; unfold H; clear H
@@ -326,7 +353,7 @@ Ltac create_protected_evar A :=
       match goal with
       | _ =>
         let x := fresh "x" in
-        unshelve evar (x : A); [ liUnfoldAllEvars; liUnfoldLetsInContext; shelve |];
+        unshelve evar (x : A); [ liUnfoldLetsInContext; liUnfoldAllEvars; shelve |];
         pose (Hevar := EVAR_ID x : A); unfold x in Hevar; clear x
       end in
   Hevar.
@@ -334,6 +361,7 @@ Ltac create_protected_evar A :=
 Ltac unfold_instantiated_evar_hook H := idtac.
 
 Ltac unfold_instantiated_evar H :=
+  liUnfoldLetsContaining H;
   unfold_instantiated_evar_hook H;
   revert H;
   repeat match goal with
@@ -368,6 +396,7 @@ Ltac unfold_instantiated_evar H :=
 Ltac instantiate_protected H' tac_with :=
   lazymatch H' with
   | protected ?H =>
+    liUnfoldLetsContaining H;
     unfold EVAR_ID in H;
     (* we have to be vary careful how we instantiate the evar, as it
     may not rely on things introduced later (even let bindings),
@@ -407,7 +436,7 @@ Ltac solve_protected_eq :=
   (* intros because it is less aggressive than move => * *)
   intros;
   solve_protected_eq_unfold_tac;
-  repeat rewrite protected_eq;
+  liUnfoldLetsInContext;
   liUnfoldAllEvars;
   lazymatch goal with |- ?a = ?b => unify a b with solve_protected_eq_db end;
   exact: eq_refl.
@@ -433,18 +462,23 @@ Ltac liCheckOwnInContext P :=
 Global Hint Extern 1 (CheckOwnInContext ?P) => (liCheckOwnInContext P; constructor; exact: I) : typeclass_instances.
 
 (** * Main lithium tactics *)
-Ltac convert_to_i2p_tac P := fail "No convert_to_i2p_tac provided!".
-Ltac convert_to_i2p P cont :=
+Ltac convert_to_i2p_tac P bind cont := fail "No convert_to_i2p_tac provided!".
+Ltac convert_to_i2p P bind cont :=
   lazymatch P with
-  | subsume ?P1 ?P2 ?T => cont uconstr:(((_ : Subsume _ _) _))
-  | subsume_list ?A ?ig ?l1 ?l2 ?f ?T => cont uconstr:(((_ : SubsumeList _ _ _ _ _) _))
-  | _ => let converted := convert_to_i2p_tac P in cont converted
+  | subsume ?P1 ?P2 ?T =>
+      bind T ltac:(fun H => uconstr:(subsume P1 P2 H));
+      cont uconstr:(((_ : Subsume _ _) _))
+  | subsume_list ?A ?ig ?l1 ?l2 ?f ?T =>
+      bind T ltac:(fun H => uconstr:(subsume_list A ig l1 l2 f H));
+      cont uconstr:(((_ : SubsumeList _ _ _ _ _) _))
+  | _ => convert_to_i2p_tac P bind cont
   end.
 Ltac extensible_judgment_hook := idtac.
 Ltac liExtensibleJudgement :=
   lazymatch goal with
-  | |- envs_entails _ ?P =>
-    convert_to_i2p P ltac:(fun converted =>
+  | |- envs_entails ?Δ ?P =>
+      convert_to_i2p P ltac:(fun T tac => li_let_bind T (fun H => let X := tac H in constr:(envs_entails Δ X)))
+                       ltac:(fun converted =>
     simple notypeclasses refine (tac_apply_i2p converted _); [solve [refine _] |]; extensible_judgment_hook
   )end.
 
@@ -732,7 +766,7 @@ Ltac liSideCond :=
 
 Ltac liSep :=
   lazymatch goal with
-  | |- envs_entails _ (bi_sep ?P _) =>
+  | |- envs_entails ?Δ (bi_sep ?P ?Q) =>
     assert_fails (has_evar P);
     lazymatch P with
     | bi_sep _ _ => notypeclasses refine (tac_sep_sep_assoc _ _ _ _ _)
@@ -743,7 +777,9 @@ Ltac liSep :=
     | (□ ?P)%I => notypeclasses refine (tac_do_intro_intuit_sep _ _ _ _ _); [li_pm_reduce|]
     | match ?x with _ => _ end => fail "should not have match in sep"
     | ?P => first [
-               convert_to_i2p P ltac:(fun converted =>
+               convert_to_i2p P
+                 ltac:(fun T tac => li_let_bind T (fun H => let X := tac H in constr:(envs_entails Δ (X ∗ Q))))
+                 ltac:(fun converted =>
                simple notypeclasses refine (tac_apply_i2p_below_sep converted _); [solve[refine _] |])
              | progress liFindHyp FICSyntactic
              | simple notypeclasses refine (tac_fast_apply (tac_do_simplify_goal 0%N _ _) _); [solve [refine _] |]
@@ -774,9 +810,11 @@ Ltac liWand :=
         simple notypeclasses refine (tac_do_intro H n' P _ _ _ _ _ _ _); [reduction.pm_reflexivity..|]
       ] in
   lazymatch goal with
-  | |- envs_entails _ (bi_wand ?P _) =>
+  | |- envs_entails ?Δ (bi_wand ?P ?T) =>
       lazymatch P with
-      | bi_sep _ _ => notypeclasses refine (tac_wand_sep_assoc _ _ _ _ _)
+      | bi_sep _ _ =>
+          li_let_bind T (fun H => constr:(envs_entails Δ (bi_wand P H)));
+          notypeclasses refine (tac_wand_sep_assoc _ _ _ _ _)
       | bi_exist _ => fail "handled by do_forall"
       | bi_emp => notypeclasses refine (tac_wand_emp _ _ _)
       | bi_pure _ => notypeclasses refine (tac_do_intro_pure _ _ _ _)

theories/typing/automation.v

@@ -47,28 +47,50 @@ Ltac solve_protected_eq_unfold_tac ::=
   | |- _ => idtac
   end.
 
+Ltac unfold_let_goal_tac H ::=
+  unfold RETURN_MARKER in H.
+
 Ltac can_solve_tac ::= solve_goal.
 
 Ltac record_destruct_hint hint info ::= add_case_distinction_info hint info.
 
-Ltac convert_to_i2p_tac P ::=
+Ltac convert_to_i2p_tac P bind cont ::=
   lazymatch P with
-  | typed_value ?v ?T => uconstr:(((_ : TypedValue _) _))
-  | typed_bin_op ?v1 ?ty1 ?v2 ?ty2 ?o ?ot1 ?ot2 ?T => uconstr:(((_ : TypedBinOp _ _ _ _ _ _ _) _))
-  | typed_un_op ?v ?ty ?o ?ot ?T => uconstr:(((_ : TypedUnOp _ _ _ _) _))
-  | typed_call ?v ?P ?vl ?tys ?T => uconstr:(((_ : TypedCall _ _ _ _) _))
-  | typed_copy_alloc_id ?v1 ?ty1 ?v2 ?ty2 ?ot ?T => uconstr:(((_ : TypedCopyAllocId _ _ _ _ _) _))
-  | typed_place ?P ?l1 ?β1 ?ty1 ?T => uconstr:(((_ : TypedPlace _ _ _ _) _))
-  | typed_if ?ot ?v ?P ?T1 ?T2 => uconstr:(((_ : TypedIf _ _ _) _ _))
-  | typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _))
-  | typed_assert ?ot ?v ?ty ?s ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedAssert _ _ _) _ _ _ _ _))
-  | typed_read_end ?a ?E ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _ _) _))
-  | typed_write_end ?a ?E ?ot ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T => uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _ _ _) _))
-  | typed_addr_of_end ?l ?β ?ty ?T => uconstr:(((_ : TypedAddrOfEnd _ _ _) _))
-  | typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _))
-  | typed_annot_expr ?n ?a ?v ?P ?T => uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) )
-  | typed_annot_stmt ?a ?l ?P ?T => uconstr:(((_ : TypedAnnotStmt _ _ _) _))
-  | typed_macro_expr ?m ?es ?T => uconstr:(((_ : TypedMacroExpr _ _) _))
+  | typed_value ?v ?T =>
+      (* One could introduce more let-bindings as follows, but too
+      many let-bindings seem to hurt performance. *)
+      (* bind T ltac:(fun H => uconstr:(typed_value v H)); *)
+      cont uconstr:(((_ : TypedValue _) _))
+  | typed_bin_op ?v1 ?ty1 ?v2 ?ty2 ?o ?ot1 ?ot2 ?T =>
+      cont uconstr:(((_ : TypedBinOp _ _ _ _ _ _ _) _))
+  | typed_un_op ?v ?ty ?o ?ot ?T =>
+      cont uconstr:(((_ : TypedUnOp _ _ _ _) _))
+  | typed_call ?v ?P ?vl ?tys ?T =>
+      cont uconstr:(((_ : TypedCall _ _ _ _) _))
+  | typed_copy_alloc_id ?v1 ?ty1 ?v2 ?ty2 ?ot ?T =>
+      cont uconstr:(((_ : TypedCopyAllocId _ _ _ _ _) _))
+  | typed_place ?P ?l1 ?β1 ?ty1 ?T =>
+      cont uconstr:(((_ : TypedPlace _ _ _ _) _))
+  | typed_if ?ot ?v ?P ?T1 ?T2 =>
+      cont uconstr:(((_ : TypedIf _ _ _) _ _))
+  | typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q =>
+      cont uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _))
+  | typed_assert ?ot ?v ?ty ?s ?fn ?ls ?fr ?Q =>
+      cont uconstr:(((_ : TypedAssert _ _ _) _ _ _ _ _))
+  | typed_read_end ?a ?E ?l ?β ?ty ?ly ?T =>
+      cont uconstr:(((_ : TypedReadEnd _ _ _ _ _ _) _))
+  | typed_write_end ?a ?E ?ot ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T =>
+      cont uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _ _ _) _))
+  | typed_addr_of_end ?l ?β ?ty ?T =>
+      cont uconstr:(((_ : TypedAddrOfEnd _ _ _) _))
+  | typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T =>
+      cont uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _))
+  | typed_annot_expr ?n ?a ?v ?P ?T =>
+      cont uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) )
+  | typed_annot_stmt ?a ?l ?P ?T =>
+      cont uconstr:(((_ : TypedAnnotStmt _ _ _) _))
+  | typed_macro_expr ?m ?es ?T =>
+      cont uconstr:(((_ : TypedMacroExpr _ _) _))
   end.
 
 (** * Main automation tactics *)
@@ -95,18 +117,15 @@ End automation.
 Ltac liRIntroduceLetInGoal :=
   lazymatch goal with
   | |- @envs_entails ?PROP ?Δ ?P =>
-    let H := fresh "GOAL" in
     lazymatch P with
-    | @bi_wand ?PROP ?Q ?T =>
-      pose H := (LET_ID T); change_no_check (@envs_entails PROP Δ (@bi_wand PROP Q H))
     | @typed_val_expr ?Σ ?tG ?e ?T =>
-      pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_val_expr Σ tG e H))
+      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_val_expr Σ tG e H)))
     | @typed_write ?Σ ?tG ?b ?e ?ot ?v ?ty ?Mov ?T =>
-      pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_write Σ tG b e ot v ty Mov H))
+      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_write Σ tG b e ot v ty Mov H)))
     | @typed_place ?Σ ?tG ?P ?l1 ?β1 ?ty1 ?T =>
-      pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H))
+      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_place Σ tG P l1 β1 ty1 H)))
     | @typed_bin_op ?Σ ?tG ?v1 ?P1 ?v2 ?P2 ?op ?ot1 ?ot2 ?T =>
-      pose (H := LET_ID T); change_no_check (@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H))
+      li_let_bind T (fun H => constr:(@envs_entails PROP Δ (@typed_bin_op Σ tG v1 P1 v2 P2 op ot1 ot2 H)))
     end
   end.
 

theories/typing/automation/proof_state.v

@@ -23,8 +23,6 @@ Ltac unfold_code_marker_and_compute_map_lookup :=
 
 Definition RETURN_MARKER `{!typeG Σ} (R : val → mtype → iProp Σ) : val → mtype → iProp Σ := R.
 Notation "'HIDDEN'" := (RETURN_MARKER _) (only printing).
-(* simplify RETURN_MARKER as soon as it is applied enough in the goal *)
-Arguments RETURN_MARKER _ _ _ _ _ /.
 
 
 (** * Tactics for manipulating location information *)