The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi,

  I think Michael refers to saturation by forward hints and I think indeed implementing this proof strategy of saturation properly and efficiently would be much easier using Ltac 2, keeping a data structure around to know which hypotheses were “saturated” before and which hypotheses they produced without doing expensive “did I do this already?” checks, ie an explicit state manipulation. Programming this with only the logical programming features of typeclasses eauto is a fun intellectual exercise (I remember hacking it up a few times) but I don’t think it’s the right language for implementing such a proof search strategy.

My 2 cents,
— Matthieu

Le mar. 13 mars 2018 à 06:29, Armaël Guéneau <armael.gueneau AT ens-lyon.fr> a écrit :

Hi,

This is a cool writeup Théo, thanks. However after reading Michael's
second message, I was thinking of something a bit different for "forward
reasoning" that what you are describing in that paper.

The way I see it, what you describe with the shelve trick is a way of
doing progress on the goal by backward reasoning, without necessarily
solving it. What I was thinking after reading Michael's explanation was
more something that would deduce more hypothesis from the current set of
hypothesis, using lemmas in a hint base ("saturating" the context in
some sense?).

Michael, is this actually what you were doing? If so, it would indeed be
something I would be very interested in having (and I can imagine how it
requires many hacks to be implemented using typeclasses eauto...).

— Armaël


On 12/03/2018 17:58, Théo Zimmermann wrote:
> Dear Michael,
>
> You may be interested in this 2-page article where I explain how to use
> typeclasses eauto to do forward search in the way that Matthieu suggested:
>
> http://www.theozimmermann.net/TTT2017/abstract/coq-prolog.pdf
>
> Best regards,
>
> Théo
>
>
> On 12/03/2018 16:24, Soegtrop, Michael wrote:
>> Dear Matthieu,
>>
>>  
>>
>> what I tried with eauto and typeclass eauto is to modify the goal to
>> True /\ old-goal, split the /\ and use eauto (or typeclass eauto) to
>> solve True, remember the new hypothesis created by forwarding and
>> “transport” these to the context of old-goal – a fairly tricky and
>> fragile process. Is this essentially what you propose? The main
>> problem was that it was fairly fragile – sometimes “transporting” the
>> new hypothesis from one goal context to another fails cause of subtle
>> dependencies, and it was terribly complicated to debug this.
>>
>>  
>>
>> I abandoned this and now use some “collection” tactics. I add to the
>> tactic be defining a new one which has new functionality and also
>> calls the old collection tactic. Then I define a tactic notation,
>> which is constantly redefined to call the top level collection tactic.
>> The tactic notation I call in an extern hint. There are a few things
>> on top like for each collection I have sub tactics with various
>> priority levels and so on. If I remember right, Jonathan Leivant
>> proposed this approach to me here on the list, and somehow I sticked
>> to it. Knuth definitely would have put it into appendix D.
>>
>>  
>>
>> It somehow works, but it is far away from being as flexible or as
>> efficient as I would like to have it. This forward backward split
>> works efficient in the sense that the number of backtracks is on
>> average no more than 3 times the total proof depth of eauto (even if
>> it is 100 or so). So it is linear with search depth, but the
>> individual steps with all the guarding and hacking are fairly slow.
>>
>>  
>>
>> Best regards,
>>
>>  
>>
>> Michael
>>
>> Intel Deutschland GmbH
>> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
>> Tel: +49 89 99 8853-0, www.intel.de
>> Managing Directors: Christin Eisenschmid, Christian Lamprechter
>> Chairperson of the Supervisory Board: Nicole Lau
>> Registered Office: Munich
>> Commercial Register: Amtsgericht Muenchen HRB 186928
>>
>