The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

    Dear Christine,

 

  I understand Karol's problem and I also don't know how to solve it. To be more explicit about the definitions:

 seq      is a definition of any reduction sequence in R

 seqInf   is a definition of any infinite reduction sequence in R

 seqFin a is a definition of a finite reduction sequence in R starting in a

 

  Now he's able to prove:

 SomeConditions -> forall s: seqInf, False.

 

  So when SomeConditions hold (whatever they are, that's not the point here) we have absence of  infinite reduction sequences in R and from this clearly well-foundedness of R follows (the fact that seqFin always hold due to single constructor has nothing to do with that, it just means that for any element of A we have sequence of length 1 starting in this element).

 

  Our idea of how to approach that was along the lines of what Thery Laurent has written, that is to do induction on the maximal length of the sequence starting in given element. That is I can easily imagine proving following lemma:

 

  forall a n,

    maximalLengthOfSequenceStartingIn a = n -> Acc a R.

 

  but now the goal is to conclude from that 'well_founded R' and the problem is with application of this lemma for which maximalLengthOfSequenceStartingIn has to be computed but cannot as A might be infinite and there might be infinitely many sequences (all of them finite) starting in some element.

  Any ideas?

   

    Kind regards,

      Adam Koprowski

 

-------------------------------------------------------------------------

- Adam Koprowski  (A.Koprowski AT tue.nl)                                  -

- Department of Mathematics and Computer Science                        -

- Technical University Eindhoven (TU/e)                                 -

-                                                                       -

- The difference between impossible and possible lies in determination  -

-      Tommy Lasorda                                                    -

-------------------------------------------------------------------------