The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

I wrote a factorial function that uses well founded induction on Z:

Require Import ZArith.
Require Import ZArith.Zwf.
Require Import Program.Wf.

Open Scope Z.

Program Fixpoint fact (x:Z) {wf (Zwf 1) x} : Z :=
  (match Z_lt_le_dec x 1 with
  | left _ => 0
  | right _ =>
      match x with
      | 1 => 1
      | _ => x * fact (x - 1)
      end
  end).
Solve Obligations using (
    intros;
    try split;
    try omega;
    try discriminate).

However, I can't evaluate calls to the function because Zwf_well_founded is opaque.

Eval compute in (fact 3).

     = (fix Fix_F_sub (x : Z)
                      (r : Acc
                             (fun x0 y : Z =>
                              (match y with
...
             end) 3 (Zwf_well_founded 1 3) 3 eq_refl)
     : Z

Since I know the depth of Zwf_well_founded's proof tree, I can work around the problem by creating a transparent well founded induction theorem that just unrolls the original theorem's proof tree.

Is there a cleaner solution? Ideally I'd like to prove that Coq can fully evaluate the function for any parameters, but I'm not sure if that's possible.

Theorem Zwf_well_founded' : forall c, well_founded (Zwf c).
Proof.
  intros c x.
  pose (n:=Z.to_nat (x - c)).
  generalize x.
  induction n.
  - constructor.
    constructor.
    apply Zwf_well_founded.
  - constructor.
    constructor.
    apply IHn.
Defined.

Local Obligation Tactic := idtac.

Program Fixpoint fact' (x:Z) {wf (Zwf 1) x} : Z :=
  (match Z_lt_le_dec x 1 with
  | left _ => 0
  | right _ =>
      match x with
      | 1 => 1
      | _ => x * fact' (x - 1)
      end
  end).
Solve Obligations using (
    intros;
    try split;
    try omega;
    try apply Zwf_well_founded';
    try discriminate).

Eval compute in (fact' 3).
     = 6
     : Z