Commit ec919792 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' into gen_proofmode

parents c906fd45 650261fc
......@@ -92,7 +92,7 @@ End inv.
Tactic Notation "iInvCore" constr(N) "as" tactic(tac) constr(Hclose) :=
let Htmp := iFresh in
let patback := intro_pat.parse_one Hclose in
let pat := constr:(IList [[IName Htmp; patback]]) in
let pat := constr:(IList [[IIdent Htmp; patback]]) in
iMod (inv_open _ N with "[#]") as pat;
[idtac|iAssumption || fail "iInv: invariant" N "not found"|idtac];
[solve_ndisj || match goal with |- ?P => fail "iInv: cannot solve" P end
......
......@@ -110,7 +110,7 @@ Qed.
Lemma ownI_open i P : wsat ownI i P ownE {[i]} wsat P ownD {[i]}.
Proof.
rewrite /ownI /wsat -!lock.
iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[? HI]".
iIntros "(Hw & Hi & HiE)". iDestruct "Hw" as (I) "[Hw HI]".
iDestruct (invariant_lookup I i P with "[$]") as (Q ?) "#HPQ".
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ $]|HiE'] HI]"; eauto.
- iSplitR "HQ"; last by iNext; iRewrite -"HPQ".
......@@ -121,7 +121,7 @@ Qed.
Lemma ownI_close i P : wsat ownI i P P ownD {[i]} wsat ownE {[i]}.
Proof.
rewrite /ownI /wsat -!lock.
iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[? HI]".
iIntros "(Hw & Hi & HP & HiD)". iDestruct "Hw" as (I) "[Hw HI]".
iDestruct (invariant_lookup with "[$]") as (Q ?) "#HPQ".
iDestruct (big_opM_delete _ _ i with "HI") as "[[[HQ ?]|$] HI]"; eauto.
- iDestruct (ownD_singleton_twice with "[$]") as %[].
......@@ -134,7 +134,7 @@ Lemma ownI_alloc φ P :
wsat P == i, ⌜φ i wsat ownI i P.
Proof.
iIntros (Hfresh) "[Hw HP]". rewrite /wsat -!lock.
iDestruct "Hw" as (I) "[? HI]".
iDestruct "Hw" as (I) "[Hw HI]".
iMod (own_unit (gset_disjUR positive) disabled_name) as "HE".
iMod (own_updateP with "[$]") as "HE".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)).
......@@ -156,7 +156,7 @@ Lemma ownI_alloc_open φ P :
( E : gset positive, i, i E φ i)
wsat == i, ⌜φ i (ownE {[i]} - wsat) ownI i P ownD {[i]}.
Proof.
iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[? HI]".
iIntros (Hfresh) "Hw". rewrite /wsat -!lock. iDestruct "Hw" as (I) "[Hw HI]".
iMod (own_unit (gset_disjUR positive) disabled_name) as "HD".
iMod (own_updateP with "[$]") as "HD".
{ apply (gset_disj_alloc_empty_updateP_strong' (λ i, I !! i = None φ i)).
......
......@@ -153,7 +153,7 @@ Section proof.
wp_store.
iDestruct (own_valid_2 with "Hauth Hγo") as
%[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_valid_discrete_2.
iDestruct "Haown" as "[[Hγo' _]|?]".
iDestruct "Haown" as "[[Hγo' _]|Haown]".
{ iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
{ apply auth_update, prod_local_update_1.
......
......@@ -49,3 +49,37 @@ Qed.
Lemma string_beq_reflect s1 s2 : reflect (s1 = s2) (string_beq s1 s2).
Proof. apply iff_reflect. by rewrite string_beq_true. Qed.
Module Export ident.
Inductive ident :=
| IAnon : positive ident
| INamed :> string ident.
End ident.
Instance maybe_IAnon : Maybe IAnon := λ i,
match i with IAnon n => Some n | _ => None end.
Instance maybe_INamed : Maybe INamed := λ i,
match i with INamed s => Some s | _ => None end.
Instance beq_eq_dec : EqDecision ident.
Proof. solve_decision. Defined.
Definition positive_beq := Eval compute in Pos.eqb.
Lemma positive_beq_true x y : positive_beq x y = true x = y.
Proof. apply Pos.eqb_eq. Qed.
Definition ident_beq (i1 i2 : ident) : bool :=
match i1, i2 with
| IAnon n1, IAnon n2 => positive_beq n1 n2
| INamed s1, INamed s2 => string_beq s1 s2
| _, _ => false
end.
Lemma ident_beq_true i1 i2 : ident_beq i1 i2 = true i1 = i2.
Proof.
destruct i1, i2; rewrite /= ?string_beq_true ?positive_beq_true; naive_solver.
Qed.
Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
From iris.bi Require Export bi.
From iris.bi Require Import tactics.
From iris.proofmode Require Export base environments classes.
From stdpp Require Import stringmap hlist.
Set Default Proof Using "Type".
Import bi.
Import env_notations.
......@@ -37,24 +36,24 @@ Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
}.
Definition envs_dom {PROP} (Δ : envs PROP) : list string :=
Definition envs_dom {PROP} (Δ : envs PROP) : list ident :=
env_dom (env_persistent Δ) ++ env_dom (env_spatial Δ).
Definition envs_lookup {PROP} (i : string) (Δ : envs PROP) : option (bool * PROP) :=
Definition envs_lookup {PROP} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
let (Γp,Γs) := Δ in
match env_lookup i Γp with
| Some P => Some (true, P)
| None => P env_lookup i Γs; Some (false, P)
end.
Definition envs_delete {PROP} (i : string) (p : bool) (Δ : envs PROP) : envs PROP :=
Definition envs_delete {PROP} (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
let (Γp,Γs) := Δ in
match p with
| true => Envs (env_delete i Γp) Γs
| false => Envs Γp (env_delete i Γs)
end.
Definition envs_lookup_delete {PROP} (i : string)
Definition envs_lookup_delete {PROP} (i : ident)
(Δ : envs PROP) : option (bool * PROP * envs PROP) :=
let (Γp,Γs) := Δ in
match env_lookup_delete i Γp with
......@@ -62,7 +61,7 @@ Definition envs_lookup_delete {PROP} (i : string)
| None => '(P,Γs') env_lookup_delete i Γs; Some (false, P, Envs Γp Γs')
end.
Fixpoint envs_lookup_delete_list {PROP} (js : list string) (remove_persistent : bool)
Fixpoint envs_lookup_delete_list {PROP} (js : list ident) (remove_persistent : bool)
(Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
match js with
| [] => Some (true, [], Δ)
......@@ -74,7 +73,7 @@ Fixpoint envs_lookup_delete_list {PROP} (js : list string) (remove_persistent :
end.
Definition envs_snoc {PROP} (Δ : envs PROP)
(p : bool) (j : string) (P : PROP) : envs PROP :=
(p : bool) (j : ident) (P : PROP) : envs PROP :=
let (Γp,Γs) := Δ in
if p then Envs (Esnoc Γp j P) Γs else Envs Γp (Esnoc Γs j P).
......@@ -86,7 +85,7 @@ Definition envs_app {PROP : bi} (p : bool)
| false => _ env_app Γ Γp; Γs' env_app Γ Γs; Some (Envs Γp Γs')
end.
Definition envs_simple_replace {PROP : bi} (i : string) (p : bool)
Definition envs_simple_replace {PROP : bi} (i : ident) (p : bool)
(Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
let (Γp,Γs) := Δ in
match p with
......@@ -94,7 +93,7 @@ Definition envs_simple_replace {PROP : bi} (i : string) (p : bool)
| false => _ env_app Γ Γp; Γs' env_replace i Γ Γs; Some (Envs Γp Γs')
end.
Definition envs_replace {PROP : bi} (i : string) (p q : bool)
Definition envs_replace {PROP : bi} (i : ident) (p q : bool)
(Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
if eqb p q then envs_simple_replace i p Γ Δ
else envs_app q Γ (envs_delete i p Δ).
......@@ -109,7 +108,7 @@ Definition envs_clear_persistent {PROP} (Δ : envs PROP) : envs PROP :=
Envs Enil (env_spatial Δ).
Fixpoint envs_split_go {PROP}
(js : list string) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
(js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
match js with
| [] => Some (Δ1, Δ2)
| j :: js =>
......@@ -119,8 +118,9 @@ Fixpoint envs_split_go {PROP}
end.
(* if [d = Right] then [result = (remaining hyps, hyps named js)] and
if [d = Left] then [result = (hyps named js, remaining hyps)] *)
Definition envs_split {PROP} (d : direction)
(js : list string) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
(js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
'(Δ1,Δ2) envs_split_go js Δ (envs_clear_spatial Δ);
if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
......@@ -223,11 +223,11 @@ Proof.
apply wand_intro_l; destruct p; simpl.
- apply and_intro; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (string_beq_reflect j i); naive_solver.
intros j; destruct (ident_beq_reflect j i); naive_solver.
+ by rewrite affinely_persistently_and and_sep_affinely_persistently assoc.
- apply and_intro; [apply pure_intro|].
+ destruct Hwf; constructor; simpl; eauto using Esnoc_wf.
intros j; destruct (string_beq_reflect j i); naive_solver.
intros j; destruct (ident_beq_reflect j i); naive_solver.
+ solve_sep_entails.
Qed.
......
From stdpp Require Export strings.
From iris.proofmode Require Import base.
From iris.algebra Require Export base.
From stdpp Require Import stringmap.
Set Default Proof Using "Type".
Inductive env (A : Type) : Type :=
| Enil : env A
| Esnoc : env A string A env A.
| Esnoc : env A ident A env A.
Arguments Enil {_}.
Arguments Esnoc {_} _ _%string _.
Arguments Esnoc {_} _ _ _.
Instance: Params (@Enil) 1.
Instance: Params (@Esnoc) 1.
Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
match Γ with
| Enil => None
| Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ
| Esnoc Γ j x => if ident_beq i j then Some x else env_lookup i Γ
end.
Module env_notations.
......@@ -37,7 +35,7 @@ Fixpoint env_to_list {A} (E : env A) : list A :=
Coercion env_to_list : env >-> list.
Instance: Params (@env_to_list) 1.
Fixpoint env_dom {A} (Γ : env A) : list string :=
Fixpoint env_dom {A} (Γ : env A) : list ident :=
match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
......@@ -48,28 +46,28 @@ Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) :=
match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end
end.
Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :=
Fixpoint env_replace {A} (i: ident) (Γi: env A) (Γ: env A) : option (env A) :=
match Γ with
| Enil => None
| Esnoc Γ j x =>
if string_beq i j then env_app Γi Γ else
if ident_beq i j then env_app Γi Γ else
match Γi !! j with
| None => Γ' env_replace i Γi Γ; Some (Esnoc Γ' j x)
| Some _ => None
end
end.
Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
Fixpoint env_delete {A} (i : ident) (Γ : env A) : env A :=
match Γ with
| Enil => Enil
| Esnoc Γ j x => if string_beq i j then Γ else Esnoc (env_delete i Γ) j x
| Esnoc Γ j x => if ident_beq i j then Γ else Esnoc (env_delete i Γ) j x
end.
Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
Fixpoint env_lookup_delete {A} (i : ident) (Γ : env A) : option (A * env A) :=
match Γ with
| Enil => None
| Esnoc Γ j x =>
if string_beq i j then Some (x,Γ)
if ident_beq i j then Some (x,Γ)
else '(y,Γ') env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
end.
......@@ -94,15 +92,15 @@ Inductive env_subenv {A} : relation (env A) :=
Section env.
Context {A : Type}.
Implicit Types Γ : env A.
Implicit Types i : string.
Implicit Types i : ident.
Implicit Types x : A.
Hint Resolve Esnoc_wf Enil_wf.
Ltac simplify :=
repeat match goal with
| _ => progress simplify_eq/=
| H : context [string_beq ?s1 ?s2] |- _ => destruct (string_beq_reflect s1 s2)
| |- context [string_beq ?s1 ?s2] => destruct (string_beq_reflect s1 s2)
| H : context [ident_beq ?s1 ?s2] |- _ => destruct (ident_beq_reflect s1 s2)
| |- context [ident_beq ?s1 ?s2] => destruct (ident_beq_reflect s1 s2)
| _ => case_match
end.
......
......@@ -3,7 +3,7 @@ From iris.proofmode Require Import base tokens sel_patterns.
Set Default Proof Using "Type".
Inductive intro_pat :=
| IName : string intro_pat
| IIdent : ident intro_pat
| IAnom : intro_pat
| IDrop : intro_pat
| IFrame : intro_pat
......@@ -73,7 +73,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
match ts with
| [] => Some k
| TName "_" :: ts => parse_go ts (SPat IDrop :: k)
| TName s :: ts => parse_go ts (SPat (IName s) :: k)
| TName s :: ts => parse_go ts (SPat (IIdent s) :: k)
| TAnom :: ts => parse_go ts (SPat IAnom :: k)
| TFrame :: ts => parse_go ts (SPat IFrame :: k)
| TBracketL :: ts => parse_go ts (SList :: k)
......@@ -98,11 +98,11 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
end
with parse_clear (ts : list token) (k : stack) : option stack :=
match ts with
| TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelName s)) :: k)
| TFrame :: TName s :: ts => parse_clear ts (SPat (IClearFrame (SelIdent s)) :: k)
| TFrame :: TPure :: ts => parse_clear ts (SPat (IClearFrame SelPure) :: k)
| TFrame :: TAlways :: ts => parse_clear ts (SPat (IClearFrame SelPersistent) :: k)
| TFrame :: TSep :: ts => parse_clear ts (SPat (IClearFrame SelSpatial) :: k)
| TName s :: ts => parse_clear ts (SPat (IClear (SelName s)) :: k)
| TName s :: ts => parse_clear ts (SPat (IClear (SelIdent s)) :: k)
| TPure :: ts => parse_clear ts (SPat (IClear SelPure) :: k)
| TAlways :: ts => parse_clear ts (SPat (IClear SelPersistent) :: k)
| TSep :: ts => parse_clear ts (SPat (IClear SelSpatial) :: k)
......@@ -134,6 +134,7 @@ Ltac parse s :=
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid list intro_pat" s
end
| ident => constr:([IIdent s])
| ?X => fail "intro_pat.parse:" s "has unexpected type" X
end.
Ltac parse_one s :=
......@@ -165,6 +166,7 @@ Ltac intro_pat_persistent p :=
| string =>
let pat := intro_pat.parse p in
eval cbv in (forallb intro_pat_persistent pat)
| ident => false
| bool => p
| ?X => fail "intro_pat_persistent:" p "has unexpected type" X
end.
......@@ -8,9 +8,12 @@ Arguments Enil {_}.
Arguments Esnoc {_} _%proof_scope _%string _%I.
Notation "" := Enil (only printing) : proof_scope.
Notation "Γ H : P" := (Esnoc Γ H P)
Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
(at level 1, P at level 200,
left associativity, format "Γ H : P '//'", only printing) : proof_scope.
Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
(at level 1, P at level 200,
left associativity, format "Γ '_' : P '//'", only printing) : proof_scope.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(envs_entails (Envs Γ Δ) Q%I)
......
......@@ -6,7 +6,7 @@ Inductive sel_pat :=
| SelPure
| SelPersistent
| SelSpatial
| SelName : string sel_pat.
| SelIdent : ident sel_pat.
Fixpoint sel_pat_pure (ps : list sel_pat) : bool :=
match ps with
......@@ -19,7 +19,7 @@ Module sel_pat.
Fixpoint parse_go (ts : list token) (k : list sel_pat) : option (list sel_pat) :=
match ts with
| [] => Some (reverse k)
| TName s :: ts => parse_go ts (SelName s :: k)
| TName s :: ts => parse_go ts (SelIdent s :: k)
| TPure :: ts => parse_go ts (SelPure :: k)
| TAlways :: ts => parse_go ts (SelPersistent :: k)
| TSep :: ts => parse_go ts (SelSpatial :: k)
......@@ -32,7 +32,9 @@ Ltac parse s :=
lazymatch type of s with
| sel_pat => constr:([s])
| list sel_pat => s
| list string => eval vm_compute in (SelName <$> s)
| ident => constr:([SelIdent s])
| list ident => eval vm_compute in (SelIdent <$> s)
| list string => eval vm_compute in (SelIdent INamed <$> s)
| string =>
lazymatch eval vm_compute in (parse s) with
| Some ?pats => pats | _ => fail "invalid sel_pat" s
......
From stdpp Require Export strings.
From iris.proofmode Require Import tokens.
From iris.proofmode Require Import base tokens.
Set Default Proof Using "Type".
Inductive goal_kind := GSpatial | GModal | GPersistent.
......@@ -7,14 +7,14 @@ Inductive goal_kind := GSpatial | GModal | GPersistent.
Record spec_goal := SpecGoal {
spec_goal_kind : goal_kind;
spec_goal_negate : bool;
spec_goal_frame : list string;
spec_goal_hyps : list string;
spec_goal_frame : list ident;
spec_goal_hyps : list ident;
spec_goal_done : bool
}.
Inductive spec_pat :=
| SForall : spec_pat
| SName : string spec_pat
| SIdent : ident spec_pat
| SPureGoal : bool spec_pat
| SGoal : spec_goal spec_pat
| SAutoFrame : goal_kind spec_pat.
......@@ -36,7 +36,7 @@ Inductive state :=
Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat) :=
match ts with
| [] => Some (reverse k)
| TName s :: ts => parse_go ts (SName s :: k)
| TName s :: ts => parse_go ts (SIdent s :: k)
| TBracketL :: TAlways :: TFrame :: TBracketR :: ts =>
parse_go ts (SAutoFrame GPersistent :: k)
| TBracketL :: TFrame :: TBracketR :: ts =>
......@@ -52,14 +52,14 @@ Fixpoint parse_go (ts : list token) (k : list spec_pat) : option (list spec_pat)
| _ => None
end
with parse_goal (ts : list token)
(ki : goal_kind) (neg : bool) (frame hyps : list string)
(ki : goal_kind) (neg : bool) (frame hyps : list ident)
(k : list spec_pat) : option (list spec_pat) :=
match ts with
| TMinus :: ts =>
guard (¬neg frame = [] hyps = []);
parse_goal ts ki true frame hyps k
| TName s :: ts => parse_goal ts ki neg frame (s :: hyps) k
| TFrame :: TName s :: ts => parse_goal ts ki neg (s :: frame) hyps k
| TName s :: ts => parse_goal ts ki neg frame (INamed s :: hyps) k
| TFrame :: TName s :: ts => parse_goal ts ki neg (INamed s :: frame) hyps k
| TDone :: TBracketR :: ts =>
parse_go ts (SGoal (SpecGoal ki neg (reverse frame) (reverse hyps) true) :: k)
| TBracketR :: ts =>
......@@ -76,11 +76,4 @@ Ltac parse s :=
| Some ?pats => pats | _ => fail "invalid list spec_pat" s
end
end.
Ltac parse_one s :=
lazymatch type of s with
| spec_pat => s
| string => lazymatch eval vm_compute in (parse s) with
| Some [?pat] => pat | _ => fail "invalid spec_pat" s
end
end.
End spec_pat.
This diff is collapsed.
......@@ -82,7 +82,7 @@ Lemma test_iAssumption_affine P Q R `{!Affine P, !Affine R} : P -∗ Q -∗ R -
Proof. iIntros "H1 H2 H3". iAssumption. Qed.
Lemma test_iDestruct_spatial_and P Q1 Q2 : P (Q1 Q2) - P Q1.
Proof. iIntros "[H1 [H2 _]]". iFrame. Qed.
Proof. iIntros "[H [? _]]". by iFrame. Qed.
Lemma test_iAssert_persistent P Q : P - Q - True.
Proof.
......@@ -96,7 +96,7 @@ Qed.
Lemma test_iSpecialize_auto_frame P Q R :
(P - True - True - Q - R) - P - Q - R.
Proof. iIntros "H HP HQ". by iApply ("H" with "[$]"). Qed.
Proof. iIntros "H ? HQ". by iApply ("H" with "[$]"). Qed.
Lemma test_iEmp_intro P Q R `{!Affine P, !Persistent Q, !Affine R} :
P - Q R - emp.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment