Require Import RIneq.
Require Import Zq.
Require Import ListSet.
Require Import listT.
Require Import ZqAux.
Require Import ZArith.
Require Import Coq.Reals.Raxioms.
Require Import R_lemma.

Hypothesis Aeq_dec : forall (V : Type) (x y : V), {x = y} + {x <> y}. 

Section Proba.
(* Note that in this section, we do not divide by cardinal E for simplify calculus *)
(*the events are of type V*)
(*E is the probability space *)
Variable V : Type.
Variable E : listT V.


Definition dec_pred (P : V -> Prop) := forall x : V, {P x} + {~ P x}.

(*an event is a predicate with a decidability*)
Record Event : Type := 
  {event_pred :> V -> Prop; event_dec : dec_pred event_pred}.


(*construction of the complementary event *)
Lemma event_diff_aux : forall P : Event, dec_pred (fun x : V => ~ P x).
unfold dec_pred in |- *.
intros.
elim (event_dec P x).
intros.
right.
intuition.
intros.
left.
try exact b.
Qed.
 
Definition Eventdiff (P : Event) : Event :=
  Build_Event (fun x : V => ~ P x) (event_diff_aux P).


(* a list of complementary events *)
Definition EvDiffList := mapT Eventdiff.

(* construction of the empty event *) 
Lemma empty : dec_pred (fun x : V => False).
unfold dec_pred in |- *.
intros.
right.
intuition.
Defined.
 
Definition empty_ev : Event := Build_Event (fun x : V => False) empty.


(*coonstruction of the full event *)
Lemma full : dec_pred (fun x : V => True).
unfold dec_pred in |- *.
intros.
left.
auto.
Qed.

Definition full_ev2 := Eventdiff empty_ev.
(*Definition full_ev:Event:=(Build_Event [x : V]True full).*)


(*construction of the union of 2 events *)
Lemma event_union_aux :
 forall P Q : Event, dec_pred (fun x : V => P x \/ Q x).
unfold dec_pred in |- *.
intros.
elim (event_dec P x).
intros.
left.
left.
auto.
intros.
elim (event_dec Q x).
intros.
left.
right.
auto.
intros.
right.
unfold not in |- *.
intros.
elim H; auto.
Qed.
 
Definition EventUnion (P Q : Event) : Event :=
  Build_Event (fun x : V => P x \/ Q x) (event_union_aux P Q).


(* construction of the union of a list of events *)
Fixpoint EvUnList (P : listT Event) : Event :=
  match P with
  | nilT => empty_ev
  | consT Q Qs => EventUnion Q (EvUnList Qs)
  end.
 
(*construction of the intersection of 2 events *)
Lemma event_inter_aux :
 forall P Q : Event, dec_pred (fun x : V => P x /\ Q x).
unfold dec_pred in |- *.
intros.
elim (event_dec P x); elim (event_dec Q x); intros.
left.
auto.
right.
unfold not in |- *.
intuition.
right.
unfold not in |- *.
intuition.
right.
unfold not in |- *.
intuition.
Qed.
 
Definition EventInter (P Q : Event) : Event :=
  Build_Event (fun x : V => P x /\ Q x) (event_inter_aux P Q).

(* construction of the intersection of a list of events *)
Fixpoint EvIntList (P : listT Event) : Event :=
  match P with
  | nilT => full_ev2
  | consT Q Qs => EventInter Q (EvIntList Qs)
  end.


(* construction of the event Q\P *)
Lemma ev_diff_aux:forall P Q:Event, dec_pred (fun x : V => ~ P x/\Q x ).
unfold dec_pred in |- *.
intros.
elim (event_dec P x); elim (event_dec Q x); intros.
right.
intuition.
right.
intuition.
left.
intuition.
right.
intuition.
Qed.

Definition ev_diff(P Q:Event):Event:=
  Build_Event (fun x : V => ~ P x/\Q x) (ev_diff_aux P Q).


(*filter removes the repetition of elements*)
Fixpoint filter (P : Event) (B : listT V) {struct B} : 
 listT V :=
  match B with
  | nilT => nilT V
  | consT b l =>
      match event_dec P b with
      | left _ => consT b (filter P l)
      | right _ => filter P l
      end
  end.

(*we do not divide by card E to simplify calculus*)
 (* Proba = length of the event *)
Definition Proba (P : Event) := lengthT (filter P E).
 

Require Import Reals.
 
(*definition of probability*)
Definition prob (L : Event) := (INR (Proba L) / INR (lengthT E))%R.
 
(*L is included in M*)
Definition EventIncl (L M : Event) := inclT (filter L E) (filter M E).

