Commit b91562fe authored by Robbert Krebbers's avatar Robbert Krebbers

Put arguments of lifting lemmas in more consistent order.

parent 15058014
...@@ -126,7 +126,7 @@ Proof. ...@@ -126,7 +126,7 @@ Proof.
Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto. Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto.
by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->. by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
Qed. Qed.
Lemma wp_plus n1 n2 E Q : Lemma wp_plus E n1 n2 Q :
Q (LitNatV (n1 + n2)) wp E (Plus (LitNat n1) (LitNat n2)) Q. Q (LitNatV (n1 + n2)) wp E (Plus (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
rewrite -(wp_lift_pure_step E (λ e', e' = LitNat (n1 + n2))) //=; rewrite -(wp_lift_pure_step E (λ e', e' = LitNat (n1 + n2))) //=;
...@@ -134,7 +134,7 @@ Proof. ...@@ -134,7 +134,7 @@ Proof.
apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->. apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
Lemma wp_le_true n1 n2 E Q : Lemma wp_le_true E n1 n2 Q :
n1 n2 n1 n2
Q LitTrueV wp E (Le (LitNat n1) (LitNat n2)) Q. Q LitTrueV wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
...@@ -143,7 +143,7 @@ Proof. ...@@ -143,7 +143,7 @@ Proof.
apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->. apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
Lemma wp_le_false n1 n2 E Q : Lemma wp_le_false E n1 n2 Q :
n1 > n2 n1 > n2
Q LitFalseV wp E (Le (LitNat n1) (LitNat n2)) Q. Q LitFalseV wp E (Le (LitNat n1) (LitNat n2)) Q.
Proof. Proof.
...@@ -152,7 +152,7 @@ Proof. ...@@ -152,7 +152,7 @@ Proof.
apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->. apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
Lemma wp_fst e1 v1 e2 v2 E Q : Lemma wp_fst E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
Q v1 wp E (Fst (Pair e1 e2)) Q. Q v1 wp E (Fst (Pair e1 e2)) Q.
Proof. Proof.
...@@ -161,7 +161,7 @@ Proof. ...@@ -161,7 +161,7 @@ Proof.
apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->. apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
Lemma wp_snd e1 v1 e2 v2 E Q : Lemma wp_snd E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2 to_val e1 = Some v1 to_val e2 = Some v2
Q v2 wp E (Snd (Pair e1 e2)) Q. Q v2 wp E (Snd (Pair e1 e2)) Q.
Proof. Proof.
...@@ -170,7 +170,7 @@ Proof. ...@@ -170,7 +170,7 @@ Proof.
apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->. apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'. by rewrite -wp_value'.
Qed. Qed.
Lemma wp_case_inl e0 v0 e1 e2 E Q : Lemma wp_case_inl E e0 v0 e1 e2 Q :
to_val e0 = Some v0 to_val e0 = Some v0
wp E e1.[e0/] Q wp E (Case (InjL e0) e1 e2) Q. wp E e1.[e0/] Q wp E (Case (InjL e0) e1 e2) Q.
Proof. Proof.
...@@ -178,7 +178,7 @@ Proof. ...@@ -178,7 +178,7 @@ Proof.
(Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto. (Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto.
by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->. by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
Qed. Qed.
Lemma wp_case_inr e0 v0 e1 e2 E Q : Lemma wp_case_inr E e0 v0 e1 e2 Q :
to_val e0 = Some v0 to_val e0 = Some v0
wp E e2.[e0/] Q wp E (Case (InjR e0) e1 e2) Q. wp E e2.[e0/] Q wp E (Case (InjR e0) e1 e2) Q.
Proof. Proof.
...@@ -188,7 +188,7 @@ Proof. ...@@ -188,7 +188,7 @@ Proof.
Qed. Qed.
(** Some derived stateless axioms *) (** Some derived stateless axioms *)
Lemma wp_le n1 n2 E P Q : Lemma wp_le E n1 n2 P Q :
(n1 n2 P Q LitTrueV) (n1 n2 P Q LitTrueV)
(n1 > n2 P Q LitFalseV) (n1 > n2 P Q LitFalseV)
P wp E (Le (LitNat n1) (LitNat n2)) Q. P wp E (Le (LitNat n1) (LitNat n2)) Q.
......
...@@ -31,17 +31,17 @@ Proof. ...@@ -31,17 +31,17 @@ Proof.
to talk to the Autosubst guys. *) to talk to the Autosubst guys. *)
by asimpl. by asimpl.
Qed. Qed.
Lemma wp_let e1 e2 E Q : Lemma wp_let E e1 e2 Q :
wp E e1 (λ v, wp E (e2.[of_val v/]) Q) wp E (Let e1 e2) Q. wp E e1 (λ v, wp E (e2.[of_val v/]) Q) wp E (Let e1 e2) Q.
Proof. Proof.
rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v. rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v.
by rewrite -wp_lam //= to_of_val. by rewrite -wp_lam //= to_of_val.
Qed. Qed.
Lemma wp_if_true e1 e2 E Q : wp E e1 Q wp E (If LitTrue e1 e2) Q. 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. Proof. rewrite -wp_case_inl //. by asimpl. Qed.
Lemma wp_if_false e1 e2 E Q : wp E e2 Q wp E (If LitFalse e1 e2) Q. 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. Proof. rewrite -wp_case_inr //. by asimpl. Qed.
Lemma wp_lt n1 n2 E P Q : Lemma wp_lt E n1 n2 P Q :
(n1 < n2 P Q LitTrueV) (n1 < n2 P Q LitTrueV)
(n1 n2 P Q LitFalseV) (n1 n2 P Q LitFalseV)
P wp E (Lt (LitNat n1) (LitNat n2)) Q. P wp E (Lt (LitNat n1) (LitNat n2)) Q.
...@@ -49,7 +49,7 @@ Proof. ...@@ -49,7 +49,7 @@ Proof.
intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=. intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=.
auto using wp_le with lia. auto using wp_le with lia.
Qed. Qed.
Lemma wp_eq n1 n2 E P Q : Lemma wp_eq E n1 n2 P Q :
(n1 = n2 P Q LitTrueV) (n1 = n2 P Q LitTrueV)
(n1 n2 P Q LitFalseV) (n1 n2 P Q LitFalseV)
P wp E (Eq (LitNat n1) (LitNat n2)) Q. P wp E (Eq (LitNat n1) (LitNat n2)) Q.
......
...@@ -73,7 +73,7 @@ Module LiftingTests. ...@@ -73,7 +73,7 @@ Module LiftingTests.
{ apply and_mono; first done. by rewrite -later_intro. } { apply and_mono; first done. by rewrite -later_intro. }
apply later_mono. apply later_mono.
(* Go on. *) (* Go on. *)
rewrite -(wp_let _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))). rewrite -(wp_let _ _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
rewrite -wp_plus. asimpl. rewrite -wp_plus. asimpl.
rewrite -(wp_bind [CaseCtx _ _]). rewrite -(wp_bind [CaseCtx _ _]).
rewrite -!later_intro /=. rewrite -!later_intro /=.
......
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