Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] inversion of an inductive

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] inversion of an inductive


Chronological Thread 
  • From: "Pierre Lescanne (at work)" <pierre.lescanne AT ens-lyon.fr>
  • To: coq-club AT inria.fr
  • Cc: pierre.lescanne AT ens-lyon.fr
  • Subject: Re: [Coq-Club] inversion of an inductive
  • Date: Sat, 16 Apr 2016 10:00:43 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.lescanne AT ens-lyon.fr; spf=Pass smtp.mailfrom=pierre.lescanne AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
  • Ironport-phdr: 9a23:uxjRMxzV3D2kRYTXCy+O+j09IxM/srCxBDY+r6Qd0eMSIJqq85mqBkHD//Il1AaPBtWLra8UwLSM+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt6U0pT8ibr60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt/fmrR3ScQza/noRSH8b1B5FGAPM6hf3dpr3qW7+p+17nieAbuPsSrVhEwyj4r1xRVfMhTwMPjg//SmXg9A4k6VBo1Pr70hnwoPOeozTMPdldarbe94ySGxaG8JAUCoHDJnqPNhHNPYIIesN99q1nFAJtxbrXQQ=

Thank you Adam and Jean-François for your answers which are very useful.  Being  able to use inversion, together with coinductive objects and dependent types  is very central in what I want to do and I know now that this is possible and can be done simply.

Le 15/04/2016 19:37, Pierre Lescanne (at work) a écrit :
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. 

Now I generalize the approach and I describe a slightly more elaborate formalism with dependent types and I am no more able to perform inversion.  Is such an inversion possible in this framework?



-- 

Best wish

---------------------------
Pierre Lescanne (Emeritus Professor)
LIP / École normale supérieure de Lyon
46 allée d'Italie
69364 LYON Cedex 07, France
tél: +33 6 85 70 94 31
http://perso.ens-lyon.fr/pierre.lescanne/
---------------------------



Archive powered by MHonArc 2.6.18.

Top of Page