Regression after !329 on recursive proofs
Here's a self-contained testcase:
From iris.proofmode Require Import tactics.
Section testcase.
Context {PROP : sbi}.
Implicit Types P Q R : PROP.
Fixpoint test_fixpoint (n : nat) {struct n} : emp ⊢@{PROP} ⌜ (n + 0)%nat = n ⌝%I.
Proof.
case: n => [|n] /=.
- iIntros "_ !%". reflexivity.
- iIntros "_".
(* Works *)
(* by iDestruct (test_fixpoint n with "[//]") as %->. *)
(* Fails *)
by iDestruct (test_fixpoint with "[//]") as %->.
Qed.
This testcase is silly, but recursive proofs for mutually recursive lemmas can make sense, especially when the proof uses a custom induction scheme that is only used once: proving it by hand has advantages, especially for automation, but can create more boilerplate than a recursive proof.
I tried out a suggestion from @robbertkrebbers, got it to work and will send a MR shortly, but I expect the result should be achieved otherwise.