coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Manual proof terms definitions and typechecking
- Date: Tue, 18 Apr 2023 14:55:21 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay8-d.mail.gandi.net
- Ironport-data: A9a23:RXo2C6J/xi74y4NQFE+RGJElxSXFcZb7ZxGr2PjKsXjdYENShjcOz 2JMWTrTbPeCY2OkeNEia4vn8xtV75bSyNdlSgUd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWCfg70s9JIGjhMsfnb9Eo/5K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LuU1m0+vNgUwIPJZQDq89FWTpj8 9kTEWVYBvyDr7reLLOTUORoj9VzacWtOYoevjdvxDfVDLAgTIyrr6fiv4YHmmhowJkeRrCEP 5NxhTlHNHwsZzVAM1oLAZR4k+asjHTlbxVDq0OOpqsy5mXJigp8zNABNfKIIYLUHZQLxy50o EqF21j9JzgIMuWixGWB8i6ppNOWhwD0Ddd6+LqQrK8y3wHOngT/EiY+Xlyi5PK9l0SWQMNaM 0VS+yw0rKF0+lbDczXmdwe1pHeV7lsQHd9ZEul85wiLxquS5QuFboQZctJfQPwE7PYwS2Np7 0eQhILAN2Q0nbuwQkvIo994sgiOESQSKGYDYwoNQg0E/8TvrekPYvTnEIwL/Emd0IWdJN3g/ 9yZhHRu1+hD16bnw43hpguX3FpAs7CUFlZd2+nBYo6yxi1DDLNJiqSy5FzS/KYFIMCcR1iF+ ncNncSfquYDEflhdRBhos1TR9lFBN7falUwZGKD+bF8r1xBHFb/LOhtDMlWfhsBDyr9UWaBj LXvkQ1Q/oRPG3ChcLV6ZYm8Y+xzk/i5Som7DKqFN4QVCnSUSONh1H81DaJ39z63+HXAbYllU XtmWZr1XCZGYUiZ5GToGo/xLoPHNghklDuMGc2jp/hW+bWXYnKUAawMKzOzghMRssu5TPHu2 48HbaOikk0BOMWnO3W/2dNNcTgicCdjbbio8ZA/XrDYeGJORjp+Y8I9NJt6JuSJaYwOyryXl px8M2cEoGfCaYrvc1jQNSE5OO+2B/6SbxsTZEQRALph4FB7Ca7H0UvVX8JfkWAPpL0zn81nB eIIYduBCflpQzHKsWZVJ5rkoYAoMFzhiQuSNmD3KHIybrxxdTzvo9XERwrI8DVRLyyVscBln aas+DmGSrU+RiNjLv3sVtSR832Ls0MwpsdOTmrTA9wKeEzT4IlgcCPwqfksIvAzExbIxxrE9 gC0BR03i7TqiNY21NyQham7sJqbScVjLGVZAmPe0+6XNDbbzEWn04RvQOaFRhGDdWLWqYGJR /RZ8OH4C9IDxG11iotbF6156I4P/P79juZ+4iU9O1uTdHWtKLdrAkfe7Pl1rqcXm4No41qna HyA6vxxGOuvOvq8NHUzOQB8TOCI9c9Mqwno9f5vfXnLvn5mzoGmD3dXEQKH0hFGDb1PN4gg/ +ctlegW5yG7iTsoKty2tT9VxUvdMk0/V7gbib9CDL/JkgYLznRwUa7YAALy47CNbIxCCVl1A zm2gKGZua9Q6HCfeFUOFF/M/9Fnu7IwhD5wwmQvHW+5wuj+uqdv3Tl60ygGcQBO/xAWj8NxI jdKMmN2F4Wv/hBpptpKBGS+EltFGBemxF3VzgYNmEb4VGitbHTGd0cmCNaO/WcY0mNSRSda9 7em01TYUS7mUcXy/ykqU2tnlqDTdsNw/Qj8h8yXJcSJMJ0kaz7DgKX1R243hzb4IME23mvrm PJL+btuVKjFKiIgma03JI2E37A2ShrfBmhjQ+lkzZwZD1PnZzC+9jifGX+fIvoXCaTxzna5L MhyKuZkdRe0jn+Opw9GI588GeZ/mfpx6ecSfr/uG3U9jIKeiThX4bbw7Sn1gVE5T+p+yfgdL pzjTBPcM2iyq0YNpUrzgphqBm6Kb+MARjXA58Gu0eBQF5s8oOBmKk4z9b2vvkSqCghs/jPKn QXlfaLm6fZr9t1wrbvND69GOV2VKMzyZsuM4guco9RDVvKREMbs5ic+iEjrABRSBpQVA+9Ir LWqtMXm+n/FsJIdcXHrq7PYG4ZnvcyNDfdqaOTpJ3xkrA6+cc7L4Spb3VunKJZMwehv1uP+S ySWMMKPJMMoAfFDz3hoag9bIRYXK4LzSozC/SqdjfC9OiIx4Dz9DuGM1CHWNDlAVyoyJZfBJ Bf+uK+u6vBmvY18PkI4KM88MaBoAm3IePUAR4T9uwDNWyPsyhmHt6D5nBUt1SDTBzPWWIzm6 JbCXV7leA70pKjMy8pDvpdvugEMSkxwmvQ0YllX7useZ+pW14LaBb913VQ65pBofujazpz8b SCdKWdkDCz8WXJLeBPw4ZLlUxv36ini/DvmDmRBwq9WQ37e6EC87H9J7SRx+HR3fz7u1qehJ M12FrjYIE2q2p8wLQoMzqXTvAqkr882AloT+lHmkM33BhsER7MHyBSN2eaLuTPvS6nwqakAG YT5qa2ojq12pY4d3PuMo0JoJSw=
- Ironport-hdrordr: A9a23:XR7TUaG8E0I4UABXpLqE5ceALOsnbusQ8zAXPjNKOH9om6uj5q eTdZUgpHvJYVkqNU3I9erwWpVoBEmskKKdgrN8AV7BZmPbUQKTRekI0WKh+V3d8kbFmNK1u5 0AT0EzMrLNMWQ=
- Ironport-phdr: A9a23:Zo9ZPhzGM/9gCYTXCzLRwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z hGZv6Q9xwKXFazgqNt6yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6y9pHJfQlFgDmwbbxyI Ri3sA7cqtQYjYx+J6k+zRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3Q qBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4 qx2ThLjlSUJOCMj8GzPicJ+gq1Urxy8qRJhzY7aYIOaO+ZxcK7GYdMXRnBMUtpNWyFPAI6xa ZYEAeobPeZfqonwv1oAogGiAgmwHuzvzCJDiH733a0+yOsuDxvG3BA9FN8Jv3Tbtsv6NLsIX uCz1qXIwjTDb/dN1jjj8ojIbgssoeqPXbNwasrRykgvFwbAjlqOs4zpJTWV2foRs2WC6edrS O2ghXI9pQ5rvjiv2tkjipPPho8N11zK+iV3zZo1KNGlS0N2Yd+pHYdRui+VKYd6XN0uTmNnt SsmzrAKpZG1cScFxpk7xhPSd/yKfoaU7h79SOucITF1j29mdrKnnxu+71Wsx+/mWsS2zFpGt DdJn9rCu3wXyRDf9tWLR/1g9Um7wzmPzRrc6uRcLEA0i6XbL5khz6YqlpUNtUTMBC/3lUbvg KCLbEkk//Kn6+XjYrn8qZ+TLYl0hRz/Mqg0nMywH/g4PhAPX2id5+u8yKXu8VPkTLhIlPE7k LXVvIrHKckYqKO1GRFZ3po+5xqnCjepytUYnX0JLFJffxKHipDkO17UL//mEfewmVKsnC1kx /DHOr3uGYvCLmLfkLr6ZrZ96E5dyBEwzdBe4pJUD68OIOjpVk/3qtPYEgc1MwqvzOn/EtVyy pseWX6TAq+eKK7erEeE5vgzLOmUeI8VpDH9JuA56P7plH81gEMSfa203ZQMc324BfRnI0CBY XX2mNsBEGEKvhA/TOPwklGCXyRTND6OWPc34Sh+A4a7B6/CQJqsifqPxnSVBJpTM09PiUyFF z/HdoGOVu0QIHadK8J9mzpCWrmlQYI7yTm1tx7hyLtiK+fOvCsVqcSwh5BO++TPmERqpnRPB MOH3jTVJ4kVtmYBRjttmbt6vVQ40VCbl65xn/1fE9VXofJPSAYzc5DGnKRhE96nfAXHc5+ST Uq+BM28CGQ+R98tytlIbEd5Edi4kjjY3DuxAL4QkrGRQpo57vGUxGD/cv500G2Oz6w9lx8jS 8pLO3ehg/tw/gXPDoiPnESdnauwaYwH3z/W92aGyGeU+kdVTF04Sr3LCFYYYEaettHl/gXCQ rupXKwgKRdEwNWeJ7FicNDthEQWAfulPd3fZyS+kmG8BFCOy6/kgJPCXWIb0W2dDUEFl1tW5 nOaLU0lAT/npWvCDTtoHFapYkX28OA4pmnpBkkzhxqHaUFszd/XslYcmOCcRvUP37kFpDZpq jN6G0y41s7XDNzIrhRofaFVa9cwqFld0meRuwt4N52mZ6ds4zxWOwt+sl/n0VN4C4FKnNI2h Ggp3RFxKKed3UkHcT6EnNjxNrDRNmju7UW3caeFvzOWmN2S+6oJ9LE5swC55V7vSRJkqiU8l YMNiij5hN2CFgcZXJPvX1xi8hF7o+qfeSwh/8bP0mUqN6CoszjE0tZvBe0/yx/mcc0MVcHMX AL0DcAeANCjbeIwnF38JB0NMfxb8ug7PseseuGa8LWoLf1jnTejgH4B5o1hmBHplWI0WqvT0 pAJzuvNlASOWiv1ihGus8T9lJpYTSoRD3G8yC3hCZQXYKBuN9Vuay/mM4i8wdNwgIToUnhT+ Qu4Bl8I78SufAKbc1332QA4OV0/mXW8gmP4yjV1l2psta+DxGnVxPykchMbO2lNTW0kjFH2I IHygcpIFESvagEoklOi6yOYj+BUraljJm+VTkZMdSXsM0l5UbqrtbuHZsNVrpUlrW1bXf+9b laTVrPm60FDjGW8Ry0HlGt9LWnz8pzi+n4ywHqQNnNysGbUdYlryBHT6cadDf9d0zwaRTVp3 DzeB1yyJd6srrD239/ItuGzUX7kV4UGK3C0i9zY8nLrviswWUTs+pL70sfqGgU7zyLhgtxjV CGT6Q35fpGuzKOid+RuYkhvAlb4rct8AIB31IUq1/RykTAXgIuY+X0fnCL9K9JejOjxZXcRT DhNzN/R6gX/xGV4LWOSxIP8U3iHhM1se5PpBwFekjJ49M1MBKqOufZLlCZpq1z+ogPVa/Vng h8Gyuo1638fhuwT/gwg0m/OZ9JaVVkdNivqmROS6tm4p6gCf2ejf4+7009mlMygBrWP8UlMH Wz0cZA4EWps/91yZRjShWbr5NiuK7yyJZoD8weZmBDag61JJYItw7AU0DF/Nzu1vGV5mbRi0 loxhdfj49jBcjQ3u/jnZ3wQfjztOZFJomm03/pUz5bE04vzTMUzSHJVANPpVa76SmtN86u/c V/eS3tl+y3cQ+q6f0fX6V86/SiWTNb0bzfOdCNfko8lH0PVJVQD0lpNA3NlxthgRlrsm5CmK x0xsTkV4hSQRgJk7OVuOlG/V27eoFztcTIoUN2EKwIQ6Ahe5kDTOMjY7+RpHige8Ifz5AqKY neWYQhFFwRrEgSNGkzjM7+y5NLB7/nQB+ywKOHLaKmPruoWXumBxJam2I9rtziWMcDHMn5nB vw9kk1NOBIxU9zegCkKQjcLmjjldcOfrQbsvyExq8m+9LLkUQTj5M2JBqcTedRj9haqgLuSY u6dgCEqTFQQnpgIxHLO1P0exAtI0n4oKGHrSORb83SVFfG1+OcfFRMQZiJtOdEd6qs92lIII svHkpbu0aY+iPcpClBDXFinm8ezZMVMLXvuUTGPTEuNKrmCIiXGhs/tZqbpA7JZgfldsVu/u DKRHlX/Fi+AhiLqVhWqPPsKiiyHdk872sn1YlN2BG7vQcizIAW8K8NyhCYqzKccnH7OPH9Md DQ6dkpMqvuf5CVUg7N5FnALvR8HZaGU3i2e6effMJMft/BmVz91m+xt63M/07JJ7StASZSde QPIo9pnsgHjnq+KwztjFhVHrDpKwoSGoRc6UU083oJDSG3H/RcI4H/WDRkW9YMN4jLHoKNB0 dvOkaf+MnFE/s6GpKMh
- Ironport-sdr: 643e933c_mTpd0FLq09GyrFdTlh2tDpBJLFhA9LwYrm55FlIgeEO3QXK xF8mAiaRm1uXJJPfAVR5tgOVJgMgkTW7E4KiyuA==
> When proving a lemma through reflexivity, I expect unification to run twice:
> once while building the proof term interactively (can be skipped with
> exact_no_check eq_refl) and once at Qed time.
Technically at Qed time is only conversion (no existential variables may
remain), but this does not matter here.
> Alternatively, I could bypass interactive proof term construction and
provide my
> proof as a definition. I would then expect the validation of the term to
take as
> long as the previous `Qed` (i.e. x seconds). Alas, I would be wrong, as it
ends
> up taking twice that time.
Elaboration of the user syntax "(@eq_refl nat 0)" to a term with expected type
"slow = 0" runs unification.
Then the kernel checks the produced term which involves running conversion.
Gaëtan Gilbert
On 18/04/2023 14:51, Matthieu Baty wrote:
Hello coq-club,
I recently ran into a puzzling Coq behavior regarding the typechecking of
manual
proof terms definitions and I would appreciate some pointers. The attached
file
contains a runnable example of what I describe in here.
When proving a lemma through reflexivity, I expect unification to run twice:
once while building the proof term interactively (can be skipped with
exact_no_check eq_refl) and once at Qed time.
Lemma interactive_proof: slow = 0.
Proof.
Time reflexivity. (* x seconds *)
Time Qed. (* also x seconds *)
Alternatively, I could bypass interactive proof term construction and provide
my
proof as a definition. I would then expect the validation of the term to take
as
long as the previous `Qed` (i.e. x seconds). Alas, I would be wrong, as it
ends
up taking twice that time.
Time Definition raw_proof: slow = 0 := (@eq_refl nat 0). (* 2x seconds *)
This is not a `Definition` issue, as using `Check` with the appropriate type
annotations yields the same behavior.
Time Check (@eq_refl nat 0: slow = 0). (* also 2x seconds *)
Tactics in terms can help with this: replacing the body of the previous
definition with ltac:(exact_no_check (<my_proof>)) makes it run in the time I
expect it to (x seconds). I can't see why all proof definitions don't behave
like this.
What exactly is going on? Is there a good reason for this behavior?
Thanks,
Matthieu Baty
- [Coq-Club] Manual proof terms definitions and typechecking, Matthieu Baty, 04/18/2023
- Re: [Coq-Club] Manual proof terms definitions and typechecking, Gaëtan Gilbert, 04/18/2023
- Re: [Coq-Club] Manual proof terms definitions and typechecking, Matthieu Baty, 04/20/2023
- Re: [Coq-Club] Manual proof terms definitions and typechecking, Gaëtan Gilbert, 04/20/2023
- Re: [Coq-Club] Manual proof terms definitions and typechecking, Matthieu Baty, 04/20/2023
- Re: [Coq-Club] Manual proof terms definitions and typechecking, Gaëtan Gilbert, 04/18/2023
Archive powered by MHonArc 2.6.19+.