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?..

does `reflexivity`

not conclude the proof?

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

?

if not, you can `destruct (v =? h)`

and use `reflexivity`

in each branch

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

come from?)

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.

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

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 :) )

Gantsev Denis has marked this topic as resolved.

Last updated: Jun 23 2024 at 23:01 UTC