coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proof automation for large terms?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Eddy Westbrook <westbrook AT galois.com>
Cc: coq-club AT inria.fr, Matthew Yacavone <myac AT galois.com>
Subject: Re: [Coq-Club] Proof automation for large terms?
Date: Fri, 12 Feb 2021 20:53:08 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f180.google.com
Ironport-phdr: 9a23:TIEEfhKr1s3H/oxbu9mcpTZWNBhigK39O0sv0rFitYgfI/nxwZ3uMQTl6Ol3ixeRBMOHsqMC1bCd6/+ocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmT6wbalzIRmoogndqssbipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2UxLjljsJOCAl/2HWksxwjbxUoBS9pxxk3oXYZJiZOOdicq/BeN8XQ3dKUMRMWCxbGo6yYYsBAfQcM+hbrYb9qVwAohSiCgejH+7v1iZIi2Xq0aAgz+gsEwfL1xEgEdIUt3TUqc34OKkQUeCyyqnIzDbDYO1S2Tjj9ofFaR8hofSWUrJxdcrd01UgFwTAjlmetIfoODGV1uMLs2ia7OpvS+avhHA5pAxqrTivw90jiojNho4P1l/E8iB5zZ8zKNalR0F1fcSqH4FMtyGGKYR2WMUiTnlntis7yrALuZ+2cTUXxZknyBPSaOGLfoeL7x/gVOucITN1iGxldb6hhxi+7FWsx+PgWsS13ltGsytInNfSunwT0RHY98aJSvx4/ki72DaP0Rje6u5FIUAolarbNoUuzqQsmZoUtETOGDL9lkbujKKOaEko5uyl5/7kb7jmvJOQKo55hh3kPqgzmcGzHfw0PhYPUmSH5Oix0aDv8EnlT7hPgfA7k7XVvIzfKMgGuKK0BwpY3Zs/5xu9ATer1dsVnXcJLF9AdhKIkYbpNE3LLfD2EPi/jU+jnTF2zP7cJLLhGI/CLn3bnbfhY7l970lcxRI2zd9F5pJUDqgNIOvvWkPsrdDYAAI1Pg+oz+r9B9V90YQeWW2LAqCHKq/drViI5uc3L+mNYo8apir9JuA76/LyiXI1g1wQcKmz0ZcKaX20Au5qL1iabHbwmtsBFH0Fvgs6TOzkkl2CVjtTam6wX6I74DE7CYGmApnHRo+znrOMxyi7HphMaWBHDlCAC2vnd4KBW/sUciKdPtdhkiAYVbimU4IuyRautBbjx7V7KurU5zYXuIn41Nl14u3TjQs9+SZ1D8SbyWGNTnt7knkGRz8sj+hDphlQxluSmZd1mOBSD9tU5LsdTQohKZTGyOt5I9/7XgXAZZGCT1PwEfu8BjRkBNA2xd4NbkJwFv2tixnC22yhBLpf3+iJA5o18a/Y0nXZKMN0ynKA364k2Qp1CvBTPHGr0/YsvzPYAJTExgDAz/7zKfYsmRXV/WLG9lKg+VlCWVcpA6rAVHEbIEDRqIahvxKQf/qVEb0idzB554uHI6pOZMfuiAwfFvjmMdXaJWm2njXpXEva9va3dIPvPl4l8mDdBUwDyV5B+H+HMU0nGn7krTuOVHphElXgZ06q+u57+iu2

On Fri, 12 Feb 2021 08:06:06 -0800
Eddy Westbrook <westbrook AT galois.com> wrote:

> Fellow Coq clubbers,
>
> Does anyone have experience using proof automation and hint databases
> to prove theorems with large terms?
>
> We are working on building a tactic to generate refinement proofs for
> monadic terms. Choosing the proof rule to apply in almost every case
> is rote, and can be done with a simple pattern-match on the top-level
> form of the terms. However, we have found that the automation really
> slows down when the terms start to get large. After profiling the
> tactic, it seems that it is just the “simple apply” rules generated
> by Resolve hints that are taking the majority of the time. I assume
> this is just unification running over large terms?
>
> Anyway, any suggestions would be greatly appreciated!
>
> Thanks,
> -Eddy

One source of inefficiency I hit recently is that Coq slows down
exponentially with the holes in constrs - see:

https://github.com/coq/coq/issues/13798

[Coq-Club] Proof automation for large terms?, Eddy Westbrook, 02/12/2021
- Re: [Coq-Club] Proof automation for large terms?, Andrew Appel, 02/12/2021
  - Re: [Coq-Club] Proof automation for large terms?, Talia Ringer, 02/12/2021
- Re: [Coq-Club] Proof automation for large terms?, Clément Pit-Claudel, 02/12/2021
- Re: [Coq-Club] Proof automation for large terms?, jonikelee AT gmail.com, 02/13/2021