The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

You also did not give a definition of isFinite but if it is that your
sequence if (finite a s) then what you try to deduce is not true.

Your definition of seqFin is always true (this is what single says) 
so there are few chance that you can deduce from that that R is
well-founded

C. Paulin

Karol Oslowski writes:
 > Hi,
 >     since about two weeks I'm completely stuck with prooving well 
 > foundness'ness of a relation R. I have the following definitions :
 > "
 >     Inductive seqFin : A -> Type :=
 >       | single: forall ( a : A ), seqFin a
 >       | cons: forall ( a b : A ) ( s : seqFin b ), R a b -> seqFin a.
 >   
 > 
 >     Definition seqInfAny := nat -> A.
 > 
 >     Definition seqInfOk2( seq : seqInfAny ) := forall n : nat, R ( seq n 
 > ) ( seq ( S n ) ).
 > 
 >     Record seqInf : Type := make_seqInf{
 >       seqi : seqInfAny;
 >       seqOk : seqInfOk2 seqi
 >     }.
 > 
 >     Inductive seq : Type :=
 >       | finite : forall ( a : A ) ( s : seqFin a ), seq
 >       | infinite : forall ( s : seqInf ), seq.
 > "
 > I've prooven that :
 > "
 >    inductive A R /\ increasing A R -> (forall s : seq A R , isFinite s ).
 > "
 > 
 > And I want to proove the theorem:
 > "
 >  inductive A R /\ increasing A R -> well_founded ( RInv R ).
 > "
 > I guess it should be very easy. I'm not giving the definitions of 
 > inductive and increasing because I guess they are not important.
 > 
 > I would be grateful for any sugestions.
 > 
 > kind regards
 > 
 > Karol Oslowski
 > 
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86