CODEWITHSUNDEEP
coqcoq-tactic
Bojaculus Horsemanicus
Bojaculus Horsemanicus

Reputation: 35

Coq: Unable to Unify

student here, just started learning Coq. I'm essentially trying to prove that [] = a::l where (a:A) and (l: list A) is False, solving all subgoals. I found a nifty Coq Library function called nil_cons but I get an error when trying to apply it. Does anyone have any advice? Thanks in advance!

Error Message Here

Proof Attempt

Upvotes: 2

Views: 963

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23582

I can't tell exactly what the result you're trying to prove means, but nil_cons is probably not the way to go. That lemma allows you to derive False when you have already established that [] = a :: l. Your goal, on the other hand, wants you to prove [] = a :: l assuming a different set of hypotheses.

Upvotes: 2

Related Questions