Skip to content

Always use magic wand in `iInduction` hypothesis

Robbert Krebbers requested to merge robbert/iInduction_wand into master

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

Merge request reports