A proof that inductive-inductive even is equivalent to directly defined even

LightQuantum.v

Inductive nat: Type :=
| S (n: nat)
| O.

Inductive even: nat -> Prop :=
| Base: even O
| Ind: forall n, even n -> even (S (S n)).

Inductive ev: nat -> Prop :=
| ev_Base: ev O
| ev_Ind: forall n, odd n -> ev (S n)
with odd: nat -> Prop :=
| odd_Ind: forall n, ev n -> odd (S n).

(* The hard part *)
(* It can only be done in this way, mutual Lemma won't work because
 * Coq don't know how the decreasing argument works.
 * The fact that we first intro & induction on n then apply the constructor
 * is very important, we can't apply the constructor first or it will fall
 * into the same problem.
 *)
Lemma ev_even: forall n,
  (
    ((ev n) -> even n) *
    ((odd n) -> even (S n))
  ).
  intros n.
  induction n as [ n f |].
  constructor.
  intro h. inversion h. apply f. assumption.
  intro h. constructor. inversion h. apply f. assumption.
  repeat constructor.
  intro h.
  inversion h.
Qed.

Theorem ev_even_eq: forall n, ev n <-> even n.
Proof.
  intros. constructor.
  apply ev_even.
  intros h. induction h. constructor. repeat constructor. assumption.
Qed.