Skip to content
GitLab
Commit 697523ea authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Also establish Closed and to_val _ = Some _ via reification.

parent 83a6cd62
Hide whitespace changes
Inline Side-by-side
_CoqProject
View file @ 697523ea
......@@ -88,7 +88,6 @@ heap_lang/wp_tactics.v
heap_lang/lifting.v
heap_lang/derived.v
heap_lang/notation.v
heap_lang/substitution.v
heap_lang/heap.v
heap_lang/lib/spawn.v
heap_lang/lib/par.v
......
heap_lang/lang.v
View file @ 697523ea
......@@ -345,93 +345,24 @@ Lemma alloc_fresh e v σ :
to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
(** Value type class *)
Class IntoValue (e : expr) (v : val) := into_value : to_val e = Some v.
Instance into_value_of_val v : IntoValue (of_val v) v.
Proof. by rewrite /IntoValue to_of_val. Qed.
Instance into_value_rec f x e `{!Closed (f :b: x :b: []) e} :
IntoValue (Rec f x e) (RecV f x e).
Proof.
rewrite /IntoValue /=; case_decide; last done.
do 2 f_equal. by apply (proof_irrel).
Qed.
Instance into_value_lit l : IntoValue (Lit l) (LitV l).
Proof. done. Qed.
Instance into_value_pair e1 e2 v1 v2 :
IntoValue e1 v1 → IntoValue e2 v2 → IntoValue (Pair e1 e2) (PairV v1 v2).
Proof. by rewrite /IntoValue /= => -> /= ->. Qed.
Instance into_value_injl e v : IntoValue e v → IntoValue (InjL e) (InjLV v).
Proof. by rewrite /IntoValue /= => ->. Qed.
Instance into_value_injr e v : IntoValue e v → IntoValue (InjR e) (InjRV v).
Proof. by rewrite /IntoValue /= => ->. Qed.
(** Closed expressions *)
Lemma is_closed_weaken X Y e : is_closed X e → X `included` Y → is_closed Y e.
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
Lemma closed_subst X e x es : Closed X e → x ∉ X → subst x es e = e.
Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
Proof.
rewrite /Closed. revert X.
induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
Lemma closed_nil_subst e x es : Closed [] e → subst x es e = e.
Proof. intros. apply closed_subst with []; set_solver. Qed.
Lemma is_closed_nil_subst e x es : is_closed [] e → subst x es e = e.
Proof. intros. apply is_closed_subst with []; set_solver. Qed.
Lemma closed_nil_closed X e : Closed [] e → Closed X e.
Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
Hint Immediate closed_nil_closed : typeclass_instances.
Instance closed_of_val X v : Closed X (of_val v).
Proof.
apply is_closed_weaken with []; last set_solver.
induction v; simpl; auto.
Qed.
Instance closed_rec X f x e : Closed (f :b: x :b: X) e → Closed X (Rec f x e).
Proof. done. Qed.
Lemma closed_var X x : bool_decide (x ∈ X) → Closed X (Var x).
Proof. done. Qed.
Hint Extern 1000 (Closed _ (Var _)) =>
apply closed_var; vm_compute; exact I : typeclass_instances.
Section closed.
Context (X : list string).
Notation C := (Closed X).
Global Instance closed_lit l : C (Lit l).
Proof. done. Qed.
Global Instance closed_unop op e : C e → C (UnOp op e).
Proof. done. Qed.
Global Instance closed_fst e : C e → C (Fst e).
Proof. done. Qed.
Global Instance closed_snd e : C e → C (Snd e).
Proof. done. Qed.
Global Instance closed_injl e : C e → C (InjL e).
Proof. done. Qed.
Global Instance closed_injr e : C e → C (InjR e).
Proof. done. Qed.
Global Instance closed_fork e : C e → C (Fork e).
Proof. done. Qed.
Global Instance closed_load e : C e → C (Load e).
Proof. done. Qed.
Global Instance closed_alloc e : C e → C (Alloc e).
Proof. done. Qed.
Global Instance closed_app e1 e2 : C e1 → C e2 → C (App e1 e2).
Proof. intros. by rewrite /Closed /= !andb_True. Qed.
Global Instance closed_binop op e1 e2 : C e1 → C e2 → C (BinOp op e1 e2).
Proof. intros. by rewrite /Closed /= !andb_True. Qed.
Global Instance closed_pair e1 e2 : C e1 → C e2 → C (Pair e1 e2).
Proof. intros. by rewrite /Closed /= !andb_True. Qed.
Global Instance closed_store e1 e2 : C e1 → C e2 → C (Store e1 e2).
Proof. intros. by rewrite /Closed /= !andb_True. Qed.
Global Instance closed_if e0 e1 e2 : C e0 → C e1 → C e2 → C (If e0 e1 e2).
Proof. intros. by rewrite /Closed /= !andb_True. Qed.
Global Instance closed_case e0 e1 e2 : C e0 → C e1 → C e2 → C (Case e0 e1 e2).
Proof. intros. by rewrite /Closed /= !andb_True. Qed.
Global Instance closed_cas e0 e1 e2 : C e0 → C e1 → C e2 → C (CAS e0 e1 e2).
Proof. intros. by rewrite /Closed /= !andb_True. Qed.
End closed.
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
(** Equality and other typeclass stuff *)
Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
......
heap_lang/lib/par.v
View file @ 697523ea
......@@ -39,7 +39,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp)
∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
⊢ WP e1 || e2 {{ Φ }}.
Proof.
iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); [done|apply into_value|].
iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done.
iFrame "Hh H". iSplitL "H1"; by wp_let.
Qed.
End proof.
heap_lang/substitution.v deleted 100644 → 0
View file @ 83a6cd62
From iris.heap_lang Require Export lang.
Import heap_lang.
Module W.
Inductive expr :=
| ClosedExpr (e : heap_lang.expr) `{!Closed [] e}
(* Base lambda calculus *)
| Var (x : string)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
(* Base types and their operations *)
| Lit (l : base_lit)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
(* Concurrency *)
| Fork (e : expr)
(* Heap *)
| Alloc (e : expr)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr).
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| ClosedExpr e H => @ClosedExpr e H
| Var y => if decide (x = y) then es else Var y
| Rec f y e =>
Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
| App e1 e2 => App (subst x es e1) (subst x es e2)
| Lit l => Lit l
| UnOp op e => UnOp op (subst x es e)
| BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
| If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
| Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
| Fst e => Fst (subst x es e)
| Snd e => Snd (subst x es e)
| InjL e => InjL (subst x es e)
| InjR e => InjR (subst x es e)
| Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
| Fork e => Fork (subst x es e)
| Alloc e => Alloc (subst x es e)
| Load e => Load (subst x es e)
| Store e1 e2 => Store (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
end.
Fixpoint to_expr (e : expr) : heap_lang.expr :=
match e with
| ClosedExpr e _ => e
| Var x => heap_lang.Var x
| Rec f x e => heap_lang.Rec f x (to_expr e)
| App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
| Lit l => heap_lang.Lit l
| UnOp op e => heap_lang.UnOp op (to_expr e)
| BinOp op e1 e2 => heap_lang.BinOp op (to_expr e1) (to_expr e2)
| If e0 e1 e2 => heap_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
| Pair e1 e2 => heap_lang.Pair (to_expr e1) (to_expr e2)
| Fst e => heap_lang.Fst (to_expr e)
| Snd e => heap_lang.Snd (to_expr e)
| InjL e => heap_lang.InjL (to_expr e)
| InjR e => heap_lang.InjR (to_expr e)
| Case e0 e1 e2 => heap_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
| Fork e => heap_lang.Fork (to_expr e)
| Alloc e => heap_lang.Alloc (to_expr e)
| Load e => heap_lang.Load (to_expr e)
| Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
end.
Ltac of_expr e :=
lazymatch e with
| heap_lang.Var ?x => constr:(Var x)
| heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
| heap_lang.App ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
| heap_lang.Lit ?l => constr:(Lit l)
| heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
| heap_lang.BinOp ?op ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
| heap_lang.If ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(If e0 e1 e2)
| heap_lang.Pair ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
| heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
| heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
| heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
| heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
| heap_lang.Case ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(Case e0 e1 e2)
| heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
| heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
| heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
| heap_lang.Store ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
| heap_lang.CAS ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(CAS e0 e1 e2)
| to_expr ?e => e
| of_val ?v => constr:(ClosedExpr (of_val v))
(* is_var e; constr:(Closed e) does not work *)
| _ => constr:(ltac:(is_var e; exact (ClosedExpr e)))
end.
Lemma to_expr_subst x er e :
to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
Proof.
induction e; simpl;
repeat case_decide; f_equal; auto using closed_nil_subst, eq_sym.
Qed.
End W.
(** * The tactic *)
Ltac simpl_subst :=
csimpl;
repeat match goal with
| |- context [subst ?x ?er ?e] =>
let er' := W.of_expr er in let e' := W.of_expr e in
change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
end;
unfold W.to_expr.
Arguments W.to_expr : simpl never.
Arguments subst : simpl never.
heap_lang/tactics.v
View file @ 697523ea
From iris.heap_lang Require Export substitution.
From iris.heap_lang Require Export lang.
From iris.prelude Require Import fin_maps.
Import heap_lang.
Module W.
Inductive expr :=
| Val (v : val)
| ClosedExpr (e : heap_lang.expr) `{!Closed [] e}
(* Base lambda calculus *)
| Var (x : string)
| Rec (f x : binder) (e : expr)
| App (e1 e2 : expr)
(* Base types and their operations *)
| Lit (l : base_lit)
| UnOp (op : un_op) (e : expr)
| BinOp (op : bin_op) (e1 e2 : expr)
| If (e0 e1 e2 : expr)
(* Products *)
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : expr) (e2 : expr)
(* Concurrency *)
| Fork (e : expr)
(* Heap *)
| Alloc (e : expr)
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| CAS (e0 : expr) (e1 : expr) (e2 : expr).
Fixpoint to_expr (e : expr) : heap_lang.expr :=
match e with
| Val v => of_val v
| ClosedExpr e _ => e
| Var x => heap_lang.Var x
| Rec f x e => heap_lang.Rec f x (to_expr e)
| App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
| Lit l => heap_lang.Lit l
| UnOp op e => heap_lang.UnOp op (to_expr e)
| BinOp op e1 e2 => heap_lang.BinOp op (to_expr e1) (to_expr e2)
| If e0 e1 e2 => heap_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
| Pair e1 e2 => heap_lang.Pair (to_expr e1) (to_expr e2)
| Fst e => heap_lang.Fst (to_expr e)
| Snd e => heap_lang.Snd (to_expr e)
| InjL e => heap_lang.InjL (to_expr e)
| InjR e => heap_lang.InjR (to_expr e)
| Case e0 e1 e2 => heap_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
| Fork e => heap_lang.Fork (to_expr e)
| Alloc e => heap_lang.Alloc (to_expr e)
| Load e => heap_lang.Load (to_expr e)
| Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
| CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
end.
Ltac of_expr e :=
lazymatch e with
| heap_lang.Var ?x => constr:(Var x)
| heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
| heap_lang.App ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
| heap_lang.Lit ?l => constr:(Lit l)
| heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
| heap_lang.BinOp ?op ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
| heap_lang.If ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(If e0 e1 e2)
| heap_lang.Pair ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
| heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
| heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
| heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
| heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
| heap_lang.Case ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(Case e0 e1 e2)
| heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
| heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
| heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
| heap_lang.Store ?e1 ?e2 =>
let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
| heap_lang.CAS ?e0 ?e1 ?e2 =>
let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
constr:(CAS e0 e1 e2)
| to_expr ?e => e
| of_val ?v => constr:(Val v)
| _ => constr:(ltac:(
match goal with H : Closed [] e |- _ => exact (@ClosedExpr e H) end))
end.
Fixpoint is_closed (X : list string) (e : expr) : bool :=
match e with
| Val _ | ClosedExpr _ _ => true
| Var x => bool_decide (x ∈ X)
| Rec f x e => is_closed (f :b: x :b: X) e
| Lit _ => true
| UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
is_closed X e
| App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
is_closed X e1 && is_closed X e2
| If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
is_closed X e0 && is_closed X e1 && is_closed X e2
end.
Lemma is_closed_correct X e : is_closed X e → heap_lang.is_closed X (to_expr e).
Proof.
revert X.
induction e; naive_solver eauto using is_closed_of_val, is_closed_weaken_nil.
Qed.
Fixpoint to_val (e : expr) : option val :=
match e with
| Val v => Some v
| Rec f x e =>
if decide (is_closed (f :b: x :b: []) e) is left H
then Some (@RecV f x (to_expr e) (is_closed_correct _ _ H)) else None
| Lit l => Some (LitV l)
| Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
| InjL e => InjLV <$> to_val e
| InjR e => InjRV <$> to_val e
| _ => None
end.
Lemma to_val_Some e v :
to_val e = Some v → heap_lang.to_val (to_expr e) = Some v.
Proof.
revert v. induction e; intros; simplify_option_eq; rewrite ?to_of_val; auto.
- do 2 f_equal. apply proof_irrel.
- exfalso. unfold Closed in *; eauto using is_closed_correct.
Qed.
Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
match e with
| Val v => Val v
| ClosedExpr e H => @ClosedExpr e H
| Var y => if decide (x = y) then es else Var y
| Rec f y e =>
Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
| App e1 e2 => App (subst x es e1) (subst x es e2)
| Lit l => Lit l
| UnOp op e => UnOp op (subst x es e)
| BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
| If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
| Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
| Fst e => Fst (subst x es e)
| Snd e => Snd (subst x es e)
| InjL e => InjL (subst x es e)
| InjR e => InjR (subst x es e)
| Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
| Fork e => Fork (subst x es e)
| Alloc e => Alloc (subst x es e)
| Load e => Load (subst x es e)
| Store e1 e2 => Store (subst x es e1) (subst x es e2)
| CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
end.
Lemma to_expr_subst x er e :
to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
Proof.
induction e; simpl; repeat case_decide;
f_equal; auto using is_closed_nil_subst, is_closed_of_val, eq_sym.
Qed.
End W.
Ltac solve_closed :=
match goal with
| |- Closed ?X ?e =>
let e' := W.of_expr e in change (Closed X (W.to_expr e'));
apply W.is_closed_correct; vm_compute; exact I
end.
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Ltac solve_to_val :=
try match goal with
| |- language.to_val ?e = Some ?v => change (to_val e = Some v)
end;
match goal with
| |- to_val ?e = Some ?v =>
let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
apply W.to_val_Some; simpl; reflexivity
end.
(** Substitution *)
Ltac simpl_subst :=
csimpl;
repeat match goal with
| |- context [subst ?x ?er ?e] =>
let er' := W.of_expr er in let e' := W.of_expr e in
change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
end;
unfold W.to_expr.
Arguments W.to_expr : simpl never.
Arguments subst : simpl never.
(** The tactic [inv_head_step] performs inversion on hypotheses of the
shape [head_step]. The tactic will discharge head-reductions starting
from values, and simplifies hypothesis related to conversions from and
......
heap_lang/wp_tactics.v
View file @ 697523ea
From iris.algebra Require Export upred_tactics.
From iris.heap_lang Require Export tactics derived substitution.
From iris.heap_lang Require Export tactics derived.
Import uPred.
(** wp-specific helper tactics *)
......@@ -11,7 +11,14 @@ Ltac wp_bind K :=
(* TODO: Do something better here *)
Ltac wp_done :=
fast_done || apply into_value || apply _ || (rewrite /= ?to_of_val; fast_done).
match goal with
| |- Closed _ _ => solve_closed
| |- to_val _ = Some _ => solve_to_val
| |- language.to_val _ = Some _ => solve_to_val
| |- Is_true (atomic _) => rewrite /= ?to_of_val; fast_done
| |- Is_true (language.atomic _) => rewrite /= ?to_of_val; fast_done
| _ => fast_done
end.
(* sometimes, we will have to do a final view shift, so only apply
pvs_intro if we obtain a consecutive wp *)
......
Supports Markdown
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