Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi again,

On 27/03/2012 23:46, Frédéric Chyzak wrote:
> For some reason, I need to define a factorial function with argument from 
> int, 
> according to the usual definition on non-negative numbers and being zero on 
> negative numbers.  The definition that I found (appended below, just for 
> reference) requires two functions: my first (naive) attempt was by trying 
> an 
> induction on an int.  I then realised the definition of int in terms of a 
> CoInductive.  This raises two questions:
> 
> 1. What is understood by a CoInductive?

The type of relative numbers is not recursive, so the only induction on such a
type is trivial and there's no use to generate induction principles that will
never be used. One side effect of using CoInductive instead of Inductive is 
that
it doesn't generate automatically induction principles, whereas Inductive 
does.

Moreover it's a common thing in the ssr library to use CoInductives instead of
non recursive Inductive, but I can never remember why ... so ask Georges.


> 2. Is there some way to do a direct Fixpoint definition based on the nat 
> behind 
> the Posz/Negz (in a single function)?

You could use the (absz : int -> nat) function, for which the notation is 
`|n| in
nat_scope. However in this particular case you may like not to use an 
induction
over `|n| but really proceed by case analysis like you did. But instead of
redefining factorial on nat, you should use the one from the library n`! :

Definition Factorial (n : int) :=
  match n with
  | Posz m => m`!%:Z
  | Negz _ => 0
  end.

Or, in a more ssreflect style :
Definition factorialz (n : int) : int := if n is m%:Z then m`! else 0%N.

You may even want this factorialz to have values in nat (but it depends on the
theory of factorialz you may build and its use) :
Definition factorialz (n : int) : nat := if n is m%:Z then m`! else 0%N.

Best,
-- 
Cyril Cohen