The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Hi Pierre,

You can use the generalization of "small inversions" explained in
http://www-verimag.imag.fr/~monin/Publis/Docs/itp13.pdf

It can handle (co)inductive with several (0 or 1, in your case) premises.
Here you can invert UassignLeaf and UassignNode using the same auxiliary
function.

Definition pr_Uassign {s} {a} {u} (x: Uassign s a u) :=
  let diag s a0 u0 :=
     match s with
     | << f >> =>
         forall X: Agent -> Utility -> Prop, 
         (forall a, X a (f a)) -> X a0 u0 
     | << a' , c , next >> =>
         forall X: Agent -> Utility -> Prop, 
         (forall a u, Uassign (next c) a u -> X a u) -> X a0 u0 
    end in
  match x in Uassign s a u return diag s a u with
  | UassignLeaf a f => fun X k => k a
  | UassignNode a a' c ut next ua => fun X k => k a ut ua
  end.

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.
intros until c. intro ua. apply (pr_Uassign ua). trivial.
Qed.

Lemma UassignLeaf_inv:
   forall (a:Agent) f (u:Utility), Uassign << f >> a u -> u = f a.
intros a f u ua. apply (pr_Uassign ua). trivial.
Qed.

Cheers,
Jean-Francois

On Fri, Apr 15, 2016 at 07:37:30PM +0200, 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?
> 
>    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
>  [1]http://perso.ens-lyon.fr/pierre.lescanne/
>  ---------------------------