Commit 487ef579 authored by Ralf Jung's avatar Ralf Jung

demonstrate an eauto bug (?)

parent 8938309e
......@@ -26,172 +26,16 @@ Module savedprop. Section savedprop.
Lemma saved_NA i : saved i (A i) ¬ A i.
Proof.
iIntros "#Hs !# #HA". iPoseProof "HA" as "HA'".
iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP".
iDestruct (sprop_agree i P (A i) with "[]") as "#[_ HP]".
{ eauto. }
iApply "HP". done.
Qed.
Lemma saved_A i : saved i (A i) A i.
Proof.
iIntros "#Hs". iExists (A i). iFrame "#".
by iApply saved_NA.
Qed.
Lemma contradiction : False.
Proof.
apply (@soundness M False 1); simpl.
iIntros "". iMod A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
iModIntro. iNext.
iApply "HN". iApply saved_A. done.
Qed.
End savedprop. End savedprop.
(** This proves that we need the when opening invariants. *)
(** We fork in [uPred M] for any M, but the proof would work in any BI. *)
Module inv. Section inv.
Context (M : ucmraT).
Notation iProp := (uPred M).
Implicit Types P : iProp.
(** Assumptions *)
(** We have the update modality (two classes: empty/full mask) *)
Inductive mask := M0 | M1.
Context (fupd : mask iProp iProp).
Hypothesis fupd_intro : E P, P fupd E P.
Hypothesis fupd_mono : E P Q, (P Q) fupd E P fupd E Q.
Hypothesis fupd_fupd : E P, fupd E (fupd E P) fupd E P.
Hypothesis fupd_frame_l : E P Q, P fupd E Q fupd E (P Q).
Hypothesis fupd_mask_mono : P, fupd M0 P fupd M1 P.
(** We have invariants *)
Context (name : Type) (inv : name iProp iProp).
Hypothesis inv_persistent : i P, PersistentP (inv i P).
Hypothesis inv_alloc : P, P fupd M1 ( i, inv i P).
Hypothesis inv_open :
i P Q R, (P Q fupd M0 (P R)) (inv i P Q fupd M1 R).
(* We have tokens for a little "two-state STS": [start] -> [finish].
state. [start] also asserts the exact state; it is only ever owned by the
invariant. [finished] is duplicable. *)
(* Posssible implementations of these axioms:
* Using the STS monoid of a two-state STS, where [start] is the
authoritative saying the state is exactly [start], and [finish]
is the "we are at least in state [finish]" typically owned by threads.
* Ex () +_ ()
*)
Context (gname : Type).
Context (start finished : gname iProp).
Hypothesis sts_alloc : fupd M0 ( γ, start γ).
Hypotheses start_finish : γ, start γ fupd M0 (finished γ).
Hypothesis finished_not_start : γ, start γ finished γ False.
Hypothesis finished_dup : γ, finished γ finished γ finished γ.
(** We assume that we cannot update to false. *)
Hypothesis consistency : ¬ (fupd M1 False).
(** Some general lemmas and proof mode compatibility. *)
Lemma inv_open' i P R : inv i P (P - fupd M0 (P fupd M1 R)) fupd M1 R.
Proof.
iIntros "(#HiP & HP)". iApply fupd_fupd. iApply inv_open; last first.
{ iSplit; first done. iExact "HP". }
iIntros "(HP & HPw)". by iApply "HPw".
Qed.
Instance fupd_mono' E : Proper (() ==> ()) (fupd E).
Proof. intros P Q ?. by apply fupd_mono. Qed.
Instance fupd_proper E : Proper ((⊣⊢) ==> (⊣⊢)) (fupd E).
Proof.
intros P Q; rewrite !uPred.equiv_spec=> -[??]; split; by apply fupd_mono.
Qed.
Lemma fupd_frame_r E P Q : fupd E P Q fupd E (P Q).
Proof. by rewrite comm fupd_frame_l comm. Qed.
Lemma elim_fupd_fupd E P Q : ElimModal (fupd E P) P (fupd E Q) (fupd E Q).
Proof. by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_fupd. Qed.
Lemma elim_fupd0_fupd1 P Q : ElimModal (fupd M0 P) P (fupd M1 Q) (fupd M1 Q).
Proof.
by rewrite /ElimModal fupd_frame_r uPred.wand_elim_r fupd_mask_mono fupd_fupd.
Qed.
Lemma exists_split_fupd0 {A} E P (Φ : A iProp) :
FromExist P Φ FromExist (fupd E P) (λ a, fupd E (Φ a)).
Proof.
rewrite /FromExist=>HP. apply uPred.exist_elim=> a.
apply fupd_mono. by rewrite -HP -(uPred.exist_intro a).
Qed.
Hint Resolve elim_fupd_fupd elim_fupd0_fupd1 exists_split_fupd0 : proofmode.
(** Now to the actual counterexample. We start with a weird form of saved propositions. *)
Definition saved (γ : gname) (P : iProp) : iProp :=
i, inv i (start γ (finished γ P)).
Global Instance saved_persistent γ P : PersistentP (saved γ P) := _.
Lemma saved_alloc (P : gname iProp) : fupd M1 ( γ, saved γ (P γ)).
Proof.
iIntros "". iMod (sts_alloc) as (γ) "Hs".
iMod (inv_alloc (start γ (finished γ (P γ))) with "[Hs]") as (i) "#Hi".
{ auto. }
iApply fupd_intro. by iExists γ, i.
Qed.
Lemma saved_cast γ P Q : saved γ P saved γ Q P fupd M1 ( Q).
Proof.
iIntros "(#HsP & #HsQ & #HP)". iDestruct "HsP" as (i) "HiP".
iApply (inv_open' i). iSplit; first done.
iIntros "HaP". iAssert (fupd M0 (finished γ)) with "[HaP]" as "> Hf".
{ iDestruct "HaP" as "[Hs | [Hf _]]".
- by iApply start_finish.
- by iApply fupd_intro. }
iDestruct (finished_dup with "Hf") as "[Hf Hf']".
iApply fupd_intro. iSplitL "Hf'"; first by eauto.
(* Step 2: Open the Q-invariant. *)
iClear (i) "HiP ". iDestruct "HsQ" as (i) "HiQ".
iApply (inv_open' i). iSplit; first done.
iIntros "[HaQ | [_ #HQ]]".
{ iExFalso. iApply finished_not_start. by iFrame. }
iApply fupd_intro. iSplitL "Hf".
{ iRight. by iFrame. }
by iApply fupd_intro.
Qed.
(** And now we tie a bad knot. *)
Notation "¬ P" := ( (P - fupd M1 False))%I : uPred_scope.
Definition A i : iProp := P, ¬P saved i P.
Global Instance A_persistent i : PersistentP (A i) := _.
Lemma A_alloc : fupd M1 ( i, saved i (A i)).
Proof. by apply saved_alloc. Qed.
Lemma saved_NA i : saved i (A i) ¬A i.
Proof.
iIntros "#Hi !# #HA". iPoseProof "HA" as "HA'".
iDestruct "HA'" as (P) "#[HNP Hi']".
iMod (saved_cast i (A i) P with "[]") as "HP".
{ eauto. }
by iApply "HNP".
Qed.
Lemma saved_A i : saved i (A i) A i.
Proof.
iIntros "#Hi". iExists (A i). iFrame "#".
by iApply saved_NA.
Qed.
Lemma contradiction : False.
Proof.
apply consistency. iIntros "".
iMod A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
iApply "HN". iApply saved_A. done.
Qed.
End inv. End inv.
(* This is where `iDestruct "HA'" as (P) "[#HNP HsP]". iApply "HNP".` ought to work but doesn't.
Let's manually step through what that tactic does. *)
eapply coq_tactics.tac_exist_destruct with "HA'" _ "HA" _ _.
env_cbv; reflexivity. unfold A.
(* Now we look at the goal that typeclass inference should be able to solve, but can't
because (by the Hint Extern in classes.v) it uses "eauto with proofmode" which fails. *)
Fail by apply _.
Fail by eauto with proofmode.
(* Strange enough, manually applying a hint that *is* in the Db works *)
by apply @class_instances.into_exist_exist.
Undo.
(* Also, using typeclasses eauto works. *)
by typeclasses eauto with proofmode.
......@@ -82,22 +82,22 @@ Global Arguments is_except_0 : clear implicits.
End classes.
(* Establish links between Hint Dbs. *)
Hint Extern 0 (FromAssumption _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoPure _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromPure _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoPersistentP _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoLaterN _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromLaterN _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoWand _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromAnd _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromSep _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoAnd _ _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromOp _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoOp _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromOr _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoOr _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromExist _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoExist _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoModal _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (ElimModal _ _ _ _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IsExcept0 _) => solve [typeclasses eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromAssumption _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoPure _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromPure _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoPersistentP _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoLaterN _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromLaterN _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoWand _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromAnd _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromSep _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoAnd _ _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromOp _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoOp _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromOr _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoOr _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (FromExist _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoExist _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IntoModal _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (ElimModal _ _ _ _) => solve [eauto with proofmode] : typeclass_instances.
Hint Extern 0 (IsExcept0 _) => solve [eauto with proofmode] : typeclass_instances.
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