Proofmode : pure implies and forall
A few weirdities (tested in gen_proofmode, but a few a these are probably a problem in master too):
Lemma test_forall_nondep (φ : Prop) :
φ → (∀ _ : φ, False : PROP) -∗ False.
Proof.
iIntros (Hφ) "Hφ".
Fail iSpecialize ("Hφ" with "[%]").
Fail iApply "Hφ".
Fail iSpecialize ("Hφ" $! _).
iSpecialize ("Hφ" $! Hφ); done.
Qed.
Lemma test_pure_impl (φ : Prop) :
φ → (⌜φ⌝ → False : PROP) -∗ False.
Proof.
iIntros (Hφ) "Hφ".
Fail iSpecialize ("Hφ" $! Hφ).
Fail iSpecialize ("Hφ" $! _).
Fail iApply "Hφ".
iSpecialize ("Hφ" with "[%]"); done.
Qed.
Lemma test_forall_nondep_impl2 (φ : Prop) P :
φ → P -∗ (∀ _ :φ, P -∗ False : PROP) -∗ False.
Proof.
iIntros (Hφ) "HP Hφ".
Fail iSpecialize ("Hφ" with "HP").
Abort.
Lemma test_pure_impl2 (φ : Prop) P :
φ → P -∗ (⌜φ⌝ → P -∗ False : PROP) -∗ False.
Proof.
iIntros (Hφ) "HP Hφ".
Fail iSpecialize ("Hφ" with "HP").
Abort.
A few remarks:
-
In the case the hypothesis starts with a forall,
iApply ("H" $! _ with "...")
should behave the same asiApply ("H" with "...")
. Moreover, it is weird thatiApply ("H" with "...")
suddenly generates a new goal. And, I think it is annoying to generated shelved goals. So I think they should both be rejected (as now, no change required for this). In my opinion, same remark foriSpecialize ("Hφ" $! Hφ)
forimpl2
test cases. -
If I remember well, we decided at some point that
∀ _ :φ,
and⌜φ⌝ →
should behave more or less the same. SoiSpecialize ("Hφ" with "[%]")
andiSpecialize ("Hφ" $! Hφ)
should both work for both forms. -
If we want to somehow support
iApply "Hφ".
, we need to infer persistence of the premises when no annotation is given. We can either do that systematically (but then, what about performances), or do that only in the case everything else fails.