(* https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Morgenstern_utility_theorem *)
From Coq Require Streams.
From Paco Require Import paco.
From mathcomp Require Import classical_sets interval all_ssreflect all_algebra order.
[Loading ML file ssrmatching_plugin.cmxs (using legacy method) ... done ]
[Loading ML file ssreflect_plugin.cmxs (using legacy method) ... done ]
[Loading ML file ring_plugin.cmxs (using legacy method) ... done ]
Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing,default]
Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing,default]
Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing,default]
Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing,default]
Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing,default]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing,default]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing,default]
New coercion path [Empty.base; Finite.base;
Choice.base] : Empty.class_of >-> Equality.mixin_of is ambiguous with existing
[Empty.mixin; Empty.eqMixin] : Empty.class_of >-> Equality.mixin_of.
New coercion path [Empty.base; Finite.base;
Choice.mixin] : Empty.class_of >-> Choice.mixin_of is ambiguous with existing
[Empty.mixin; Empty.choiceMixin] : Empty.class_of >-> Choice.mixin_of.
[ambiguous-paths,coercions,default]
New coercion path [Empty.base; Finite.mixin;
Finite.mixin_base] : Empty.class_of >-> Countable.mixin_of is ambiguous with existing
[Empty.mixin; Empty.countMixin] : Empty.class_of >-> Countable.mixin_of.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subring_closedM;
GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.sdivr_closed_div;
GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.subalg_closedBM;
GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divring_closed_div;
GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.divalg_closedBdiv;
GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,coercions,default]
New coercion path [GRing.Pred.subring_smul;
GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,coercions,default]
From mathcomp.analysis Require Import reals topology measure .
[Loading ML file coq-elpi.elpi ... done ]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done ]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done ]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done ]
Import Order.Theory.
From GTF Require Import GiryClasses.
Module VNM (Number : Interval).
Module P := Probability Number.
Import P.
End VNM .
Module Type DiscreteDistribution (Number : Interval).
Context (O : finPOrderType tt).
Local Open Scope ring_scope.
Class rv : Type := {
pmf :> {ffun O -> Number.unit_compact};
convex : foldr (@GRing.add Number.t) (0 : Number.t) (map pmf (enum O)) = 1 ;
}.
A coercion will be introduced instead of an instance
in future versions when using ':>' in 'Class'
declarations. Replace ':>' with '::' (or use
'#[global ] Existing Instance field .' for compatibility
with Coq < 8 .18 ). Beware that the default locality for
'::' is #[export], as opposed to #[global ] for ':>'
currently. Add an explicit #[global ] attribute to the
field if you need to keep the current behavior. For
example: "Class foo := { #[global] field :: bar }."
[future-coercion-class-field ,deprecated-since-8 .17 ,deprecated,default]
Ignored instance declaration for “pmf”: “rv ->
{ffun O ->
Number.unit_compact}” is not a class
[not-a-class,default]
End DiscreteDistribution .
Module Type Lottery (Number : Interval) (Dist : DiscreteDistribution Number).
Local Open Scope order_scope.
Notation "o1 == o2" := (o1 <= o2 && o2 <= o1) : order_scope.
Close Scope order_scope.
Parameter (O : finPOrderType tt).
Definition t : Type := seq (Number.unit_compact * O).
Definition lottery (ps : Number.fin_unit_compact) `{Number.convex ps} {H : length ps = #|O|} : t
:= zip ps (enum O).
Local Open Scope ring_scope.
Definition singletonOutcome (o : O) : t := nseq Nat.one ((1 : Number.t), o).
Declare Scope lottery_scope.
Delimit Scope lottery_scope with lottery.
Notation "'.|' o '|'" := (singletonOutcome o) : lottery_scope.
Parameter (o1 : O).
Check {ffun O -> Number.unit_compact}.
{ffun O -> Number.unit_compact}
: predArgType
Check .|o1|%lottery.
End Lottery .
Module Type Rationality
(Number : Interval)
(Dist : DiscreteDistribution Number)
(Lott : Lottery Number Dist)
.
Local Open Scope order_scope.
Local Open Scope lottery_scope.
Class axioms : Type := {
completeness : forall (o1 o2 : Lott.O), (o1 <= o2) || (o2 <= o1) || (o1 == o2);
transitivity : forall (o1 o2 o3 : Lott.O), o1 <= o2 -> o2 <= o3 -> o1 <= o3;
}.
End Rationality .