The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  here's another way to do the axiom-free proof without resorting to natP. 
The trick is to use the inversion lemmas which do not require any axioms.

Variable (A:Type).

CoInductive LList :=
  | LNil: LList
  | LCons : A -> LList -> LList.

Inductive Finite : LList -> Prop :=
  |Finite_LNil: Finite LNil
  |Finite_LCons   : forall a l, Finite l-> Finite (LCons a l).

Lemma finite_lnil_inv : forall f : Finite LNil, f = Finite_LNil.
Proof. intros.
  refine (match f as f' in Finite l return 
            (match l return Finite l -> Prop with
               | LNil => fun f => f = Finite_LNil 
               | _ => fun _ => True end) f'
            with Finite_LNil => eq_refl
              | Finite_LCons a l f => I
          end).
Qed.

Lemma finite_lcons_inv a l : forall f : Finite (LCons a l), 
  exists f', f = Finite_LCons a l f'.
Proof. intros.
  refine (match f as f' in Finite l return 
            (match l return Finite l -> Prop with
               | LNil => fun f => True
               | LCons a l => fun f => exists f'', f = Finite_LCons a l f'' 
end) f'
            with Finite_LNil => I
              | Finite_LCons a l f => ex_intro _ f eq_refl
          end).
Qed.

Lemma finite_l_eq : forall {l} (H H0:Finite l), H = H0.
Proof. fix 2. intros.
  destruct H. rewrite finite_lnil_inv. reflexivity.
  destruct (finite_lcons_inv _ _ H0). rewrite H1. f_equal. apply finite_l_eq.
Qed.

Print Assumptions finite_l_eq.

-- Matthieu