How to introduce a new variable in Coq?

Question

I was wondering if there is a way to introduce an entirely new variable during the proof of a theorem in Coq?

For a complete example, consider the following property from here about the evenness of the length of a list.

Inductive ev_list {X:Type}: list X -> Prop :=
  | el_nil : ev_list []
  | el_cc  : forall x y l, ev_list l -> ev_list (x :: y :: l).

Now I want to prove that for any list l if its length is even, then ev_list l holds:

Lemma ev_length__ev_list': forall X (l : list X), ev (length l) -> ev_list l.
Proof.
  intros X l H.

which gives:

1 subgoals
X : Type
l : list X
H : ev (length l)
______________________________________(1/1)
ev_list l

Now, I'd like to "define" a new free variable n and a hypothesis n = length l. In hand-written math, I think we can do this, and then do induction about n. But is there a way to do the same in Coq?

Note. the reasons I ask are that:

1. I don't want to introduce this n artificially into the statement of the theorem itself, as is done in the page linked earlier, which IMHO is unnatural.

2. I tried to induction H., but it seems not working. Coq wasn't able to do case analysis on length l's ev-ness, and no induction hypothesis (IH) was generated.

Thanks.

Answer 1

This is a common issue in Coq proofs. You can use the remember tactic:

remember (length l) as n.

If you're doing induction on H as well, you might also have to generalize over l beforehand, by doing

generalize dependent l.
induction H.

Answer 2

If you want to add a new variable only for your induction, you can use directly

induction (length l) eqn:H0

Answer 3

According to the Curry-Howard Isomorphism, hypothesis in your context are just variables. You can define new variables with a function. The following refine tactic extends the goal with a fresh variable n (that is set to length l) and a proof e that n = length l (that is set to eq_refl).

Lemma ev_length__ev_list': forall X (l : list X), ev (length l) -> ev_list l.
Proof.
  intros X l H.
  refine ((fun n (e:n = length l) => _) (length l) eq_refl).
  (* proof *)
Admitted.