Commit 0f96e059 authored by Robbert Krebbers's avatar Robbert Krebbers

More clean up.

parent caa2e4e8
......@@ -9,47 +9,47 @@ Section lang_rules.
Ltac inv_step :=
repeat match goal with
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
| H : prim_step _ _ _ _ _ |- _ => destruct H; subst
| H : _ = fill ?K ?e |- _ =>
destruct K as [|[]];
simpl in H; first [subst e|discriminate H|injection H as H]
(* ensure that we make progress for each subgoal *)
| H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
apply values_head_stuck, (fill_not_val K) in H;
by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if e is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
| _ => progress simplify_map_eq/= (* simplify memory stuff *)
| H : to_val _ = Some _ |- _ => apply of_to_val in H
| H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
| H : prim_step _ _ _ _ _ |- _ => destruct H; subst
| H : _ = fill ?K ?e |- _ =>
destruct K as [|[]];
simpl in H; first [subst e|discriminate H|injection H as H]
(* ensure that we make progress for each subgoal *)
| H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
apply values_head_stuck, (fill_not_val K) in H;
by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
| H : head_step ?e _ _ _ _ |- _ =>
try (is_var e; fail 1); (* inversion yields many goals if e is a variable
and can thus better be avoided. *)
inversion H; subst; clear H
end.
Ltac reshape_val e tac :=
let rec go e :=
match e with
| of_val ?v => v
| Pair ?e1 ?e2 =>
let v1 := reshape_val e1 in let v2 := reshape_val e2 in constr:(PairV v1 v2)
| InjL ?e => let v := reshape_val e in constr:(InjLV v)
| InjR ?e => let v := reshape_val e in constr:(InjRV v)
end in let v := go e in first [tac v | fail 2].
match e with
| of_val ?v => v
| Pair ?e1 ?e2 =>
let v1 := reshape_val e1 in let v2 := reshape_val e2 in constr:(PairV v1 v2)
| InjL ?e => let v := reshape_val e in constr:(InjLV v)
| InjR ?e => let v := reshape_val e in constr:(InjRV v)
end in let v := go e in first [tac v | fail 2].
Ltac reshape_expr e tac :=
let rec go K e :=
match e with
| _ => tac (reverse K) e
| App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
| Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
| Fst ?e => go (FstCtx :: K) e
| Snd ?e => go (SndCtx :: K) e
| InjL ?e => go (InjLCtx :: K) e
| InjR ?e => go (InjRCtx :: K) e
| Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
end in go (@nil ectx_item) e.
match e with
| _ => tac (reverse K) e
| App ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (AppRCtx v1 :: K) e2)
| App ?e1 ?e2 => go (AppLCtx e2 :: K) e1
| Pair ?e1 ?e2 => reshape_val e1 ltac:(fun v1 => go (PairRCtx v1 :: K) e2)
| Pair ?e1 ?e2 => go (PairLCtx e2 :: K) e1
| Fst ?e => go (FstCtx :: K) e
| Snd ?e => go (SndCtx :: K) e
| InjL ?e => go (InjLCtx :: K) e
| InjR ?e => go (InjRCtx :: K) e
| Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
end in go (@nil ectx_item) e.
Ltac do_step tac :=
try match goal with |- language.reducible _ _ => eexists _, _, _ end;
......@@ -71,36 +71,35 @@ Section lang_rules.
(** Helper Lemmas for weakestpre. *)
Lemma wp_bind {E e} K Q :
wp E e (λ v, wp E (fill K (of_val v)) Q) wp E (fill K e) Q.
WP e @ E {{ v, WP fill K (# v) @ E {{ Q }} }} WP fill K e @ E {{ Q }}.
Proof. apply weakestpre.wp_bind. Qed.
Lemma wp_lam E e1 e2 v Q :
to_val e2 = Some v wp E e1.[e2 /] Q wp E (App (Lam e1) e2) Q.
to_val e2 = Some v
WP e1.[e2/] @ E {{ Q }} WP App (Lam e1) e2 @ E {{ Q }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (App _ _) e1.[of_val v /] None) //=; auto.
- by rewrite right_id.
Qed.
Lemma wp_TLam E e Q :
wp E e Q wp E (TApp (TLam e)) Q.
Lemma wp_TLam E e Q : WP e @ E {{ Q }} WP TApp (TLam e) @ E {{ Q }}.
Proof.
rewrite -(wp_lift_pure_det_step (TApp _) e None) //=; auto.
- by rewrite right_id.
Qed.
Lemma wp_Fold E e v Q :
to_val e = Some v
Q v wp E (Unfold (Fold e)) Q.
to_val e = Some v Q v WP Unfold (Fold e) @ E {{ Q }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Unfold _) (of_val v) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
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 Fst (Pair e1 e2) @ E {{ Q }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Fst (Pair _ _)) (of_val v1) None) //=; auto.
......@@ -109,7 +108,7 @@ Section lang_rules.
Lemma wp_snd E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2
Q v2 wp E (Snd (Pair e1 e2)) Q.
Q v2 WP Snd (Pair e1 e2) @ E {{ Q }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Snd (Pair _ _)) (of_val v2) None) //=; auto.
......@@ -118,7 +117,7 @@ Section lang_rules.
Lemma wp_case_inl E e0 v0 e1 e2 Q :
to_val e0 = Some v0
wp E e1.[e0/] Q wp E (Case (InjL e0) e1 e2) Q.
WP e1.[e0/] @ E {{ Q }} WP Case (InjL e0) e1 e2 @ E {{ Q }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjL _) _ _) (e1.[of_val v0/]) None) //=; auto.
......@@ -127,7 +126,7 @@ Section lang_rules.
Lemma wp_case_inr E e0 v0 e1 e2 Q :
to_val e0 = Some v0
wp E e2.[e0/] Q wp E (Case (InjR e0) e1 e2) Q.
WP e2.[e0/] @ E {{ Q }} WP Case (InjR e0) e1 e2 @ E {{ Q }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjR _) _ _) (e2.[of_val v0/]) None) //=; auto.
......
......@@ -13,7 +13,7 @@ Fixpoint interp (τ : type) (w : val) : iProp lang Σ :=
| TSum τ1 τ2 =>
( w1, w = InjLV w1 interp τ1 w1) ( w2, w = InjRV w2 interp τ2 w2)
| TArrow τ1 τ2 =>
v, interp τ1 v wp (App (of_val w) (of_val v)) (interp τ2)
v, interp τ1 v WP App (of_val w) (of_val v) {{ interp τ2 }}
end%I.
Global Instance interp_always_stable τ v : PersistentP (interp τ v).
......
......@@ -70,11 +70,11 @@ Section lang_rules.
(** Helper Lemmas for weakestpre. *)
Lemma wp_bind {E e} K Q :
wp E e (λ v, wp E (fill K (of_val v)) Q) wp E (fill K e) Q.
WP e @ E {{ v, WP fill K (of_val v) @ E {{ Q }} }} WP fill K e @ E {{ Q }}.
Proof. apply weakestpre.wp_bind. Qed.
Lemma wp_lam E e1 e2 v Q :
to_val e2 = Some v wp E e1.[e2 /] Q wp E (App (Lam e1) e2) Q.
to_val e2 = Some v WP e1.[e2 /] @ E {{ Q }} WP App (Lam e1) e2 @ E {{ Q }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (App _ _) e1.[of_val v /] None) //=; auto.
......@@ -83,7 +83,7 @@ Section lang_rules.
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 Fst (Pair e1 e2) @ E {{ Q }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Fst (Pair _ _)) (of_val v1) None) //=; auto.
......@@ -92,7 +92,7 @@ Section lang_rules.
Lemma wp_snd E e1 v1 e2 v2 Q :
to_val e1 = Some v1 to_val e2 = Some v2
Q v2 wp E (Snd (Pair e1 e2)) Q.
Q v2 WP Snd (Pair e1 e2) @ E {{ Q }}.
Proof.
intros <-%of_to_val <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Snd (Pair _ _)) (of_val v2) None) //=; auto.
......@@ -101,16 +101,16 @@ Section lang_rules.
Lemma wp_case_inl E e0 v0 e1 e2 Q :
to_val e0 = Some v0
wp E e1.[e0/] Q wp E (Case (InjL e0) e1 e2) Q.
WP e1.[e0/] @ E {{ Q }} WP Case (InjL e0) e1 e2 @ E {{ Q }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjL _) _ _) (e1.[of_val v0/]) None) //=; auto.
- rewrite right_id; auto using uPred.later_mono, wp_value'.
Qed.
Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Q :
to_val e0 = Some v0
wp E e2.[e0/] Q wp E (Case (InjR e0) e1 e2) Q.
WP e2.[e0/] @ E {{ Q }} WP Case (InjR e0) e1 e2 @ E {{ Q }}.
Proof.
intros <-%of_to_val.
rewrite -(wp_lift_pure_det_step (Case (InjR _) _ _) (e2.[of_val v0/]) None) //=; auto.
......
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