coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] folding under binders

From: Clément Pit-Claudel <cpitclaudel AT gmail.com>
To: coq-club AT inria.fr
Cc: Istvan K Chung <ikdc AT mit.edu>
Subject: Re: [Coq-Club] folding under binders
Date: Tue, 25 Sep 2018 01:12:30 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f48.google.com
Ironport-phdr: 9a23:bzqwghHFDPU00Vo/p11V/51GYnF86YWxBRYc798ds5kLTJ7zp82wAkXT6L1XgUPTWs2DsrQY07WQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOSMn/mHZisJ+j6xVrxyuqBN934Hab5qYNOZ9c67HYd8WWWRMU8RXWidcAo28dYwPD+8ZMOtGq4n6vV4OogW4BQmwHOzh0D5IhmPv0aAk1+QuCxzG0xE+ENIKrX/Zq8n6NL8TUeCp0KbIyS/Mb+5L1jjj7IjFaR8hofSWUrJxdcrd01UgFwTAjliJr4HuIjCb1vwVvmSF8+ZtUfijhm0npg1rvzSix9oghpPGi48W0lzI6yR0zJooKdC9VUJ2YtGpHZ5fui2HNIZ6XsYvTmBptSkkyLALvJy2cDUIxZkmwhPQd+KLfoyG7x/mW+uRLzV1i2lgdb+7gxu96kitx+vhXceuyllKtDBKktzUu3ANyRPT7s+HR+N4/ki72DaP0xnf6+FKIEwpjKbbJZEsz70qmpoctkTDGSD2mEHog6OMakok/e2o5/zmYrXguJCcK5d5hh/iPqkqgMCyAuQ1PhITU2Wa5OiwzrLu8E7hTLVPlPI2k63ZsJ7AJcQco660GxNa0p4i6xajEzim1M4XnWQaI11bfBKKlIfpO1TUL/D5CfezmUijkDBux/zeJL3uHo3NLmTfkLfmZbty90lcyBMqwd9D45JUF6oOLenoWk7xsdzYFgU2Pxa1w+bhEtV915kRVXiBAq+DY+vutgqD4ftqKO2RbqcUviz8Ir4r/a3Al3g8zHQZ/Kyk24cgUHGkW99iKliVbH6k1twZEHsBugMjQOHuoFKHWD9XIX21WvRvtXkAFIu6ANKbFciWi7ub0XLjR8wEViV9ElmJVEzQWcCBUvYIZjiVJ5Y4wDMBXLmlDYQm0EP37VOo+/9cNuPRvxYgm9f7ztEsvr/ckBgz8Xp/CMHPizjQHVExpXsBQnoN5I46oUF5zQ3eg61xgvgdBMMKov0VAkE1MpnTy+E8ANf3CFrM

On 2018-09-24 23:41, Abhishek Anand wrote:
> Is there a general advanced fold tactic such that `advanced_fold add2`
> changes "n+2" to "add2 n"?

I usually use [change (?n + 2) with (add2 n)]. It works in Coq 8.4, but
unfortunately not in 8.8, apparently. I don't know when it stopped working.

Another similar example from a few months ago still works:

Goal (forall n : nat, ((n >= 0) -> False) -> False) -> True.
intro.
repeat change (?a -> False) with (not a) in H.

Clément.

[Coq-Club] folding under binders, Abhishek Anand, 09/25/2018
- Re: [Coq-Club] folding under binders, Clément Pit-Claudel, 09/25/2018
  - Re: [Coq-Club] folding under binders, Hugo Herbelin, 09/25/2018