coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] How to construct this simple proof term with tactics?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] How to construct this simple proof term with tactics?
Date: Mon, 16 Apr 2018 12:37: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 mga18.intel.com
Ironport-phdr: 9a23:EqiMmxVk+4ajA5iYc0PfrY5FqSvV8LGtZVwlr6E/grcLSJyIuqrYbBGBt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRxxwYHUYZ2aO/VxcK7GYdMVXm5MUtpNWyBdAI6xaZYEAeobPeZfqonwv1UCowa5BQayC+Pv1iVIhnju3aEizu8vFgDG0xAgH90UrnvUqNv5P7oVXOCwzanH0TXDYOlI1jf58oTIaRchru+DXbJsa8rRzlEvGhjEjlWWtYzqITeV2v4RvGic6uptTOSigHMppQF2pzig3MYsio/Ri4IUzFDE6Tt2wIIvKdKlVkF2Z8OvHphItyyCKod7TMwvT3t1tCs0xbAKo4O3cSYLxZg92hLTdf2Kf5CV7h/iWuudOzl1iXx/dL6hiRu/9VKsxvD/W8WqyFpGsytIn93WunwT1xHe5dKLRuVn8ku82DuC2Abe4fxeL08uj6rUMZshz6YwlpUNtUTDGTf7mED5jKCMa0kp+fKk6+XhYrX6uJCcM5V4hR35MqQrgsC/AOI4PRYSX2WD5Oix2rLu8VfkTLhEgfA6iLTVvZ7bKMgBu6K1HQ5Y3p4m6xmlDjem1NoYnWMALFJAYB+HionpNE3OIP/iE/i/h06gkCxsx//YMb3hHo/NLn/bkLr6fLZ97VJcxxQ3zdxF+51UDbQBLOrpWkDtrNzYEgM5Mwuszun7D9V9z5oSVn6LAq+EK6zfqkSI5+IqI+mUfoAZojf9K/4/5/7vl3A1g1EdfbP6lacQPTqzGe0jKEGEa1LthM0AGCEEpEB2GOftkRiJVSNZT3e0RaM1oD8hXtGIF4DGE8qWh7GOwD28BtkeQ2FNClmBFT2gI4CFUPcFZSbUOchsnSAeUqCJSok92BXovwj/nek0ZtHI8zEV4MqwnON+4PfewElrpG5ESv+F2mTIdFla22YBRjs4xqd6+BUvy1Gf3Kw+iPtdR4UKu6F5FzwiPJuZ9NRUTsjoU1uYLNaPVFuiBN6hBGNpF49j85o1e094Xu6aoFXD0i6tWuBHkrOCXcxy86TA0ny3LMF4mS7L

Dear all,

thanks for the quick help! Yes I indeed missed the obvious - as you pointed
out, the 1:1 translation of the proof term to tactics:

H (or_intror (fun Pw: P => H (or_introl Pw))).

apply H. right. intro Pw. apply H. left. apply Pw.

Sometimes ...

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] How to construct this simple proof term with tactics?, Soegtrop, Michael, 04/16/2018
- Re: [Coq-Club] How to construct this simple proof term with tactics?, Jean-Francois Monin, 04/16/2018
  - RE: [Coq-Club] How to construct this simple proof term with tactics?, Soegtrop, Michael, 04/16/2018
- Re: [Coq-Club] How to construct this simple proof term with tactics?, Laurent Thery, 04/16/2018
- Re: [Coq-Club] How to construct this simple proof term with tactics?, Gaëtan Gilbert, 04/16/2018