Hello!(sorry for the duplicated post, I accidentally deleted the other one)
I’m working my way around the Multiset.v file from the VFA book and I am hard stuck on the following proof.
Lemma contents_cons_inv : forall l x n,
S n = contents l x ->
exists l1 l2,
l = l1 ++ x :: l2
/\ contents (l1 ++ l2) x = n.
Proof.
destruct l.
simpl.
unfold empty.
discriminate.
simpl.
unfold union, singleton.
intros x.
bdestruct (x =? v).
intros.
exists [], l.
simpl.
split.
inv H.
auto.
injection H0.
intros H1.
symmetry.
apply H1.
simpl.
Now the goal looks like this:
v : value
l : list value
x : value
H : x <> v
============================
forall n : nat,
S n = contents l x -> exists l1 l2 : list value, v :: l = l1 ++ x :: l2 /\ contents (l1 ++ l2) x = n
It doesn’t matter what I try, I never manage to get past that.
It even seems to be impossible, given that we won’t ever be able to equal v :: l with l1 ++ x :: l2 unless l is a combination of (x :: l2) and l1 is [v].
Could anyone give me a tip on how to progress further?