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.
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?..
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
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 (
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: Oct 01 2023 at 18:01 UTC