The Coq mailing list

[Théo Winterhalter <theo.winterhalter AT ens-cachan.fr>]

Hello,

I had some similar troubles. Some obligations might need to be proven using 
Defined if they are likely to produce computations. This includes singleton 
elimination, meaning that unfortunately sometimes proof terms produced by 
omega or such will block computation.

To avoid computing all the unnecessary obligations, using `Eval lazy` instead 
of compute might solve the problem. As opposed to the other, I would use as 
much transparent things as possible.

Also, it may be that you wait for some equality to be refl, but Program often 
use Jmeq_eq as an axiom.

There is also Equations which you can use without it adding axioms. It should 
replace Program someday I expect.

> Le 21 sept. 2019 à 05:40, Xuanrui Qi 
> <xuanrui AT cs.tufts.edu>
>  a écrit :
> 
> 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
>