Commit 988a526e authored by Dan Frumin's avatar Dan Frumin

Get rid of all the admits

parent b3e7473a
......@@ -298,18 +298,28 @@ Proof.
eapply IHe; eauto.
rewrite dom_delete.
(* TODO: set_solver does not solve this *)
admit.
set_unfold.
intros y [Hy|Hy]; subst; eauto.
destruct (Hdom _ Hy); eauto.
destruct (decide (y = x)); subst; eauto.
+ simpl in Hcl.
eapply IHe; eauto.
rewrite dom_delete.
admit. (* TODO: same story *)
set_unfold.
intros y [Hy|Hy]; subst; eauto.
destruct (Hdom _ Hy); eauto.
destruct (decide (y = f)); subst; eauto.
+ simpl in Hcl.
eapply IHe; eauto.
rewrite delete_commute.
rewrite !dom_delete.
admit.
set_unfold.
intros y [Hx|[Hf|Hy]]; subst; eauto.
destruct (Hdom _ Hy); eauto.
destruct (decide (y = f)); subst; eauto.
destruct (decide (y = x)); subst; eauto.
}
Admitted.
Qed.
Lemma subst_p_insert (x : binder) v (m : stringmap val) e :
subst_p (<[x:=v]>m) e =
......
......@@ -1011,15 +1011,17 @@ Proof.
iExists k.
done.
Qed.
End test.
Lemma steps_release E ρ j K l b:
Section test2.
Context `{heapIG Σ, !cfgSG Σ}.
(* TODO: Coq complains if I make it a section variable *)
Axiom (steps_release : forall E ρ j K l b,
nclose specN E
spec_ctx ρ - l ↦ₛ (#v b) - j fill K (App (Lit Unit) (Loc l))
={E}= j fill K (Lit Unit) l ↦ₛ (#v false).
admit. Admitted.
={E}= j fill K (Lit Unit) l ↦ₛ (#v false)).
Lemma test_apply E ρ j b K l:
Theorem test_apply E ρ j b K l:
nclose specN E
spec_ctx ρ -
l ↦ₛ (#v b) - j fill K (App (Lit Unit) (Loc l))
......@@ -1030,4 +1032,4 @@ Proof.
done.
Qed.
End test.
End test2.
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