Using remember in induction over proposition gives 'ill-typed' error in Coq

Question

Here are the inductive & computational definitions of evenness of natural numbers.

Inductive ev : nat -> Prop :=
  | ev_0 : ev O
  | ev_SS : forall n:nat, ev n -> ev (S (S n)).

Definition even (n:nat) : Prop := 
  evenb n = true.

And the proof that one implies the other.

Theorem ev__even : forall n,
  ev n -> even n.
intros n E.
induction E as [ | n' E' ]. 
reflexivity. apply IHE'. Qed.

I didn't think much of this proof at first, but on a closer look I find something troubling. The problem is that after the reflexivity step, I expect to see the context

1 subgoal
n' : nat
E : ev (S (S n'))
E' : ev n'
IHE' : ev n' -> even n'
====================================================================== (1/1)
even (S (S n'))

But what I actually get instead is

1 subgoal
n' : nat
E' : ev n'
IHE' : even n'
====================================================================== (1/1)
even (S (S n'))

Although the theorem is still provable as is, it is disturbing to see hypotheses mysteriously disappear. I'd like to know how to get the context I initially expected. From web searches I understand that this is a general problem with induction over constructed terms in Coq. One proposed solution on SO suggests using the remember tactic on hypotheses to be kept. But when I try that in this proof,

Theorem ev__even : forall n,
  ev n -> even n.
intros n E.
remember E.
induction E as [ | n' E' ].

I get the following error message at the induction step.

Error: Abstracting over the term "n" leads to a term
"fun n : nat => forall e : ev n, e = E -> even n" which is ill-typed.

Which I do not really understand. I think the problem is that E has a free variable, but in that case I would be stuck, since there is no way to introduce E without also introducing n. (generalize dependent n would generalize E with it)

Is there any way to obtain the initially expected context?

I don't understand why you expect to see E : ev (S (S n')) and IHE' : ev n' -> even n' — Konstantin Weitz
If you use the induction principle forall P, P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n, then ev will occur in the induction hypothesis like you expect it to. The induction principle for ev is ev_ind, which has type forall P, P 0 -> (forall n, ev n -> P n -> P (S (S n))) -> forall n, ev n -> P n. When performing induction on ev you shouldn't expect ev to be a premise of the induction hypothesis, just like when performing induction on a nat you shouldn't expect a nat to be universally quantified in the induction hypothesis. — user3551663

Konstantin Weitz Konstantin Weitz · Accepted Answer · 2014-06-28T16:35:27

I don't understand what the induction tactic is doing here. Whenever I don't understand what a tactic is doing, I try to just write the proof term myself. If you invoke the induction principle by hand, you can keep the original hypothesis:

Theorem ev__even : forall n, ev n -> even n.
  intros n E.
  refine (ev_ind even _ _ n E).
  - reflexivity.
  - intros n' E' IH.
    apply IH.
Qed.

This is what the context looks like in the second case of the induction:

  n : nat
  E : ev n
  n' : nat
  E' : ev n'
  IH : even n'
  ============================
   even (S (S n'))

Assuming

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => evenb n'
  end.

Using remember in induction over proposition gives 'ill-typed' error in Coq

2 Answers