# Stuck on proof in Coq

This is an exercise from Software foundations for my discrete math & functional programming class. I am a little stuck with the end of the code because it works for the first two examples but it doesn't work for my false case and I can't figure out why...


(** **** Exercise: 2 stars, standard (eqblist)

Fill in the definition of [eqblist], which compares

lists of numbers for equality. Prove that [eqblist l l]

yields [true] for every list [l]. *)

Fixpoint eqblist (l1 l2 : natlist) : bool :=

match l1, l2 with

| nil, nil => true

| (h1 :: t1), (h2 :: t2) => true

| _,_ => false

end.

Example test_eqblist1 :

(eqblist nil nil = true).

Proof. reflexivity. Qed. (works)

Example test_eqblist2 :

eqblist [1;2;3] [1;2;3] = true.

Proof. reflexivity. Qed. (works)

Example test_eqblist3 :

eqblist [1;2;3] [1;2;4] = false.

Proof. reflexivity. Qed. (this one doesn't work! )

$$$$

• I'm not sure whether debugging your Coq code is on-topic here. Any community votes? – D.W. Feb 25 '20 at 0:25
• I’m inclined to say it’s more about debugging code than CS principles, but I don’t have much weight – D. Ben Knoble Feb 25 '20 at 0:29

Your definition is wrong. Every pair of lists will evaluate to true. You need to actually check that h1 and h2 are the same, and that the lists are the same length.
If I recall the exercises correctly, you may want to look back at beq_nat and andb`.