iRewrite fails when non-expansive function have multiple arguments
Tried to make a meaningful title, but I think this example succinctly demonstrates the issue:
From iris.proofmode Require Import classes tactics.
From iris.si_logic Require Export bi siprop.
Require Import iris.proofmode.coq_tactics.
Require Import iris.proofmode.reduction.
Program Definition constt {A B : ofe} : A -n> B -n> B := λne a b, b.
Solve All Obligations with solve_proper.
Lemma test (A B : ofe) (a1 a2 : A) (b1 : B) :
(⊢ a1 ≡ a2 → constt a1 b1 ≡ constt a2 b1 : siProp)%I.
Proof.
iIntros "H". iRewrite "H".
The tactic fails with:
Error: Tactic failure: Nothing to rewrite.
The core of the issue
The problem with this is not even necessarily in Iris, but with rewriting in Coq in general. However this specific issue can be down to the following. The iRewrite
tactic applies the lemma tac_rewrite
with tac_rewrite _ "H" _ _ Right
and then tries to discharge the goals. It succeeds in finding the right 'context' for rewriting (using iRewriteFindPred
). However, the last goal is to show that this context is in fact non-expansive. In this specific case the goal is
NonExpansive (λ a0 : A, (constt a0 b1 ≡ constt a2 b1)%I)
The tactic iRewrite
tries to solve this goal with intros ??? ->
, which fails because of the issues with Coq rewriting.
Potential solution
One potential solution is to change the iRewrite
so it calls solve_proper for proving the NonExpansiveness:
Local Tactic Notation "iRewriteCore" constr(lr) open_constr(lem) :=
iPoseProofCore lem as true (fun Heq =>
eapply (tac_rewrite _ Heq _ _ lr);
[pm_reflexivity ||
let Heq := pretty_ident Heq in
fail "iRewrite:" Heq "not found"
|tc_solve ||
let P := match goal with |- IntoInternalEq ?P _ _ ⊢ _ => P end in
fail "iRewrite:" P "not an equality"
|iRewriteFindPred
| solve [ intros ??? ->; reflexivity | solve_proper ]
|pm_prettify; iClearHyp Heq]).
With this change the proof above goes through. Of course, sometimes solve_proper
can quite a bit of time. However, this will only be a regression for goals for which iRewrite
does not work in any case.