Commit eba4ac6e authored by Robbert Krebbers's avatar Robbert Krebbers

Use a named representation of binding in heap_lang.

We can use a named representation because we only substitute closed values. This
idea is borrowed from Pierce's Software Foundations.

The named representation has the following advantages:
* Programs are much better readable than those using De Bruijn indexes.
* Substitutions on closed terms (where all variables are explicit strings) can
  be performed by a mere simpl instead of Autosubst's asimpl. The performance
  of simpl seems better than asimpl.
* Syntactic sugar refolds better.
parent af8d4175
......@@ -5,7 +5,6 @@ This version is known to compile with:
- Coq 8.5
- Ssreflect 1.6
- Autosubst 1.4
For development, better make sure you have a version of Ssreflect that includes
commit be724937 (no such version has been released so far, you will have to
......
Require Export Autosubst.Autosubst.
Require Export program_logic.language.
Require Export program_logic.language prelude.strings.
Require Import prelude.gmap.
Module heap_lang.
......@@ -15,9 +14,8 @@ Inductive bin_op : Set :=
Inductive expr :=
(* Base lambda calculus *)
| Var (x : var)
| Rec (e : {bind 2 of expr}) (* These are recursive lambdas.
The *inner* binder is the recursive call! *)
| Var (x : string)
| Rec (f x : string) (e : expr)
| App (e1 e2 : expr)
(* Base types and their operations *)
| Lit (l : base_lit)
......@@ -31,7 +29,7 @@ Inductive expr :=
(* Sums *)
| InjL (e : expr)
| InjR (e : expr)
| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
| Case (e0 : expr) (x1 : string) (e1 : expr) (x2 : string) (e2 : expr)
(* Concurrency *)
| Fork (e : expr)
(* Heap *)
......@@ -41,14 +39,8 @@ Inductive expr :=
| Store (e1 : expr) (e2 : expr)
| Cas (e0 : expr) (e1 : expr) (e2 : expr).
Instance Ids_expr : Ids expr. derive. Defined.
Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
Inductive val :=
| RecV (e : {bind 2 of expr}) (* These are recursive lambdas.
The *inner* binder is the recursive call! *)
| RecV (f x : string) (e : expr) (* e should be closed *)
| LitV (l : base_lit)
| PairV (v1 v2 : val)
| InjLV (v : val)
......@@ -57,7 +49,7 @@ Inductive val :=
Fixpoint of_val (v : val) : expr :=
match v with
| RecV e => Rec e
| RecV f x e => Rec f x e
| LitV l => Lit l
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
......@@ -66,7 +58,7 @@ Fixpoint of_val (v : val) : expr :=
end.
Fixpoint to_val (e : expr) : option val :=
match e with
| Rec e => Some (RecV e)
| Rec f x e => Some (RecV f x e)
| 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
......@@ -92,7 +84,7 @@ Inductive ectx_item :=
| SndCtx
| InjLCtx
| InjRCtx
| CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
| CaseCtx (x1 : string) (e1 : expr) (x2 : string) (e2 : expr)
| AllocCtx
| LoadCtx
| StoreLCtx (e2 : expr)
......@@ -117,7 +109,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| SndCtx => Snd e
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| CaseCtx x1 e1 x2 e2 => Case e x1 e1 x2 e2
| AllocCtx => Alloc e
| LoadCtx => Load e
| StoreLCtx e2 => Store e e2
......@@ -128,49 +120,78 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
end.
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
(** Substitution *)
(** We have [subst e "" v = e] to deal with anonymous binders *)
Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
match e with
| Var y => if decide (x = y x "") then of_val v else Var y
| Rec f y e => Rec f y (if decide (x f x y) then subst e x v else e)
| App e1 e2 => App (subst e1 x v) (subst e2 x v)
| Lit l => Lit l
| UnOp op e => UnOp op (subst e x v)
| BinOp op e1 e2 => BinOp op (subst e1 x v) (subst e2 x v)
| If e0 e1 e2 => If (subst e0 x v) (subst e1 x v) (subst e2 x v)
| Pair e1 e2 => Pair (subst e1 x v) (subst e2 x v)
| Fst e => Fst (subst e x v)
| Snd e => Snd (subst e x v)
| InjL e => InjL (subst e x v)
| InjR e => InjR (subst e x v)
| Case e0 x1 e1 x2 e2 =>
Case (subst e0 x v)
x1 (if decide (x x1) then subst e1 x v else e1)
x2 (if decide (x x2) then subst e2 x v else e2)
| Fork e => Fork (subst e x v)
| Loc l => Loc l
| Alloc e => Alloc (subst e x v)
| Load e => Load (subst e x v)
| Store e1 e2 => Store (subst e1 x v) (subst e2 x v)
| Cas e0 e1 e2 => Cas (subst e0 x v) (subst e1 x v) (subst e2 x v)
end.
(** The stepping relation *)
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
match op, l with
| NegOp, LitBool b => Some $ LitBool (negb b)
| NegOp, LitBool b => Some (LitBool (negb b))
| _, _ => None
end.
Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
match op, l1, l2 with
| PlusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 + n2)
| MinusOp, LitNat n1, LitNat n2 => Some $ LitNat (n1 - n2)
| LeOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 n2)
| LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 < n2)
| EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ bool_decide (n1 = n2)
| PlusOp, LitNat n1, LitNat n2 => Some (LitNat (n1 + n2))
| MinusOp, LitNat n1, LitNat n2 => Some (LitNat (n1 - n2))
| LeOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 n2)))
| LtOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 < n2)))
| EqOp, LitNat n1, LitNat n2 => Some (LitBool (bool_decide (n1 = n2)))
| _, _, _ => None
end.
Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
| BetaS e1 e2 v2 σ :
| BetaS f x e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Rec e1) e2) σ e1.[(Rec e1),e2/] σ None
| UnOpS op l l' σ:
head_step (App (Rec f x e1) e2) σ
(subst (subst e1 f (RecV f x e1)) x v2) σ None
| UnOpS op l l' σ :
un_op_eval op l = Some l'
head_step (UnOp op (Lit l)) σ (Lit l') σ None
| BinOpS op l1 l2 l' σ:
| BinOpS op l1 l2 l' σ :
bin_op_eval op l1 l2 = Some l'
head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
| IfTrueS e1 e2 σ :
head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
head_step (If (Lit (LitBool true)) e1 e2) σ e1 σ None
| IfFalseS e1 e2 σ :
head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
head_step (If (Lit (LitBool false)) e1 e2) σ e2 σ None
| FstS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Fst (Pair e1 e2)) σ e1 σ None
| SndS e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
head_step (Snd (Pair e1 e2)) σ e2 σ None
| CaseLS e0 v0 e1 e2 σ :
| CaseLS e0 v0 x1 e1 x2 e2 σ :
to_val e0 = Some v0
head_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ None
| CaseRS e0 v0 e1 e2 σ :
head_step (Case (InjL e0) x1 e1 x2 e2) σ (subst e1 x1 v0) σ None
| CaseRS e0 v0 x1 e1 x2 e2 σ :
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
head_step (Case (InjR e0) x1 e1 x2 e2) σ (subst e2 x2 v0) σ None
| ForkS e σ:
head_step (Fork e) σ (Lit LitUnit) σ (Some e)
| AllocS e v σ l :
......@@ -185,14 +206,14 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
| CasFailS l e1 v1 e2 v2 vl σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some vl vl v1
head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
head_step (Cas (Loc l) e1 e2) σ (Lit (LitBool false)) σ None
| CasSucS l e1 v1 e2 v2 σ :
to_val e1 = Some v1 to_val e2 = Some v2
σ !! l = Some v1
head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
head_step (Cas (Loc l) e1 e2) σ (Lit (LitBool true)) (<[l:=v2]>σ) None.
(** Atomic expressions *)
Definition atomic (e: expr) :=
Definition atomic (e: expr) : Prop :=
match e with
| Alloc e => is_Some (to_val e)
| Load e => is_Some (to_val e)
......@@ -302,6 +323,8 @@ Lemma alloc_fresh e v σ :
to_val e = Some v head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
Lemma subst_empty e v : subst e "" v = e.
Proof. induction e; simpl; repeat case_decide; intuition auto with f_equal. Qed.
End heap_lang.
(** Language *)
......
......@@ -80,12 +80,13 @@ Proof.
by rewrite -(wp_value' _ _ (Lit _)) //; apply const_intro.
Qed.
Lemma wp_rec E erec e v Q :
to_val e = Some v
wp E erec.[Rec erec, e /] Q wp E (App (Rec erec) e) Q.
Lemma wp_rec E f x e1 e2 v Q :
to_val e2 = Some v
wp E (subst (subst e1 f (RecV f x e1)) x v) Q wp E (App (Rec f x e1) e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (App _ _) erec.[Rec erec, e /] None)
?right_id //=; last by intros; inv_step; eauto.
intros. rewrite -(wp_lift_pure_det_step (App _ _)
(subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
last by intros; inv_step; eauto.
Qed.
Lemma wp_un_op E op l l' Q :
......@@ -138,19 +139,19 @@ Proof.
by rewrite -wp_value'.
Qed.
Lemma wp_case_inl E e0 v0 e1 e2 Q :
Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
to_val e0 = Some v0
wp E e1.[e0/] Q wp E (Case (InjL e0) e1 e2) Q.
wp E (subst e1 x1 v0) Q wp E (Case (InjL e0) x1 e1 x2 e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _) e1.[e0/] None)
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e1 x1 v0) None)
?right_id //; last by intros; inv_step; eauto.
Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Q :
Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
to_val e0 = Some v0
wp E e2.[e0/] Q wp E (Case (InjR e0) e1 e2) Q.
wp E (subst e2 x2 v0) Q wp E (Case (InjR e0) x1 e1 x2 e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _) e2.[e0/] None)
intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e2 x2 v0) None)
?right_id //; last by intros; inv_step; eauto.
Qed.
......
......@@ -2,30 +2,12 @@ Require Export heap_lang.heap_lang heap_lang.lifting.
Import uPred heap_lang.
(** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
Definition Let (e1 : expr) (e2: {bind expr}) := App (Lam e2) e1.
Definition Seq (e1 e2 : expr) := Let e1 e2.[ren(+1)].
Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
(* Prove and "register" compatibility with substitution. *)
Lemma Lam_subst e s : (Lam e).[s] = Lam e.[up s].
Proof. by unfold Lam; asimpl. Qed.
Hint Rewrite Lam_subst : autosubst.
Global Opaque Lam.
Lemma Let_subst e1 e2 s : (Let e1 e2).[s] = Let e1.[s] e2.[up s].
Proof. by unfold Let; asimpl. Qed.
Hint Rewrite Let_subst : autosubst.
Global Opaque Let.
Lemma Seq_subst e1 e2 s : (Seq e1 e2).[s] = Seq e1.[s] e2.[s].
Proof. by unfold Seq; asimpl. Qed.
Hint Rewrite Seq_subst : autosubst.
Global Opaque Seq.
Notation Lam x e := (Rec "" x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let "" e1 e2).
Notation LamV x e := (RecV "" x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx "" e2).
Module notations.
Delimit Scope lang_scope with L.
......@@ -36,16 +18,12 @@ Module notations.
Coercion LitBool : bool >-> base_lit.
(* No coercion from base_lit to expr. This makes is slightly easier to tell
apart language and Coq expressions. *)
Coercion Loc : loc >-> expr.
Coercion LocV : loc >-> val.
Coercion Var : string >-> expr.
Coercion App : expr >-> Funclass.
(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
first. *)
(* What about Arguments for hoare triples?. *)
(* The colons indicate binders. "let" is not consistent here though,
thing are only bound in the "in". *)
Notation "# n" := (ids (term:=expr) n) (at level 1, format "# n") : lang_scope.
Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
......@@ -57,14 +35,19 @@ Module notations.
Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
(* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
Notation "e1 ; e2" := (Seq e1%L e2%L)
(at level 100, e2 at level 200) : lang_scope.
Notation "'let:' e1 'in' e2" := (Let e1%L e2%L)
(at level 102, e2 at level 200) : lang_scope.
Notation "'λ:' e" := (Lam e%L) (at level 102, e at level 200) : lang_scope.
Notation "'rec::' e" := (Rec e%L) (at level 102, e at level 200) : lang_scope.
Notation "'rec:' f x := e" := (Rec f x e%L)
(at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
(at level 200, e1, e2, e3 at level 200) : lang_scope.
(* derived notions, in order of declaration *)
Notation "λ: x , e" := (Lam x e%L)
(at level 102, x at level 1, e at level 200) : lang_scope.
(* FIXME: the ones below are not being pretty printed *)
Notation "'let:' x := e1 'in' e2" := (Let x e1%L e2%L)
(at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
Notation "e1 ; e2" := (Seq e1%L e2%L)
(at level 100, e2 at level 200) : lang_scope.
End notations.
Section suger.
......@@ -73,34 +56,26 @@ Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val iProp heap_lang Σ.
(** Proof rules for the sugar *)
Lemma wp_lam E ef e v Q :
to_val e = Some v wp E ef.[e/] Q wp E (App (Lam ef) e) Q.
Proof.
intros Hv. rewrite -wp_rec; last eassumption.
(* RJ: This pulls in functional extensionality. If that bothers us, we have
to talk to the Autosubst guys. *)
by asimpl.
Qed.
Lemma wp_lam E x ef e v Q :
to_val e = Some v wp E (subst ef x v) Q wp E (App (Lam x ef) e) Q.
Proof. intros. by rewrite -wp_rec ?subst_empty; eauto. Qed.
Lemma wp_let E e1 e2 Q :
wp E e1 (λ v, wp E (e2.[of_val v/]) Q) wp E (Let e1 e2) Q.
Lemma wp_let E x e1 e2 Q :
wp E e1 (λ v, wp E (subst e2 x v) Q) wp E (Let x e1 e2) Q.
Proof.
rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v.
rewrite -(wp_bind [LetCtx x e2]). apply wp_mono=>v.
by rewrite -wp_lam //= to_of_val.
Qed.
Lemma wp_seq E e1 e2 Q :
wp E e1 (λ _, wp E e2 Q) wp E (Seq e1 e2) Q.
Proof.
rewrite -wp_let. apply wp_mono=>v. by asimpl.
Qed.
Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, wp E e2 Q) wp E (Seq e1 e2) Q.
Proof. rewrite -wp_let. apply wp_mono=>v. by rewrite subst_empty. Qed.
Lemma wp_le E (n1 n2 : nat) P Q :
(n1 n2 P Q (LitV true))
(n1 > n2 P Q (LitV false))
P wp E (BinOp LeOp (Lit n1) (Lit n2)) Q.
Proof.
intros ? ?. rewrite -wp_bin_op //; [].
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 n2)); by eauto with omega.
Qed.
......@@ -109,7 +84,7 @@ Lemma wp_lt E (n1 n2 : nat) P Q :
(n1 n2 P Q (LitV false))
P wp E (BinOp LtOp (Lit n1) (Lit n2)) Q.
Proof.
intros ? ?. rewrite -wp_bin_op //; [].
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
Qed.
......@@ -118,7 +93,7 @@ Lemma wp_eq E (n1 n2 : nat) P Q :
(n1 n2 P Q (LitV false))
P wp E (BinOp EqOp (Lit n1) (Lit n2)) Q.
Proof.
intros ? ?. rewrite -wp_bin_op //; [].
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
Qed.
......
......@@ -7,12 +7,18 @@ Module LangTests.
Definition add := (Lit 21 + Lit 21)%L.
Goal σ, prim_step add σ (Lit 42) σ None.
Proof. intros; do_step done. Qed.
Definition rec_app : expr := (rec:: #0 #1) (Lit 0).
Definition rec_app : expr := (rec: "f" "x" := "f" "x") (Lit 0).
Goal σ, prim_step rec_app σ rec_app σ None.
Proof. intros; do_step done. Qed.
Definition lam : expr := λ: #0 + Lit 21.
Proof.
intros. rewrite /rec_app. (* FIXME: do_step does not work here *)
by eapply (Ectx_step _ _ _ _ _ []), (BetaS _ _ _ _ (LitV (LitNat 0))).
Qed.
Definition lam : expr := λ: "x", "x" + Lit 21.
Goal σ, prim_step (lam (Lit 21)) σ add σ None.
Proof. rewrite /lam /Lam. intros; do_step done. Qed.
Proof.
intros. rewrite /lam. (* FIXME: do_step does not work here *)
by eapply (Ectx_step _ _ _ _ _ []), (BetaS "" "x" ("x" + Lit 21) _ (LitV 21)).
Qed.
End LangTests.
Module LiftingTests.
......@@ -20,22 +26,23 @@ Module LiftingTests.
Implicit Types P : iProp heap_lang Σ.
Implicit Types Q : val iProp heap_lang Σ.
Definition e : expr := let: ref (Lit 1) in #0 <- !#0 + Lit 1; !#0.
Goal σ E, (ownP σ : iProp heap_lang Σ) (wp E e (λ v, (v = LitV 2))).
Definition e : expr :=
let: "x" := ref (Lit 1) in "x" <- !"x" + Lit 1; !"x".
Goal σ E, (ownP σ : iProp heap_lang Σ) (wp E e (λ v, (v = LitV 2))).
Proof.
move=> σ E. rewrite /e.
rewrite -wp_let. rewrite -wp_alloc_pst; last done.
rewrite -wp_let /= -wp_alloc_pst //=.
apply sep_intro_True_r; first done.
rewrite -later_intro. apply forall_intro=>l.
apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
rewrite -later_intro. asimpl.
rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
rewrite -later_intro; apply forall_intro=>l; apply wand_intro_l.
rewrite right_id; apply const_elim_l=> _.
rewrite -later_intro.
rewrite -(wp_bindi (SeqCtx (Load (Loc _)))) /=.
(* FIXME: doing simpl here kills the Seq, turns it all the way into Rec *)
rewrite -(wp_bindi (StoreRCtx (LocV _))).
rewrite -(wp_bindi (BinOpLCtx PlusOp _)).
rewrite -(wp_bindi (StoreRCtx (LocV _))) /=.
rewrite -(wp_bindi (BinOpLCtx PlusOp _)) /=.
rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
{ by rewrite lookup_insert. } (* RJ FIXME: figure out why apply and eapply fail. *)
rewrite -later_intro. apply wand_intro_l. rewrite right_id.
rewrite -later_intro; apply wand_intro_l; rewrite right_id.
rewrite -wp_bin_op // -later_intro.
rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
{ by rewrite lookup_insert. }
......@@ -49,56 +56,50 @@ Module LiftingTests.
Qed.
Definition FindPred (n2 : expr) : expr :=
rec:: let: #1 + Lit 1 in if #0 < n2.[ren(+3)] then #1 #0 else #2.
rec: "pred" "y" :=
let: "yp" := "y" + Lit 1 in
if "yp" < n2 then "pred" "yp" else "y".
Definition Pred : expr :=
λ: if #0 Lit 0 then Lit 0 else FindPred #0 (Lit 0).
λ: "x", if "x" Lit 0 then Lit 0 else FindPred "x" (Lit 0).
Lemma FindPred_spec n1 n2 E Q :
( (n1 < n2) Q (LitV $ pred n2)) wp E (FindPred (Lit n2) (Lit n1)) Q.
( (n1 < n2) Q (LitV (pred n2))) wp E (FindPred (Lit n2) (Lit n1)) Q.
Proof.
revert n1. apply löb_all_1=>n1.
rewrite -wp_rec //. asimpl.
(* Get rid of the ▷ in the premise. *)
etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
{ apply and_mono; first done. by rewrite -later_intro. }
apply later_mono.
rewrite (commutative uPred_and ( _)%I) associative; apply const_elim_r=>?.
rewrite -wp_rec //=.
(* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
rewrite ->(later_intro (Q _)).
rewrite -!later_and; apply later_mono.
(* Go on *)
rewrite -wp_let.
rewrite -wp_bin_op //. asimpl.
rewrite -(wp_bindi (IfCtx _ _)).
rewrite -!later_intro /=.
apply wp_lt; intros Hn12.
* rewrite -wp_if_true.
rewrite -!later_intro. asimpl.
rewrite (forall_elim (S n1)).
eapply impl_elim; first by eapply and_elim_l. apply and_intro.
+ apply const_intro; omega.
+ by rewrite !and_elim_r.
* rewrite -wp_if_false.
rewrite -!later_intro -wp_value' //.
rewrite and_elim_r. apply const_elim_l=>Hle.
by replace n1 with (pred n2) by omega.
rewrite -wp_let -wp_bin_op //= -(wp_bindi (IfCtx _ _)) /= -!later_intro.
apply wp_lt=> ?.
- rewrite -wp_if_true.
rewrite -!later_intro (forall_elim (n1 + 1)) const_equiv; last omega.
by rewrite left_id impl_elim_l.
- assert (n1 = pred n2) as -> by omega.
rewrite -wp_if_false.
by rewrite -!later_intro -wp_value' // and_elim_r.
Qed.
Lemma Pred_spec n E Q :
Q (LitV $ pred n) wp E (Pred $ Lit n) Q.
Lemma Pred_spec n E Q : Q (LitV (pred n)) wp E (Pred (Lit n)) Q.
Proof.
rewrite -wp_lam //. asimpl.
rewrite -wp_lam //=.
rewrite -(wp_bindi (IfCtx _ _)).
apply later_mono, wp_le=> Hn.
- rewrite -wp_if_true.
rewrite -!later_intro -wp_value' //.
by replace n with 0 by omega.
rewrite -!later_intro -wp_value' //=.
auto with f_equal omega.
- rewrite -wp_if_false.
rewrite -!later_intro -FindPred_spec.
auto using and_intro, const_intro with omega.
Qed.
Goal E,
True wp (Σ:=Σ) E (let: Pred $ Lit 42 in Pred #0) (λ v, (v = LitV 40)).
True wp (Σ:=Σ) E (let: "x" := Pred (Lit 42) in Pred "x")
(λ v, (v = LitV 40)).
Proof.
intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro /=.
rewrite -Pred_spec -later_intro. by apply const_intro.
Qed.
End LiftingTests.
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