## Stream: Coq users

### Topic: ✔ Stuck in bag_theorem

#### Gantsev Denis (Jan 04 2022 at 23:51):

Hello,
I am working thru https://softwarefoundations.cis.upenn.edu/lf-current/Lists.html
and I am stuck at following (bag_theorem):

``````Lemma eqb_lemma: forall v:nat, v =? v = true.
Proof.
induction v. simpl. reflexivity. simpl. apply IHv.
Qed.
Theorem bag_theorem : forall (n v:nat), forall s:bag,
S (count v s) = count v (add v s).
Proof.
induction s as [| h t].
- simpl. rewrite eqb_lemma. reflexivity.
- simpl. rewrite eqb_lemma.
``````

Gives:

``````1 goal
n, v, h : nat
t : natlist
IHt : S (count v t) = count v (add v t)
______________________________________(1/1)
S match v =? h with
| true => S (count v t)
| false => count v t
end = S match v =? h with
| true => S (count v t)
| false => count v t
end
``````

This looks completely obvious to me, but I don't understand how I make that obvious to Coq?
Whatever the result of `v =? h`, both left and right side of equation in Goal would be identical...
(Ideally I would like to use only tactics mentioned so far in the course, like destruct, case, induction, reflexivity, rewrite, replace, simpl).
How should I proceed?..

#### Paolo Giarrusso (Jan 05 2022 at 00:21):

does `reflexivity` not conclude the proof?

#### Paolo Giarrusso (Jan 05 2022 at 00:22):

maybe I can’t read but the goal looks of shape `x = x`?

#### Paolo Giarrusso (Jan 05 2022 at 00:23):

if not, you can `destruct (v =? h)` and use `reflexivity` in each branch

#### Paolo Giarrusso (Jan 05 2022 at 00:24):

but I’m a bit confused because your goal doesn’t match your proof script (where does `Eq` come from?)

#### Paolo Giarrusso (Jan 05 2022 at 02:11):

after guessing what `count` looks like (which I won't post to not spoil the exercise), I confirm that `reflexivity` should work. In fact, it seems you can skip the `induction` altogether.

#### Paolo Giarrusso (Jan 05 2022 at 02:12):

Either way, it'd be good to understand both proofs I suggested; feel free to ask follow-up questions.

#### Gantsev Denis (Jan 05 2022 at 15:50):

Ohhh I am sorry, I have posted the wrong proof state, because I was trying to solve it while posting here. Edited.
And yes I confirm reflexivity works! I have haven't tried it, because untill now, it only worked for trivial equality (`a=a`)...
Alright my post is useless, and thank you very much. (I better have been sleeping at 1am :) )

#### Notification Bot (Jan 05 2022 at 15:50):

Gantsev Denis has marked this topic as resolved.

Last updated: Jan 29 2023 at 05:03 UTC