Ssreflect Users Discussion List

[Yves Bertot <>]

I am currently modeling simple graphs corresponding to meshes or 
triangulations.

I have a simple function that is only injective  in a subset of its 
type, where it is also stable.  I would like to derive the fact that 
orbits of this function are cycles, for all elements in the subset where 
the function is injective.  Unfortunately, fingraph.v only contains this 
results for functions that are injective on the whole type.  I can't 
guarantee this.

As a result, I implemented the following two theorems, by mimicking the 
proofs of existing theorems f_finv and cycle_orbit.

Lemma subset_f_finv (T : finType) (S : pred T) (f : T -> T) :
  {in S, forall x, f x \in S} ->
  {in S &, injective f} ->
  {in S, cancel (finv f) f}.
Proof.
move => stable inj x sx.
have stable_i : forall i, iter i f x \in S.
  by elim => [ | i Hi] //; rewrite iterS; apply/stable.
move: (looping_order f x) (orbit_uniq f x).
rewrite /looping /orbit -orderSpred looping_uniq /= /looping; set n := _.-1.
case/predU1P=> // /trajectP[i lt_i_n]; rewrite -iterSr => /=.
have itnS : iter n f x \in S by apply/stable_i.
have itiS : iter i f x \in S by apply/stable_i.
move/inj => /(_ itnS) /(_ itiS) ->.
by case/trajectP; exists i.
Qed.

Lemma subset_cycle_orbit (T : finType) (S : pred T) (f :  T -> T) :
  {in S, forall x, f x \in S} ->
  {in S &, injective f} ->
  {in S, forall x, (fcycle f) (orbit f x)}.
Proof.
move => stable inj x sx.
rewrite /orbit -orderSpred (cycle_path x) /= last_traject -/(finv f x).
by rewrite fpath_traject (subset_f_finv stable inj) ?andbT.
Qed.

Actually, f_finv and cycle_orbit are easy consequences of these two more 
general theorems.  I have the feeling that subset_f_finv and 
subset_cycle_orbit could also be consequences of f_finv and cycle_orbit, 
but I would not qualify them as easy consequences (because one needs to 
change type to use cycle_orbit on a subset type, while subset_cycle_orbit
is about the same function with the same input and output type, 
regardless of the subset being chosen).

I will probably make a pull request, but preparing one takes time, and I 
wished to trigger discussion on this topic ahead of time. What is the 
prevailing opinion on these theorems?

Yves