Commit 6646e43c authored by Robbert Krebbers's avatar Robbert Krebbers

Notations for LitTrue and LitFalse.

parent eba4ac6e
......@@ -7,6 +7,8 @@ Definition loc := positive. (* Really, any countable type. *)
Inductive base_lit : Set :=
| LitNat (n : nat) | LitBool (b : bool) | LitUnit.
Notation LitTrue := (LitBool true).
Notation LitFalse := (LitBool false).
Inductive un_op : Set :=
| NegOp.
Inductive bin_op : Set :=
......@@ -177,9 +179,9 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
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 LitTrue) e1 e2) σ e1 σ None
| IfFalseS e1 e2 σ :
head_step (If (Lit (LitBool false)) e1 e2) σ e2 σ None
head_step (If (Lit LitFalse) 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
......@@ -206,11 +208,11 @@ 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 LitFalse) σ 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 LitTrue) (<[l:=v2]>σ) None.
(** Atomic expressions *)
Definition atomic (e: expr) : Prop :=
......
......@@ -56,23 +56,24 @@ 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 $ LitV $ LitBool false)) wp E (Cas (Loc l) e1 e2) Q.
(ownP σ (ownP σ - Q (LitV LitFalse))) wp E (Cas (Loc l) e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool false) σ None) ?right_id //;
last by intros; inv_step; eauto.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitFalse) σ 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 $ LitV $ LitBool true)) wp E (Cas (Loc l) e1 e2) Q.
(ownP σ (ownP (<[l:=v2]>σ) - Q (LitV LitTrue)))
wp E (Cas (Loc l) e1 e2) Q.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (LitV $ LitBool true) (<[l:=v2]>σ) None)
intros. rewrite -(wp_lift_atomic_det_step σ (LitV LitTrue) (<[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 = LitV $ LitUnit)).
wp (Σ:=Σ) coPset_all e (λ _, True) wp E (Fork e) (λ v, (v = LitV LitUnit)).
Proof.
rewrite -(wp_lift_pure_det_step (Fork e) (Lit LitUnit) (Some e)) //=;
last by intros; inv_step; eauto.
......@@ -107,15 +108,13 @@ Proof.
by rewrite -wp_value'.
Qed.
Lemma wp_if_true E e1 e2 Q :
wp E e1 Q wp E (If (Lit $ LitBool true) e1 e2) Q.
Lemma wp_if_true E e1 e2 Q : wp E e1 Q wp E (If (Lit LitTrue) e1 e2) Q.
Proof.
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.
Lemma wp_if_false E e1 e2 Q : wp E e2 Q wp E (If (Lit LitFalse) e1 e2) Q.
Proof.
rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
?right_id //; last by intros; inv_step; eauto.
......@@ -123,7 +122,7 @@ Qed.
Lemma wp_fst E e1 v1 e2 v2 Q :
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.
intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
last by intros; inv_step; eauto.
......
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