The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

   Dear all,

  I have problems with reducing a function defined by means of a Program with a measure. The manual promises:

The reduction is a little more involved, although it works using lazy evaluation;  

  This does not seem to be the case for me. Attached please find a simplified example showing the problem. The [eval] function does not reduce as expected, see the last line. Few comments:

•  I'm showing a simplified example of a problem I have (yes, I know that here [eval] is not recursive),

•  it's for the trunk version of Coq; I don't remember and have a difficult time figuring out what was the syntax for measures over several arguments in Coq 8.2.

•  I changed several things to axioms for space considerations - defining them does not resolve the problem.

   Any help greatly appreciated,
   Adam


Require Import Relations Program Wf.
Set Implicit Arguments.

Section Acc_fun_image.


  Variables (A B : Type) (R : relation A) (S : relation B) (f : A -> B).


  Variable RS_spec : forall x y : A, R x y -> S (f x) (f y).

  Lemma acc_fun_image : forall x, Acc S (f x) -> Acc R x.


  Proof. Admitted.

End Acc_fun_image.


Inductive X : Type -> Type :=
| Nil : X True


| Seq : forall A B, X A -> X B -> X (A * B).

Inductive Res (T : Type) : Type :=


| Ok (res : T)
| Fail.


Definition ctx := { T : Type & (X T * nat)%type }.
Definition build_ctx (T : Type) (x : X T) (n : nat) : ctx := existT _ T (x, n).


Axiom x_measure : relation ctx.
Axiom x_measure_wf : well_founded x_measure.


Program Fixpoint eval (T : Type) (x : X T) (n : nat)
  { measure (build_ctx x n) (x_measure) } : Res T :=


  match x return Res T with
  | _ => @Fail T


  end.
Next Obligation.


Proof with auto.
  unfold MR. intro x.


  apply acc_fun_image with (S := x_measure)
    (f := fun (x : {T : Type & { _ : X T & nat}}) =>


    let xx := projT2 x in build_ctx (projT1 xx) (projT2 xx))...
  apply x_measure_wf.


Defined.

Eval lazy in eval Nil 0.


-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski


The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================