(*a belongs to L/\M => a belongs to M *) 
Lemma InT_inter :
 forall (L M : Event) (a : V) (l : listT V),
 InT a (filter (EventInter L M) l) -> InT a (filter M l).
intros.
induction  l as [| a0 l Hrecl].
absurd (InT a (filter (EventInter L M) (nilT V))).
simpl in |- *; auto.
exact H.
generalize H.
simpl in |- *.
case (event_inter_aux L M a0).
simpl in |- *.
intros.
case (event_dec M a0).
simpl in |- *.
intros.
case H0.
auto.
intros.
constructor 2.
apply Hrecl.
exact H1.
intros.
absurd (M a0).
exact n.
case a1.
auto.
case (event_dec M a0).
intros.
simpl in |- *.
constructor 2.
apply Hrecl.
exact H0.
intros.
apply Hrecl.
exact H0.
Qed.

(*a1 belongs to a::L/\M => a1 belongs to a::M *)
Lemma InT_inter2 :
 forall (L M : Event) (a a1 : V) (l : listT V),
 InT a1 (consT a (filter (EventInter L M) l)) ->
 InT a1 (consT a (filter M l)).
simpl in |- *.
intros.
case H.
auto.
intros.
constructor 2.
eapply InT_inter.
apply H0.
Qed.

(*definition of conditional probability *)
Definition prob_cond (L M : Event) := (prob (EventInter L M) / prob M)%R.

Definition PrCondList (L : Event) (M : listT Event) :=
  prob_cond L (EvIntList (EvDiffList M)).

(*a mettre ds liste*)
Fixpoint subListT (A : Type) (l1 l2 : listT A) {struct l2} : Prop :=
  match l1 with
  | nilT => True
  | consT x xs =>
      match l2 with
      | nilT => False
      | consT y ys => x = y /\ subListT A xs ys \/ subListT A l1 ys
      end
  end.


Fixpoint SumList (l : listT R) : R :=
  match l with
  | nilT => 0%R
  | consT x xs => (x + SumList xs)%R
  end.


Lemma ev_dec : forall A : Event, dec_pred  A.
intros.
elim A.
auto.
Qed.


Lemma dec_pred_equiv :
 forall A B : Event,
 dec_pred  A -> dec_pred B -> dec_pred (fun x => A x <-> B x).
unfold dec_pred in |- *.
intros.
assert ({A x} + {~ A x}).
auto with *.
assert ({B x} + {~ B x}).
auto with *.
intuition.
Qed.

(*the event A<=>B *)
Definition EquivEv (A B : Event) : Event :=
  Build_Event (fun f => A f <-> B f)
    (dec_pred_equiv A B (ev_dec A) (ev_dec B)).

(*definition of the independance of 2 events*)
Definition indep (A B : Event) :=
  prob (EventInter A B) = (Rdefinitions.Rmult (prob A)  (prob B)).

(*a mettre ds nat *)
Lemma plus_min_ass:forall a b c : nat,c <= b->a+(b-c)=a+b-c.
intros.
induction a.
simpl.
auto.
induction c.
simpl.
auto with * .
simpl.
rewrite plus_n_Sm.
rewrite minus_Sn_m.
simpl.
auto with * .
auto.
Qed.


Fixpoint list_prob(l:listT V)(A:Event){struct l}:listT R:= 
                  match l with 
		    |nilT=>nilT _
		    |consT x xs=> match event_dec A x with
				    | left _ => consT (Rdiv R1 (INR (lengthT l))) (list_prob xs A)
				    | right _ => (list_prob xs A) end
		    end.

(*a mettre ds list*)
Fixpoint Sum(l:listT V)(f:V->R){struct l}:R:= 
                  match l with 
		    |nilT=>R0
		    |consT x xs=>((f x)+(Sum xs f))%R end.


End Proba.

(*let us assume that a=a1,. ,an   b=b1,  ,bn
a1\/   \/an\/b1\/   \/bn <=> (a1\/  \/an)\/(b1\/  \/bn) *)
Lemma EvUnList_un :
 forall (A:Type)(a b : listT (Event A)) (f : A),
 EvUnList A (appT a b) f <->
 EvUnList A a f \/ EvUnList A b f.
simple induction a.
simpl in |- *; intros.
intuition.
simpl in |- *; intros.
unfold iff in |- *.
unfold iff in H.
elim (H b f).
intros.
split.
intros.
intuition.
intros.
intuition.
Qed.


Section mk_ev.
(* In this section we take an event of type V and we construct an event of type VxW *)
 (*                                 and                             W                                                             VxW *)

Variable V W:Type.
Variable Ev:listT V.
Variable Ew:listT W.
Require Import Logic_Type.

