cmra_tactics.v 2.15 KB
Newer Older
1 2
From iris.algebra Require Export cmra.
From iris.algebra Require Import cmra_big_op.
3 4 5

(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
6
  Context  {A : ucmraT}.
7 8 9 10 11 12 13

  Inductive expr :=
    | EVar : nat  expr
    | EEmpty : expr
    | EOp : expr  expr  expr.
  Fixpoint eval (Σ : list A) (e : expr) : A :=
    match e with
14
    | EVar n => from_option id  (Σ !! n)
15 16 17 18 19 20 21 22 23 24
    | 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 :
25
    eval Σ e  big_op ((λ n, from_option id  (Σ !! n)) <$> flatten e).
26
  Proof.
27 28
    induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //.
    by rewrite fmap_app IH1 IH2 big_op_app.
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66
  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.

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.