Skip to content

Commit

Permalink
stub failing proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
markusdemedeiros committed Sep 10, 2024
1 parent 9b33b4e commit fa0720f
Show file tree
Hide file tree
Showing 5 changed files with 48 additions and 3 deletions.
4 changes: 4 additions & 0 deletions theories/prob/monad/integrate.v
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,9 @@ Section giryM_integrate_laws.
pose HApprox := (nnsfun_approx HMTop (@measurable_mapP _ _ _ _ f)).

(* Move under the measurable_fun *)
(* Broken by new mathcomp-analysis *)

(*
erewrite (Setoid1 _ _ _ _ _ _ (fun (μ : giryM T) => _)); last first.
{ apply functional_extensionality; intro μ.
(* Rewrite this integral to the limit of a finite sum *)
Expand All @@ -68,6 +71,7 @@ Section giryM_integrate_laws.
(* Search topology.lim "sum". *)
reflexivity.
}
*)

(* Target: *)
(*Search measurable_fun "sum".
Expand Down
5 changes: 5 additions & 0 deletions theories/prob/monad/join.v
Original file line number Diff line number Diff line change
Expand Up @@ -190,8 +190,13 @@ Section giryM_join_definition.
}
rewrite H1.
rewrite /giryM_join_meas_map_pre.
(* Broken by new mathcomp-analysis *)

Admitted.
(*
apply measurable_mapP.
Qed.
*)

