coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Automation with existential goals

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Automation with existential goals
Date: Wed, 16 Nov 2016 14:38:39 -0500
Authentication-results: mail3-smtp-sop.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-qk0-f170.google.com
Ironport-phdr: 9a23:YZx2ixK0kcO9DznwFtmcpTZWNBhigK39O0sv0rFitYgeKfnxwZ3uMQTl6Ol3ixeRBMOAuqkC0rad6vq+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6zbL9oMRm7ogrdutQIjYZjN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhyAbOjM38mzahNV8gL5UrRm8oxByw5LYbISTOfFjfK3SYMkaSHJcUMhPWSxPAoCyYYUBAOUOP+lXs4bzqkASrRa8HwSgGP/jxzFKi3LwwKY00/4hEQbD3AE4G9wOt3LUo8/pNKcSS++1yrTDwzPdYPNXxzfy9o7Icgw8qvyLX7JwdszRyUgsFwzbilWft5LqMiia1uQIqWeb7u5gWfizhG4grgF8uz6izdoihInOg4Ia0FHE9SNhzYY0I924Uk97bsS+HJterSGWL4R2QsI+Q2FopSY10acKtoK8fCgPzpks2h3Ra+SffoSW/h7uUPydLDR4iX5/Zr6zmQq+/VK9xuD+SsW4yFRHojdfntXSuH0A2Abf5tWJR/dh5EutxziC2gLV5+pZO047j7DbJIQkwrMolpocr0DDHijulUXzlqCWd0Ek9vGx6+Tkfrnqv5GcO5J2hw3iKKgulcu/AeM3MggKQWeX4/iz1Lrm/UHhQbVKiOM5krXBvZzEOcgWorS1DgxV34o59RqzESuq3M4FkXQFMF5JYBeHgJLoO1HKLvD4F/C/g1G0nTdpwPDGOLzhApbTIXjHjrjuY61w60FZyAUpzNBf44hYBa0GIPL2QkPxrsDXDgclMwyoxObqEMly1oQHWW6WHqCZNL7SvkST6+I0I+iMYZcVtyznJ/gk4f7ul345lkUHcamnx5tEIEy/S/9hOgCSZWfmqtYHC2YD+AQkH8Lwj1jXczlVbmqyVqR0wjw6Fo+gEc+XRIergb+M2Cq2NpJTb2FCTFuLFCG7JM2/R/4QZXfKcYdamTseWO38E4I=

On 11/14/2016 10:03 AM, Jonathan Leivent wrote:

...

Coincidentally, I am writing a draft of something I might make into a CEP about just this. It is an extension of the discussion with Hugo in bug https://coq.inria.fr/bugs/show_bug.cgi?id=3918 that he recently prompted me to look at again. My point in this draft will be that in many cases, the above trick keeps proofs solvable, whereas otherwise they become unsolvable - and so perhaps there should be a setting that makes this happen automatically when possible.

See: https://github.com/coq/ceps/blob/master/text/011-coevolving-evars.md

-- Jonathan

[Coq-Club] Automation with existential goals, Klaus Ostermann, 11/14/2016
- Re: [Coq-Club] Automation with existential goals, Pierre Courtieu, 11/14/2016
  - Re: [Coq-Club] Automation with existential goals, Klaus Ostermann, 11/14/2016
    - Re: [Coq-Club] Automation with existential goals, Pierre Courtieu, 11/14/2016
      - Re: [Coq-Club] Automation with existential goals, Jonathan Leivent, 11/14/2016
        
        Re: [Coq-Club] Automation with existential goals, Jonathan Leivent, 11/16/2016