Commit 83a6cd62 authored by Ralf Jung's avatar Ralf Jung

Merge branch 'rk/substitution' of gitlab.mpi-sws.org:FP/iris-coq into rk/substitution

parents d405b75c dd543f95
Pipeline #2279 passed with stage
......@@ -369,12 +369,6 @@ Proof. by rewrite /IntoValue /= => ->. Qed.
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.
Instance of_val_closed X v : Closed X (of_val v).
Proof.
apply is_closed_weaken with []; last set_solver.
induction v; simpl; auto.
Qed.
Lemma closed_subst X e x es : Closed X e x X subst x es e = e.
Proof.
rewrite /Closed. revert X.
......@@ -390,7 +384,10 @@ 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 of_val_closed. Qed.
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).
......
From iris.heap_lang Require Export derived.
From iris.heap_lang Require Import wp_tactics substitution notation.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
Definition Assert (e : expr) : expr :=
if: e then #() else #0 #0. (* #0 #0 is unsafe *)
Definition assert : val :=
λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
(* just below ;; *)
Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
Global Opaque assert.
Instance closed_assert X e : Closed X e Closed X (Assert e) := _.
Instance do_subst_assert x es e er :
Subst x es e er Subst x es (Assert e) (Assert er).
Proof. intros; red. by rewrite /Assert /subst -/subst; f_equal/=. Qed.
Typeclasses Opaque Assert.
Lemma wp_assert {Σ} (Φ : val iProp heap_lang Σ) :
Φ #() WP Assert #true {{ Φ }}.
Proof. by rewrite -wp_if_true -wp_value. Qed.
Lemma wp_assert' {Σ} (Φ : val iProp heap_lang Σ) e :
WP e {{ v, v = #true Φ #() }} WP Assert e {{ Φ }}.
Lemma wp_assert {Σ} (Φ : val iProp heap_lang Σ) e `{!Closed [] e} :
WP e {{ v, v = #true Φ #() }} WP assert: e {{ Φ }}.
Proof.
rewrite /Assert. wp_focus e; apply wp_mono=>v.
apply uPred.pure_elim_l=>->. apply wp_assert.
iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
wp_if. done.
Qed.
From iris.heap_lang Require Export lang.
Import heap_lang.
(** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
can be tuned by declaring [Subst] instances. *)
(** * Substitution *)
Class Subst (x : string) (es : expr) (e : expr) (er : expr) :=
do_subst : subst x es e = er.
Hint Mode Subst + + + - : typeclass_instances.
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).
(* Variables *)
Lemma do_subst_var_eq x er : Subst x er (Var x) er.
Proof. intros; red; simpl. by case_decide. Qed.
Lemma do_subst_var_neq x y er : bool_decide (x y) Subst x er (Var y) (Var y).
Proof. rewrite bool_decide_spec. intros; red; simpl. by case_decide. Qed.
Hint Extern 0 (Subst ?x ?v (Var ?y) _) =>
first [apply do_subst_var_eq
|apply do_subst_var_neq, I] : typeclass_instances.
(** Rec *)
Lemma do_subst_rec_true {x es f y e er} :
bool_decide (BNamed x f BNamed x y)
Subst x es e er Subst x es (Rec f y e) (Rec f y er).
Proof. rewrite bool_decide_spec. intros; red; f_equal/=; by case_decide. Qed.
Lemma do_subst_rec_false {x es f y e} :
bool_decide (¬(BNamed x f BNamed x y))
Subst x es (Rec f y e) (Rec f y e).
Proof. rewrite bool_decide_spec. intros; red; f_equal/=; by case_decide. Qed.
Local Ltac bool_decide_no_check := vm_cast_no_check I.
Hint Extern 0 (Subst ?x ?v (Rec ?f ?y ?e) _) =>
match eval vm_compute in (bool_decide (BNamed x f BNamed x y)) with
| true => eapply (do_subst_rec_true ltac:(bool_decide_no_check))
| false => eapply (do_subst_rec_false ltac:(bool_decide_no_check))
end : typeclass_instances.
Lemma do_subst_closed x es e : Closed [] e Subst x es e e.
Proof. apply closed_nil_subst. Qed.
Hint Extern 10 (Subst ?x ?v ?e _) =>
is_var e; class_apply do_subst_closed : typeclass_instances.
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.
(* Values *)
Instance do_subst_of_val x es v : Subst x es (of_val v) (of_val v) | 0.
Proof. eapply closed_nil_subst, of_val_closed. Qed.
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.
(* Boring connectives *)
Section subst.
Context (x : string) (es : expr).
Notation Sub := (Subst x es).
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.
(* Ground terms *)
Global Instance do_subst_lit l : Sub (Lit l) (Lit l).
Proof. done. Qed.
Global Instance do_subst_app e1 e2 e1r e2r :
Sub e1 e1r Sub e2 e2r Sub (App e1 e2) (App e1r e2r).
Proof. intros; red; f_equal/=; apply: do_subst. Qed.
Global Instance do_subst_unop op e er : Sub e er Sub (UnOp op e) (UnOp op er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_binop op e1 e2 e1r e2r :
Sub e1 e1r Sub e2 e2r Sub (BinOp op e1 e2) (BinOp op e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_if e0 e1 e2 e0r e1r e2r :
Sub e0 e0r Sub e1 e1r Sub e2 e2r Sub (If e0 e1 e2) (If e0r e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_pair e1 e2 e1r e2r :
Sub e1 e1r Sub e2 e2r Sub (Pair e1 e2) (Pair e1r e2r).
Proof. by intros ??; red; f_equal/=. Qed.
Global Instance do_subst_fst e er : Sub e er Sub (Fst e) (Fst er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_snd e er : Sub e er Sub (Snd e) (Snd er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_injL e er : Sub e er Sub (InjL e) (InjL er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_injR e er : Sub e er Sub (InjR e) (InjR er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_case e0 e1 e2 e0r e1r e2r :
Sub e0 e0r Sub e1 e1r Sub e2 e2r Sub (Case e0 e1 e2) (Case e0r e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_fork e er : Sub e er Sub (Fork e) (Fork er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_alloc e er : Sub e er Sub (Alloc e) (Alloc er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_load e er : Sub e er Sub (Load e) (Load er).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_store e1 e2 e1r e2r :
Sub e1 e1r Sub e2 e2r Sub (Store e1 e2) (Store e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
Global Instance do_subst_cas e0 e1 e2 e0r e1r e2r :
Sub e0 e0r Sub e1 e1r Sub e2 e2r Sub (CAS e0 e1 e2) (CAS e0r e1r e2r).
Proof. by intros; red; f_equal/=. Qed.
End subst.
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 ?es ?e] => progress rewrite (@do_subst x es e)
| |- _ => progress csimpl
end.
| |- 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.
......@@ -14,8 +14,8 @@ Definition one_shot_example : val := λ: <>,
InjL <> => #()
| InjR "n" =>
match: !"x" with
InjL <> => Assert #false
| InjR "m" => Assert ("n" = "m")
InjL <> => assert: #false
| InjR "m" => assert: "n" = "m"
end
end)).
Global Opaque one_shot_example.
......@@ -79,7 +79,7 @@ Proof.
iCombine "Hγ" "Hγ'" as "Hγ".
iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
iSplitL "Hl"; [iRight; by eauto|].
wp_match. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
Qed.
Lemma hoare_one_shot (Φ : val iProp) :
......
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