Commit 4bbf89ee authored by Dan Frumin's avatar Dan Frumin

Update the code for Coq 8.6.1

parent f638d4f9
......@@ -58,7 +58,7 @@ Section masked.
iModIntro. value_case'; eauto.
Qed.
Lemma bin_log_related_unit Δ Γ : {E,E;Δ;Γ} Unit log Unit : TUnit.
Lemma bin_log_related_unit Δ Γ : {E,E;Δ;Γ} tt log tt : TUnit.
Proof.
value_case.
Qed.
......
......@@ -51,7 +51,7 @@ Section hax.
Qed.
Lemma weird_bind e Q :
WP App e () {{ Q }} WP e {{ v, WP (App v ()) {{ Q }} }}.
WP App e tt {{ Q }} WP e {{ v, WP (App v tt) {{ Q }} }}.
Proof.
(* ugh, turns out this is just the inverse bind:
Check (wp_bind_inv (fun v => App v #())). *)
......@@ -73,16 +73,16 @@ Section hax.
iSplitR; eauto.
iNext.
iIntros (e2 σ2 efs) "Hpst". iDestruct "Hpst" as %Hpst.
iSpecialize ("wp" $! (App e2 ()) σ2 efs).
iAssert (prim_step (e (Lit Unit))%E σ1 (e2 (Lit Unit)%E) σ2 efs)%I as "Hprim'".
iSpecialize ("wp" $! (App e2 tt) σ2 efs).
iAssert (prim_step (e (Lit tt))%E σ1 (e2 (Lit tt)%E) σ2 efs)%I as "Hprim'".
{ iPureIntro.
inversion Hpst; simpl in *; subst; clear Hpst.
eapply (Ectx_step _ σ1 _ σ2 efs (K++[AppLCtx (())%E])); simpl; eauto.
eapply (Ectx_step _ σ1 _ σ2 efs (K++[AppLCtx (Lit tt)%E])); simpl; eauto.
by rewrite fill_app.
by rewrite fill_app. }
iMod ("wp" with "Hprim'") as "[$ [wp $]]". iModIntro.
by iApply "IH".
Admitted.
Abort.
(* Lemma wp_step_back Γ (e t : expr) (x : string) (v ev : val) τ : *)
(* Closed (Lam x e) *)
......
......@@ -57,7 +57,7 @@ Section logrel.
Solve Obligations with solve_proper.
Program Definition interp_unit : listC D -n> D := λne Δ ww,
(ww.1 = LitV Unit ww.2 = LitV Unit)%I.
(ww.1 = LitV tt ww.2 = LitV tt)%I.
Solve Obligations with solve_proper_alt.
Program Definition interp_nat : listC D -n> D := λne Δ ww,
......
......@@ -19,7 +19,7 @@ Section logrel.
from_option id (cconst True)%I (Δ !! x).
Solve Obligations with solve_proper_alt.
Definition interp_unit : listC D -n> D := λne Δ w, w = UnitV%I.
Definition interp_unit : listC D -n> D := λne Δ w, w = ttV%I.
Definition interp_nat : listC D -n> D := λne Δ w, ⌜∃ n, w = #nv n%I.
Definition interp_bool : listC D -n> D := λne Δ w, ⌜∃ n, w = #v n%I.
......
......@@ -11,9 +11,8 @@ Coercion of_val : val >-> expr.
Coercion Nat : nat >-> Literal.
Coercion Bool : bool >-> Literal.
Definition litunit : unit -> Literal := fun _ => Unit.
Coercion litunit : unit >-> Literal.
Notation "'tt'" := lang.Unit.
Coercion litunit (z : ()) : Literal := Unit.
Coercion Lit : Literal >-> expr.
Coercion BNamed : string >-> binder.
......@@ -25,7 +24,7 @@ Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV x e := (RecV BAnon x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq Unit Unit).
Notation Skip := (Seq tt tt).
(* No scope for the values, does not conflict and scope is often not inferred
properly. *)
......
......@@ -400,7 +400,7 @@ Section properties.
Lemma bin_log_related_fork_l Δ Γ E1 E2 K (e t : expr) (τ : type)
(Hclosed : Closed e) :
(|={E1,E2}=> (WP e {{ _, True }})
{E2,E1;Δ;Γ} fill K (Lit Unit) log t : τ) -
{E2,E1;Δ;Γ} fill K (Lit tt) log t : τ) -
{E1,E1;Δ;Γ} fill K (Fork e) log t : τ.
Proof.
iIntros "Hlog".
......@@ -457,7 +457,7 @@ Section properties.
Lemma bin_log_related_store_l Δ Γ E1 E2 K l e v' t τ :
(to_val e = Some v')
(|={E1,E2}=> v, (l ↦ᵢ v)
(l ↦ᵢ v' - {E2,E1;Δ;Γ} fill K (Lit Unit) log t : τ))
(l ↦ᵢ v' - {E2,E1;Δ;Γ} fill K (Lit tt) log t : τ))
- {E1,E1;Δ;Γ} fill K (Store (Loc l) e) log t : τ.
Proof.
iIntros (?) "Hlog".
......@@ -469,7 +469,7 @@ Section properties.
Lemma bin_log_related_store_l' Δ Γ E K l e v v' t τ :
(to_val e = Some v')
(l ↦ᵢ v) -
(l ↦ᵢ v' - {E,E;Δ;Γ} fill K (Lit Unit) log t : τ)
(l ↦ᵢ v' - {E,E;Δ;Γ} fill K (Lit tt) log t : τ)
- {E,E;Δ;Γ} fill K (Store (Loc l) e) log t : τ.
Proof.
iIntros (?) "Hl Hlog".
......@@ -731,7 +731,7 @@ Section properties.
(Hmasked : nclose specN E1)
(Hclosed : Closed e) :
( i, i e -
{E1,E2;Δ;Γ} t log fill K (Lit Unit) : τ) -
{E1,E2;Δ;Γ} t log fill K (Lit tt) : τ) -
{E1,E2;Δ;Γ} t log fill K (Fork e) : τ.
Proof.
iIntros "Hlog".
......@@ -785,7 +785,7 @@ Section properties.
(Hmasked : nclose specN E1) :
(to_val e = Some v')
l ↦ₛ v -
(l ↦ₛ v' - {E1,E2;Δ;Γ} t log fill K (Lit Unit) : τ)
(l ↦ₛ v' - {E1,E2;Δ;Γ} t log fill K (Lit tt) : τ)
- {E1,E2;Δ;Γ} t log fill K (Store (Loc l) e) : τ.
Proof.
iIntros (?) "Hl Hlog".
......
......@@ -62,7 +62,7 @@ Section lang_rules.
Lemma wp_store E l v' e v :
to_val e = Some v
{{{ l ↦ᵢ v' }}} Store (Loc l) e @ E
{{{ RET (LitV ()); l ↦ᵢ v }}}.
{{{ RET (LitV tt); l ↦ᵢ v }}}.
Proof.
iIntros (<-%of_to_val Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
......@@ -175,10 +175,10 @@ Section lang_rules.
Qed.
Lemma wp_fork E e Φ :
(|={E}=> Φ (LitV ())) WP e {{ _, True }} WP Fork e @ E {{ Φ }}.
(|={E}=> Φ (LitV tt)) WP e {{ _, True }} WP Fork e @ E {{ Φ }}.
Proof.
rewrite -(wp_lift_pure_det_head_step (Fork e) Unit [e]) //=; eauto.
- rewrite -(wp_value_fupd _ _ (Lit Unit)); auto.
rewrite -(wp_lift_pure_det_head_step (Fork e) tt [e]) //=; eauto.
- rewrite -(wp_value_fupd _ _ (Lit tt)); auto.
by rewrite -step_fupd_intro // right_id later_sep.
- intros; inv_head_step; eauto.
Qed.
......
......@@ -214,7 +214,7 @@ Section cfg.
Lemma step_store E ρ j K l v' e v:
to_val e = Some v nclose specN E
spec_ctx ρ j fill K (Store (Loc l) e) l ↦ₛ v'
={E}= j (fill K (Lit ())%E) l ↦ₛ v.
={E}= j (fill K (Lit tt)%E) l ↦ₛ v.
Proof.
iIntros (??) "(#Hinv & Hj & Hl)".
rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
......@@ -225,13 +225,13 @@ Section cfg.
as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1, singleton_local_update,
(exclusive_local_update _ (Excl (fill K (Lit ())%E))). }
(exclusive_local_update _ (Excl (fill K (Lit tt)%E))). }
iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
{ eapply auth_update, prod_local_update_2, singleton_local_update,
(exclusive_local_update _ (1%Qp, to_agree v)); last done.
by rewrite /to_gen_heap lookup_fmap Hl. }
iFrame "Hj Hl". iApply "Hclose". iNext.
iExists (<[j:=fill K (Lit ())%E]> tp), (<[l:=v]>σ).
iExists (<[j:=fill K (Lit tt)%E]> tp), (<[l:=v]>σ).
rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
Qed.
......@@ -352,7 +352,7 @@ Section cfg.
Lemma step_fork E ρ j K e :
nclose specN E
spec_ctx ρ j fill K (Fork e) ={E}= j', j fill K (Lit ())%E j' e.
spec_ctx ρ j fill K (Fork e) ={E}= j', j fill K (Lit tt)%E j' e.
Proof.
iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
iInv specN as (tp σ) ">[Hown %]" "Hclose".
......@@ -361,14 +361,14 @@ Section cfg.
assert (j < length tp) by eauto using lookup_lt_Some.
iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
{ by eapply auth_update, prod_local_update_1,
singleton_local_update, (exclusive_local_update _ (Excl (fill K (Lit Unit)))). }
singleton_local_update, (exclusive_local_update _ (Excl (fill K (Lit tt)))). }
iMod (own_update with "Hown") as "[Hown Hfork]".
{ eapply auth_update_alloc, prod_local_update_1,
(alloc_singleton_local_update _ (length tp) (Excl e)); last done.
rewrite lookup_insert_ne ?tpool_lookup; last omega.
by rewrite lookup_ge_None_2. }
iExists (length tp). iFrame "Hj Hfork". iApply "Hclose". iNext.
iExists (<[j:=fill K (Lit Unit)]> tp ++ [e]), σ.
iExists (<[j:=fill K (Lit tt)]> tp ++ [e]), σ.
rewrite to_tpool_snoc insert_length to_tpool_insert //. iFrame. iPureIntro.
eapply rtc_r, step_insert; eauto. econstructor; eauto.
Qed.
......
......@@ -58,7 +58,7 @@ Reserved Notation "Γ ⊢ₜ e : τ" (at level 74, e, τ at next level).
Inductive typed (Γ : stringmap type) : expr type Prop :=
| Var_typed x τ : Γ !! x = Some τ Γ ⊢ₜ Var x : τ
| Unit_typed : Γ ⊢ₜ Unit : TUnit
| Unit_typed : Γ ⊢ₜ tt : TUnit
| Nat_typed n : Γ ⊢ₜ #n n : TNat
| Bool_typed b : Γ ⊢ₜ # b : TBool
| BinOp_typed_nat op e1 e2 τ :
......
......@@ -2,11 +2,11 @@
This version is known to compile with:
- Coq 8.6
- Coq 8.6.1
- Ssreflect 1.6
- Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
- std++ version [ee6200b4d74bfd06034f3cc36d1afdc309427e5c](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/ee6200b4d74bfd06034f3cc36d1afdc309427e5c)
- Iris version [398bae9d092b6568cf8d504ca98d8810979eea33](https://gitlab.mpi-sws.org/FP/iris-coq/tree/398bae9d092b6568cf8d504ca98d8810979eea33)
- std++ version [fa6ff9d18aefb29e839e815aa170262d330bd108](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/fa6ff9d18aefb29e839e815aa170262d330bd108)
- Iris version [d85fdb0ea89edebcd10056e073ab9c7edc6c2050](https://gitlab.mpi-sws.org/FP/iris-coq/tree/d85fdb0ea89edebcd10056e073ab9c7edc6c2050)
# Compilation
......
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