The Coq mailing list

[Sylvain Boulmé <Sylvain.Boulme AT univ-grenoble-alpes.fr>]

Hello,

Yes, I suspect that there is a lot of noise due to dependent types 
involved in proving the termination of Subst (and maybe some opaque 
constant on the way).

Hence extracting to OCaml is a good idea: on these examples, the 
computations are instantaneous!

I have rewritten the last 2 lines of the Coq files into:

----
Definition subst1 := Subst X (eUni) (eId X) (FV eUni).
Compute subst1.

Definition subst2 := Subst X (eUni) (eAbs Y (eUni) (eId X)) empty.
(* Timeout 300 Compute subst2. *)

Definition subst3 := Subst X (eUni) (eAbs Y (eUni) (eId Y)) empty.

Extract Constant atom => "int".
Extract Constant atomeq_dec => "fun x y -> if x=y then Left else Right".
Extract Constant fresh =>
  "let c = ref 0 in fun _ -> let n = !c in c:=n+1;n".
Extraction "subst.ml" subst1 subst2 subst3.
----

Then, in the "ocaml" toplevel, I write the directive:

#use "subst.ml";;


And, I get the following output:

val subst1 : cCexp = EUni
val subst2 : cCexp = EAbs (2, EUni, EUni)
val subst3 : cCexp = EAbs (3, EUni, EId 3)

Regards,

Sylvain.

Le 23/09/2019 à 17:05, Jason -Zhong Sheng- Hu a écrit :
> have you tried to extract to ocaml or haskell to reduce noise from Prop?
>
> *Thanks,*
> *Jason Hu*
> *https://hustmphrrr.github.io/*
> ****
> ------------------------------------------------------------------------
> *From:* coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf 
> of William J. Bowman <wilbowma AT ccs.neu.edu>
> *Sent:* September 20, 2019 8:46 PM
> *To:* 
> coq-club AT inria.fr
>  
> <coq-club AT inria.fr>
> *Subject:* Re: [Coq-Club] Debugging an apparently diverging Coq program
> I don’t think that’s the problem. Another model does get stuck on that 
> equality and returns the if statement waiting for an interpretation of 
> “==“. I didn’t expect Program to be efficient, but I do expect it to 
> terminate quickly on this example, without using 20 GB of memory.
>
> I’ll see if I can reduce the other model to something as small.
>
> --
> Sent from my phoneamajig
>
> On Sep 20, 2019, at 17:35, Abhishek Anand <abhishek.anand.iitg AT gmail.com 
> <mailto:abhishek.anand.iitg AT gmail.com>> wrote:
>
> > 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 <mailto: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