Always use magic wand in `iInduction` hypothesis
The current behavior is inconsistent:
Lemma foo {PROP : bi} (n : nat) (Hn : 0 < n) (P : nat → PROP) : ⊢ P n.
Proof.
iInduction n as [|n] "IH" forall (Hn); first lia.
Restart.
iInduction n as [|n] "IH"; first lia.
Abort.
In the first case (manual revert via forall
clause), we get a wand; in the second case (auto revert), we get an implication.
In !789 (merged) we decided that wands are preferred, but we missed the case for the automated revert.
Small note: I am using MakeAffinely
instead of FromAffinely
, that is because MakeAffinely
gives an ⊣⊢
instead of ⊢
and we actually need the other direction. This is consistent with IntoWand
instances where we also use MakeAffinely
. Since we use it on ⌜ _ ⌝
and not a compound assertion, this should not make a difference.
Edited by Robbert Krebbers