The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hello Everyone,

I have a computation f and domain ( a, b, c, d )  in which I start from d and  move up to fixpoint ( a ).

      f(d) = c

      f(c) = b

      f(b) = a

      f(a) = a ( fixpoint ).

If I write this code in Coq

Fixpoint moveup ( f : nat -> nat ) ( n : nat ) :=

   if beq_nat ( f ( n ) )  n then n else moveup f ( f n ).

Coq will not accept it because it is not convinced about termination.  One idea is certainly iterative function, pass a big number such that fixpoint is reached.  (* Z.iter :  Z -> forall A : Type, (A -> A) -> A -> A *).  Other idea is pass this as a proof ( well_founded relation )  to computation.

Fix
     : forall (A : Type) (R : A -> A -> Prop),
       well_founded R ->
       forall P : A -> Type,
       (forall x : A, (forall y : A, R y x -> P y) -> P x) ->
       forall x : A, P x

How to encode this as well_founded relation. Any paper, idea or related work will be great help.

Regards,

Mukesh Tiwari