The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

Dear Jacques,
first of all thank you to use Function. This feature is still under
development.  
Can you please send me a a the full scrip in order to let me do some
experiments ?
The ordering you use is probably not the problem. To answer you
question: When you do a Qed, 
coq defines the function itself and its equation lemma (forall args, f
args = body(f) ), then it computes the graph of the function and derive
from it induction principles attached to the function and also
inversion Lemma. 

Please let me also now which version of coq you are running since many
inefficiencies has been solved in trunk but not reported in 8.1.

Cheers, 
Julien Forest


On Fri, 29 Feb 2008 12:19:54 +0900 (JST)
Jacques Garrigue 
<garrigue AT math.nagoya-u.ac.jp>
 wrote:

> 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>
> 
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club