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.forall (X : Type) (l : list X),
ev (length l) -> ev_list l
Proof.forall (X : Type) (l : list X),
ev (length l) -> ev_list l
  intros X l H.X: Type
l: list X
H: ev (length l)
ev_list l

which gives:

1 subgoal

  X : Type
  l : list X
  H : ev (length l)
  ============================
  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:

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.
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.

Answer (Arthur Azevedo De Amorim)

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

  remember (length l) as n.X: Type
l: list X
n: nat
Heqn: n = length l
H: ev n
ev_list l

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

  generalize dependent l.X: Type
n: nat
H: ev n
forall l : list X, n = length l -> ev_list l
  induction H.X: Type
forall l : list X, 0 = length l -> ev_list l
X: Type
n: nat
H: ev n
IHev: forall l : list X, n = length l -> ev_list l
forall l : list X, S (S n) = length l -> ev_list l

Answer (eponier)

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

  induction (length l) eqn:H0.X: Type
l: list X
H0: length l = 0
H: ev 0
ev_list l
X: Type
l: list X
n: nat
H0: length l = S n
H: ev (S n)
IHn: length l = n -> ev n -> ev_list l
ev_list l

Answer (Konstantin Weitz)

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.forall (X : Type) (l : list X),
ev (length l) -> ev_list l
Proof.forall (X : Type) (l : list X),
ev (length l) -> ev_list l
  intros X l H.X: Type
l: list X
H: ev (length l)
ev_list l
  refine ((fun n (e:n = length l) => _) (length l) eq_refl).X: Type
l: list X
H: ev (length l)
n: nat
e: n = length l
ev_list l
  (* proof *)
Admitted.