The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Thanks a lot !
Pierre



Le 20/05/2011 12:36, AUGER Cedric a écrit :
> 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.
>