The Coq mailing list

[Venanzio Capretta <Venanzio.Capretta AT sophia.inria.fr>]

Hi,
  here is the trick that I use to "compute" functions defined with an
accessibility predicate in Coq: Since for every argument there is only
one constructor of the accessibility predicate that can be applied, you
can generate the proof of accessibility automathically:

fAcc: A -> Set
f: (x:A)(fAcc x) -> B.

To compute (fAcc a) for a specific a, first generate automatically the
proof of (fAcc a):

Definition ha:(fAcc a).
  Repeat Constructor.
Defined.

Eval Compute in (f a ha).

You can also prove and compute at the same time:

Definition result: B.
  Apply (f a).
  Repeat Constructor.
Defined.

Eval Compute in result.


EXAMPLE:

-------------------------------------------------
Require Arith.

Fixpoint div2 [n:nat]: nat:=
Cases n of
  O => O
| (S O) => O
| (S (S n)) => (S (div2 n))
end.

(*
f 0 = 1
f n+1 = n*(f (div2 n))
*)

Inductive fAcc: nat -> Set:=
  facc0: (fAcc O)
| faccS: (n:nat)(fAcc (div2 n))->(fAcc n).

Fixpoint f [n:nat; h:(fAcc n)]: nat:=
Cases h of
  facc0 => (S O)
| (faccS n h) => (mult n (f (div2 n) h))
end.


Definition fAcc10: (fAcc (10)).
Repeat Constructor.
Defined.

Eval Compute in (f (10) fAcc10).

Definition result: nat.
Apply (f (10)).
Repeat Constructor.
Defined.

Eval Compute in result.

--------------------------------------------------


Bye,
  Venanzio