The Coq mailing list

[Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>]

Hi,

it seems that proof irrelevance is not yet needed for this induction 
principle.

> Inductive even : nat -> Prop :=
>   | zero_even : even O
>   | ss_even : forall n : nat, even n -> even (S (S n)).
>
> Definition even_nat := {n : nat | even n}.
> Definition exist_even := exist (fun x : nat => even x).
>
> Definition even_O : even_nat := exist_even O zero_even.
> Definition even_SS (en : even_nat) : even_nat :=
>   match en with
>   exist n p => exist_even (S (S n)) (ss_even n p)
>   end.
>
> Lemma even_nat_ind :
>   forall P : even_nat -> Prop,
>   P even_O ->
>   (forall en : even_nat, P en -> P (even_SS en)) ->
>   forall en : even_nat, P en.
> Proof.
destruct en.
generalize x e; clear x e.
refine(
  fix ind (x:nat) (e:even x) {struct e} : P (exist (fun n=>even n) x e) 
:=
  match e as e' in even x' return P (exist (fun n=>even n) x' e') with
  | zero_even => _
  | ss_even x xe => _
  end).
exact H.
apply(H0 (exist_even x0 xe)).
apply ind.
Qed.

But I agree with Benjamin that you'll run into trouble later for the 
reason he explained.

As pointed out proof irrelevance can be proven explicitly for your 
predicate.
It can also be made implicit by defining "even" in a different way:

Fixpoint even (n:nat) : Prop := match n with
| 0 => True
| S 0 => False
| S (S n) => even n
end.

Now all the proofs of even are convertible !

Definition even_nat := sig even.

Definition even_O : even_nat := exist even O I.
Definition even_SS (en : even_nat) : even_nat :=
  match en with
  exist n p => exist even (S (S n)) p
  end.

Your induction principle can now be proven by induction over the 
certificate of being even (i.e. the half).

Require Import Omega.

Lemma even_is_double : forall a, even a -> exists i, i*2 = a.
cut(forall n a, a < n ->even a -> exists i, i*2 = a).
  intros.
  apply H with (n:=S (S a)); auto.
induction n; intros.
  inversion H.
destruct a.
  exists 0; apply refl_equal.
destruct a.
  inversion H0.
destruct(fun X => IHn a X H0).
  omega.
exists (S x).
  simpl; rewrite H1; apply refl_equal.
Defined.

Lemma true_unique : forall P (a:True), P I -> P a.
intros.
exact(match a as a' return P a' with I => X end).
Qed.

Lemma even_nat_ind :
  forall P : even_nat -> Prop,
  P even_O ->
  (forall en : even_nat, P en -> P (even_SS en)) ->
  forall en : even_nat, P en.
destruct en.
destruct(even_is_double x e) as [i Hi].
generalize e; clear e; rewrite <- Hi; clear Hi; intros.
induction i; simpl.
pattern e; apply true_unique.
exact H.
apply (H0 (exist even (i*2) e)).
apply IHi.
Qed.

Good luck !

Roland

--
http://www.lix.polytechnique.fr/~zumkeller/