Overeager simplification in 'iIntros' and 'iSplit'
Consider the following lemma:
Lemma lc_test n m :
£ (S n + m) -∗ £ (S n).
Proof.
iIntros "[Hlc1 Hlc2]".
I would expect the state after this script to be such that Hlc1
is £ (S n)
, such that iExact "Hlc1"
finishes the proof. However, the state we actually get is this:
"Hlc1" : £ 1
"Hlc2" : £
((fix add (n0 m0 : nat) {struct n0} : nat :=
match n0 with
| 0 => m0
| S p => S (add p m0)
end) n m)
That is clearly terrible -- something in the IPM simplification machinery seems to be going wrong...
(The workaround is to rewrite lc_split
so that simplification has no chance of kicking in.)