CODEWITHSUNDEEP
coq
Attila Karoly
Attila Karoly

Reputation: 1031

Why can't Coq unify goal and hypothesis?

After some work on an exercise, I've reached the following proof state:

(tail1 is a nat list pattern generator, lng is generalized)

1 subgoal
n' : nat
IH_n' : forall lng : nat, lng > n' -> nth n' (update (tail1 lng) 0 1) 9 = 1
lng : nat
H : S lng > S n'
______________________________________(1/1)
nth (S n') (update (tail1 (S lng)) 0 1) 9 = 1

Using apply IH_n' fails with the following error:

Unable to unify "nth n' (update (tail1 ?M1305) 0 1) 9 = 1" with "nth (S n') (update (tail1 (S lng)) 0 1) 9 = 1".

Upvotes: 1

Views: 215

Answers (2)

Guillaume Melquiond
Guillaume Melquiond

Reputation: 1263

Hypothesis IH_n' is universally quantified by lng:nat. To apply it to the goal, Coq needs to instantiate it. ?M1305 is the name it gives to the value of lng it has yet to find.

The error message does not necessarily mean that ?M1305 and (S lng) cannot be unified. The issue might come from elsewhere. For example, your goal starts with nth (S n'), while the hypothesis starts with nth n'. Obviously, (S n') and n' cannot be unified.

Your first step, assuming the goal is provable, is to make sure it starts with nth n'. To do so, you need the second argument of nth to be of the form (cons foo bar).

Upvotes: 1

Lucien David
Lucien David

Reputation: 320

The problem here is that you are trying to apply an hypothesis on n' for S n', whereas n' is not quantified in IH_n'.

It would only work if your hypothesis was:

IH_n' : forall n' lng : nat, lng > n' -> nth n' (update (tail1 lng) 0 1) 9 = 1

To answer your other question, ?_ is the existential variable which would be replaced if your hypothesis was applicable, because the variable lng is quantified in the hypothesis.

If you want some help on how to prove this goal, could you share the code please ? (even though I think you should do unfold nth, update; simpl to see if you can apply your hypothesis somewhere.

Upvotes: 1

Related Questions