The Coq mailing list

[Fl�vio Leonardo Cavalcanti de Moura <flaviomoura AT unb.br>]

Hi there, 

        I defined the following recursive function:

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.


As expected 


"Eval compute in (prod_in 0 1)" returns 0, but if I declare a variable m
of type nat

"Eval compute in (prod_in 0 m)" doesn't evaluate to 0. In fact, Coq
returns

     = (fix prod_in (n m : nat) : nat :=
          match n with
          | 0%nat => 0%nat
          | S j =>
              match m with
              | 0%nat => 0%nat
              | S i =>
                  if (fix F (n0 : nat) :
                        forall m0 : nat,
                        {(n0 <= m0)%nat} + {(S m0 <= n0)%nat} :=
                        match
                          n0 as n1
                          return
                            (forall m0 : nat,
                             {(n1 <= m0)%nat} + {(S m0 <= n1)%nat})
                        with
                        | 0%nat =>
                            fun m0 : nat => left (S m0 <= 0)%nat (le_O_n
m0)
                        | S n1 =>
                            fun m0 : nat =>
                            match
                              m0 as n2
                              return
                                ({(S n1 <= n2)%nat} + {(S n2 <= S n1)%
nat})
                            with
                            | 0%nat =>
                                right (S n1 <= 0)%nat
                                  (gt_le_S 0 (S n1) (lt_O_Sn n1))
                            | S m1 =>
                                match F n1 m1 with
                                | left a =>
                                    left (S (S m1) <= S n1)%nat
                                      (gt_le_S n1 (S m1) (le_lt_n_Sm n1
m1 a))
                                | right b =>
                                    right (S n1 <= S m1)%nat
                                      (gt_le_S (S m1) 
                                         (S n1) (le_lt_n_Sm (S m1) n1
b))
                                end
                            end
                        end) i j
                  then m
                  else
                   (fix mult (n0 m0 : nat) : nat :=
                      match n0 with
                      | 0%nat => 0%nat
                      | S p =>
                          (fix plus (n1 m1 : nat) : nat :=
                             match n1 with
                             | 0%nat => m1
                             | S p0 => S (plus p0 m1)
                             end) m0 (mult p m0)
                      end) m (prod_in n i)
              end
          end) 0%nat m
     : nat

I see no reason to explain why the first match (the most external one)
cannot be solved, once n is 0 in this case. Could it be related to the fact 
that the recursive argument is the second one?

Cheers, 

Flávio de Moura.