coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] refine/apply: do not instantiate any evar

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] refine/apply: do not instantiate any evar
Date: Mon, 4 Nov 2019 18:30:31 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f179.google.com
Ironport-phdr: 9a23:/SNvmxM+LV/sQ7jpe9Yl6mtUPXoX/o7sNwtQ0KIMzox0IvzyrarrMEGX3/hxlliBBdydt6sfzbOP7+u8BiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+Ngi6oRjeu8UZjoZvKLs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZoga1UoByvqR9xzZPKbo6JL/dxZL/RcMkASGZdQspcVSpMCZ68YYsVCOoBOP5VopXmqFsOrBu+HgmsC/3syjRVmnL227c10+I8Hgrb2wEvBckBsHTVrNXuNKcdT+O1wLPSwjXFdfxW3yry5JLJchAgvfGMUql9ccXUyUY1FgPFik+cppDiPzOQz+kAtXWQ4eRnVeKqkWEnqgdxryCzyccrkInJgJwaylTA9Slj3ok6OMC4RUhmatCnCJtdrz+WO5dyT884QGxluDw2xqAHtJO6ZiQG1ZYqyhrZZveaaYaH+AjjW/yUITpghHJqZra/hxGq/Eil0OL8V8203E9LripBj9XAr34N2wHR58WDUPd98UCh2TGA1wDX9O5IO1w7la3eK5I5w74wkIQcsVjbEyPohEn7iLWae0Yk9+Sy9ujqY7TrqoWBO4J2jgzyKqEulda+AeQ8PAgORW+b+eGk2bL55kL5QLRKjuY2kqbHs5DWP94UpqijDA9Tz4kv8Re/Dza60NQXhnQHI1dFdwiGj4jtIV3BPPf4DfKnj1S2jDhr3+zGPqHmApjVMnfDl67hca9h5E5Y1Qo81stS54lUC7EEOPL8QFX9tN3eDh8jMgy72fzrCNtn1tBWZWXaCaiAdajWrFXAsukoOqyHYJIfkDf7MfksofD02ywXg1gYKICj3ZoMaH27Vt1gKkOVKS7liNcACmcHvUw3SuXshBuDUCJcT3m3VqM4oDo8DdT1Xs/4WomxjenZj2+AFZpMazUeUw3eITLTb4yBHsw0RmeSL8tmyGJWULGgT8og0UjrulalmvxoKe3b/iBevpXmhoAstr/j0Coq/DkxNPyzlmSETmV6hGQNHmZk06V2oEg7wVCGg/Eh365oUOdL7vYMaT8UcIbGxrUjWd/3UwPFONyOTQT+Tw==

Is it possible to tell the basic tactics (e.g. refine, apply) to NOT instantiate any evar?

I guess I can guard those tactics by writing a tactic that checks for the absence of evars, but that may be too expensive.

Lemma sss: exists x, exists y, x+y=1+0 /\ y=1.
eexists. eexists.
split.
apply @eq_refl. (* is there a way to make this fail because this would instantiate evars *)

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] refine/apply: do not instantiate any evar, Abhishek Anand, 11/05/2019