cmra_tactics.v 2.18 KB
Newer Older
 Robbert Krebbers committed Mar 10, 2016 1 2 ``````From iris.algebra Require Export cmra. From iris.algebra Require Import cmra_big_op. `````` Ralf Jung committed Jan 03, 2017 3 ``````Set Default Proof Using "Type*". `````` Robbert Krebbers committed Feb 01, 2016 4 5 6 `````` (** * Simple solver for validity and inclusion by reflection *) Module ra_reflection. Section ra_reflection. `````` Robbert Krebbers committed May 27, 2016 7 `````` Context {A : ucmraT}. `````` Robbert Krebbers committed Feb 01, 2016 8 9 10 11 12 13 14 `````` Inductive expr := | EVar : nat → expr | EEmpty : expr | EOp : expr → expr → expr. Fixpoint eval (Σ : list A) (e : expr) : A := match e with `````` Robbert Krebbers committed May 27, 2016 15 `````` | EVar n => from_option id ∅ (Σ !! n) `````` Robbert Krebbers committed Feb 01, 2016 16 17 18 19 20 21 22 23 24 25 `````` | 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 : `````` Robbert Krebbers committed May 27, 2016 26 `````` eval Σ e ≡ big_op ((λ n, from_option id ∅ (Σ !! n)) <\$> flatten e). `````` Robbert Krebbers committed Feb 01, 2016 27 `````` Proof. `````` Robbert Krebbers committed May 27, 2016 28 29 `````` induction e as [| |e1 IH1 e2 IH2]; rewrite /= ?right_id //. by rewrite fmap_app IH1 IH2 big_op_app. `````` Robbert Krebbers committed Feb 01, 2016 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 67 `````` 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.``````