Commit e786f3dd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 2f67cbdc 0b645878
......@@ -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" := (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" := (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)
......@@ -65,35 +65,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,12 +56,12 @@ Module LiftingTests.
Definition FindPred' (n1 Sn1 n2 f : expr) : expr :=
if Sn1 < n2 then f Sn1 else n1.
Definition FindPred (n2 : expr) : expr :=
rec:: let: #1 + 1 in FindPred' #2 #0 n2.[ren(+3)] #1.
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.
λ: (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.
......@@ -70,45 +69,44 @@ Module LiftingTests.
etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
{ apply and_mono; first done. by rewrite -later_intro. }
apply later_mono.
(* "rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2)))" started to
(* Go on *)
(* FIXME "rewrite -(wp_let _ _ (FindPred' n1 #0 n2 (FindPred n2)))" started to
fail after we changed # n to use ids instead of Var *)
pose proof (wp_let (Σ:=Σ) E (n1 + 1)%L (FindPred' n1 #0 n2 (FindPred n2)) Q).
pose proof (wp_let (Σ:=Σ) E (Lit n1 + Lit 1)%L
(FindPred' (Lit n1) #0 (Lit n2) (FindPred (Lit n2))) Q).
unfold Let, Lam in H; rewrite -H.
rewrite -wp_plus. asimpl.
rewrite -(wp_bindi (CaseCtx _ _)).
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.