coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] getting a definition as an equality theorem

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] getting a definition as an equality theorem
Date: Tue, 13 Nov 2018 03:22:30 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-ME1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:kqMntxSv+zH8YWU329i+M5UwVtpsv+yvbD5Q0YIujvd0So/mwa6yYxaN2/xhgRfzUJnB7Loc0qyK6/+mATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfbF/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpx1jzIDbb46YL+Z+cbjHcN8GWWZNQsRcWipcCY28dYsPCO8BMP5coYbjvVsBsx6+BAmxD+3h0DBJiGT23ao80+88FgzI2BIvH8gQv3TRrNT5LqkcXvq7zanTyjXDaehb1i376IjVaBwuv+yDXa9qfcXL1EkiDgXIhUiTp4z9Jz6Y2fgBv3KG4+Z8V++jkXMrpg9wrzS128sglIfEipoIxl3E6Sl12pg5KcG2RUJhf9KoDYdcuzuHO4Z4Rs4uW29otzg5x7EavJO2eSYKx4kpyhLCbvGKd4aF7xDtVOuUPDh1hnFod666ihmv7Eev1/HzW8+p21hQtCVFiMPDtnUV2hzT9MeHTvx981+91DmByg7f9vxILVkzm6TUNpIt27kwmYENvkjZGS/2hVn2g7SRdkU5/Oin9v7rYq38pp+bK497lB3xMrgvmsy4B+Q0KA8OX3WH+eS4073j+k75TK9Wgf0xl6nVqJHaJcIFqa6lGwJY3Zov5wyiAzu60tkUh2QLIVxEdR6dkoTlJV/DLOj9DfilglSslDlrx+rBPr3kGpjDKmbMkK3/crZ4609Q0gQ9wspR5pJPDbEBJun+VVX3tNzFFBM2LRG7w/v9BNpny4MSQXiPDbOBMKPOrV+I4foiLPWLZI8MoTryN/wl5+P1gnIigl8cfayp3YMNZ3yiH/RmJV+ZYXv2jdsbH2cKpFl2cOu/wlaFSHtYY2u4d6M6/DAyToy8R8+XTYe0xbeFwS2TH5tMZ2kABEraQlnycIDRefoWZSeDauNojScDU/D1aYI72BS/8iPz1KFgKMLd/DBeuJ7+ktFosb6A3Sou/CB5WpzOm1qGSHt5yztRFm0GmZtnqEk48W+tlK1xgvhWD9tWvqkbWwEnc5PQ0qpzFoKrA16TTpKyUF+jB+6eL3QpVNtomY0HZVs7Ftm/yBnejXLzXu0l0oeTDZlxyZrymnj8I8EhlCTv6ZJ51hwDb5IKMmerwKli6wLUGojF1V2DkLqnfrgd2yiL83qfyW2JvwdTVwsiCKg=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi coq-club,

Having made a definition f x y z = a b c
how do I get this as an equality theorem that can be used to rewrite
a b c to f x y z?

(I realise I can set it out as a lemma and prove it using unfold, but
I'm assuming it's already there as a theorem that I just need to find
out how to get hold of it)

thanks

Jeremy

[Coq-Club] getting a definition as an equality theorem, Jeremy Dawson, 11/13/2018
- Re: [Coq-Club] getting a definition as an equality theorem, Laurent Thery, 11/13/2018
- Re: [Coq-Club] getting a definition as an equality theorem, Tej Chajed, 11/13/2018
- Re: [Coq-Club] getting a definition as an equality theorem, Dominique Larchey-Wendling, 11/13/2018
  - RE: [Coq-Club] getting a definition as an equality theorem, Jason -Zhong Sheng- Hu, 11/13/2018