coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] inversion of an inductive
- Date: Fri, 15 Apr 2016 13:44:24 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing.csail.mit.edu
- Ironport-phdr: 9a23:FMn1/RGAxn33DlI9FS9s7p1GYnF86YWxBRYc798ds5kLTJ75pMSwAkXT6L1XgUPTWs2DsrQf27qQ7v+rAzBeqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7D0psKYOVkWzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB0wamx8AKAjB7QnzWp655iL2v+928CKBNMzyC7U1RXKv47o9G0ygszsOKzNsqDKfscd3lq8O+B8=
On 04/15/2016 01:37 PM, Pierre Lescanne (at work) wrote:I have developed in Coq exercises in extensive game theory (for economics). A first development was with coinductive. In this development I was able to perform inversion. Yes: Lemma UassignNode_inv': forall (s:StratProf) (a:Agent) (u:Utility), Uassign s a u -> match s with | << a', c, next >> => Uassign (next c) a u | _ => True end. Proof. destruct 1; auto. Qed. Lemma UassignNode_inv: forall (a a':Agent) (u:Utility) (next:Choice a' -> StratProf) (c:Choice a'), Uassign (<<a',c,next>>) a u -> Uassign (next c) a u. Proof. intros. apply UassignNode_inv' in H. assumption. Qed. For a more general introduction to this approach, see Section 12.3.4 of CPDT <http://adam.chlipala.net/cpdt/>. Here is the script I am stuck on. |
- [Coq-Club] inversion of an inductive, Pierre Lescanne (at work), 04/15/2016
- Re: [Coq-Club] inversion of an inductive, Adam Chlipala, 04/15/2016
- Re: [Coq-Club] inversion of an inductive, Jean-Francois Monin, 04/15/2016
- Re: [Coq-Club] inversion of an inductive, Pierre Lescanne (at work), 04/16/2016
Archive powered by MHonArc 2.6.18.