Ssreflect Users Discussion List

[Yves Bertot <>]

I finally proved the lemmas I needed and I found more errors in the 
expected statements.  Here are the right statements:

Lemma fconnect_step (T : finType) (f : T -> T) (x y : T) :
  fconnect f x y -> (x == y) || (fconnect f (f x) y).

Lemma order_step (T : finType) (f : T -> T) (x : T) :
  order f x = order f (f x) /\ iter (order f x) f x = x \/
  order f x = (order f (f x)).+1.

Lemma findex_step (T : finType) (f : T -> T) (x y : T) :
  fconnect f x y ->
  y != x -> findex f x y = (findex f (f x) y).+1.

I have one more lemma about findex and a few lemmas about fcycle that I 
will collect in a pull request.  I will be happy to discuss naming 
conventions.

Yves

On 09/07/2018 08:08 AM, Yves Bertot wrote:
> The statement expected for fconnect_step should be:
>
> Lemma fconnect_step (T : finType) (f : T -> T) (x y : T) :
>   fconnect f x y -> (f x == y) || (fconnect f (f x) y).
>
>
> On 09/07/2018 08:07 AM, Yves Bertot wrote:
> > Hello,
> >
> > I would like to show the following theorems.
> >
> > Lemma fconnect_step (T : finType) (f : T -> T) (x y : T) :
> >   fconnect f x y -> f x == y || fconnect (f x) y.
> >
> > Lemma order_step (T : finType) (f : T -> T) (x y : T) :
> >   fingraph.order f x = fingraph.order f (f x) /\
> >     iter (fingraph.order f x) f x = x \/
> >   order f x = (order f (f x)).+1.
> >
> > Lemma findex_step (T : finType) (f : T -> T) (x y : T) :
> >   fconnect f x y ->
> >   y != x -> findex f x y = (findex f (f x) y).+1.
> >
> > Each one is expected to be useful for the next one.  But the 
> > interfaces provided for connect, findex, and order are very slim and 
> > I am wondering whether I am using the right level of abstraction.  
> > Does anybody have an opinion on this?
> >
> > Yves