`solve_proper` having troubles proving non-expansiveness
In the snippet belowsolve_proper
is not able to prove non-expansiveness of a higher-order predicate.
solve_proper
is defined as solve_proper_core ltac:(fun _ => f_equiv)
.
However, one can use solve_proper_core ltac:(fun _ => simpl; f_equiv)
to automatically discharge the obligations.
Is there a reason why this simplification is not happening in solve_proper_core
?
Is it for the performance reasons?
From iris.heap_lang Require Import lang proofmode tactics notation.
Section linkedlist.
Context `{heapG Σ}.
Program Definition pre_isLinkedList : (valC -n> iProp Σ) -n> (valC -n> iProp Σ) :=
λne P v, (⌜v = InjLV #()⌝
∨ ∃ (h t : val) (l : loc),
⌜v = InjRV (PairV h #l)⌝
∗ l ↦ t
∗ ▷ (P t))%I.
Solve Obligations with solve_proper_core ltac:(fun _ => simpl; f_equiv).
End linkedlist.