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: Apr 19 2024 at 20:01 UTC