Subject: Ssreflect Users Discussion List
List archive
- From: (Emilio Jesús Gallego Arias)
- To: Boris Djalal <>
- Cc:
- Subject: Re: [ssreflect] Behavior of "rewrite h => [ ]"
- Date: Thu, 09 Mar 2017 19:46:43 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Neutral ; spf=None
- Ironport-phdr: 9a23:0BMf5BF11fM9/XMsuJ7kwZ1GYnF86YWxBRYc798ds5kLTJ78rsqwAkXT6L1XgUPTWs2DsrQf2reQ7/6rADVbqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLdyIRmsogjct8YajZZ/Jqs/1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOiUn+2/LlMN/kKNboAqgpxNhxY7UfJqVP+d6cq/EYN8WWXZNUsNXWidcAI2zcpEPAvIBM+hGsof9oFUOoxW8CgevCuzgxSNHi2Tq3aEmyektDR3K0RYiEt8IrX/arM/1NKAXUe2t0qbF1jrCYvBK1Tvn74jIaB8hquyIUbx/dMrRyE0vFwLCjl6NrYLqISiVzv4Ws2OG7uRvT+avi2o5pAF+pTik29shipPIho0P0VDI8CN0y5s2K92gUEN3fNqpHZRKuy2EKod7TdkuT3xotSs50LEKpJC2cSoSxJkkxhPTcf2KfoqS7h/nTuqcLzV1iXR4c7ylnRmy61KvyujkW8m0zllKqi1Fn8HQuX8RzhDT9tWHSuNn8UenwDqPzQfT5ftBIUA1k6rbJIctzaQqmpUNt0TDBSr2mF3sgK+YbEUo4umo6+L5bbX6vpKQKot5hw7kPqgwh8CyDv40PhUOUmWY4+iwybPu8E/hTLVPlPI2k63ZsJ7AJcQco660GxFa350s6hu8EzuqytMYnWMILF5dYhKIk5DpO03SIPD/Ffq/mE+skC11yPDIOr3uHInCLmTYnbf6fbd97lZcxxApwdBe4ZJUELABL+jpVk//rtyLRiM+Ziaz2ef8QPl/34cXXSrbCKiDMbiUvV2B4usrC+iKfo4c/jjnfasL/fnr2HIRiQ9FO66z0tNXRXW5GvVha2eUeuj3yvgIFWMHsQ12ZfbrgUbDAm0bXGq7Q69pvmJzM4mhF4qWA9n12LE=
- Organization: X80 Heavy Industries
Dear Boris,
Boris Djalal
<>
writes:
> P, Q, R : Prop
> h : P = Q
> ============================
> P /\ R -> R
>
> If I do "rewrite h => []", I obtain the following goal: Q /\ R -> R
> whereas I expect to obtain: Q -> R -> R.
You need to do "rewrite => -[]".
If you look closely in the manual you will see that indeed "[]" as the
first token after => is interpreted not as case, but as a "disjunctive
introduction", as in "elim: n => [|n ihn]" .
[Anyways I don't know all the details but indeed I do remember the
manual did a good job explaining this]
--
Emilio
- [ssreflect] Reminder: JAR Special Issue on Milestones in Interactive Theorem Proving, Jeremy Avigad, 03/09/2017
- [ssreflect] Behavior of "rewrite h => [ ]", Boris Djalal, 03/09/2017
- Re: [ssreflect] Behavior of "rewrite h => [ ]", Emilio Jesús Gallego Arias, 03/09/2017
- Re: [ssreflect] Behavior of "rewrite h => [ ]", Boris Djalal, 03/10/2017
- Re: [ssreflect] Behavior of "rewrite h => [ ]", Emilio Jesús Gallego Arias, 03/09/2017
- [ssreflect] Behavior of "rewrite h => [ ]", Boris Djalal, 03/09/2017
Archive powered by MHonArc 2.6.18.