The Coq mailing list

[Jacques Garrigue <garrigue AT math.nagoya-u.ac.jp>]

Dear Club,

I am trying to define a function by well-founded induction, and I'm
encountering the following problem: after I have finished proving all
the requisites, when I enter the final Qed, Coq 8.1pl3 takes ages,
becomes huge (500M if I wait more than 10 minutes), and doesn't return
to prompt.
The function itself doesn't strike me as huge, so I'm wondering where
the problem comes from.

Function subtyp_infl (k:kind) (tl12:list typ * list typ) {wf lt_typ2l tl12}
  : option (list (typ*typ)) :=
  match k, tl12 with
  | (true,p)::k', (Tconstr n1 tl1::ul1, Tconstr n2 tl2::ul2) =>
      if eq_nat_dec n1 n2 then
        match variance n1 with
        | None => None
        | Some k1 =>
          app_option (subtyp_infl k' (ul1,ul2))
            (subtyp_infl (map (prod2p true p) k1) (tl1, tl2))
        end
      else match p with
      | P =>
        match expansion n1 with
        | Some t =>
          app_option (subtyp_infl k' (ul1,ul2))
            (subtyp_infl ((true,P)::nil)
              (subst (mkenv 0 tl1) t::nil, Tconstr n2 tl2::nil))
        | None => None
        end
      | N =>
        match expansion n2 with
        | Some t =>
          app_option (subtyp_infl k' (ul1,ul2))
            (subtyp_infl ((true,N)::nil)
              (Tconstr n1 tl1::nil, subst (mkenv 0 tl2) t::nil))
        | None => None
        end
      end
  | (b,p)::k', (t1::ul1, t2::ul2) =>
    if (if p then true else b) then
      app_option (Some((t1,t2)::nil)) (subtyp_infl k' (ul1, ul2))
    else subtyp_infl k' (ul1, ul2)
  | _, _ => None
  end.
Proof.
(* about 1 page of proof *)
Qed. (* here everything stops *)

What is Function doing when I write Qed?
Is this related to the polynomial order I use?

After reading this thread
http://pauillac.inria.fr/pipermail/coq-club/2007/002931.html
I realize that I will probably have difficulties computing with this
function anyway, but it would still be nice to be able to define it...

I also tried defining the function itself in proof mode, using
well_founded_induction, but then I do not have nice induction
principles to manipulate it.

Cheers,

---------------------------------------------------------------------------
Jacques Garrigue      Nagoya University     garrigue at math.nagoya-u.ac.jp
                   <A HREF=http://www.math.nagoya-u.ac.jp/~garrigue/>JG</A>