Skip to content
Snippets Groups Projects
Commit 95f8fdda authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge commit '63f6c55b' into gen_proofmode

parents eb0aa8f8 63f6c55b
No related branches found
No related tags found
No related merge requests found
*.v gitlab-language=coq
......@@ -7,7 +7,7 @@ This is the Coq development of the [Iris Project](http://iris-project.org).
This version is known to compile with:
- Coq 8.6.1 / 8.7.0
- Ssreflect 1.6.2
- Ssreflect 1.6.4
- A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
If you need to work with Coq 8.5, please check out the
......
......@@ -195,7 +195,7 @@ Proof.
destruct e=> //=; repeat (simplify_eq/=; case_match=>//);
inversion 1; simplify_eq/=; rewrite ?to_of_val; eauto.
unfold subst'; repeat (simplify_eq/=; case_match=>//); eauto.
- apply ectxi_language_sub_values=> /= Ki e' Hfill.
- apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
naive_solver eauto using to_val_is_Some.
Qed.
......
......@@ -62,7 +62,9 @@ Section ectx_language.
Definition head_irreducible (e : expr) (σ : state) :=
e' σ' efs, ¬head_step e σ e' σ' efs.
Definition sub_values (e : expr) :=
(* All non-value redexes are at the root. In other words, all sub-redexes are
values. *)
Definition sub_redexes_are_values (e : expr) :=
K e', e = fill K e' to_val e' = None K = empty_ectx.
Inductive prim_step (e1 : expr) (σ1 : state)
......@@ -103,21 +105,21 @@ Section ectx_language.
Qed.
Lemma prim_head_reducible e σ :
reducible e σ sub_values e head_reducible e σ.
reducible e σ sub_redexes_are_values e head_reducible e σ.
Proof.
intros (e'&σ'&efs&[K e1' e2' -> -> Hstep]) ?.
assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
rewrite fill_empty /head_reducible; eauto.
Qed.
Lemma prim_head_irreducible e σ :
head_irreducible e σ sub_values e irreducible e σ.
head_irreducible e σ sub_redexes_are_values e irreducible e σ.
Proof.
rewrite -not_reducible -not_head_reducible. eauto using prim_head_reducible.
Qed.
Lemma ectx_language_atomic e :
( σ e' σ' efs, head_step e σ e' σ' efs irreducible e' σ')
sub_values e
sub_redexes_are_values e
Atomic e.
Proof.
intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
......
......@@ -90,8 +90,9 @@ Section ectxi_language.
fill_not_val, fill_app, step_by_val, foldl_app.
Next Obligation. intros K1 K2 ?%app_eq_nil; tauto. Qed.
Lemma ectxi_language_sub_values e :
( Ki e', e = fill_item Ki e' is_Some (to_val e')) sub_values e.
Lemma ectxi_language_sub_redexes_are_values e :
( Ki e', e = fill_item Ki e' is_Some (to_val e'))
sub_redexes_are_values e.
Proof.
intros Hsub K e' ->. destruct K as [|Ki K _] using @rev_ind=> //=.
intros []%eq_None_not_Some. eapply fill_val, Hsub. by rewrite /= fill_app.
......
......@@ -40,8 +40,7 @@ Lemma sum_loop_wp `{!heapG Σ} v t l (n : Z) :
{{{ RET #(); l #(sum t + n) is_tree v t }}}.
Proof.
iIntros (Φ) "[Hl Ht] HΦ".
iLöb as "IH" forall (v t l n Φ). wp_rec. wp_let.
destruct t as [n'|tl tr]; simpl in *.
iInduction t as [n'|tl ? tr] "IH" forall (v l n Φ); wp_rec; wp_let.
- iDestruct "Ht" as "%"; subst.
wp_match. wp_load. wp_op. wp_store.
by iApply ("HΦ" with "[$Hl]").
......@@ -49,7 +48,7 @@ Proof.
wp_match. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htl"). iIntros "[Hl Htl]".
wp_seq. wp_proj. wp_load.
wp_apply ("IH" with "Hl Htr"). iIntros "[Hl Htr]".
wp_apply ("IH1" with "Hl Htr"). iIntros "[Hl Htr]".
iApply "HΦ". iSplitL "Hl".
{ by replace (sum tl + sum tr + n) with (sum tr + (sum tl + n)) by omega. }
iExists ll, lr, vl, vr. by iFrame.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment