The Coq mailing list

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

Hi Pierre,

Thank you for reply. Sorry for not being clear about problem.

On Tue, Feb 3, 2015 at 8:02 PM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

Hi, I found bizarre that you put f as an argument of moveup.

The idea is, I have a tree and each node has parent. Root is parent of itself. Now I am looking for path from any given node ( n )  to root.  I am storing node as key and its parent as value in map.

Fixpoint f  node map :=

  match find node map with

    | None => None

    | Some parent => if beq_nat node parent then node else find parent map

  end.

This function is not accepted in Coq because Coq is not convinced about termination. If I have well founded relation between node and its parent then it will be convinced.  I am looking for how encode this property as well founded relation. I don't know the path length in advance but all I know is, it will go to root and there my computation will terminate.

Regards,
Mukesh Tiwari

 

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
>
>