Lemma dec_pred_fst :
 forall A : V -> Prop,
 dec_pred V A -> dec_pred (prodT V W) (fun f : prodT V W => A (fstT f)).
unfold dec_pred in |- *.
auto with *.
Qed.

(* A |->  [f](A (fstT f)) *)
Definition mk_ev_fst (A : Event V) : Event (prodT V W) :=
  Build_Event (prodT V W) (fun f => A (fstT f))
    (dec_pred_fst  A (ev_dec V A)).

Lemma dec_pred_snd :
 forall A : W -> Prop,
 dec_pred W A -> dec_pred (prodT V W) (fun f : prodT V W => A (sndT f)).
unfold dec_pred in |- *.
auto with *.
Qed.

(* A |->  [f](A (sndT f)) *)
Definition mk_ev_snd (A : Event W) : Event (prodT V W) :=
  Build_Event (prodT V W) (fun f => A (sndT f))
    (dec_pred_snd  A (ev_dec W A)).

Unset Strict Implicit.
Set Implicit Arguments.

(*a mettre de proof_prob *)
Lemma eq_mkfst_map:forall (A : Event V) (a:W)(l:(listT V)),(lengthT
        (filter (prodT V W) (mk_ev_fst A)
           (mapT (fun z : V => pairT z a) l)))= (lengthT (filter V A l)).
induction l.
simpl;intros;auto.
simpl;intros.
case (dec_pred_fst A (ev_dec  V A) (pairT a0 a)).
case (event_dec V A a0).
simpl;intros.
auto with *.
simpl;intros;intuition.
case (event_dec V A a0).
simpl;intros;intuition.
simpl;intros.
auto with *.
Qed.

Lemma lgt_filt_app :
 forall (W : Type) (l g : listT W) (A : Event W),
 lengthT (filter W A (appT l g)) =
 lengthT (filter W A l) + lengthT (filter W A g).
simple induction l.
simpl in |- *; intros; auto with *.
simpl in |- *; intros.
case (event_dec W0 A a); simpl in |- *; intros; auto with *.
Qed.

(*a mettre ds nat*)
Lemma eq_S_simpl:forall a b c:nat,S (a+(b+a*c))=S (b+a*S c).
intros.
rewrite <-mult_n_Sm.
rewrite Plus.plus_comm .
auto with *.
Qed.
End mk_ev.

Section dec_prod.
(* In this section we take an event of type V and we construct an event of type VxVxW *)
 (* and                                                             W                                                             VxVxW *)
Variables V W:Type.

Lemma dec_pdT_lem_fst :
 forall A : V -> Prop,
 dec_pred V A -> dec_pred (PdT V V W) (fun f : PdT V V W => A (FtT f)).
unfold dec_pred in |- * .
auto with *.
Qed.

(* A |->  [f](A (FtT f)) *)
Definition mk_pdT_ev_fst (A : Event V): Event (PdT V V W) :=
  Build_Event (PdT V V W) (fun f => A (FtT  f))
    (dec_pdT_lem_fst (ev_dec V A)).


Lemma dec_pdT_lem_snd :
 forall A : V -> Prop,
 dec_pred V A -> dec_pred (PdT V V W) (fun f : PdT V V W => A (SdT f)).
unfold dec_pred in |- *.
auto with *.
Qed.

(* A |->  [f](A (SdT f)) *)
Definition mk_pdT_ev_snd (A : Event V) : Event (PdT V V W) :=
  Build_Event (PdT V V W) (fun f => A (SdT f))
    (dec_pdT_lem_snd (ev_dec V A)).

Lemma dec_pdT_lem_trd :
 forall A : W -> Prop,
 dec_pred W A -> dec_pred (PdT V V W) (fun f : PdT V V W => A (TdT f)).
unfold dec_pred in |- *.
auto with *.
Qed.

(* A |->  [f](A (fstT f)) *)
Definition mk_pdT_ev_trd (A : Event W) : Event (PdT V V W) :=
  Build_Event (PdT V V W) (fun f => A (TdT f))
    (dec_pdT_lem_trd (ev_dec W A)).

Lemma dec_pdT_trd :
 forall A : (prodT V W) -> Prop,
 dec_pred (prodT V W) A -> dec_pred (PdT W W V) (fun f : PdT W W V=> A (pairT (TdT f) (FtT f))).
unfold dec_pred in |- *.
auto with *.
Qed.

Definition mk_pdT_trd (A : Event (prodT V W) ): Event (PdT W W V) :=
  Build_Event (PdT W W V) (fun f => A (pairT (TdT f) (FtT f)))
    (dec_pdT_trd (ev_dec (prodT V W) A)).
End dec_prod.