The Coq mailing list

[Matthew Brecknell <matthew AT brecknell.net>]

Hi Flávio,

You wrote:
> Fixpoint prod_in (n m:nat) {struct m} := 
>   match n with 
>     | 0%nat => 0%nat
>     | S j =>   match m with
>                  | 0%nat => 0%nat
>                  | S i => 
>                    match (le_gt_dec i j) with 
>                      | right _ => mult m (prod_in n i) 
>                      | _ => m
>                    end
>                end
>   end.

In this case, you can lift the non-recursive parameter outside the
recursive definition:

Definition prod_in (n: nat) : nat -> nat :=
  match n with
    | 0 => fun m => 0
    | S j => fix p m :=
      match m with
        | 0 => 0
        | S i =>
          match (le_gt_dec i j) with
            | right _ => mult m (p i)
            | _ => m
          end
      end
  end.

Then Coq should perform the reduction you expect.

Regards,
Matthew