 # How to prove this self-defined Bag Theorem?

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
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!!

The answer may depend on how exactly you define `add` and `count`. However you are probably trying too much to rely on `induction`/`destruct` even when it is not necessary:

• I would not be surprised if your lemma `add_null` could be proved by just `reflexivity.`,
• and concerning `bag_theorem1`, starting by `intros n b; simpl.` might give you some hint on what you should do.

Thank you for your suggestions. I tried starting by `intros n b; simpl` but nothing has changed in the goal. Here are the definitions about `add` and `count`:

Definition add (v:nat) (s:bag) : bag :=
match v with
| O => O::s
| S v’ => (S v’)::s
end.

Fixpoint equal(a b:nat): bool:=
match a, b with
| O, O => true
| S a’, S b’ => equal a’ b’
| O, S b’ => false
| S a’, O => false
end.

Fixpoint count (v:nat) (s:bag) : nat :=
match s with
| nil => O
| sh::st => match (equal sh v) with
| true => S (count v st)
| _ => count v st
end
end.

Let us focus on your definition of `add`: it starts with a `match` on `v` which explains why you need to `destruct v` each time you want to compute with `add`.
Then two possibilities for the `intros n b; simpl.` to show what may help you in `bag_theorem1`:

• either keep your definition of `add` and use `intros n b; destruct n as [|n]; simpl.` in `bag_theorem1` (to make `add` compute, thanks to the `destruct`)
• or remark in the definition of `add` that what you do in both branches is exactly the same: `x => x::s`, meaning that the `match` is in fact not necessary, and you can simplify the definition of `add`. ! Thank you very much. I tried your two solutions. They both worked. It looks very easy, now. I do realise that I didn’t understand how to make functions compute very well before. By the way, I am still wondering whether there is an easier way to solve this subgoal:

1 subgoal
n : nat
b : bag
S (count n b) =
match equal n n with
| true => S (count n b)
| false => count n b
end

I tried to use `simpl` it didn’t work. So I used `assert (equal n n = true) as H` then it worked. So, it shows that to make `equal n n` compute, we have to do either `destruct n` or `induction n`. Right?

Indeed `equal a b` is really defined by induction on `a` and `b` so you need to work on them to derive most of the properties of `equal`. Here the statement `forall n, equal n n = true` is a natural one to prove and requires induction on `n`.