CODEWITHSUNDEEP
coq
limp_chimp
limp_chimp

Reputation: 15163

Eliminating cases with propositions in Coq

Given an obvious definition of a natural number list type, and a function last that takes the last element or returns a default, I'm trying to prove the following lemma:

Lemma last_ignores_first : forall l : natlist, forall def n : nat,
  length l > 0 ->
  last def (n :: l) = last def l.

Now, I want to prove it by noting that since l is not empty, it must be able to be written in the form h::t for some h and t, and thus the proof will follow from the definition of last. But how can I use that knowledge in Coq? If I do induction or destruct on l, I will have to account for the case where l is [], a case which is prevented by the hypothesis. How to I tell it that l must follow a certain form?

Upvotes: 1

Views: 77

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23592

You just have to use inversion on your hypothesis that states that length l > 0:

intros [|x l] def n H.
- (* Case l = [], contradiction *)
  simpl in H. inversion H.
- (* Continue normally *)

Upvotes: 3

Related Questions