I am working on the exercises in the List chapter of Software Foundation. I am working particularly on this exercise - “Adding a value to a bag should increase the value’s count by one. State that as a theorem and prove it.”

I am trying to figure out how to prove this theorem:

Blockquote

Theorem bag_theorem1 : forall (n : nat) (b:bag),

S (count n b) = count n (add n b).

I am able to solve the case “b=[]” with two lemmas as follows:

Blockquote

Lemma add_null: forall n, add n [] = [n].

Proof.

intros. destruct n.

simpl. reflexivity.

simpl. reflexivity.

Qed.

Blockquote

Lemma count_p: forall p, count p [p] = 1.

Proof.

intros p.

induction p as [|p’ IHp].

simpl. reflexivity.

simpl in IHp. simpl. assumption.

Qed.

Blockquote

Theorem bag_theorem1 : forall (n:nat) (b:bag),

S (count n b) = count n (add n b).

Proof.

intros n b.

induction b as [|x l IHb].

simpl. rewrite add_null. rewrite → count_p. reflexivity.

(how to solve the second case?)

However, I got stuck in the second case.

Thank you very much for your help!!