try if tac_apply_i2p is faster

theories/lithium/interpreter.v

@@ -28,6 +28,14 @@ Section coq_tactics.
     (P1 -∗ P2) → envs_entails Δ (P1 ∗ T) → envs_entails Δ (P2 ∗ T).
   Proof. by rewrite envs_entails_eq => -> HP. Qed.
 
+  Lemma tac_apply_i2p {Δ} {P : iProp Σ} (P' : iProp_to_Prop P) :
+    envs_entails Δ P'.(i2p_P) → envs_entails Δ P.
+  Proof. rewrite envs_entails_eq. etrans; [done|]. apply i2p_proof. Qed.
+
+  Lemma tac_apply_i2p_below_sep {Δ} {P T : iProp Σ} (P' : iProp_to_Prop P) :
+    envs_entails Δ (P'.(i2p_P) ∗ T) → envs_entails Δ (P ∗ T).
+  Proof. rewrite envs_entails_eq. etrans; [done|]. apply bi.sep_mono_l. apply i2p_proof. Qed.
+
   Lemma tac_protected_eq_app {A} (f : A → Prop) a :
     f a → f (protected a).
   Proof. by rewrite protected_eq. Qed.
@@ -435,8 +443,8 @@ Global Hint Extern 1 (CheckOwnInContext ?P) => (liCheckOwnInContext P; construct
 Ltac convert_to_i2p_tac P := fail "No convert_to_i2p_tac provided!".
 Ltac convert_to_i2p P cont :=
   lazymatch P with
-  | subsume ?P1 ?P2 ?T => cont uconstr:(((_ : Subsume _ _) _).(i2p_proof))
-  | subsume_list ?A ?ig ?l1 ?l2 ?f ?T => cont uconstr:(((_ : SubsumeList _ _ _ _ _) _).(i2p_proof))
+  | 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
   end.
 Ltac extensible_judgment_hook := idtac.
@@ -444,7 +452,7 @@ Ltac liExtensibleJudgement :=
   lazymatch goal with
   | |- envs_entails _ ?P =>
     convert_to_i2p P ltac:(fun converted =>
-    simple notypeclasses refine (tac_fast_apply converted _); [solve [refine _] |]; extensible_judgment_hook
+    simple notypeclasses refine (tac_apply_i2p converted _); [solve [refine _] |]; extensible_judgment_hook
   )end.
 
 Ltac liSimpl :=
@@ -734,7 +742,7 @@ Ltac liSep :=
     | match ?x with _ => _ end => fail "should not have match in sep"
     | ?P => first [
                convert_to_i2p P ltac:(fun converted =>
-               simple notypeclasses refine (tac_fast_apply_below_sep converted _); [solve[refine _] |])
+               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 _] |]
              | simple notypeclasses refine (tac_fast_apply (tac_intro_subsume_related _ _) _); [solve [refine _] |];

theories/typing/automation.v

@@ -53,22 +53,22 @@ Ltac record_destruct_hint hint info ::= add_case_distinction_info hint info.
 
 Ltac convert_to_i2p_tac P ::=
   lazymatch P with
-  | typed_value ?v ?T => uconstr:(((_ : TypedValue _) _).(i2p_proof))
-  | typed_bin_op ?v1 ?ty1 ?v2 ?ty2 ?o ?ot1 ?ot2 ?T => uconstr:(((_ : TypedBinOp _ _ _ _ _ _ _) _).(i2p_proof))
-  | typed_un_op ?v ?ty ?o ?ot ?T => uconstr:(((_ : TypedUnOp _ _ _ _) _).(i2p_proof))
-  | typed_call ?v ?P ?vl ?tys ?T => uconstr:(((_ : TypedCall _ _ _ _) _).(i2p_proof))
-  | typed_copy_alloc_id ?v1 ?ty1 ?v2 ?ty2 ?ot ?T => uconstr:(((_ : TypedCopyAllocId _ _ _ _ _) _).(i2p_proof))
-  | typed_place ?P ?l1 ?β1 ?ty1 ?T => uconstr:(((_ : TypedPlace _ _ _ _) _).(i2p_proof))
-  | typed_if ?ot ?v ?P ?T1 ?T2 => uconstr:(((_ : TypedIf _ _ _) _ _).(i2p_proof))
-  | typed_switch ?v ?ty ?it ?m ?ss ?def ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedSwitch _ _ _) _ _ _ _ _ _ _).(i2p_proof))
-  | typed_assert ?ot ?v ?ty ?s ?fn ?ls ?fr ?Q => uconstr:(((_ : TypedAssert _ _ _) _ _ _ _ _).(i2p_proof))
-  | typed_read_end ?a ?E ?l ?β ?ty ?ly ?T => uconstr:(((_ : TypedReadEnd _ _ _ _ _ _) _).(i2p_proof))
-  | typed_write_end ?a ?E ?ot ?v1 ?ty1 ?l2 ?β2 ?ty2 ?T => uconstr:(((_ : TypedWriteEnd _ _ _ _ _ _ _ _) _).(i2p_proof))
-  | typed_addr_of_end ?l ?β ?ty ?T => uconstr:(((_ : TypedAddrOfEnd _ _ _) _).(i2p_proof))
-  | typed_cas ?ot ?v1 ?P1 ?v2 ?P2 ?v3 ?P3 ?T => uconstr:(((_ : TypedCas _ _ _ _ _ _ _) _).(i2p_proof))
-  | typed_annot_expr ?n ?a ?v ?P ?T => uconstr:(((_ : TypedAnnotExpr _ _ _ _) _) .(i2p_proof))
-  | typed_annot_stmt ?a ?l ?P ?T => uconstr:(((_ : TypedAnnotStmt _ _ _) _).(i2p_proof))
-  | typed_macro_expr ?m ?es ?T => uconstr:(((_ : TypedMacroExpr _ _) _).(i2p_proof))
+  | 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 _ _) _))
   end.
 
 (** * Main automation tactics *)