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: 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. 

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?

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.

Section Games.

Variable Agent : Set.
Variable Choice : Agent -> Set.
Variable Utility: Set.

(* Strategy profiles *)
CoInductive StratProf  : Set :=
| sLeaf : (Agent -> Utility) -> StratProf
| sNode : forall (a:Agent), Choice a -> (Choice a -> StratProf) -> StratProf.
  Notation "<< f >>" := (sLeaf f).
  Notation "<< a , c , next >>" := (sNode a c next).

(* Utility assignment as a relation*)
Inductive Uassign : StratProf -> Agent -> Utility -> Prop :=
| UassignLeaf: forall a f, Uassign (<<f>>) a (f a)
| UassignNode: forall  (a a':Agent)(c:Choice a') (u:Utility) (next:Choice a' -> StratProf),
    Uassign (next c) a u  -> Uassign (<<a',c,next>>) a u.

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.

 
-- 

Thank you in advance

---------------------------
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