Require Export Uprop.

Definition M (A:Type) := MF A -m> U.

Instance app_mon (A:Type) (x:A) : monotonic (fun (f:MF A) ⇒ f x).
Save.

Definition unit (A:Type) (x:A) : M A := mon (fun (f:MF A) ⇒ f x).

Definition star : ∀ (A B:Type), M A → (A → M B) → M B.
Defined.

Lemma star_simpl : ∀ (A B:Type) (a:M A) (F:A → M B)(f:MF B),
        star a F f = a (fun x ⇒ F x f).

Lemma law1 : ∀ (A B:Type) (x:A) (F:A → M B) (f:MF B), star (unit x) F f ≈ F x f.

Lemma law2 :
 ∀ (A:Type) (a:M A) (f:MF A), star a (fun x:A ⇒ unit x) f ≈ a (fun x:A ⇒ f x).

Lemma law3 :
 ∀ (A B C:Type) (a:M A) (F:A → M B) (G:B → M C)
   (f:MF C), star (star a F) G f ≈ star a (fun x:A ⇒ star (F x) G) f.

Definition stable_inv (A:Type) (m:M A) : Prop := ∀ f :MF A, m (finv f) ≤ [1-] (m f).

Definition stable_plus (A:Type) (m:M A) : Prop :=
  ∀ f g:MF A, fplusok f g → m (fplus f g) ≈ (m f) + (m g).

Definition le_plus (A:Type) (m:M A) : Prop :=
  ∀ f g:MF A, fplusok f g → (m f) + (m g) ≤ m (fplus f g).

Definition le_esp (A:Type) (m:M A) : Prop :=
  ∀ f g: MF A, (m f) & (m g) ≤ m (fesp f g).

Definition le_plus_cte (A:Type) (m:M A) : Prop :=
  ∀ (f : MF A) (k:U), m (fplus f (fcte A k)) ≤ m f + k.

Definition stable_mult (A:Type) (m:M A) : Prop :=
  ∀ (k:U) (f:MF A), m (fmult k f) ≈ k * (m f).

Lemma stable_minus_distr : ∀ (A:Type) (m:M A),
     stable_plus m → stable_inv m →
     ∀ (f g : MF A), g ≤ f → m (fminus f g) ≈ m f - m g.

Hint Resolve stable_minus_distr.

Lemma inv_minus_distr : ∀ (A:Type) (m:M A),
     stable_plus m → stable_inv m →
     ∀ (f : MF A), m (finv f) ≈ m (fone A) - m f.
Hint Resolve inv_minus_distr.

Lemma le_minus_distr : ∀ (A : Type)(m:M A),
    ∀ (f g:A → U), m (fminus f g) ≤ m f.
Hint Resolve le_minus_distr.

Lemma le_plus_distr : ∀ (A : Type)(m:M A),
    stable_plus m → stable_inv m → ∀ (f g:MF A), m (fplus f g) ≤ m f + m g.
Hint Resolve le_plus_distr.

Lemma le_esp_distr : ∀ (A : Type) (m:M A),
     stable_plus m → stable_inv m → le_esp m.

Lemma unit_stable_eq : ∀ (A:Type) (x:A), stable (unit x).

Lemma star_stable_eq : ∀ (A B:Type) (m:M A) (F:A → M B), stable (star m F).

Lemma unit_monotonic : ∀ (A:Type) (x:A) (f g : MF A),
   f ≤ g → unit x f ≤ unit x g.

Lemma star_monotonic : ∀ (A B:Type) (m:M A) (F:A → M B) (f g : MF B),
      f ≤ g → star m F f ≤ star m F g.

Lemma star_le_compat : ∀ (A B:Type) (m1 m2:M A) (F1 F2:A → M B),
       m1 ≤ m2 → F1 ≤ F2 → star m1 F1 ≤ star m2 F2.
Hint Resolve star_le_compat.

Lemma unit_stable_inv : ∀ (A:Type) (x:A), stable_inv (unit x).

Lemma star_stable_inv : ∀ (A B:Type) (m:M A) (F:A → M B),
   stable_inv m → (∀ a:A, stable_inv (F a)) → stable_inv (star m F).

Lemma unit_stable_plus : ∀ (A:Type) (x:A), stable_plus (unit x).

Lemma star_stable_plus : ∀ (A B:Type) (m:M A) (F:A → M B),
   stable_plus m →
   (∀ a:A, ∀ f g, fplusok f g → (F a f) ≤ Uinv (F a g))
   → (∀ a:A, stable_plus (F a)) → stable_plus (star m F).

Lemma unit_le_plus : ∀ (A:Type) (x:A), le_plus (unit x).

Lemma star_le_plus : ∀ (A B:Type) (m:M A) (F:A → M B),
   le_plus m →
   (∀ a:A, ∀ f g, fplusok f g → (F a f) ≤ Uinv (F a g))
   → (∀ a:A, le_plus (F a)) → le_plus (star m F).

Lemma unit_stable_mult : ∀ (A:Type) (x:A), stable_mult (unit x).

Lemma star_stable_mult : ∀ (A B:Type) (m:M A) (F:A → M B),
   stable_mult m → (∀ a:A, stable_mult (F a)) → stable_mult (star m F).

Lemma unit_continuous : ∀ (A:Type) (x:A), continuous (unit x).

Lemma star_continuous : ∀ (A B : Type) (m : M A)(F: A → M B),
    continuous m → (∀ x, continuous (F x)) → continuous (star m F).