The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi, I found bizarre that you put f as an argument of moveup. If you do
that then you need more information on this argument. Whereas if you
fix f to the "real" f you showed above, then you can define your
function easily with Function (or Program Fixpoint) using the
"measure" termination tag. This should also work with Program
Fixpoint.

Best regards,
Pierre

Require Import Recdef.
Inductive D : Type := a | b | c | d.

Definition f x :=
  match x with
  | d => c
  | c => b
  | b => a
  | a => a
  end.

Definition beq_D n m :=
  match n,m with
  | a,a => true
  | b,b => true
  | c,c => true
  | d,d => true
  | _,_ => false
  end.

Definition mes n :=
  match n with
  | a => 0
  | b => 1
  | c => 2
  | d => 3
  end.

Function moveup ( n : D ) { measure mes n} :=
  if beq_D ( f ( n ) )  n then n else moveup ( f n ).
Proof.
  intros n teq.
  destruct n;simpl in *;try discriminate;auto with arith.
Defined.


2015-02-03 14:54 GMT+01:00 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
>
>