Commit f1ae6242 authored by Amin Timany's avatar Amin Timany

Squashed commit of the following:

commit 392b7b43
Author: Amin Timany <amintimany@gmail.com>
Date:   Tue May 3 21:25:10 2016 +0200

    Finish using new iris with "proof mode"

    In Fμ and Fμ_ref we do support reduction under Fold.
    In fact `Unfold (Fold v)` is reduced to `v` if and only if v is a variable.

commit 9825e341
Author: Amin Timany <amintimany@gmail.com>
Date:   Mon May 2 20:35:57 2016 +0200

    Prove fundamental lemma of stlc is proven

    Change the Fμ to make the operational semantics reduce under Fold.
    Fundamental lemma for Fμ is partially proven (up to App).
parent a0f07fe1
This diff is collapsed.
......@@ -36,7 +36,7 @@ Module lang.
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
| FoldV (e : expr).
| FoldV (v : val).
Fixpoint of_val (v : val) : expr :=
match v with
......@@ -46,7 +46,7 @@ Module lang.
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
| FoldV e => Fold e
| FoldV v => Fold (of_val v)
end.
Fixpoint to_val (e : expr) : option val :=
match e with
......@@ -56,7 +56,7 @@ Module lang.
| 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
| Fold e => Some (FoldV e)
| Fold e => v to_val e; Some (FoldV v)
| _ => None
end.
......@@ -72,6 +72,7 @@ Module lang.
| InjLCtx
| InjRCtx
| CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
| FoldCtx
| UnfoldCtx.
Notation ectx := (list ectx_item).
......@@ -88,6 +89,7 @@ Module lang.
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| FoldCtx => Fold e
| UnfoldCtx => Unfold e
end.
Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
......@@ -114,14 +116,15 @@ Module lang.
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
(* Recursive Types *)
| Unfold_Fold e σ :
| Unfold_Fold e v σ :
to_val e = Some v
head_step (Unfold (Fold e)) σ e σ None
(* Polymorphic Types *)
| TBeta e σ :
head_step (TApp (TLam e)) σ e σ None.
(** Atomic expressions: we don't consider any atomic operations. *)
Definition atomic (e: expr) := False.
Definition atomic (e: expr) := false.
(** Close reduction under evaluation contexts.
We could potentially make this a generic construction. *)
......@@ -247,4 +250,4 @@ Global Instance lang_ctx_item Ki :
LanguageCtx lang (lang.fill_item Ki).
Proof. change (LanguageCtx lang (lang.fill [Ki])). by apply _. Qed.
Export lang.
\ No newline at end of file
Export lang.
......@@ -17,11 +17,10 @@ Section logrel.
Class Val_to_IProp_AlwaysStable (f : leibniz_val -n> iProp lang Σ) :=
val_to_iprop_always_stable : v : val, Persistent ((cofe_mor_car _ _ f) v).
val_to_iprop_always_stable : v : val, PersistentP ((cofe_mor_car _ _ f) v).
Arguments val_to_iprop_always_stable /.
Definition interp_unit : leibniz_val -n> iProp lang Σ :=
{|
cofe_mor_car := λ w, (w = UnitV)%I
......@@ -124,22 +123,22 @@ Section logrel.
(rec_apr : (leibniz_val -n> iProp lang Σ))
: (leibniz_val -n> iProp lang Σ) :=
{|
cofe_mor_car := λ w, ( ( e, w = FoldV e WP e @ {{ λ v, τi rec_apr v}}))%I
cofe_mor_car := λ w, ( ( v, w = FoldV v (τi rec_apr v)))%I
|}.
Global Instance interp_rec_pre_proper : Proper (() ==> () ==> ()) interp_rec_pre.
Proof.
intros τ1 τ1' H1 τ2 τ2' H2 w.
apply always_proper; apply exist_proper=>e; apply and_proper; trivial.
apply later_proper, wp_proper=>v.
apply always_proper, exist_proper=>e; apply and_proper; trivial.
apply later_proper.
rewrite H1 H2; trivial.
Qed.
Global Instance interp_rec_pre_ne n : Proper (dist n ==> dist n ==> dist n) interp_rec_pre.
Proof.
intros τ1 τ1' H1 τ2 τ2' H2 w.
apply always_ne; apply exist_ne=>e; apply and_ne; trivial.
apply (contractive_ne _), wp_ne=>v.
apply always_ne, exist_ne=>e; apply and_ne; trivial.
apply (contractive_ne _).
rewrite H1 H2; trivial.
Qed.
......@@ -149,9 +148,9 @@ Section logrel.
Contractive (interp_rec_pre τi).
Proof.
intros n f g H w; cbn.
apply always_ne;apply exist_ne; intros e; apply and_ne; trivial.
apply always_ne, exist_ne; intros e; apply and_ne; trivial.
apply later_contractive =>i Hi.
apply wp_ne; intros v; rewrite H; trivial.
rewrite H; trivial.
Qed.
Definition interp_rec (τi : (leibniz_val -n> iProp lang Σ) -n> (leibniz_val -n> iProp lang Σ))
......@@ -242,12 +241,21 @@ Section logrel.
let H := fresh "H" in intros H; inversion H; congruence
end.
Qed.
Lemma interp_closed_irrel_turnstile
(k : nat) (τ : type) (HC HC': closed_type k τ)
(Δ : Vlist (leibniz_val -n> iProp lang Σ) k)
(v : val)
: interp k τ HC Δ v interp k τ HC' Δ v.
Proof.
rewrite interp_closed_irrel; trivial.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl k Δ τ e w ws :
typed k Δ e τ -> length Δ = S (length ws)
typed k Δ e τ -> List.length Δ = S (List.length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)]
.
Proof.
......@@ -264,7 +272,7 @@ Section logrel.
(f : leibniz_val -n> iProp lang Σ)
{Hf : Val_to_IProp_AlwaysStable f}
(v : val)
: Persistent (f v).
: PersistentP (f v).
Proof. apply Hf. Qed.
Global Instance interp_always_stable
......@@ -272,20 +280,21 @@ Section logrel.
{HΔ : VlistAlwaysStable Δ}
: Val_to_IProp_AlwaysStable (interp k τ H Δ).
Proof.
induction τ; cbn; intros v; try apply _.
- rewrite /interp_rec /Persistent fixpoint_unfold /interp_rec_pre.
apply always_intro'; trivial.
- apply (@force_lookup_Forall
_ _
(λ f : leibniz_val -n> iProp lang Σ, Persistent (f v))).
apply Forall_forall => f H1.
eapply Forall_forall in HΔ; [apply HΔ|trivial].
revert k H Δ HΔ.
induction τ; cbn; intros k H Δ HΔ v; try apply _.
- rewrite /PersistentP /interp_rec fixpoint_unfold /interp_rec_pre; cbn.
apply always_intro'; trivial.
- apply (@force_lookup_Forall
_ _
(λ f : leibniz_val -n> iProp lang Σ, PersistentP (f v))).
apply Forall_forall => f H1.
eapply Forall_forall in HΔ; [apply HΔ|trivial].
Qed.
Global Instance alwyas_stable_Δ k Δ Γ vs
(Hctx : closed_ctx k Γ)
{HΔ : VlistAlwaysStable Δ}
: Persistent (Π∧ zip_with (λ τ v, interp k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I.
: PersistentP (Π∧ zip_with (λ τ v, interp k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I.
Proof. typeclasses eauto. Qed.
Global Instance alwyas_stable_Vlist_cons k f Δ
......@@ -318,6 +327,25 @@ Section logrel.
- apply IHΓ.
Qed.
Lemma type_context_closed_irrel_turnstile
(k : nat) (Δ : Vlist (leibniz_val -n> iProp lang Σ) k) (Γ : list type)
(vs : list leibniz_val)
(Hctx Hctx' : closed_ctx k Γ) :
(Π∧ zip_with
(λ (τ : {τ : type | closed_type k τ}) (v0 : leibniz_val),
((interp k (` τ) (proj2_sig τ)) Δ) v0)
(closed_ctx_list k Γ Hctx)
vs)%I
(Π∧ zip_with
(λ (τ : {τ : type | closed_type k τ}) (v : leibniz_val),
((interp k (` τ) (proj2_sig τ)) Δ) v)
(closed_ctx_list k Γ Hctx')
vs)%I.
Proof.
rewrite type_context_closed_irrel; trivial.
Qed.
Local Ltac ipropsimpl :=
repeat
match goal with
......@@ -514,4 +542,4 @@ Section logrel.
- apply IHΓ.
Qed.
End logrel.
\ No newline at end of file
End logrel.
......@@ -94,11 +94,13 @@ Section lang_rules.
- by rewrite right_id.
Qed.
Lemma wp_Fold E e Q :
wp E e Q wp E (Unfold (Fold e)) Q.
Lemma wp_Fold E e v Q :
to_val e = Some v
Q v wp E (Unfold (Fold e)) Q.
Proof.
rewrite -(wp_lift_pure_det_step (Unfold _) e None) //=; auto.
- by rewrite right_id.
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 :
......
......@@ -334,4 +334,14 @@ Proof.
(s1 s2 : nat A) x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega typed_subst_invariant.
Qed.
Lemma closed_ctx_map_S_back (k : nat) (Γ : list type) (e : expr) (τ : type) :
closed_ctx k Γ
closed_ctx (S k) (map (λ t : type, t.[ren (+1)]) Γ).
Proof.
intros H.
eapply closed_ctx_map; [eassumption|].
clear; intros τ' H'.
set (HW := closed_type_S_ren2 τ' 1 0); cbn in HW; apply HW; trivial.
Qed.
\ No newline at end of file
This diff is collapsed.
......@@ -53,7 +53,7 @@ Module lang.
| PairV (v1 v2 : val)
| InjLV (v : val)
| InjRV (v : val)
| FoldV (e : expr)
| FoldV (v : val)
| LocV (l : loc).
Global Instance val_dec_eq (v v' : val) : Decision (v = v').
......@@ -72,7 +72,7 @@ Module lang.
| PairV v1 v2 => Pair (of_val v1) (of_val v2)
| InjLV v => InjL (of_val v)
| InjRV v => InjR (of_val v)
| FoldV e => Fold e
| FoldV v => Fold (of_val v)
| LocV l => Loc l
end.
......@@ -84,7 +84,7 @@ Module lang.
| 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
| Fold e => Some (FoldV e)
| Fold e => v to_val e; Some (FoldV v)
| Loc l => Some (LocV l)
| _ => None
end.
......@@ -101,6 +101,7 @@ Module lang.
| InjLCtx
| InjRCtx
| CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
| FoldCtx
| UnfoldCtx
| AllocCtx
| LoadCtx
......@@ -121,6 +122,7 @@ Module lang.
| InjLCtx => InjL e
| InjRCtx => InjR e
| CaseCtx e1 e2 => Case e e1 e2
| FoldCtx => Fold e
| UnfoldCtx => Unfold e
| AllocCtx => Alloc e
| LoadCtx => Load e
......@@ -152,7 +154,8 @@ Module lang.
to_val e0 = Some v0
head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
(* Recursive Types *)
| Unfold_Fold e σ :
| Unfold_Fold e v σ :
to_val e = Some v
head_step (Unfold (Fold e)) σ e σ None
(* Polymorphic Types *)
| TBeta e σ :
......@@ -171,10 +174,13 @@ Module lang.
(** Atomic expressions: we don't consider any atomic operations. *)
Definition atomic (e: expr) :=
match e with
| Alloc e => is_Some (to_val e)
| Load e => is_Some (to_val e)
| Store e1 e2 => is_Some (to_val e1) is_Some (to_val e2)
| _ => False
| Alloc e => match (to_val e) with | Some _ => true | None => false end
| Load e => match (to_val e) with | Some _ => true | None => false end
| Store e1 e2 =>
andb
match (to_val e1) with | Some _ => true | None => false end
match (to_val e2) with | Some _ => true | None => false end
| _ => false
end.
(** Close reduction under evaluation contexts.
......@@ -226,7 +232,7 @@ We could potentially make this a generic construction. *)
Proof. destruct e; cbn; intuition auto. Qed.
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) is_Some (to_val e).
Proof. destruct Ki; cbn; intuition. Qed.
Proof. destruct Ki; cbn; repeat destruct (to_val _); cbn; intuition eauto. Qed.
Lemma atomic_fill K e : atomic (fill K e) to_val e = None K = [].
Proof.
......@@ -240,8 +246,9 @@ We could potentially make this a generic construction. *)
atomic e1 head_step e1 σ1 e2 σ2 ef is_Some (to_val e2).
Proof.
intros H1 H2.
destruct e1; inversion H1; inversion H2; subst;
try rewrite to_of_val; eauto using mk_is_Some.
destruct e1; cbn in *; inversion H2;
try destruct (to_val e1); cbn in *; try inversion H1;
eauto 2 using to_of_val.
Qed.
Lemma atomic_step e1 σ1 e2 σ2 ef :
......
......@@ -18,7 +18,7 @@ Section logrel.
Canonical Structure leibniz_val := leibnizC val.
Class Val_to_IProp_AlwaysStable (f : leibniz_val -n> iPropG lang Σ) :=
val_to_iprop_always_stable : v : val, Persistent ((cofe_mor_car _ _ f) v).
val_to_iprop_always_stable : v : val, PersistentP ((cofe_mor_car _ _ f) v).
Arguments val_to_iprop_always_stable /.
......@@ -124,14 +124,14 @@ Section logrel.
(rec_apr : (leibniz_val -n> iPropG lang Σ))
: (leibniz_val -n> iPropG lang Σ) :=
{|
cofe_mor_car := λ w, ( ( e, w = FoldV e WP e @ {{ λ v, τi rec_apr v}}))%I
cofe_mor_car := λ w, ( ( v, w = FoldV v τi rec_apr v))%I
|}.
Global Instance interp_rec_pre_proper : Proper (() ==> () ==> ()) interp_rec_pre.
Proof.
intros τ1 τ1' H1 τ2 τ2' H2 w.
apply always_proper; apply exist_proper=>e; apply and_proper; trivial.
apply later_proper, wp_proper=>v.
apply later_proper.
rewrite H1 H2; trivial.
Qed.
......@@ -139,7 +139,7 @@ Section logrel.
Proof.
intros τ1 τ1' H1 τ2 τ2' H2 w.
apply always_ne; apply exist_ne=>e; apply and_ne; trivial.
apply (contractive_ne _); apply wp_ne=>v.
apply (contractive_ne _).
rewrite H1 H2; trivial.
Qed.
......@@ -151,7 +151,7 @@ Section logrel.
intros n f g H w; cbn.
apply always_ne;apply exist_ne; intros e; apply and_ne; trivial.
apply later_contractive =>i Hi.
apply wp_ne; intros v; rewrite H; trivial.
rewrite H; trivial.
Qed.
Definition interp_rec (τi : (leibniz_val -n> iPropG lang Σ) -n> (leibniz_val -n> iPropG lang Σ))
......@@ -295,12 +295,21 @@ Section logrel.
let H := fresh "H" in intros H; inversion H; congruence
end.
Qed.
Lemma interp_closed_irrel_turnstile
(k : nat) (τ : type) (HC HC': closed_type k τ)
(Δ : Vlist (leibniz_val -n> iPropG lang Σ) k)
(v : val)
: interp k τ HC Δ v interp k τ HC' Δ v.
Proof.
rewrite interp_closed_irrel; trivial.
Qed.
Definition env_subst (vs : list val) (x : var) : expr :=
from_option (Var x) (of_val <$> vs !! x).
Lemma typed_subst_head_simpl k Δ τ e w ws :
typed k Δ e τ -> length Δ = S (length ws)
typed k Δ e τ -> List.length Δ = S (List.length ws)
e.[# w .: env_subst ws] = e.[env_subst (w :: ws)]
.
Proof.
......@@ -317,7 +326,7 @@ Section logrel.
(f : leibniz_val -n> iPropG lang Σ)
{Hf : Val_to_IProp_AlwaysStable f}
(v : val)
: Persistent (f v).
: PersistentP (f v).
Proof. apply Hf. Qed.
Global Instance interp_always_stable
......@@ -326,11 +335,11 @@ Section logrel.
: Val_to_IProp_AlwaysStable (interp k τ H Δ).
Proof.
induction τ; cbn; intros v; try apply _.
- rewrite /interp_rec /Persistent fixpoint_unfold /interp_rec_pre.
- rewrite /interp_rec /PersistentP fixpoint_unfold /interp_rec_pre.
apply always_intro'; trivial.
- apply (@force_lookup_Forall
_ _
(λ f : leibniz_val -n> iPropG lang Σ, Persistent (f v))).
(λ f : leibniz_val -n> iPropG lang Σ, PersistentP (f v))).
apply Forall_forall => f H1.
eapply Forall_forall in HΔ; [apply HΔ|trivial].
Qed.
......@@ -338,7 +347,7 @@ Section logrel.
Global Instance alwyas_stable_Δ k Δ Γ vs
(Hctx : closed_ctx k Γ)
{HΔ : VlistAlwaysStable Δ}
: Persistent (Π∧ zip_with (λ τ v, interp k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I.
: PersistentP (Π∧ zip_with (λ τ v, interp k (` τ) (proj2_sig τ) Δ v) (closed_ctx_list _ Γ Hctx) vs)%I.
Proof. typeclasses eauto. Qed.
Global Instance alwyas_stable_Vlist_cons k f Δ
......@@ -369,7 +378,26 @@ Section logrel.
apply and_proper.
- apply interp_closed_irrel.
- apply IHΓ.
Qed.
Qed.
Lemma type_context_closed_irrel_turnstile
(k : nat) (Δ : Vlist (leibniz_val -n> iPropG lang Σ) k) (Γ : list type)
(vs : list leibniz_val)
(Hctx Hctx' : closed_ctx k Γ) :
(Π∧ zip_with
(λ (τ : {τ : type | closed_type k τ}) (v0 : leibniz_val),
((interp k (` τ) (proj2_sig τ)) Δ) v0)
(closed_ctx_list k Γ Hctx)
vs)%I
(Π∧ zip_with
(λ (τ : {τ : type | closed_type k τ}) (v : leibniz_val),
((interp k (` τ) (proj2_sig τ)) Δ) v)
(closed_ctx_list k Γ Hctx')
vs)%I.
Proof.
rewrite type_context_closed_irrel; trivial.
Qed.
Local Ltac ipropsimpl :=
repeat
......
......@@ -8,7 +8,7 @@ From iris.program_logic Require Import ownership auth.
Import uPred.
Section lang_rules.
Definition heapR : cmraT := mapR loc (fracR (dec_agreeR val)).
Definition heapR : cmraT := gmapR loc (fracR (dec_agreeR val)).
(** The CMRA we need. *)
Class heapG Σ :=
......@@ -35,7 +35,7 @@ Section lang_rules.
Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
Proof. solve_proper. Qed.
Global Instance heap_ctx_always_stable N : Persistent (heap_ctx N).
Global Instance heap_ctx_always_stable N : PersistentP (heap_ctx N).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque heap_ctx heap_mapsto.
......@@ -186,7 +186,7 @@ Section lang_rules.
induction σ as [|l v σ Hl IH] using map_ind.
{ rewrite big_sepM_empty; apply True_intro. }
rewrite to_heap_insert big_sepM_insert //.
rewrite (map_insert_singleton_op (to_heap σ));
rewrite (insert_singleton_op (to_heap σ));
last rewrite lookup_fmap Hl; auto.
(* FIXME: investigate why we have to unfold auth_own here. *)
by rewrite auth_own_op IH.
......@@ -197,16 +197,16 @@ Section lang_rules.
(** General properties of mapsto *)
Lemma heap_mapsto_op_eq l q1 q2 v :
(l {q1} v l {q2} v)%I (l {q1+q2} v)%I.
Proof. by rewrite -auth_own_op map_op_singleton Frac_op dec_agree_idemp. Qed.
Proof. by rewrite -auth_own_op op_singleton Frac_op dec_agree_idemp. Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 :
(l {q1} v1 l {q2} v2)%I (v1 = v2 l {q1+q2} v1)%I.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq const_equiv // left_id. }
rewrite -auth_own_op map_op_singleton Frac_op dec_agree_ne //.
rewrite -auth_own_op op_singleton Frac_op dec_agree_ne //.
apply (anti_symm ()); last by apply const_elim_l.
rewrite auth_own_valid map_validI (forall_elim l) lookup_singleton.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
Qed.
......@@ -231,7 +231,7 @@ Section lang_rules.
cbn; rewrite to_of_val.
apply const_elim_l=>-[l [-> [-Heq [-> ?]]]]; inversion Heq; subst.
by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
cbn; eauto.
cbn; rewrite H; eauto.
Qed.
Lemma wp_load_pst E σ l v Φ :
......@@ -250,6 +250,7 @@ Section lang_rules.
Proof.
intros. rewrite -(wp_lift_atomic_det_step σ (UnitV) (<[l:=v]>σ) None)
?right_id //; cbn; eauto.
rewrite H; auto.
by intros; inv_step; eauto.
Qed.
......@@ -260,11 +261,11 @@ Section lang_rules.
P ( l, l v - Φ (LocV l))
P WP Alloc e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ??? HP.
rewrite /heap_ctx /heap_inv=> H ?? HP.
trans (|={E}=> auth_own heap_name P)%I.
{ by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I.
with N heap_name ; simpl; eauto with I; [rewrite H; auto|].
rewrite -later_intro. apply sep_mono_r,forall_intro=> h; apply wand_intro_l.
rewrite -assoc left_id; apply const_elim_sep_l=> ?.
rewrite -(wp_alloc_pst _ (of_heap h)) //.
......@@ -275,8 +276,8 @@ Section lang_rules.
repeat erewrite <-exist_intro by apply _; simpl.
rewrite -of_heap_insert left_id right_id.
rewrite /heap_mapsto. ecancel [_ - Φ _]%I.
rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
rewrite const_equiv; last by apply (map_insert_valid h).
rewrite -(insert_singleton_op h); last by apply of_heap_None.
rewrite const_equiv; last by apply (insert_valid h).
by rewrite left_id -later_intro.
Qed.
......@@ -302,9 +303,10 @@ Section lang_rules.
P ( l v' (l v - Φ UnitV))
P WP Store (Loc l) e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv=> ??? HPΦ.
rewrite /heap_ctx /heap_inv=> H ?? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I;
[rewrite H; auto|].
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> ?.
rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
......@@ -332,11 +334,13 @@ Section lang_rules.
- intros. inv_step; auto.
Qed.
Lemma wp_Fold E e Φ :
WP e @ E {{Φ}} WP (Unfold (Fold e)) @ E {{Φ}}.
Lemma wp_Fold E e v Φ :
to_val e = Some v
Φ v WP (Unfold (Fold e)) @ E {{Φ}}.
Proof.
rewrite -(wp_lift_pure_det_step (Unfold _) e None) //=.
- by rewrite right_id.
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'.
- intros. inv_step; auto.
Qed.
......
......@@ -345,4 +345,14 @@ Proof.
(s1 s2 : nat A) x, (x 0 s1 (pred x) = s2 (pred x)) up s1 x = up s2 x).
{ intros A H1 H2. rewrite /up=> s1 s2 [|x] //=; auto with f_equal omega. }
induction Htyped => s1 s2 Hs; f_equal/=; eauto using lookup_lt_Some with omega typed_subst_invariant.
Qed.
Lemma closed_ctx_map_S_back (k : nat) (Γ : list type) (e : expr) (τ : type) :
closed_ctx k Γ
closed_ctx (S k) (map (λ t : type, t.[ren (+1)]) Γ).
Proof.
intros H.
eapply closed_ctx_map; [eassumption|].
clear; intros τ' H'.
set (HW := closed_type_S_ren2 τ' 1 0); cbn in HW; apply HW; trivial.
Qed.
\ No newline at end of file
......@@ -334,7 +334,7 @@ Next Obligation.
Proof. repeat intros ?; constructor; trivial. Qed.
Next Obligation.
Proof.
repeat intros?; constructor; trivial; apply Forall2_Forall, Forall_forall; trivial.
repeat intros?; constructor; trivial. apply Forall_Forall2, Forall_forall; trivial.
Qed.
Program Definition Vlist_cons_apply {A : cofeT} {k}
......@@ -367,4 +367,4 @@ Proof.
cbn -[Vlist_cons_morph].
apply cofe_mor_car_ne; trivial.
rewrite H1; trivial.
Qed.
\ No newline at end of file
Qed.
Require Export iris.proofmode.tactics.
From iris.program_logic Require Import wsat.
Require Import iris.program_logic.weakestpre.
Require Import iris.program_logic.language.
From mathcomp Require Export ssreflect.
From iris.prelude Require Export prelude.
Global Set Bullet Behavior "Strict Subproofs".
Global Open Scope general_if_scope.
Ltac done := prelude.tactics.done.
\ No newline at end of file
Ltac done := prelude.tactics.done.
Section uPred_Lemmas.