HB.instance Definition _ :=
isMeasurableMap.Build _ _ (giryM (giryM T)) (giryM T) (giryM_join_def' : giryM (giryM T) -> (giryM T)) giryM_join_def'_measurable.
Expand Down
34 changes: 32 additions & 2 deletions theories/prob/monad/laws.v
Original file line number Diff line number Diff line change
Expand Up @@ -272,20 +272,26 @@ Section monad_laws.
Proof.
rewrite giryM_integrate_eval.
rewrite giryM_integrate_eval.
(* Broken by latest mathcomp-analysis *)
Admitted.
(*
rewrite integral_pushforward; cycle 1.
- by apply measurable_mapP.
- by apply measurable_mapP.
- by apply Hg.
f_equal.
Qed.

*)

Lemma giryM_join_map_map {d1 d2} {T1 : measurableType d1} {T2 : measurableType d2}
(mf : measurable_map T1 T2) (m : giryM (giryM T1)) :
giryM_join (giryM_map (giryM_map mf) m) ≡μ giryM_map mf (giryM_join m).
Proof.
intros S HS.
rewrite giryM_join_eval.
(* Broken by latest mathcomp-analysis *)
Admitted.
(*
rewrite integral_pushforward; cycle 1.
- by apply measurable_mapP.
- by apply base_eval_measurable.
Expand All @@ -295,6 +301,7 @@ Section monad_laws.
rewrite giryM_join_eval.
f_equal.
Qed.
*)

Lemma giryM_join_map_join {d1} {T1 : measurableType d1} (m : giryM (giryM (giryM T1))) :
giryM_join (giryM_map giryM_join m) = giryM_join (giryM_join m).
Expand All @@ -316,6 +323,9 @@ Section monad_laws.
Proof.
intros S HS.
rewrite giryM_join_eval.
(* Broken by latest mathcomp-analysis*)
Admitted.
(*
rewrite integral_pushforward; cycle 1.
- by apply measurable_mapP.
- by apply base_eval_measurable.
Expand All @@ -327,6 +337,7 @@ Section monad_laws.
- by apply @measurableT.
- done.
Qed.
*)

Lemma giryM_join_ret {d1} {T1 : measurableType d1} (μ : (giryM T1)) :
giryM_join (giryM_ret R μ) ≡μ μ.
Expand Down Expand Up @@ -361,6 +372,9 @@ Section monad_laws.
Proof.
intros S HS.
rewrite giryM_join_eval.
(* Broken by latest mathcomp-analysis *)
Admitted.
(*
rewrite integral_pushforward; cycle 1.
- by apply measurable_mapP.
- by apply base_eval_measurable.
Expand All @@ -370,25 +384,33 @@ Section monad_laws.
- by rewrite mul0e.
- by apply @measurableT.
Qed.
*)

(* TODO: Can I fit this into the framework? *)
Lemma giryM_bind_eval {d1 d2} {T1 : measurableType d1} {T2 : measurableType d2}
(m : giryM T1) {S : set T2} (HS : measurable S) (f : measurable_map T1 (giryM T2)) :
(giryM_bind f m S = \int[m]_x (f x S))%E.
Proof.
rewrite giryM_join_eval.
(* Broken by latest mathcomp-analysis *)
Admitted.
(*
rewrite integral_pushforward /=; cycle 1.
- by apply measurable_mapP.
- by apply base_eval_measurable.
- by intro u; apply (measure_ge0 u).
done.
Qed.
*)

Lemma giryM_bind_ret_l {d1 d2} {T1 : measurableType d1} {T2 : measurableType d2} {f : measurable_map T1 (giryM T2)} t :
giryM_bind f (giryM_ret R t) ≡μ f t.
Proof.
intros S HS.
rewrite giryM_join_eval.
(* Broken by latest mathcomp-analysis *)
Admitted.
(*
rewrite integral_pushforward; cycle 1.
- by apply measurable_mapP.
- by apply base_eval_measurable.
Expand All @@ -402,14 +424,17 @@ Section monad_laws.
- by apply base_eval_measurable.
- by apply measurable_mapP.
Qed.

*)

Lemma giryM_bind_ret_r_meas {d1 d2} {T1 : measurableType d1} {T2 : measurableType d2} {f : measurable_map T1 (giryM T2)}
(m : giryM T1) :
giryM_bind (giryM_ret R) m ≡μ m.
Proof.
intros S HS.
rewrite giryM_join_eval.
(* Broken by latest mathcomp-analysis *)
Admitted.
(*
rewrite integral_pushforward; cycle 1.
- by apply measurable_mapP.
- by apply base_eval_measurable.
Expand All @@ -420,6 +445,7 @@ Section monad_laws.
- by apply @measurableT.
- done.
Qed.
*)

Lemma giryM_bind_bind_meas {d1 d2 d3} {T1 : measurableType d1} {T2 : measurableType d2} {T3 : measurableType d3}
{f : measurable_map T1 (giryM T2)} {g : measurable_map T2 (giryM T3)}
Expand All @@ -428,6 +454,9 @@ Section monad_laws.
Proof.
intros S HS.
rewrite giryM_join_eval.
(* Broken by latest mathcomp-analysis *)
Admitted.
(*
rewrite integral_pushforward; cycle 1.
- by apply measurable_mapP.
- by apply base_eval_measurable.
Expand Down Expand Up @@ -474,6 +503,7 @@ Section monad_laws.
- by intro u; apply (measure_ge0 u).
f_equal.
Qed.
*)

Lemma giryM_join_bind {d} {T : measurableType d} (m : giryM (giryM T)) :
giryM_join m = giryM_bind m_id m.
Expand Down
4 changes: 3 additions & 1 deletion theories/prob/monad/map.v
Original file line number Diff line number Diff line change
Expand Up @@ -126,9 +126,11 @@ Section giryM_map_definition.
reflexivity.
}
simpl.
apply measurable_if_pushfowrard_subset.



(*
apply measurable_if_pushfowrard_subset.
Check (@measurability _ _ _ _ setT _ ereal_borel_subbase _).
Search subset smallest.
rewrite /subset.
Expand Down
4 changes: 4 additions & 0 deletions theories/prob/monad/types.v
Original file line number Diff line number Diff line change
Expand Up @@ -189,6 +189,9 @@ Section giry_lemmas.
Lemma base_eval_measurable {d1} {T1 : measurableType d1} (S : set T1) (HS : measurable S):
measurable_fun [set: giryM T1] ((SubProbability.sort (R:=R))^~ S).
Proof.
(* Breaks w/ new mathcomp-analysis *)
Admitted.
(*
eapply (@measurability _ _ _ _ _ _ 'measurable).
{ rewrite /measurable/=.
symmetry.
Expand All @@ -215,6 +218,7 @@ Section giry_lemmas.
- done.
- by rewrite setTI.
Qed.
*)

End giry_lemmas.

Expand Down

0 comments on commit fa0720f

Please sign in to comment.