coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] ill-typed evar instantiated (caught later at Qed)
- Date: Mon, 18 Jan 2021 16:11:44 -0800
- Authentication-results: mail3-smtp-sop.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-io1-f41.google.com
- Ironport-phdr: 9a23:n1yIURf3QWbJ4f84o2CjOYPElGMj4u6mDksu8pMizoh2WeGdxcW4YB7h7PlgxGXEQZ/co6odzbaP4ua4CCdZuN7B6ClELMUTEUddyI0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/Lqs90AfFr39Hd+hL2G9jOFafkwrh6suq85Nv7iZdt+g9+8JcVKnxYrg1Q6FfADk6KW4++dfltQPETQuB53scVnsZnx9VCAXb7x/0Q4n8vDLiuuVyxCeVM8v2TaspWTu59KdkVAXoiCYcODEn9mzcl9F9g7haoBKloBx/3pLUbYSIP/dwYq/RYdUXTndHU81MVSJOH5m8YpMAAOQBM+hWrJTzqUUSohalHwagGPnixyVUinPq36A31fkqHwHc3AwnGtIDqGjZo871NKcTSuC1zLfHzTbeZP5K3zfy8o7IfQ08qvyLR71/asrRyUg0FwPFkFqQqpbpMCmT1usXtWiU8vBsVeOui247pAF8uTevxsI2hYnIgoIZ0EzL9SJ8wIssI9CzVUF0b8K+HpRKqyGaK5V5QtkkQ2xwpis0yqMLtIO0cSYF1Zkr2RDSZ+KEfoWU7B/tVPidLDh8iX9nZb6yhQu//EigxOD+VcS50kpGojRbntTPtX0A2Rre4dWJRPt6+0euwzeP1wbL5+5YJkA0j6zbJIAlwr40jJYcr1nMHjLwlU7rj6GWbl0p9va05+njeLnrpZ+RO5Vphgz/M6kigMOyDfk+PwMTRWaU4/6826fm/UDhQLVFkPk2kq7BvZDfP8sbp6q5DxZU0oYk9hqzFjmm3dsFkXUdI1JFfxWHj4ftO17QOvz3EfC/g1G0nDdqwfDJIKHhD43TInTflLrtZ7Vw5k5GxAYuzN1S5ohYB74cLP7rX0/+rt3YDhs3MwyuxObnDc1w2ZkFVmKPA6+ZK6PSvkGL5u41OeaMYpUauDDgJPQ/5v7ujGM5mVAGcKmm2JsYcnG4HvB8L0qFZnrsh88NEX0WsQomUOzqlFqCXCZPaHa1RqIw/y00CIa7DYjYXY2tm7yA3CKjHpJMfGxGC1aMEW3pd4qeQfsMZjiScYddlWkPUqHkQIs831n6vwjjjrFjM+D8+ysCtJul2sIjtMPJkhRn3DZ0Dt+d3mLFZmd9mG9AEzY83KFkoUF+jF6F2K50xf1ZCdN76PZAUwN8PpnZmb8pQ+vuUx7MK4/aAG2tRc+rVGloH4ABhuQWakM4IO2MyxXK3i6kGbgQzuXZC5k986aa1H/0dZ8klyT2kZI5hlxjefNhcHW8j/cmpQfWDo/N1U6ekvTyLPlO7Gv27G6GiFG2kgRYXQp3C/iXWHkeYg7Xqo286B+bCbCpDrsjP01KzsvQcqY=
In large proof, I was able to get an evar instantiated by an ill-typed term. I minimized it down the following example:
Require Import ZArith.
Open Scope Z_scope.
Lemma xx : exists f, (exists x, x=1) -> 1 + 2= f 2.
eexists.
intros xx.
destruct xx.
rewrite <- H.
Fail instantiate (1 := fun _ => x+2).
match goal with
[ |- ?L = _ _ ] => instantiate (1 := fun _ => L)
end; reflexivity. (* succeeds! *)
Qed. (* Error: No such section variable or assumption: x. *)
It is surprising why `instantiate` didn't typecheck the term. Also surprising is that it works correctly in the following variant:
Open Scope Z_scope.
Lemma xx : exists f, (exists x, x=1) -> 1 + 2= f 2.
eexists.
intros xx.
destruct xx.
rewrite <- H.
Fail instantiate (1 := fun _ => x+2).
match goal with
[ |- ?L = _ _ ] => instantiate (1 := fun _ => L)
end; reflexivity. (* succeeds! *)
Qed. (* Error: No such section variable or assumption: x. *)
It is surprising why `instantiate` didn't typecheck the term. Also surprising is that it works correctly in the following variant:
Lemma xxx : exists f, (exists x, x=1) -> 1 = f 2.
eexists.
intros xx.
destruct xx.
rewrite <- H.
Fail match goal with
[ |- ?L = _ _ ] => instantiate (1 := fun _ => L) (* Error: Instance is not well-typed in the environment of ?f. *)
end.
Abort.
eexists.
intros xx.
destruct xx.
rewrite <- H.
Fail match goal with
[ |- ?L = _ _ ] => instantiate (1 := fun _ => L) (* Error: Instance is not well-typed in the environment of ?f. *)
end.
Abort.
[abhishek@optiplex ~]$ coqc -v
The Coq Proof Assistant, version 8.12.1 (November 2020)
compiled on Nov 23 2020 17:05:44 with OCaml 4.07.1
The Coq Proof Assistant, version 8.12.1 (November 2020)
compiled on Nov 23 2020 17:05:44 with OCaml 4.07.1
Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/- [Coq-Club] ill-typed evar instantiated (caught later at Qed), Abhishek Anand, 01/19/2021
Archive powered by MHonArc 2.6.19+.