The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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