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?