try new version of unification

linux/pkvm/proofs/spinlock/spinlock_proof.v

@@ -4,12 +4,6 @@ From refinedc.linux.pkvm.spinlock Require Import generated_spec.
 From refinedc.linux.pkvm.spinlock Require Import spinlock_def.
 Set Default Proof Using "Type".
 
-Ltac get_head e :=
-  match e with
-  | ?h _ => get_head constr:(h)
-  | _    => constr:(e)
-  end.
-
 (* TODO: allow pattern, but add underscores if it does not match *)
 Tactic Notation "liRStepUntil" open_constr(id) :=
   repeat lazymatch goal with

theories/lang/base.v

@@ -37,6 +37,11 @@ Ltac fast_reflexivity :=
   | |- ?x = ?y => lazymatch x with | y => exact: (eq_refl x) end
   end.
 
+Ltac get_head e :=
+  lazymatch e with
+  | ?h _ => get_head constr:(h)
+  | _    => constr:(e)
+  end.
 
 Definition Z_of_bool (b : bool) : Z :=
   if b then 1 else 0.

theories/lang/lang.v

@@ -628,6 +628,10 @@ Proof.
     apply Nat.pow_le_mono_r; lia.
 Qed.
 
+Lemma ly_size_ly_set_size ly n:
+  ly_size (ly_set_size ly n) = n.
+Proof. done. Qed.
+
 Lemma ly_align_ly_set_size ly n:
   ly_align (ly_set_size ly n) = ly_align ly.
 Proof. done. Qed.

theories/lithium/interpreter.v

@@ -162,7 +162,7 @@ Section coq_tactics.
     envs_entails Δ (∃ a : A, Φ a ∗ Q) → envs_entails Δ ((∃ a : A, Φ a) ∗ Q).
   Proof. by rewrite bi.sep_exist_r. Qed.
 
-  Lemma tac_do_simplify_goal (P : iProp Σ) T {SG : SimplifyGoal P (Some 0%N)} :
+  Lemma tac_do_simplify_goal (n : N) (P : iProp Σ) T {SG : SimplifyGoal P (Some n)} :
     (SG (λ P, P ∗ T)%I).(i2p_P) -∗ P ∗ T.
   Proof. iIntros "HP". iDestruct (i2p_proof with "HP") as (?) "(H&?&$)". by iApply "H". Qed.
 
@@ -321,29 +321,22 @@ Ltac unfold_instantiated_evar_hook H := idtac.
 
 Ltac unfold_instantiated_evar H :=
   unfold_instantiated_evar_hook H;
-  (* first we need to rewrap unfolded evars in H*)
-  repeat match goal with
-         | He := EVAR_ID ?x2 |- _ => progress unfold He in H
-         end;
   revert H;
-  repeat lazymatch goal with
-         | |- let _ := EVAR_ID ?body in _  =>
-           lazymatch body with
-           | context [EVAR_ID ?x1] =>
-             match goal with
-             | He := EVAR_ID ?x2 |- _ => constr_eq x1 x2;
-                                        (* we have found the
-                                        hypotheses for the unfolded
-                                        evar in body. Now do a funny
-                                        dance to refold it. *)
-                                        pattern (EVAR_ID x2);
-                                        simple refine (tac_protected_eq_app_rev _ _ _);
-                                        lazymatch goal with
-                                        | |- ?f (protected _) => change (f (protected He))
-                                        end; cbv beta
-             end
-           end
-         end;
+  repeat match goal with
+        | |- let _ := EVAR_ID ?body in _ =>
+          match goal with
+          | He := EVAR_ID ?var |- _ => is_evar var;
+          lazymatch body with
+          | context [ var ] => pattern var;
+          lazymatch goal with
+          | |- ?G ?E =>
+            change (G He);
+            simple refine (tac_protected_eq_app_rev _ _ _);
+            cbv beta
+          end
+          end
+          end
+        end;
   (* This is copied from the end of instantiate_protected *)
   let tmp := fresh "tmp" in
   intros tmp;
@@ -392,17 +385,17 @@ Ltac unfold_instantiated_evars :=
          | H := EVAR_ID ?x |- _ => assert_fails (is_evar x); unfold_instantiated_evar H
          end.
 
