From iris.algebra Require Export cmra.
From iris.algebra Require Import cmra_big_op.

Module ra_reflection. Section ra_reflection.
  Context {A : ucmraT}.

  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 id ∅ (Σ !! 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 id ∅ (Σ !! n)) <$> flatten e).
  Proof.
    induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
    by rewrite fmap_app IH1 IH2 big_op_app.
  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.
  Lemma flatten_correct_equiv Σ e1 e2 :
    flatten e1 ≡ₚ flatten e2 →
    eval Σ e1 ≡ eval Σ e2.
  Proof.
    by intros He; rewrite !eval_flatten; apply big_op_permutation; 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
    | |- @equiv _ _ ?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.

Ltac solve_equiv :=
  ra_reflection.quote;
  apply ra_reflection.flatten_correct_equiv, (bool_decide_unpack _);
  vm_compute; apply I.

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_validN_le, Hn; eapply cmra_validN_included, Hx; apply H
  end.

Ltac solve_valid :=
  match goal with
  | H : ✓ ?y |- ✓ ?x ⇒
     let Hn := fresh in let Hx := fresh in
     assert (x ≼ y) as Hx by solve_included;
     eapply cmra_valid_included, Hx; apply H
  end.