Commit 66f99021 authored by Ralf Jung's avatar Ralf Jung

add basic notions of literals, unary operators and binary operators, and use...

add basic notions of literals, unary operators and binary operators, and use them to define +, -, <=, ...
parent eb82a9c7
......@@ -6,18 +6,24 @@ Module heap_lang.
(** Expressions and vals. *)
Definition loc := positive. (* Really, any countable type. *)
Inductive base_lit : Set :=
| LitNat (n : nat) | LitBool (b : bool) | LitUnit.
Inductive un_op : Set :=
| NegOp.
Inductive bin_op : Set :=
| PlusOp | MinusOp | LeOp | LtOp | EqOp.
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! *)
| App (e1 e2 : expr)
(* Natural numbers *)
| LitNat (n : nat)
| Plus (e1 e2 : expr)
| Le (e1 e2 : expr)
(* Unit *)
| LitUnit
(* 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)
......@@ -40,29 +46,19 @@ Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
(* This sugar is used by primitive reduction riles (<=, CAS) and hence
defined here. *)
Notation LitTrue := (InjL LitUnit).
Notation LitFalse := (InjR LitUnit).
Inductive val :=
| RecV (e : {bind 2 of expr}) (* These are recursive lambdas.
The *inner* binder is the recursive call! *)
| LitNatV (n : nat)
| LitUnitV
| LitV (l : base_lit)
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
| LocV (l : loc).
Definition LitTrueV := InjLV LitUnitV.
Definition LitFalseV := InjRV LitUnitV.
Fixpoint of_val (v : val) : expr :=
match v with
| RecV e => Rec e
| LitNatV n => LitNat n
| LitUnitV => LitUnit
| LitV l => Lit l
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
......@@ -71,8 +67,7 @@ Fixpoint of_val (v : val) : expr :=
Fixpoint to_val (e : expr) : option val :=
match e with
| Rec e => Some (RecV e)
| LitNat n => Some (LitNatV n)
| LitUnit => Some LitUnitV
| 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
......@@ -87,10 +82,10 @@ Definition state := gmap loc val.
Inductive ectx_item :=
| AppLCtx (e2 : expr)
| AppRCtx (v1 : val)
| PlusLCtx (e2 : expr)
| PlusRCtx (v1 : val)
| LeLCtx (e2 : expr)
| LeRCtx (v1 : val)
| UnOpCtx (op : un_op)
| BinOpLCtx (op : bin_op) (e2 : expr)
| BinOpRCtx (op : bin_op) (v1 : val)
| IfCtx (e1 e2 : expr)
| PairLCtx (e2 : expr)
| PairRCtx (v1 : val)
| FstCtx
......@@ -112,10 +107,10 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
match Ki with
| AppLCtx e2 => App e e2
| AppRCtx v1 => App (of_val v1) e
| PlusLCtx e2 => Plus e e2
| PlusRCtx v1 => Plus (of_val v1) e
| LeLCtx e2 => Le e e2
| LeRCtx v1 => Le (of_val v1) e
| UnOpCtx op => UnOp op e
| BinOpLCtx op e2 => BinOp op e e2
| BinOpRCtx op v1 => BinOp op (of_val v1) e
| IfCtx e1 e2 => If e e1 e2
| PairLCtx e2 => Pair e e2
| PairRCtx v1 => Pair (of_val v1) e
| FstCtx => Fst e
......@@ -134,18 +129,43 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
(** 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)
| _, _ => None
end.
(* FIXME RJ I am *sure* this already exists somewhere... but I can't find it. *)
Definition sum2bool {A B} (x : { A } + { B }) : bool :=
match x with
| left _ => true
| right _ => false
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 $ sum2bool $ decide (n1 n2)
| LtOp, LitNat n1, LitNat n2 => Some $ LitBool $ sum2bool $ decide (n1 < n2)
| EqOp, LitNat n1, LitNat n2 => Some $ LitBool $ sum2bool $ decide (n1 = n2)
| _, _, _ => None
end.
Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
| BetaS e1 e2 v2 σ :
to_val e2 = Some v2
head_step (App (Rec e1) e2) σ e1.[(Rec e1),e2/] σ None
| PlusS n1 n2 σ:
head_step (Plus (LitNat n1) (LitNat n2)) σ (LitNat (n1 + n2)) σ None
| LeTrueS n1 n2 σ :
n1 n2
head_step (Le (LitNat n1) (LitNat n2)) σ LitTrue σ None
| LeFalseS n1 n2 σ :
n1 > n2
head_step (Le (LitNat n1) (LitNat n2)) σ LitFalse σ 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' σ:
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
| IfFalseS e1 e2 σ :
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
......@@ -159,7 +179,7 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
| ForkS e σ:
head_step (Fork e) σ LitUnit σ (Some e)
head_step (Fork e) σ (Lit LitUnit) σ (Some e)
| AllocS e v σ l :
to_val e = Some v σ !! l = None
head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
......@@ -168,15 +188,15 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
head_step (Load (Loc l)) σ (of_val v) σ None
| StoreS l e v σ :
to_val e = Some v is_Some (σ !! l)
head_step (Store (Loc l) e) σ LitUnit (<[l:=v]>σ) None
head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
| 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) σ LitFalse σ 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) σ LitTrue (<[l:=v2]>σ) None.
head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
(** Atomic expressions *)
Definition atomic (e: expr) :=
......@@ -263,7 +283,7 @@ Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
fill_item Ki1 e1 = fill_item Ki2 e2 Ki1 = Ki2.
Proof.
destruct Ki1, Ki2; intros; try discriminate; simplify_equality';
try match goal with
repeat match goal with
| H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
end; auto.
Qed.
......
......@@ -38,14 +38,13 @@ Ltac reshape_expr e tac :=
lazymatch e1 with
| of_val ?v1 => go (AppRCtx v1 :: K) e2 | _ => go (AppLCtx e2 :: K) e1
end
| Plus ?e1 ?e2 =>
| UnOp ?op ?e =>
go (UnOpCtx op :: K) e
| BinOp ?op ?e1 ?e2 =>
lazymatch e1 with
| of_val ?v1 => go (PlusRCtx v1 :: K) e2 | _ => go (PlusLCtx e2 :: K) e1
end
| Le ?e1 ?e2 =>
lazymatch e1 with
| of_val ?v1 => go (LeRCtx v1 :: K) e2 | _ => go (LeLCtx e2 :: K) e1
| of_val ?v1 => go (BinOpRCtx op v1 :: K) e2 | _ => go (BinOpLCtx op e2 :: K) e1
end
| If ?e0 ?e1 ?e2 => go (IfCtx e1 e2 :: K) e0
| Pair ?e1 ?e2 =>
lazymatch e1 with
| of_val ?v1 => go (PairRCtx v1 :: K) e2 | _ => go (PairLCtx e2 :: K) e1
......
......@@ -48,36 +48,36 @@ Qed.
Lemma wp_store_pst E σ l e v v' Q :
to_val e = Some v σ !! l = Some v'
(ownP σ (ownP (<[l:=v]>σ) - Q LitUnitV)) wp E (Store (Loc l) e) Q.
(ownP σ (ownP (<[l:=v]>σ) - Q $ LitV LitUnit)) wp E (Store (Loc l) e) Q.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ) None)
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitUnit) (<[l:=v]>σ) None)
?right_id //; last by intros; inv_step; eauto.
Qed.
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v' v' v1
(ownP σ (ownP σ - Q LitFalseV)) wp E (Cas (Loc l) e1 e2) Q.
(ownP σ (ownP σ - Q $ LitV $ LitBool false)) wp E (Cas (Loc l) e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ LitFalseV σ None) ?right_id //;
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None) ?right_id //;
last by intros; inv_step; eauto.
Qed.
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2 σ !! l = Some v1
(ownP σ (ownP (<[l:=v2]>σ) - Q LitTrueV)) wp E (Cas (Loc l) e1 e2) Q.
(ownP σ (ownP (<[l:=v2]>σ) - Q $ LitV $ LitBool true)) wp E (Cas (Loc l) e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ) None)
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true) (<[l:=v2]>σ) None)
?right_id //; last by intros; inv_step; eauto.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
Lemma wp_fork E e :
wp (Σ:=Σ) coPset_all e (λ _, True) wp E (Fork e) (λ v, (v = LitUnitV)).
wp (Σ:=Σ) coPset_all e (λ _, True) wp E (Fork e) (λ v, (v = LitV $ LitUnit)).
Proof.
rewrite -(wp_lift_pure_det_step (Fork e) LitUnit (Some e)) //=;
rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_step; eauto.
apply later_mono, sep_intro_True_l; last done.
by rewrite -(wp_value' _ _ LitUnit) //; apply const_intro.
by rewrite -(wp_value' _ _ (Lit _)) //; apply const_intro.
Qed.
Lemma wp_rec E erec e v Q :
......@@ -88,30 +88,36 @@ Proof.
?right_id //=; last by intros; inv_step; eauto.
Qed.
Lemma wp_plus E n1 n2 Q :
Q (LitNatV (n1 + n2)) wp E (Plus (LitNat n1) (LitNat n2)) Q.
Lemma wp_un_op E op l l' Q :
un_op_eval op l = Some l'
Q (LitV l') wp E (UnOp op (Lit l)) Q.
Proof.
rewrite -(wp_lift_pure_det_step (Plus _ _) (LitNat (n1 + n2)) None)
intros Heval. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
?right_id //; last by intros; inv_step; eauto.
by rewrite -wp_value'.
Qed.
Lemma wp_le_true E n1 n2 Q :
n1 n2
Q LitTrueV wp E (Le (LitNat n1) (LitNat n2)) Q.
Lemma wp_bin_op E op l1 l2 l' Q :
bin_op_eval op l1 l2 = Some l'
Q (LitV l') wp E (BinOp op (Lit l1) (Lit l2)) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Le _ _) LitTrue None) ?right_id //;
last by intros; inv_step; eauto with omega.
intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
?right_id //; last by intros; inv_step; eauto.
by rewrite -wp_value'.
Qed.
Lemma wp_le_false E n1 n2 Q :
n1 > n2
Q LitFalseV wp E (Le (LitNat n1) (LitNat n2)) Q.
Lemma wp_if_true E e1 e2 Q :
wp E e1 Q wp E (If (Lit $ LitBool true) e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_pure_det_step (Le _ _) LitFalse None) ?right_id //;
last by intros; inv_step; eauto with omega.
by rewrite -wp_value'.
rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
?right_id //; last by intros; inv_step; eauto.
Qed.
Lemma wp_if_false E e1 e2 Q :
wp E e2 Q wp E (If (Lit $ LitBool false) e1 e2) Q.
Proof.
rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
?right_id //; last by intros; inv_step; eauto.
Qed.
Lemma wp_fst E e1 v1 e2 v2 Q :
......@@ -148,15 +154,4 @@ Proof.
?right_id //; last by intros; inv_step; eauto.
Qed.
(** Some derived stateless axioms *)
Lemma wp_le E n1 n2 P Q :
(n1 n2 P Q LitTrueV)
(n1 > n2 P Q LitFalseV)
P wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof.
intros; destruct (decide (n1 n2)).
* rewrite -wp_le_true; auto.
* rewrite -wp_le_false; auto with omega.
Qed.
End lifting.
......@@ -5,11 +5,6 @@ Import uPred heap_lang.
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 If (e0 e1 e2 : expr) := Case e0 e1.[ren(+1)] e2.[ren(+1)].
Definition Lt e1 e2 := Le (Plus e1 $ LitNat 1) e2.
Definition Eq e1 e2 :=
Let e1 (Let e2.[ren(+1)]
(If (Le (Var 0) (Var 1)) (Le (Var 1) (Var 0)) LitFalse)).
Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
......@@ -21,8 +16,10 @@ Module notations.
Bind Scope lang_scope with expr.
Arguments wp {_ _} _ _%L _.
Coercion LitNat : nat >-> expr.
Coercion LitNatV : nat >-> val.
Coercion LitNat : nat >-> base_lit.
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 App : expr >-> Funclass.
......@@ -35,10 +32,13 @@ Module notations.
Notation "# n" := (Var 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" := (Plus e1%L e2%L)
Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
(at level 50, left associativity) : lang_scope.
Notation "e1 ≤ e2" := (Le e1%L e2%L) (at level 70) : lang_scope.
Notation "e1 < e2" := (Lt e1%L e2%L) (at level 70) : lang_scope.
Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)
(at level 50, left associativity) : lang_scope.
Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope.
Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope.
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) : lang_scope.
......@@ -46,7 +46,7 @@ Module notations.
Notation "'λ:' e" := (Lam e%L) (at level 102) : lang_scope.
Notation "'rec::' e" := (Rec e%L) (at level 102) : 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, only parsing) : lang_scope.
(at level 200, e1, e2, e3 at level 200) : lang_scope.
End notations.
Section suger.
......@@ -63,35 +63,39 @@ Proof.
to talk to the Autosubst guys. *)
by asimpl.
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.
Proof.
rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v.
by rewrite -wp_lam //= to_of_val.
Qed.
Lemma wp_if_true E e1 e2 Q : wp E e1 Q wp E (If LitTrue e1 e2) Q.
Proof. rewrite -wp_case_inl //. by asimpl. Qed.
Lemma wp_if_false E e1 e2 Q : wp E e2 Q wp E (If LitFalse e1 e2) Q.
Proof. rewrite -wp_case_inr //. by asimpl. Qed.
Lemma wp_lt E n1 n2 P Q :
(n1 < n2 P Q LitTrueV)
(n1 n2 P Q LitFalseV)
P wp E (Lt (LitNat n1) (LitNat n2)) Q.
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 //; [].
destruct (decide _); by eauto with omega.
Qed.
Lemma wp_lt E (n1 n2 : nat) P Q :
(n1 < n2 P Q (LitV true))
(n1 n2 P Q (LitV false))
P wp E (BinOp LtOp (Lit n1) (Lit n2)) Q.
Proof.
intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=.
auto using wp_le with lia.
intros ? ?. rewrite -wp_bin_op //; [].
destruct (decide _); by eauto with omega.
Qed.
Lemma wp_eq E n1 n2 P Q :
(n1 = n2 P Q LitTrueV)
(n1 n2 P Q LitFalseV)
P wp E (Eq (LitNat n1) (LitNat n2)) Q.
Lemma wp_eq E (n1 n2 : nat) P Q :
(n1 = n2 P Q (LitV true))
(n1 n2 P Q (LitV false))
P wp E (BinOp EqOp (Lit n1) (Lit n2)) Q.
Proof.
intros HPeq HPne.
rewrite -wp_let -wp_value' // -later_intro; asimpl.
rewrite -wp_rec //; asimpl.
rewrite -(wp_bind [CaseCtx _ _]) -later_intro; asimpl.
apply wp_le; intros; asimpl.
* rewrite -wp_case_inl // -!later_intro. apply wp_le; auto with lia.
* rewrite -wp_case_inr // -later_intro -wp_value' //; auto with lia.
intros ? ?. rewrite -wp_bin_op //; [].
destruct (decide _); by eauto with omega.
Qed.
End suger.
......@@ -4,15 +4,14 @@ Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang uPred notations.
Module LangTests.
Definition add := (21 + 21)%L.
Goal σ, prim_step add σ 42 σ None.
Definition add := (Lit 21 + Lit 21)%L.
Goal σ, prim_step add σ (Lit 42) σ None.
Proof. intros; do_step done. Qed.
Definition rec : expr := rec:: #0 #1. (* fix f x => f x *)
Definition rec_app : expr := rec 0.
Definition rec_app : expr := (rec:: #0 #1) (Lit 0).
Goal σ, prim_step rec_app σ rec_app σ None.
Proof. Set Printing All. intros; do_step done. Qed.
Definition lam : expr := λ: #0 + 21.
Goal σ, prim_step (App lam (LitNat 21)) σ add σ None.
Definition lam : expr := λ: #0 + Lit 21.
Goal σ, prim_step (lam (Lit 21)) σ add σ None.
Proof. intros; do_step done. Qed.
End LangTests.
......@@ -22,8 +21,8 @@ Module LiftingTests.
Implicit Types Q : val iProp heap_lang Σ.
(* FIXME: Fix levels so that we do not need the parenthesis here. *)
Definition e : expr := let: ref 1 in #0 <- !#0 + 1; !#0.
Goal σ E, (ownP σ : iProp heap_lang Σ) (wp E e (λ v, (v = 2))).
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))).
Proof.
move=> σ E. rewrite /e.
rewrite -wp_let. rewrite -wp_alloc_pst; last done.
......@@ -35,11 +34,11 @@ Module LiftingTests.
all so nicely. *)
rewrite -(wp_bindi (SeqCtx (Load (Loc _)))).
rewrite -(wp_bindi (StoreRCtx (LocV _))).
rewrite -(wp_bindi (PlusLCtx _)).
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 -wp_plus -later_intro.
rewrite -wp_bin_op // -later_intro.
rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
{ by rewrite lookup_insert. }
{ done. }
......@@ -57,13 +56,13 @@ Module LiftingTests.
Definition FindPred' n1 Sn1 n2 f : expr :=
if Sn1 < n2 then f Sn1 else n1.
Definition FindPred n2 : expr :=
rec:: (let: #1 + 1 in FindPred' #2 #0 n2.[ren(+3)] #1)%L.
rec:: (let: #1 + Lit 1 in FindPred' #2 #0 n2.[ren(+3)] #1)%L.
Definition Pred : expr :=
λ: (if #0 0 then 0 else FindPred #0 0)%L.
λ: (if #0 Lit 0 then Lit 0 else FindPred #0 (Lit 0))%L.
Lemma FindPred_spec n1 n2 E Q :
((n1 < n2) Q (pred n2))
wp E (FindPred n2 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.
......@@ -72,42 +71,39 @@ Module LiftingTests.
{ apply and_mono; first done. by rewrite -later_intro. }
apply later_mono.
(* Go on. *)
rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2))).
rewrite -wp_plus. asimpl.
rewrite -(wp_bindi (CaseCtx _ _)).
rewrite -(wp_let _ _ (FindPred' (Lit n1) #0 (Lit n2) (FindPred (Lit n2)))).
rewrite -wp_bin_op //. asimpl.
rewrite -(wp_bindi (IfCtx _ _)).
rewrite -!later_intro /=.
apply wp_lt; intros Hn12.
* (* TODO RJ: It would be better if we could use wp_if_true here
(and below). But we cannot, because the substitutions in there
got already unfolded. *)
rewrite -wp_case_inl //.
* 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_case_inr //.
* 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.
Qed.
Lemma Pred_spec n E Q :
Q (pred n) wp E (Pred n) Q.
Q (LitV $ pred n) wp E (Pred $ Lit n) Q.
Proof.
rewrite -wp_lam //. asimpl.
rewrite -(wp_bindi (CaseCtx _ _)).
rewrite -(wp_bindi (IfCtx _ _)).
apply later_mono, wp_le=> Hn.
- rewrite -wp_case_inl //.
- rewrite -wp_if_true.
rewrite -!later_intro -wp_value' //.
by replace n with 0 by omega.
- rewrite -wp_case_inr //.
- 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 42 in Pred #0) (λ v, (v = 40)).
True wp (Σ:=Σ) E (let: Pred $ Lit 42 in Pred #0) (λ 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? *)
......
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