The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

I finally got some weird (axiom free) proof.
I guess it can be simplified.

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

Inductive Pnat: Prop :=
| PO: Pnat
| PS: Pnat -> Pnat.

Fixpoint length l (H: Finite l): Pnat :=
  match H with
  | Finite_LNil => PO
  | Finite_LCons a l H => PS (length l H)
  end.

Lemma finite_irrelevant:
 forall l1 H1 l2 H2, l1 = l2 ->
  length l1 H1 = length l2 H2.
Proof.
 fix 2; intros _ [] _ [] Heq.
    split.
   discriminate.
  discriminate.
 simpl.
 f_equal.
 apply finite_irrelevant.
 now inversion_clear Heq.
Qed.

Lemma rebuild: Pnat -> forall l, Finite l \/ True.
Proof.
 fix 1; intros [] [].
    left; left.
   right; split.
  left; left.
 intros a l; destruct (rebuild H l); clear H.
  left; right; auto.
 right; auto.
Defined.

Lemma rerebuild: forall l (H: Finite l),
 rebuild (length l H) l = or_introl _ H.
Proof.
 fix 2; intros _ []; simpl.
  split.
 intros.
 rewrite rerebuild.
 split.
Qed.

Lemma final: forall l (H H0:Finite l), H=H0.
 intros.
 assert (L1 := finite_irrelevant l H l H0 (eq_refl _)).
 assert (L2 := rerebuild l H).
 assert (L3 := rerebuild l H0).
 rewrite L1 in L2.
 rewrite L2 in L3.
 change ((match or_introl True H with or_introl H2 => H2 | _ => H
end)=H0). rewrite L3.
 split.
Qed.