coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] logical simplification

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] logical simplification
Date: Mon, 14 May 2018 10:14:25 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga01.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:0Skm4hRuh5Ar8FbmLmzO4XQSvtpsv+yvbD5Q0YIujvd0So/mwa6yYBCN2/xhgRfzUJnB7Loc0qyK6/umATRIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfb1/IA+qoQnNq8IbnZZsJqEtxxXTv3BGYf5WxWRmJVKSmxbz+MK994N9/ipTpvws6ddOXb31cKokQ7NYCi8mM30u683wqRbDVwqP6WACXWgQjxFFHhLK7BD+Xpf2ryv6qu9w0zSUMMHqUbw5Xymp4qF2QxHqlSgHLSY0/mHJhMJtkKJVrhGvpxJ9zI7VfI6aO/Vwc7jBfdwBQWdNQtpdWzBDD466coABD/ABPeFdr4TlqVcAsBy+ChejBOPz0D9IgWf20bUn2OomEAHJwAwgEMgQv3TQotn+KaAfUeW0zKbUzTXMde1Z2TPn5IjTdRAuv/6MXa5qccrW0UkiDALFjlOMqYP7OzOZzPgCs2+e7+d5U++klmApqwZ0oje1x8csjJHEhoMTylDY6yp5xJw5KsCmR0N9fNWqE4NQujmHO4ZyXM8uWWFltSYgxrAGp5K3ZisHxZc/yxLCavGKfZKE7xztWeqLPzt1inZodKiiixux7ESs0vDwW8iw3VpQsCZIktbBumoT2xDJ9MSKRf9w80G80jiVzQ/T8PtLIUUsmKrbNZEhxrkwm4IWsUTMBCD6hFj6gLWXdkUi5uin9eDnbq/6qZ+bMo94kgD+MqIwlcyjGek0LwwDU3aB9em81LDv5030TKtQgvA1kaTVqJXaKt4apq69DQ9VyIEj6xOnAjej0dQXgXkHI0hbdxKDlYTpIFbOL+73DfejmVSsly9ryuvHPr3nHpXCMHzDnK39crZ67k5Q0BAzwsxH55JIFrEBJ+r+VVP2tNzBFxM2Lwi0w/v8B9hmzYMfWWePAreDP6/IsF+I4PgvI+iWa4MPtjb9Matt2/m7x3Q+gBoWebSj9ZoRcnGxWPp8aQ3Nan31x9wFDG0ivwwkTeWshkfUAhBJYHPnFZk76z4nEoW+Sc/mR4utibGFlm/vG5xdZmlLDhaXFnrna5+DQ98Nbj6fJolqlTlSBuvpcJMoyRz77Fyy8LFgNOeBonRJ56Km78B84qjorT938DV1C8qH1GTUFjN1mH8FQ3k926Ut+BUhmGfG6rBxhrljLfIW/+lAC15oNJjAwug8ANf3CFqYI4W5DW2+S9DjOgkfC9I8x9hXPBR4FNz611bC2TanB/kekLnZXJE=

Dear Gergely,

you can solve it using intro, rewrite + reflexivity, which you have learned
at this point in SF. Try to think a bit longer and to experiment with the
tactics you have earned so far.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] logical simplification, Gergely Buday, 05/14/2018
- Re: [Coq-Club] logical simplification, Tadeusz Litak, 05/14/2018
- RE: [Coq-Club] logical simplification, Soegtrop, Michael, 05/14/2018
- Re: [Coq-Club] logical simplification, Saulo Araujo, 05/14/2018
  - Re: [Coq-Club] logical simplification, Théo Zimmermann, 05/14/2018
    - RE: [Coq-Club] logical simplification, Soegtrop, Michael, 05/14/2018
      - Re: [Coq-Club] logical simplification, Théo Zimmermann, 05/14/2018
        
        RE: [Coq-Club] logical simplification, Soegtrop, Michael, 05/14/2018