The Coq mailing list

["Pierre Lescanne (at work)" <pierre.lescanne AT ens-lyon.fr>]

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?

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