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] simpl problem
- Date: Mon, 26 Aug 2019 16:03:32 -0700
- 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-f43.google.com
- Ironport-phdr: 9a23:7EIm7By4++JblfPXCy+O+j09IxM/srCxBDY+r6Qd2+oVIJqq85mqBkHD//Il1AaPAdyBrasZ1qGP7ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVmjaxe65+IRW2oAneq8UbgJZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8N/jKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMMPpDoIn9plsOthu+ChevBOjy1jJIgGX53asn3O88FgzJxhcvH9IPsHTPrNX6KqQSXfqvw6nO1zrDae5Z1S386IjJbhAhruqBXb11ccXLyEkvExnJgUmXqYzgJj6Y0PkGvWac7+plT+2vimgnphltrTio3McsjJfGhoYRylze6yp23Zs1KNulQ0B4ed6pCIVcuz2eOodsQc4vQ3tktDs7x7AHo5K2cyYHxZI6zBDFcfOHaZKH4hf7WeaRPzh4gHVldaq6hxmo8EigzvTwVsiz0FpXtyZFnNbBu34X2xzc7ciHTfR9/kO/1jqVyw/T7eRELVg1lardNZEh3qY9moQPvUnHBCP7m0X7gLWLekgl++Wk8evqb7v+qp+ZLYB0iwX+Mqo0msy4BOQ1KhIBUHOb+eS9z73j/VP2QLZQgvIslKnWqpbaKtkBqq64Ag9Vzokj5g2wDzejytsYnH0HIEhZdxKAiojlI0vOL+zgDfejn1Ssly9myOzBPr34G5nCMnzDkKr6crtm8E5dyA8zzchF6J5OC7EBJujzWk7ru9DCAB85KV/8/+GyA9Jkk4gaRGjHVqSeKebZtUKCzuMpOeiFIoEP7mXTMf8gstfkjX4imVIeNYCv1J0bICSxFPRnOEWUYjzlhN4HHSELvxYxZOPvgVyGFzVUYiDhDOoH+jgnBdf+Xs/4TYe3jenZhXrpLthtfmlDT2u0PzLoeoGDAapebSuTJopglWVBW+T6DYAm0h6quUnxzL81drOIqB1djorq0Z1O38OWjQs7rGUmAMGU0mXLRGZxzDtRFm0GmZtnqEk48W+tlK1xgvhWD9tWvqobXQIzNJqaxOt/WYn/
simpl seems to get stuck forever below:
Lemma slow (x:Z): 0 <= 2 ^ 64 - x.
simpl. (* seems to take forever *)
The following is fast:
Lemma quick: 0 <= 2 ^ 64 - 1.
simpl.
simpl.
-- Abhishek
http://www.cs.cornell.edu/~aa755/- [Coq-Club] simpl problem, Abhishek Anand, 08/27/2019
- Re: [Coq-Club] simpl problem, Laurent Thery, 08/27/2019
Archive powered by MHonArc 2.6.18.