Reflective solver for included and validN.

modures/cmra.v

@@ -230,6 +230,16 @@ Hint Extern 0 (_ ≼{0} _) => apply cmra_included_0.
 (* Also via [cmra_cofe; cofe_equivalence] *)
 Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.
 
+(* Solver for validity *)
+Ltac solve_validN :=
+  match goal with
+  | H : ✓{?n} ?y |- ✓{?n'} ?x =>
+     let Hn := fresh in let Hx := fresh in
+     assert (n' ≤ n) as Hn by omega;
+     assert (x ≼ y) as Hx by solve_included;
+     eapply cmra_valid_le, Hn; eapply cmra_valid_included, Hx; apply H
+  end.
+
 Instance cmra_monotone_id {A : cmraT} : CMRAMonotone (@id A).
 Proof. by split. Qed.
 Instance cmra_monotone_ra_monotone {A B : cmraT} (f : A → B) :

modures/ra.v

@@ -139,6 +139,14 @@ Proof.
   induction xs as [|x xs IH]; simpl; first by rewrite ?(left_id _ _).
   by rewrite IH (associative _).
 Qed.
+Lemma big_op_contains xs ys : xs `contains` ys → big_op xs ≼ big_op ys.
+Proof.
+  induction 1 as [|x xs ys|x y xs|x xs ys|xs ys zs]; rewrite //=.
+  * by apply ra_preserving_l.
+  * by rewrite !(associative _) (commutative _ y); apply ra_preserving_r.
+  * by transitivity (big_op ys); [|apply ra_included_r].
+  * by transitivity (big_op ys).
+Qed.
 
 Context `{FinMap K M}.
 Lemma big_opM_empty : big_opM (∅ : M A) ≡ ∅.
@@ -168,3 +176,58 @@ Proof.
   by rewrite insert_delete.
 Qed.
 End ra.
+
+(* Simple solver for inclusion by reflection *)
+Module ra_reflection. Section ra_reflection.
+  Context `{RA A, Empty A, !RAIdentity A}.
+
+  Inductive expr :=
+    | EVar : nat → expr
+    | EEmpty : expr
+    | EOp : expr → expr → expr.
+  Fixpoint eval (Σ : list A) (e : expr) : A :=
+    match e with
+    | EVar n => from_option ∅ (Σ !! n)
+    | EEmpty => ∅
+    | EOp e1 e2 => eval Σ e1 ⋅ eval Σ e2
+    end.
+  Fixpoint flatten (e : expr) : list nat :=
+    match e with
+    | EVar n => [n]
+    | EEmpty => []
+    | EOp e1 e2 => flatten e1 ++ flatten e2
+    end.
+  Lemma eval_flatten Σ e :
+    eval Σ e ≡ big_op ((λ n, from_option ∅ (Σ !! n)) <$> flatten e).
+  Proof.
+    by induction e as [| |e1 IH1 e2 IH2];
+      rewrite /= ?(right_id _ _) ?fmap_app ?big_op_app ?IH1 ?IH2.
+  Qed.
+  Lemma flatten_correct Σ e1 e2 :
+    flatten e1 `contains` flatten e2 → eval Σ e1 ≼ eval Σ e2.
+  Proof.
+    by intros He; rewrite !eval_flatten; apply big_op_contains; rewrite ->He.
+  Qed.
+
+  Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
+  Global Instance quote_empty: Quote E1 E1 ∅ EEmpty.
+  Global Instance quote_var Σ1 Σ2 e i:
+    rlist.QuoteLookup Σ1 Σ2 e i → Quote Σ1 Σ2 e (EVar i) | 1000.
+  Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
+    Quote Σ1 Σ2 x1 e1 → Quote Σ2 Σ3 x2 e2 → Quote Σ1 Σ3 (x1 ⋅ x2) (EOp e1 e2).
+  End ra_reflection.
+
+  Ltac quote :=
+    match goal with
+    | |- @included _ _ _ ?x ?y =>
+      lazymatch type of (_ : Quote [] _ x _) with Quote _ ?Σ2 _ ?e1 =>
+      lazymatch type of (_ : Quote Σ2 _ y _) with Quote _ ?Σ3 _ ?e2 =>
+        change (eval Σ3 e1 ≼ eval Σ3 e2)
+      end end
+    end.
+End ra_reflection.
+
+Ltac solve_included :=
+  ra_reflection.quote;
+  apply ra_reflection.flatten_correct, (bool_decide_unpack _);
+  vm_compute; apply I.