+Create HintDb solve_protected_eq_db discriminated.
+Hint Constants Opaque : solve_protected_eq_db.
+
+Ltac solve_protected_eq_unfold_tac := idtac.
 Ltac solve_protected_eq :=
   (* intros because it is less aggressive than move => * *)
-  intros; repeat rewrite protected_eq;
-  try (
-      liUnfoldAllEvars;
-      lazymatch goal with |- ?a = ?b => unify a b with typeclass_instances end;
-      (* We need to solve the constraints for the has_evar to work *)
-      solve_constraints;
-      lazymatch goal with
-      | |- ?g => assert_fails (has_evar g)
-      end);
+  intros;
+  solve_protected_eq_unfold_tac;
+  repeat rewrite protected_eq;
+  liUnfoldAllEvars;
+  lazymatch goal with |- ?a = ?b => unify a b with solve_protected_eq_db end;
   exact: eq_refl.
 
 Ltac liEnforceInvariantAndUnfoldInstantiatedEvars :=
@@ -656,9 +649,10 @@ Ltac liSep :=
                convert_to_i2p P ltac:(fun converted =>
                simple notypeclasses refine (tac_fast_apply_below_sep converted _); [solve[refine _] |])
              | progress liFindHyp
-             | simple notypeclasses refine (tac_fast_apply (tac_do_simplify_goal _ _) _); [solve [refine _] |]
+             | 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
+             | simple notypeclasses refine (tac_fast_apply (tac_do_simplify_goal _ _ _) _); [| solve [refine _] |]
              | fail "do_sep: unknown sidecondition" P
       ]
     end

theories/lithium/simpl_instances.v

@@ -435,7 +435,7 @@ Global Instance simpl_Some {A} o (x x' : A) `{!FastDone (o = Some x)}:
   SimplBothRel (=) (o) (Some x') (x = x') | 1.
 Proof. unfold FastDone in *; subst. split; naive_solver. Qed.
 
-Global Instance simpl_both_fmap_Some A f (o : option A) (x : A): SimplBothRel (=) (f <$> o) (Some x) (∃ x', o = Some  x' ∧ x = f x').
+Global Instance simpl_both_fmap_Some A B f (o : option A) (x : B): SimplBothRel (=) (f <$> o) (Some x) (∃ x', o = Some  x' ∧ x = f x').
 Proof. unfold SimplBothRel. rewrite fmap_Some. naive_solver. Qed.
 
 Global Instance simplify_option_fmap_None {A B} (f : A → B) (x : option A) :

theories/typing/automation.v

@@ -32,6 +32,24 @@ Ltac custom_exist_tac A protect ::=
     | Movable _ => eexists _
     end.
 
+Hint Transparent ly_size : solve_protected_eq_db.
+Ltac solve_protected_eq_unfold_tac ::=
+  lazymatch goal with
+  (* unfold constants for function types *)
+  | |- @eq (_ → fn_params) ?a (λ x, _) =>
+    lazymatch a with
+    | (λ x, _) => idtac
+    | _ =>
+      let h := get_head a in
+      unfold h;
+      (* necessary to reduce after unfolding because of the strict
+      opaqueness settings for unification *)
+      liSimpl
+    end
+  (* don't fail if nothing matches *)
+  | |- _ => idtac
+  end.
+
 Ltac can_solve_tac ::= solve_goal.
 
 Ltac record_destruct_hint hint info ::= add_case_distinction_info hint info.

theories/typing/automation/normalize.v

@@ -29,6 +29,7 @@ Hint Rewrite @bool_decide_eq_x_x_true @if_bool_decide_eq_branches : refinedc_rew
 Hint Rewrite keep_factor2_is_power_of_two keep_factor2_min_eq using can_solve_tac : refinedc_rewrite.
 Hint Rewrite keep_factor2_min_1 keep_factor2_twice : refinedc_rewrite.
 Hint Rewrite ly_align_ly_with_align ly_align_ly_offset ly_align_ly_set_size : refinedc_rewrite.
+Hint Rewrite ly_size_ly_set_size : refinedc_rewrite.
 
 Local Definition lookup_insert_gmap A K `{Countable K} := lookup_insert (M := gmap K) (A := A).
 Hint Rewrite lookup_insert_gmap : refinedc_rewrite.