The Coq mailing list

[Xuanrui Qi <xuanrui AT cs.tufts.edu>]

Hello all,

This looks really weird to me. 

> `Program` often produces humongous functions

While this is generally true, I'm not sure it's the case here. You can
print the term and see that its size is not really humongous.

I tried using `Function` instead of `Program Fixpoint` and changing the
Defined into a Qed, but nothing changed. It could be the non-opaque
obligations thing but I'm not entirely sure.

It seems like a Coq bug to me now...

Best,
Xuanrui

-- 
Xuanrui Qi

xuanrui AT cs.tufts.edu
me AT xuanruiqi.com
https://www.xuanruiqi.com


On Sat, 2019-09-21 at 00:47 +0000, Jason -Zhong Sheng- Hu wrote:
> I suspect that Solve Obligations closes proofs transparently, which
> should consume much time to compute something irrelevant.
> 
> https://coq.inria.fr/refman/addendum/program.html#coq:flag.transparent-obligations
> Program — Coq 8.9.1 documentation
> We present here the Program tactic commands, used to build certified
> Coq programs, elaborating them from their algorithmic skeleton and a
> rich specification .It can be thought of as a dual of Extraction.The
> goal of Program is to program as in a regular functional programming
> language whilst using as rich a specification as desired and proving
> that the code meets the specification using the ...
> coq.inria.fr
> 
> > Controls whether all obligations should be declared as transparent
> (the default), or if the system should infer which obligations can be
> declared opaque.
> 
> Thanks,
> Jason Hu
> https://hustmphrrr.github.io/
> From: 
> coq-club-request AT inria.fr
>  
> <coq-club-request AT inria.fr>
>  on behalf
> of Abhishek Anand 
> <abhishek.anand.iitg AT gmail.com>
> Sent: September 20, 2019 8:35 PM
> To: coq-club 
> <coq-club AT inria.fr>
> Subject: Re: [Coq-Club] Debugging an apparently diverging Coq program
>  
> Perhaps they forgot to instantiate the atom type?  the computation
> would get stuck on (x == x'). `Program` often produces
>  humongous functions.
> 
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
> 
> 
> On Fri, Sep 20, 2019 at 5:15 PM William J. Bowman <
> wjb AT williamjbowman.com>
>  wrote:
> > All,
> > 
> > At the following URL is a model of a language with capture-avoiding 
> > substitution
> > that a student wrote:
> > 
> >   https://gist.github.com/wilbowma/acf125222c64ff715a33b26a0ce8b4ab
> > 
> > The program looks (to me) like it ought to terminate quickly, and
> > it's proven
> > terminating using Program, yet when we run the substitution
> > function on a small
> > example... coqtop eats about 20 GB of memory and doesn't terminate
> > within 5
> > minutes.
> > I'm using Coq 8.9.1 on MacOS 10.14.2; the same behavior is also
> > observed on
> > Windows 10.
> > 
> > I'd appreciate any help debugging this.
> > 
> > --
> > William J. Bowman