Allow semantic instead of syntactic comparison for finding hypothesis

linux/pkvm/proofs/early_alloc/instances.v

@@ -2,6 +2,32 @@ From refinedc.typing Require Import typing.
 From refinedc.linux.pkvm.early_alloc Require Import generated_spec.
 Set Default Proof Using "Type".
 
+(*** Demonstration of FindHypEqual ***)
+(* Instance simpl_loc_offset_0_times (l : loc) (n : Z): *)
+(*   SimplLoc (l +ₗ 0%nat * n) l. *)
+(* Proof. assert (0%nat * n = 0) as -> by lia. by rewrite shift_loc_0. Qed. *)
+
+(* TODO: move this to own.v or somewhere in the automation folder *)
+Inductive FICLocSemantic : Set :=.
+Global Instance find_in_context_type_loc_semantic_inst `{!typeG Σ} l :
+  FindInContext (FindLoc l) 2%nat FICLocSemantic :=
+  λ T, i2p (find_in_context_type_loc_id l T).
+
+(* TODO: move this to somewhere in the automation folder *)
+Lemma tac_solve_loc_eq `{!typeG Σ} l1 β1 ty1 l2 β2 ty2:
+  l1 = l2 →
+  FindHypEqual FICLocSemantic (l1 ◁ₗ{β1} ty1) (l2 ◁ₗ{β2} ty2) (l1 ◁ₗ{β2} ty2).
+Proof. by move => ->. Qed.
+
+(* TODO: move this to somewhere in the automation folder and implement
+it properly. *)
+Ltac solve_loc_eq :=
+  rewrite ?shift_loc_0; done.
+
+(* TODO: move this to somewhere in the automation folder *)
+Hint Extern 10 (FindHypEqual FICLocSemantic (_ ◁ₗ{_} _) (_ ◁ₗ{_} _) _) =>
+  (notypeclasses refine (tac_solve_loc_eq _ _ _ _ _ _ _); solve_loc_eq) : typeclass_instances.
+
 (*** Simplification of locations ***)
 
 Class SimplLoc (l1 l2 : loc) : Prop := simpl_loc : l1 = l2.
@@ -18,10 +44,6 @@ Instance simpl_loc_shift_loc_assoc (l : loc) (n1 n2 : Z):
   SimplLoc (l +ₗ n1 +ₗ n2) (l +ₗ (n1 + n2)).
 Proof. by rewrite shift_loc_assoc. Qed.
 
-Instance simpl_loc_offset_0_times (l : loc) (n : Z):
-  SimplLoc (l +ₗ 0%nat * n) l.
-Proof. assert (0%nat * n = 0) as -> by lia. by rewrite shift_loc_0. Qed.
-
 Instance simpl_loc_offset_add_assoc id p n1 n2:
   SimplLoc (id, p + n1 + n2) (id, p + (n1 + n2)).
 Proof. by rewrite Z.add_assoc. Qed.

theories/lithium/classes.v

