cmra_tactics.v 2.13 KB
Newer Older
1
2
Require Export algebra.cmra.
Require Import algebra.cmra_big_op.
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
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

(** * Simple solver for validity and inclusion by reflection *)
Module ra_reflection. Section ra_reflection.
  Context `{CMRAIdentity 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.

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.