coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] "Sequence is associative." (?)

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] "Sequence is associative." (?)
Date: Thu, 24 Jan 2019 22:43:15 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.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:+lXMNxAw9nS9Z6XLQsAiUyQJP3N1i/DPJgcQr6AfoPdwSPT8o8bcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xbrhCupx1jzIDbb46YL+Z+cbjHcN8GWWZNQsRcWipcCY28dYsPCO8BMP5coYbjvVsBsx6+BAmxD+3h0DBJiGT23ao80+88FgzI2BIvH8gQv3TRrNT5LqkcXvq7zanTyjXDaehb1i376IjVaBwuv+yDXa9qfcXL1EkiDgXIhUiTp4z9Jz6Y2fgBv3KG4+Z8V++jkXMrpg9wrzS128sglIrEipoax13A7yl13YI4KN2iREJmf9KoDIFcuzyUOoZ1Ws8iTX9ntSUmxrADvJO2eCsHx48oyhPadvCKfZaH7Q/mWeafPzh1h25pdbehixmp/0itxevxXdSu3llQtCpKiNzMu2gN1xPN7siHTeNw81uv1jiSywzf9/hIL0c7m6bGMpIhxaU/mYQJvUTEAy/2hF75jKiLdkUi5+ek8fznYq/hpp+AKYB7lh3+MqUpmsy5G+g4NRUOX3Sf+eS7073j/lf1T6lNjv0ziqXZsZbaKtoHpqOhDAJZzpwv5wujAzqkytgUgHcKIVNfdB6akYTkOEnCIPXiAve+h1Ssni1rx/fDPrD5BpvCMGLDn6nkfbd98UJSxhA8zN5E55JTDLEMO+j8WknstNDCEBA2LhG0z/z9B9Vgzo8eQ36AAreFMKPOtl+F/v4gI+6VZIMMpDn9L+Ul6OX1gH8imV4deLGp0oENZHC5GPRmOUSZbmD2jtcPC2dZ9jY5Gabhj0THWjpObV6zWbg973c1EsjuWYzEX8WmhKGL9Ca9BJxfIG5cXAOiC3DtIqeJQfoJeWq+K9B6lTpMAZqsUYIkxFeCvRDhzLxPJ+zJvCAUqNTqyY4mtKXoiRgu+GksXIym2GaXQjQsxzJad3oNxKl65HdF5BKG2Kl8jeZfEIUJtfpPT0E3OYOaxvEoUomuCDKERc+ATROdevvjGSs4F4hjytkTJUtxBpOrk0Kbhnf4M/ouj7WOQacM3Ofc0nz2e5kv4kv9jPBkqnR/B8xFOCuhm7J18BXVC8jRiUKFmq22dKMaminQ6GOEymnIt0ZdAld9

Well the previous examples
(eg, two goals ?x = a and ?x = b) and the tactic reflexivity
show how the behaviour simply has to be as though the tactic works on
one goal before the other.

So the question remains, in a construction like
all : reflexivity.
what determines the behaviour?

Thanks

Jeremy

On 01/24/2019 12:15 AM, Théo Zimmermann wrote:
>
> This is because by default tactics work on multiple goals at the same
> time, and ";" will carry this property.

[Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/23/2019
- Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
  - Re: [Coq-Club] "Sequence is associative." (?), Cao Qinxiang, 01/23/2019
    - Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
      - Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
        
        Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/23/2019
  - Re: [Coq-Club] "Sequence is associative." (?), Jean-Christophe Léchenet, 01/23/2019
    - Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
      - Re: [Coq-Club] "Sequence is associative." (?), Théo Zimmermann, 01/23/2019
        
        Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/24/2019
        
        Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/24/2019
  - Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
    - Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
      - Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
        
        Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
        
        Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
        
        Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
        Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
        Re: [Coq-Club] "Sequence is associative." (?), Pierre Courtieu, 01/28/2019
        Re: [Coq-Club] "Sequence is associative." (?), Jeremy Dawson, 01/28/2019
        Re: [Coq-Club] [SUSPECTED SPAM] Re: "Sequence is associative." (?), COURTIEU Pierre, 01/28/2019