@@ -19,8 +19,11 @@ Record find_in_context_info {Σ} : Type := {
 (* The nat n is necessary to allow different options, they are tried starting from 0. *)
 Definition find_in_context {Σ} (fic : find_in_context_info) (T : fic.(fic_A) → iProp Σ) : iProp Σ :=
   (∃ b, fic.(fic_Prop) b ∗ T b).
-Class FindInContext {Σ} (fic : find_in_context_info) (n : nat) : Type :=
-  find_in_context_proof T: iProp_to_Prop (Σ:=Σ) (find_in_context fic T).
+Class FindInContext {Σ} (fic : find_in_context_info) (n : nat) (key : Set) : Type :=
+  find_in_context_proof T: iProp_to_Prop (Σ:=Σ) (find_in_context fic T)
+.
+Hint Mode FindInContext + + + - : typeclass_instances.
+Inductive FICSyntactic : Set :=.
 
 (** ** Instances  *)
 Definition FindDirect {Σ A} (P : A → iProp Σ) := {| fic_A := A; fic_Prop := P; |}.
@@ -31,9 +34,12 @@ Lemma find_in_context_direct {Σ B} P (T : B → iProp Σ):
    find_in_context (FindDirect P) T.
 Proof. done. Qed.
 Global Instance find_in_context_direct_inst {Σ B} (P : _ → iProp Σ) :
-  FindInContext (FindDirect P) 0%nat :=
+  FindInContext (FindDirect P) 0%nat FICSyntactic :=
   λ T : B → _, i2p (find_in_context_direct P T).
 
+(** ** [FindHypEqual]  *)
+Class FindHypEqual {Σ} (key : Type) (Q P P' : iProp Σ) := find_hyp_equal_equal: P = P'.
+Hint Mode FindHypEqual + + + ! - : typeclass_instances.
 
 (** * [destruct_hint] *)
 Inductive destruct_hint_info :=
@@ -48,6 +54,7 @@ Arguments destruct_hint : simpl never.
 Class RelatedTo {Σ} (pat : iProp Σ) : Type := {
   rt_fic : find_in_context_info (Σ:=Σ);
 }.
+Hint Mode RelatedTo + + : typeclass_instances.
 Arguments rt_fic {_ _} _.
 
 (** * [IntroPersistent] *)
@@ -55,6 +62,7 @@ Arguments rt_fic {_ _} _.
 Class IntroPersistent {Σ} (P P' : iProp Σ) := {
   ip_persistent : P -∗ □ P'
 }.
+Hint Mode IntroPersistent + + - : typeclass_instances.
 (** ** Instances *)
 Global Instance intro_persistent_intuit Σ (P : iProp Σ) : IntroPersistent (□ P) P.
 Proof. constructor. iIntros "$". Qed.

theories/lithium/interpreter.v

@@ -41,6 +41,10 @@ Section coq_tactics.
     (∃ (a : A) (x : f a), P (existT a x)) → @ex (sigT f) P.
   Proof. move => [?[??]]. eauto. Qed.
 
+  Lemma tac_find_hyp_equal key (Q P P' R : iProp Σ) Δ `{!FindHypEqual key Q P P'}:
+    envs_entails Δ (P' ∗ R) →
+    envs_entails Δ (P ∗ R).
+  Proof. by revert select (FindHypEqual _ _ _ _) => ->. Qed.
 
   Lemma tac_find_hyp Δ i p R (P : iProp Σ) :
     envs_lookup i Δ = Some (p, P) →
@@ -51,7 +55,6 @@ Section coq_tactics.
       by apply bi.sep_mono_r.
   Qed.
 
-
   Lemma tac_do_exist A Δ (P : A → iProp Σ) :
     (∃ x, envs_entails Δ (P x)) → envs_entails Δ (∃ x : A, P x).
   Proof.
@@ -122,13 +125,14 @@ Section coq_tactics.
     end →
     envs_entails Δ (P -∗ T).
   Proof.
+    revert select (IntroPersistent _ _) => Hpers.
     rewrite envs_entails_eq => HP. iIntros "Henv HP".
     destruct o as [[|?] |]. {
       iDestruct (HP with "Henv") as "HSH".
       iDestruct (i2p_proof with "HSH HP") as "$".
     }
     all: case_match => //.
-    all: iDestruct (ip_persistent with "HP") as "#HP'".
+    all: iDestruct (@ip_persistent _ _ _ Hpers with "HP") as "#HP'".
     all: rewrite envs_app_sound //=; simpl.
     all: iDestruct ("Henv" with "[$]") as "Henv".
     all: by iDestruct (HP with "Henv") as "$".
@@ -422,11 +426,13 @@ Ltac liSimpl :=
 
 Ltac liShow := liUnfoldLetsInContext.
 
-Ltac liFindHyp :=
+Ltac liFindHyp key :=
   let rec go P Hs :=
       lazymatch Hs with
       | Esnoc ?Hs2 ?id ?Q =>
         first [
+            lazymatch key with
+            | FICSyntactic =>
            (* we first try to unify using the opaquenes hints of
               typeclass_instances. Directly doing exact: eq_refl
               sometimes takes 30 seconds to fail (e.g. when trying
@@ -434,7 +440,14 @@ Ltac liFindHyp :=
               different names. ) TODO: investigate if constr_eq
               could help even more
               https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.constr-eq*)
-            unify Q P with typeclass_instances;
+              unify Q P with typeclass_instances
+            | _ =>
+              notypeclasses refine (tac_find_hyp_equal key Q _ _ _ _ _); [solve [refine _] | ];
+              lazymatch goal with
+              | |- envs_entails _ (?P' ∗ _) =>
+                unify Q P' with typeclass_instances
+              end
+            end;
             notypeclasses refine (tac_find_hyp _ id _ _ _ _ _); [li_pm_reflexivity | li_pm_reduce]
           | go P Hs2 ]
       end in
@@ -454,10 +467,10 @@ Ltac liFindHyp :=
     end
   end.
 
-Ltac liFindHypOrTrue :=
+Ltac liFindHypOrTrue key :=
   first [
       notypeclasses refine (tac_sep_true _ _ _)
-    | progress liFindHyp
+    | progress liFindHyp key
   ].
 
 Ltac custom_exist_tac A protect := fail "No custom_exist_tac provided.".
@@ -491,11 +504,15 @@ Ltac liFindInContext :=
   lazymatch goal with
   | |- envs_entails _ (find_in_context ?fic ?T) =>
     let rec go n :=
-        match n with
-        | _ => simple notypeclasses refine (tac_fast_apply ((_ : FindInContext fic n) _).(i2p_proof) _); [solve [refine _] || fail 1 "no more instances to try" |]; simpl;
-          repeat liExist false; liFindHypOrTrue
-        | _ => go constr:(S n)
-        end
+        let inst := eval cbv beta in (_ : FindInContext fic n _) in
+        first [
+          lazymatch (type of inst) with
+          | FindInContext _ _ ?key =>
+          simple notypeclasses refine (tac_fast_apply (inst _).(i2p_proof) _); simpl;
+          repeat liExist false; liFindHypOrTrue key
+          end
+         | go constr:(S n)
+        ]
     in
     go constr:(0%nat)
   end.
@@ -648,7 +665,7 @@ Ltac liSep :=
     | ?P => first [
                convert_to_i2p P ltac:(fun converted =>
                simple notypeclasses refine (tac_fast_apply_below_sep converted _); [solve[refine _] |])
-             | progress liFindHyp
+             | 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 _] |];
                simpl; liFindInContext

theories/typing/automation.v

@@ -160,7 +160,7 @@ Ltac liRStmt :=
       | W.Switch _ _ _ _ _ => notypeclasses refine (tac_fast_apply (type_switch _ _ _ _ _ _ _ _ _) _)
       | W.Assert _ _ => notypeclasses refine (tac_fast_apply (type_assert _ _ _ _ _ _) _)
       | W.Goto ?bid => first [
-         notypeclasses refine (tac_fast_apply (type_goto_precond _ _ _ _ _ _) _); progress liFindHyp
+         notypeclasses refine (tac_fast_apply (type_goto_precond _ _ _ _ _ _) _); progress liFindHyp FICSyntactic
        | lazymatch goal with
          | H : BLOCK_PRECOND bid ?P |- _ =>
            notypeclasses refine (tac_fast_apply (tac_typed_single_block_rec P _ _ _ _ _ _ _) _);[compute_map_lookup|]

theories/typing/globals.v

@@ -95,7 +95,7 @@ Section globals.
     find_in_context (FindInitialized name A) T.
   Proof. iDestruct 1 as (x) "[Hinit HT]". iExists _. iFrame. Qed.
   Global Instance find_in_context_initialized_inst name A :
-    FindInContext (FindInitialized name A) 0%nat :=
+    FindInContext (FindInitialized name A) 0%nat FICSyntactic :=
     λ T, i2p (find_in_context_initialized name A T).
 
   Lemma subsume_initialized name A (x1 x2 : A) T:

theories/typing/own.v

@@ -332,7 +332,7 @@ Section own.
     iSplit => //. by iFrame.
   Qed.
   Global Instance find_in_context_type_loc_own_inst l :
-    FindInContext (FindLoc l) 1%nat :=
+    FindInContext (FindLoc l) 1%nat FICSyntactic :=
     λ T, i2p (find_in_context_type_loc_own l T).
 
   Lemma find_in_context_type_val_own l T:
@@ -340,7 +340,7 @@ Section own.
     find_in_context (FindVal l) T.
   Proof. iDestruct 1 as (ty) "[Hl HT]". iExists _ => /=. by iFrame. Qed.
   Global Instance find_in_context_type_val_own_inst (l : loc) :
-    FindInContext (FindVal l) 1%nat :=
+    FindInContext (FindVal l) 1%nat FICSyntactic :=
     λ T, i2p (find_in_context_type_val_own l T).
 
   Lemma find_in_context_type_val_own_singleton (l : loc) T:
@@ -348,7 +348,7 @@ Section own.
     find_in_context (FindVal l) T.
   Proof. iIntros "[_ HT]". iExists _ => /=. iFrame "HT". simpl. done. Qed.
   Global Instance find_in_context_type_val_own_singleton_inst (l : loc):
-    FindInContext (FindVal l) 2%nat :=
+    FindInContext (FindVal l) 2%nat FICSyntactic :=
     λ T, i2p (find_in_context_type_val_own_singleton l T).
 
   (* We cannot use place here as it can easily lead to an infinite
@@ -361,7 +361,7 @@ Section own.
     find_in_context (FindValP l) T.
   Proof. rewrite /place'. iIntros "[_ HT]". iExists _. iFrame "HT" => //=. Qed.
   Global Instance find_in_context_type_val_P_own_singleton_inst (l : loc):
-    FindInContext (FindValP l) 2%nat :=
+    FindInContext (FindValP l) 2%nat FICSyntactic :=
     λ T, i2p (find_in_context_type_val_P_own_singleton l T).
 End own.
 Typeclasses Opaque place'.

theories/typing/programs.v

@@ -407,7 +407,7 @@ Section typing.
     find_in_context (FindLoc l) T.
   Proof. iDestruct 1 as (β ty) "[Hl HT]". iExists (_, _) => /=. iFrame. Qed.
   Global Instance find_in_context_type_loc_id_inst l :
-    FindInContext (FindLoc l) 0%nat :=
+    FindInContext (FindLoc l) 0%nat FICSyntactic :=
     λ T, i2p (find_in_context_type_loc_id l T).
 
   Lemma find_in_context_type_val_id v T:
@@ -415,7 +415,7 @@ Section typing.
     find_in_context (FindVal v) T.
   Proof. iDestruct 1 as (ty) "[Hl HT]". iExists _ => /=. iFrame. Qed.
   Global Instance find_in_context_type_val_id_inst v :
-    FindInContext (FindVal v) 0%nat :=
+    FindInContext (FindVal v) 0%nat FICSyntactic :=
     λ T, i2p (find_in_context_type_val_id v T).
 
   Lemma find_in_context_type_val_P_id v T:
@@ -423,7 +423,7 @@ Section typing.
     find_in_context (FindValP v) T.
   Proof. iDestruct 1 as (ty) "[Hl HT]". iExists (ty_own_val _ _) => /=. iFrame. Qed.
   Global Instance find_in_context_type_val_P_id_inst v :
-    FindInContext (FindValP v) 0%nat :=
+    FindInContext (FindValP v) 0%nat FICSyntactic :=
     λ T, i2p (find_in_context_type_val_P_id v T).
 
   Lemma find_in_context_type_val_P_loc_id l T:
@@ -431,7 +431,7 @@ Section typing.
     find_in_context (FindValP l) T.
   Proof. iDestruct 1 as (β ty) "[Hl HT]". iExists (ty_own _ _ _) => /=. iFrame. Qed.
   Global Instance find_in_context_type_val_P_loc_id_inst (l : loc) :
-    FindInContext (FindValP l) 1%nat :=
+    FindInContext (FindValP l) 1%nat FICSyntactic :=
     λ T, i2p (find_in_context_type_val_P_loc_id l T).
 
   Lemma find_in_context_loc_in_bounds l T :
@@ -439,7 +439,7 @@ Section typing.
     find_in_context (FindLocInBounds l) T.
   Proof. iDestruct 1 as (n) "[??]". iExists (loc_in_bounds _ _) => /=. iFrame. Qed.
   Global Instance find_in_context_loc_in_bounds_inst l :
-    FindInContext (FindLocInBounds l) 0 :=
+    FindInContext (FindLocInBounds l) 0 FICSyntactic :=
     λ T, i2p (find_in_context_loc_in_bounds l T).
 
   Lemma find_in_context_loc_in_bounds_loc l T :
@@ -447,7 +447,7 @@ Section typing.
     find_in_context (FindLocInBounds l) T.
   Proof. iDestruct 1 as (β ty) "[??]". iExists (ty_own _ _ _) => /=. iFrame. Qed.
   Global Instance find_in_context_loc_in_bounds_loc_inst l :
-    FindInContext (FindLocInBounds l) 1 :=
+    FindInContext (FindLocInBounds l) 1 FICSyntactic :=
     λ T, i2p (find_in_context_loc_in_bounds_loc l T).
 
   Global Instance related_to_loc l β ty : RelatedTo (l ◁ₗ{β} ty) := {| rt_fic := FindLoc l |}.