Library U_prop

Properties of operators on 0,1


Set Implicit Arguments.

Set Strict Implicit.

Require Import U_base.

Require Export Arith.

Module Univ_prop (Univ:Universe).

Import Univ.




Hint Resolve Ueq_refl.

Hint Resolve Upos Unit Udiff_0_1 Unth_prop Ueq_le.

Hint Resolve Uplus_sym Uplus_assoc Umult_sym Umult_assoc.

Hint Resolve Uinv_one Uinv_opp_left Uinv_plus_left.

Hint Resolve Uplus_zero_left Umult_one_left Udistr_plus_right Udistr_inv_right.

Hint Resolve Uplus_le_compat_right Umult_le_compat_right Uinv_le_compat.

Hint Resolve lub_le le_lub lub_eq_mult lub_eq_plus_cte_right.

Hint Resolve Ule_total.

Hint Immediate Ueq_sym Ule_antisym Ueq_double_neg.

Open Scope U_scope.




Lemma Ule_0_1 : U0 <= U1.




Lemma Ule_refl : forall x:U,(x <= x).

Hint Resolve Ule_refl.




Lemma Ueq_trans : forall x y z:U, x == y -> y == z -> x == z.

Hint Resolve Ueq_trans.




Lemma Uplus_eq_compat_right :

    forall x y z:U, x == y -> (x + z) == (y + z).




Hint Resolve Uplus_eq_compat_right.




Lemma Uplus_eq_compat_left : 

  forall x y z:U, x == y -> (z + x) == (z + y).




Lemma Umult_eq_compat_right : 

forall x y z:U, x == y -> (x * z) == (y * z).

Hint Resolve Umult_eq_compat_right.




Lemma Umult_eq_compat_left : 

  forall x y z:U, x == y -> (z * x) == (z * y).




Hint Resolve Uplus_eq_compat_left Umult_eq_compat_left.




Lemma Uinv_opp_right : forall x, x + Uinv x == U1.

Hint Resolve Uinv_opp_right.

Definition of


Definition Ult (r1 r2:U) : Prop := ~(r2 <= r1).




Infix "<" := Ult : U_scope.




Hint Unfold Ult.




Lemma Usetoid : Setoid_Theory U Ueq.




Add Setoid U Ueq Usetoid.




Add Morphism Uplus : Uplus_eq_compat.




Add Morphism Umult : Umult_eq_compat.




Add Morphism Ule : Ule_eq_compat.




Add Morphism Uinv : Uinv_eq_compat.




Add Morphism Ult : Ult_eq_compat.

Left normal form with respect to associativity


Ltac norm_assoc_left := 

     match goal with 

      | |- context [(Uplus ?X1 (Uplus ?X2 ?X3))] 

        => (setoid_rewrite (Uplus_assoc X1 X2 X3))

     end.




Ltac norm_assoc_right := 

     match goal with 

      | |- context [(Uplus (Uplus ?X1 ?X2) ?X3)] 

        => (setoid_rewrite <- (Uplus_assoc X1 X2 X3))

     end.

Properties of





Lemma Ule_double_neg : 

      forall x y, ~~x <= y -> x <= y.




Lemma Ule_zero_eq : 

     forall x, x <= U0 -> x == U0.




Lemma Uge_one_eq : 

     forall x, U1 <= x -> x == U1.




Hint Immediate Ule_zero_eq Uge_one_eq.

Properties of





Lemma Ult_neq : forall x y:U, x < y -> ~x == y.




Lemma Ult_neq_rev : forall x y:U, x < y -> ~y == x.




Lemma Ult_le : forall x y:U, x < y -> x <= y.




Lemma Ule_diff_lt : forall x y : U, 

    x <= y -> ~x==y -> x < y.




Hint Immediate Ult_neq Ult_neq_rev Ult_le.

Hint Resolve Ule_diff_lt.




Lemma Udistr_plus_left : 

    forall x y z:U, (y <= (Uinv z)) -> (x * (y + z)) == (x * y + x * z).




Lemma Udistr_inv_left : 

  forall x y:U, Uinv (x * y) == (x * (Uinv y)) + Uinv x.




Hint Resolve Uinv_eq_compat Udistr_plus_left Udistr_inv_left.




Lemma Uplus_perm2 : forall x y z : U, x + (y + z) == y + (x + z).




Lemma Umult_perm2 : forall x y z : U, x * (y * z) == y * (x * z).




Lemma Uplus_perm3 : forall x y z : U, (x + (y + z)) == z + (x + y).




Lemma Umult_perm3 : forall x y z : U, (x * (y * z)) == z * (x * y).




Hint Resolve Uplus_perm2 Umult_perm2 Uplus_perm3 Umult_perm3.




Lemma Uplus_le_compat_left :

forall x y z:U, (x <= y) -> (z + x <= z + y).




Hint Resolve Uplus_le_compat_left.




Lemma Uplus_le_compat :

forall x y z t:U, (x <= y) -> (z <= t) -> (x + z <= y + t).

Hint Immediate Uplus_le_compat.




Lemma Uplus_zero_right : forall x:U, (x + U0) == x.

Hint Resolve Uplus_zero_right.




Lemma Uinv_zero : (Uinv U0) == U1.

Hint Resolve Uinv_zero.




Lemma Uinv_inv : forall x : U, Uinv (Uinv x) == x.

Hint Resolve Uinv_inv.




Lemma Uinv_simpl : 

  forall x y : U, (Uinv x) == Uinv y -> x == y.




Hint Immediate Uinv_simpl.




Lemma Umult_le_compat_left : 

 forall x y z: U,  x <= y -> (z * x) <= (z * y).




Hint Resolve Umult_le_compat_left.




Lemma Umult_one_right : forall x:U, (x * U1) == x.




Hint Resolve Umult_one_right.




Lemma Uplus_eq_simpl_right : 

forall x y z:U, (z <= (Uinv x)) -> (z <= (Uinv y)) -> ((x + z) == (y + z)) -> (x == y).




Lemma Ule_plus_right : forall x y, (x <= x + y).




Lemma Ule_plus_left : forall x y, (y <= x + y).




Hint Resolve Ule_plus_right Ule_plus_left.




Lemma Ule_mult_right : forall x y, (x * y <= x ).




Lemma Ule_mult_left : forall x y, (x * y <= y).




Hint Resolve Ule_mult_right Ule_mult_left.




Lemma Uinv_le_perm_right : 

   forall x y:U, (x <= (Uinv y)) -> y <= (Uinv x).

Hint Resolve Uinv_le_perm_right.




Lemma Uinv_le_perm_left : 

   forall x y:U, ((Uinv x) <= y) -> (Uinv y) <= x.

Hint Resolve Uinv_le_perm_left.




Lemma Uinv_eq_perm_left : 

   forall x y:U, (x == (Uinv y)) -> Uinv x == y.




Hint Immediate Uinv_eq_perm_left.




Lemma Uinv_eq_perm_right : 

   forall x y:U, (Uinv x == y) ->  x == (Uinv y).




Hint Immediate Uinv_eq_perm_right.




Lemma Uinv_plus_right : 

  forall x y, y <= (Uinv x) -> Uinv (x + y) + y == Uinv x.

Hint Resolve Uinv_plus_right.




Lemma Uplus_eq_simpl_left : 

forall x y z:U, (x <= (Uinv y)) -> (x <= (Uinv z )) 

    -> ((x + y) == (x + z)) -> (y == z).




Lemma Uplus_eq_zero_left : 

forall x y:U, (x <= Uinv y) -> (x + y) == y -> x == U0.




Lemma Uinv_le_trans : 

forall x y z t, (x <= Uinv y) -> z<=x -> t<=y -> z<=Uinv t.

disequality





Lemma neq_sym : forall x y, ~ (x==y) -> ~y==x.




Hint Immediate neq_sym.




Lemma Uinv_neq_compat : forall x y, ~ (x == y) -> ~ (Uinv x == Uinv y).




Lemma Uinv_neq_simpl : forall x y, ~ (Uinv x == Uinv y) -> ~ (x == y).




Hint Resolve Uinv_neq_compat.

Hint Immediate Uinv_neq_simpl.




Lemma Uinv_neq_left : forall x y, ~ (x == Uinv y) -> ~ (Uinv x == y).




Lemma Uinv_neq_right : forall x y, ~ (Uinv x == y) -> ~ (x == Uinv y).

strict order





Lemma Ult_antirefl : forall x:U, ~ x < x.




Lemma Ult_0_1 : (U0 < U1).




Lemma Ule_lt_trans : forall x y z:U, x <= y -> y < z -> x < z.




Lemma Ult_le_trans : forall x y z:U, x < y -> y <= z -> x < z.




Lemma Ult_trans : forall x y z:U, x < y -> y < z -> x < z.




Hint Resolve Ult_0_1 Ult_antirefl.




Lemma not_Ult_le : forall x y, ~x < y -> y <= x.




Lemma Ule_not_lt : forall x y, x <= y -> ~ y < x.




Hint Immediate not_Ult_le Ule_not_lt.




Theorem Uplus_le_simpl_left : 

  forall x y z : U, z <= Uinv x -> z + x <= z + y -> x <= y.




Lemma Uplus_lt_compat_right : 

forall x y z:U, (z <= Uinv y) -> (x < y) -> ((x + z) < (y + z)).




Lemma Uplus_lt_compat_left :

forall x y z:U, (z <= Uinv y) -> (x < y) -> (z + x < z + y).




Hint Resolve Uplus_lt_compat_right Uplus_lt_compat_left.




Lemma Uplus_lt_compat :

forall x y z t:U, (z <= Uinv x) -> (t <= Uinv y) ->

    (x < y) -> (z < t) -> (x + z < y + t).




Hint Immediate Uplus_lt_compat.




Lemma Uplus_lt_simpl_left :

forall x y z:U, (z <= Uinv y) -> (z + x) < (z + y) -> x < y.




Lemma Uplus_lt_simpl_right :

forall x y z:U, (z <= Uinv y) -> (x + z) < (y + z) -> x < y.




Lemma Uplus_one_le : forall x y, x + y == U1 -> Uinv y <= x.

Hint Immediate Uplus_one_le.




Theorem Uplus_eq_zero : 

 forall x : U, (x <= Uinv x) -> (x + x) == x -> x == U0.




Lemma Umult_zero_left : forall x:U, (U0 * x) == U0.




Hint Resolve Umult_zero_left.




Lemma Umult_zero_right : forall x:U, (x * U0) == U0.




Hint Resolve Uplus_eq_zero Umult_zero_right.

Compatibility of operations with respect to order.





Lemma Umult_le_simpl_right : 

 forall x y z:U, ~(U0 == z) -> (x * z) <= (y * z) -> x <= y.

Hint Resolve Umult_le_simpl_right.




Lemma Umult_simpl_right : 

 forall x y z:U, ~(U0 == z) -> (x * z) == (y * z) -> x == y.




Lemma Umult_simpl_left : 

 forall x y z:U, ~(U0 == x) -> (x * y) == (x * z) -> y == z.




Lemma Umult_lt_compat_right :

 forall x y z:U, ~(U0 == z) -> x < y -> (x * z) < (y * z).




Lemma Umult_lt_compat_left :

 forall x y z:U, ~(U0 == z) -> x < y -> (z * x) < (z * y).




Lemma Umult_lt_simpl_right :

 forall x y z:U, ~(U0 == z) -> (x * z) < (y * z) -> x < y.




Lemma Umult_lt_simpl_left :

 forall x y z:U, ~(U0 == z) -> (z * x) < (z * y) -> x < y.




Hint Resolve Umult_lt_compat_left Umult_lt_compat_right.

More Properties





Lemma Uplus_one : forall x y:U, 

    Uinv x <= y -> x + y == U1.

Hint Resolve Uplus_one.




Lemma Uplus_one_right : forall x:U, x + U1 == U1.




Lemma Uplus_one_left : forall x:U, U1 + x == U1.

Hint Resolve Uplus_one_right Uplus_one_left. 




Lemma Uinv_mult_simpl : forall x y z t, 

    x <= Uinv y -> (x * z) <= Uinv (y * t).

Hint Resolve Uinv_mult_simpl.




Lemma Umult_inv_plus : 

  forall x y, x * Uinv y + y == x + y * Uinv x.




Hint Resolve Umult_inv_plus.




Lemma Umult_inv_plus_le : 

  forall x y z, y <= z -> x * Uinv y + y <= x * Uinv z + z.




Hint Resolve Umult_inv_plus_le.

Definition of


Fixpoint Uexp (x:U) (n:nat) {struct n} : U :=

   match n with O => U1 | (S p) => x * Uexp x p end.

Definition of

A conjonction operation which coincides with min and mult on 0 and 1, see Morgan & McIver





Definition Uesp (x y:U) := Uinv (Uinv x + Uinv y).




Infix "&" := Uesp  (left associativity, at level 40) : U_scope.




Lemma Uinv_plus_esp : 

   forall x y, Uinv (x + y) == Uinv x & Uinv y.

Hint Resolve Uinv_plus_esp.




Lemma Uinv_esp_plus : 

   forall x y, Uinv (x & y) == Uinv x + Uinv y.

Hint Resolve Uinv_esp_plus.




Lemma Uesp_sym : forall x y : U, x & y == y & x.




Lemma Uesp_one_right : forall x : U, x & U1 == x.




Lemma Uesp_zero : 

   forall x y, x <= Uinv y -> x & y == U0.




Hint Resolve Uesp_sym Uesp_one_right Uesp_zero.




Lemma Uesp_zero_right : forall x : U, x & U0 == U0.




Lemma Uesp_zero_left : forall x : U, U0 & x == U0.




Hint Resolve Uesp_zero_right Uesp_zero_left.

Definition of





Definition Uminus (x y:U) := Uinv (Uinv x + y).




Infix "-" := Uminus : U_scope.




Lemma Uminus_le_compat_left : 

  forall x y z, x <= y -> x - z <= y - z.




Lemma Uminus_le_compat_right : 

  forall x y z, y <= z -> x - z <= x - y.




Hint Resolve Uminus_le_compat_left Uminus_le_compat_right.




Add Morphism Uminus : Uminus_eq_compat.

Hint Immediate Uminus_eq_compat.




Lemma Uminus_zero_right : forall x, x - U0 == x.




Lemma Uminus_one_left : forall x, U1 - x == Uinv x.




Lemma Uminus_le_zero : forall x y, x <= y -> x - y == U0.




Hint Resolve Uminus_zero_right Uminus_one_left Uminus_le_zero.




Lemma Uminus_plus_simpl : 

  forall x y, y <= x -> (x - y) + y == x.




Lemma Uminus_plus_zero :

  forall x y, x <= y -> (x - y) + y == y.




Hint Resolve Uminus_plus_simpl Uminus_plus_zero.




Lemma Uesp_minus_distr_left : 

  forall x y z, (x & y) - z  == (x - z) & y.




Lemma Uesp_minus_distr_right : 

  forall x y z, (x & y) - z  == x & (y - z).




Hint Resolve Uesp_minus_distr_left Uesp_minus_distr_right.




Lemma Uesp_minus_distr : 

  forall x y z t, (x & y) - (z + t) == (x - z) & (y - t).

Hint Resolve Uesp_minus_distr.

Definition of max





Definition max (x y : U) : U := (x - y) + y.




Lemma max_le_right : forall x y : U, y <= x -> (max x y) == x.




Lemma max_le_left : forall x y : U, x <= y -> (max x y) == y.




Hint Resolve max_le_right max_le_left.




Lemma max_le_case : forall x y : U, (max x y) == x \/ (max x y) == y.




Add Morphism max : max_eq_compat.




Lemma Uplus_minus_simpl_right : 

  forall x y, y <= Uinv x -> (x + y) - y == x.

Hint Resolve Uplus_minus_simpl_right.




Lemma Uplus_minus_simpl_left : 

  forall x y, y <= Uinv x -> (x + y) - x == y.




Lemma Uminus_assoc_left : 

  forall x y z, (x - y) - z == x - (y + z).




Hint Resolve Uminus_assoc_left.




Lemma Uminus_le_perm_left : 

  forall x y z, y <= x -> x - y <= z -> x <= z + y.




Lemma Uplus_le_perm_left : 

  forall x y z, y <= x -> x <= y + z  -> x - y <= z.




Lemma Uminus_eq_perm_left : 

  forall x y z, y <= x -> x - y == z -> x == z + y.




Lemma Uplus_eq_perm_left : 

  forall x y z, y <= Uinv z -> x == y + z  -> x - y == z.




Hint Resolve Uminus_le_perm_left Uminus_eq_perm_left.

Hint Resolve Uplus_le_perm_left Uplus_eq_perm_left.




Lemma Uminus_le_perm_right : 

  forall x y z, z <= y -> x <= y - z -> x + z <= y.




Lemma Uplus_le_perm_right : 

  forall x y z, z <= Uinv x -> x + z <= y  -> x <= y - z.




Hint Resolve Uminus_le_perm_right Uplus_le_perm_right.




Lemma Uminus_le_perm : 

  forall x y z, z <= y -> x <= Uinv z -> x <= y - z -> z <= y - x.




Hint Resolve Uminus_le_perm.




Lemma Uminus_eq_perm_right : 

  forall x y z, z <= y -> x == y - z -> x + z == y.




Hint Resolve Uminus_eq_perm_right.




Lemma Uminus_zero_le : 

forall x y, x - y == U0 -> x <= y.




Lemma Uminus_lt_non_zero : 

forall x y, x < y -> ~y - x == U0.

Hint Immediate Uminus_zero_le Uminus_lt_non_zero.




Lemma Ult_le_nth : 

forall x y, x < y -> (exists n, x <= y - Unth n).




Lemma Uminus_distr_left : 

forall x y z, (x - y) * z == (x * z) - (y * z).




Hint Resolve Uminus_distr_left.




Lemma Uminus_distr_right : 

forall x y z,  x * (y - z) == (x * y) - (x * z).




Hint Resolve Uminus_distr_right.




Lemma Uminus_assoc_right : 

  forall x y z, y <= x -> z <= y -> x - (y - z) == (x - y) + z.

Properties of generalized sums





Definition sigma (alpha : nat -> U) (n:nat) := comp Uplus U0 alpha n.




Lemma sigma0 : forall (alpha : nat -> U) (n:nat), sigma alpha 0 = U0.




Lemma sigmaS : forall (alpha : nat -> U) (n:nat), 

    sigma alpha (S n) = (alpha n) + (sigma alpha n).




Lemma sigma_incr : forall (f : nat -> U) (n m:nat), 

 (n <= m)%nat -> (sigma f n) <= (sigma f m).




Hint Resolve sigma_incr.




Lemma sigma_eq_compat : forall (f g: nat -> U) (n:nat), 

 (forall k, (k <= n)%nat -> f k == g k) -> (sigma f n) == (sigma g n).




Lemma sigma_le_compat : forall (f g: nat -> U) (n:nat), 

 (forall k, (k <= n)%nat -> f k <= g k) -> (sigma f n) <= (sigma g n).




Hint Resolve sigma_eq_compat sigma_le_compat.

Properties of `Unth`


Lemma Unth_zero : Unth 0 == U1.




Lemma Unth_one : Unth 1 == Uinv (Unth 1).




Hint Resolve Unth_zero Unth_one.




Lemma Unth_one_plus : Unth 1 + Unth 1 == U1.




Hint Resolve Unth_one_plus.




Lemma Unth_not_null : forall n, ~(U0 == Unth n).




Hint Resolve Unth_not_null.




Lemma Unth_prop_sigma : forall n, 

      Unth n == Uinv (sigma (fun k => Unth n) n).




Hint Resolve Unth_prop_sigma.




Lemma Unth_sigma_n : 

  forall n : nat, ~(U1 == sigma (fun k => Unth n) n).




Lemma Unth_sigma_Sn : 

  forall n : nat, U1 == sigma (fun k => Unth n) (S n).




Hint Resolve Unth_sigma_n Unth_sigma_Sn.




Lemma Unth_decr : forall n, Unth (S n) < Unth n.

Hint Resolve Unth_decr.




Lemma Unth_le_half : forall n, Unth (S n) <= Unth 1.

Hint Resolve Unth_le_half.

mean of two numbers


Definition mean (x y:U) := Unth 1 * x + Unth 1 * y.




Lemma mean_eq : forall x:U, mean x x ==x.




Lemma mean_le_compat_right : 

  forall x y z, y <= z -> mean x y <= mean x z.




Lemma mean_le_compat_left : 

  forall x y z, x <= y -> mean x z <= mean y z.




Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right.




Lemma mean_lt_compat_right : 

  forall x y z, y < z -> mean x y < mean x z.




Lemma mean_lt_compat_left : 

  forall x y z, x < y -> mean x z < mean y z.




Hint Resolve mean_eq mean_le_compat_left mean_le_compat_right.

Hint Resolve mean_lt_compat_left mean_lt_compat_right.




Lemma mean_le_up : forall x y, x <= y -> mean x y <= y.




Lemma mean_le_down : forall x y, x <= y -> x <= mean x y.




Lemma mean_lt_up : forall x y, x < y -> mean x y < y.




Lemma mean_lt_down : forall x y, x < y -> x < mean x y.




Hint Resolve mean_le_up mean_le_down mean_lt_up mean_lt_down.




Lemma le_half_inv : 

   forall x, x <= Unth 1 -> x <= Uinv x.




Hint Immediate le_half_inv.




Lemma ge_half_inv : 

   forall x, Unth 1 <= x  -> Uinv x <= x.




Hint Immediate ge_half_inv.




Lemma Uinv_le_half_left : forall x, x <= Unth 1 -> Unth 1 <= Uinv x.




Lemma Uinv_le_half_right : forall x, Unth 1 <= x -> Uinv x <= Unth 1.




Hint Resolve Uinv_le_half_left Uinv_le_half_right.




Lemma half_twice : forall x, 

   (x <= Unth 1) -> (Unth 1) * (x + x) == x.




Lemma half_twice_le : forall x, (Unth 1) * (x + x) <= x.




Lemma Uinv_half : forall x, 

 (Unth 1) * (Uinv x)  + (Unth 1) == Uinv ((Unth 1) * x).




Lemma half_esp : 

forall x, 

   (Unth 1 <= x) -> (Unth 1) * (x & x) + Unth 1 == x.




Lemma half_esp_le : 

  forall x, x <= (Unth 1) * (x & x) + Unth 1.

Hint Resolve half_esp_le.

Density


Lemma Ule_lt_lim : 

        forall x y,  (forall t, t < x -> t <= y) -> x <= y.

Properties of





Lemma half_le : 

   forall x y, y <= Uinv y -> x <= y + y -> (Unth 1) * x <= y.




Lemma half_Unth : forall n, (Unth 1)*(Unth n) <= Unth (S n).




Hint Resolve half_le half_Unth.




Lemma half_exp : 

   forall n, Uexp (Unth 1) n == Uexp (Unth 1) (S n) + Uexp (Unth 1) (S n).

Properties of least upper bounds





Section lubs.




Lemma lub_le_stable : 

   forall f g : nat -> U, (forall n, f n <= g n)

    -> lub f <= lub g.




Hint Resolve lub_le_stable.




Lemma lub_eq_stable : 

   forall f g, (forall n, f n == g n) -> lub f == lub g.




Hint Resolve lub_eq_stable.




Lemma lub_zero : (lub (fun n => U0)) == U0.




Lemma lub_un : (lub (fun n => U1)) == U1.




Lemma lub_cte : forall c:U, (lub (fun n => c)) == c.




Hint Resolve lub_zero lub_un lub_cte.




Lemma lub_eq_plus_cte_left : 

   forall (f : nat -> U) (k:U), lub (fun n => k + (f n)) == k + (lub f).

Hint Resolve lub_eq_plus_cte_left.




Variables f g : nat -> U.




Hypothesis monf : (mon_seq Ule f).

Hypothesis mong : (mon_seq Ule g).




Lemma lub_lift : forall n, 

    (lub f) == (lub (fun k => f (n+k)%nat)).




Hint Resolve lub_lift.




Let sum := fun n => f n + g n.




Lemma mon_sum : mon_seq Ule sum.




Hint Resolve mon_sum.




Lemma lub_eq_plus : lub (fun n => (f n) + (g n)) == (lub f) + (lub g).

Hint Resolve lub_eq_plus.




Variables k : U.

Let prod := fun n => k * f n.




Lemma mon_prod : mon_seq Ule prod.




Let inv:= fun n => Uinv (g n).




Lemma lub_inv : 

   (forall n, f n <= inv n) -> lub f <= Uinv (lub g).




End lubs.

Properties of barycentre of two points


Section Barycentre.

Variables a b : U.

Hypothesis sum_le_one : a <= Uinv b.




Lemma Uinv_bary : 

   forall x y : U, 

   Uinv (a * x + b * y) == a * Uinv x + b * Uinv y + Uinv (a + b).

End Barycentre.




Lemma sigma_plus : 

  forall (f g : nat -> U) (n:nat),

  (sigma (fun k => (f k) + (g k)) n) == (sigma f n) + (sigma g n).




Definition retract (f : nat -> U) := 

   forall n, (f n) <= Uinv (sigma f n).




Lemma sigma_mult : 

  forall (f : nat -> U) (n:nat) (c:U),

  retract f -> (sigma (fun k => c * (f k)) n) == c * (sigma f n).

Hint Resolve sigma_mult.




Lemma sigma_prod_maj : 

 forall (f g : nat -> U), 

 forall n, (sigma (fun k => (f k) * (g k)) n) <= (sigma f n).




Hint Resolve sigma_prod_maj.




Lemma sigma_prod_le : 

 forall (f g : nat -> U) (c:U), 

 (forall k, (f k) <= c) -> (retract g) ->

 forall n, (sigma (fun k => (f k) * (g k)) n) <= c * (sigma g n).




Lemma sigma_prod_ge : 

 forall (f g : nat -> U) (c:U), 

 (forall k, c <= (f k)) -> (retract g) ->

 forall n, c * (sigma g n) <= (sigma (fun k => (f k) * (g k)) n).




Hint Resolve sigma_prod_maj sigma_prod_le  sigma_prod_ge.




Lemma sigma_inv : 

  forall (f g : nat -> U) (n:nat), (retract f) ->

  Uinv (sigma (fun k => (f k) * (g k)) n) ==

  (sigma (fun k => (f k) * Uinv (g k)) n) + Uinv (sigma f n).

Product by an integer





Definition Nmult (n: nat) (x : U) : U := sigma (fun k => x) n.

Condition for n */ x to be exact


Definition Nmult_def (n: nat) (x : U) := 

   match n with O => True | S p => x <= Unth p end.




Lemma Nmult_def_O : forall x, Nmult_def O x.

Hint Resolve Nmult_def_O.




Lemma Nmult_def_pred : 

  forall n x, Nmult_def (S n) x -> Nmult_def n x.




Hint Immediate Nmult_def_pred.

Hint Unfold Nmult_def.




Infix "*/" := Nmult (at level 60) : U_scope.




Lemma Nmult_0 : forall (x:U), (0*/x) = U0.




Lemma Nmult_S : forall (n:nat) (x:U), (S n*/x) = x + (n*/x).




Add Morphism Nmult : Nmult_eq_compat.




Lemma Nmult_le_compat_left : 

   forall (n:nat) (x y:U), (x <= y) -> (n */ x) <= (n */ y).




Lemma Nmult_le_compat_right : 

   forall (n m:nat) (x:U), (n <= m)%nat -> (n */ x) <= (m */ x).




Lemma Nmult_Unth_prop : 

   forall n:nat, Unth n == Uinv (n*/ (Unth n)).

Hint Resolve Nmult_Unth_prop.




Lemma Nmult_Unth : 

   forall n:nat, (n*/ Unth n) == Uinv (Unth n).




Hint Immediate Nmult_eq_compat.




Hint Resolve Nmult_le_compat_left Nmult_le_compat_right Nmult_Unth.




Lemma Nmult_Umult_assoc 

  : forall (n:nat) (x y:U), (Nmult_def n x) -> (n*/(x*y))== (n*/x)*y.

Tactic for simplification of goals





Ltac Usimpl := 

   match goal with 

      |- context [(Uplus U0 ?x)] =>     

                  setoid_rewrite (Uplus_zero_left x)

 |    |- context [(Uplus ?x U0)] =>     

                  setoid_rewrite (Uplus_zero_right x)

 |    |- context [(Uplus U1 ?x)] =>     

                  setoid_rewrite (Uplus_one_left x)

 |    |- context [(Uplus ?x U1)] =>     

                  setoid_rewrite (Uplus_one_right x)

 |    |- context [(Umult U0 ?x)] =>     

                  setoid_rewrite (Umult_zero_left x)

 |    |- context [(Umult ?x U0)] =>     

                  setoid_rewrite (Umult_zero_right x)

 |    |- context [(Umult U1 ?x)] =>     

                  setoid_rewrite (Umult_one_left x)

 |    |- context [(Umult ?x U1)] =>     

                  setoid_rewrite (Umult_one_right x)

 |    |- context [(Uminus U0 ?x)] =>     

                  setoid_rewrite (Uminus_le_zero U0 x); 

                  [apply (Upos x)| idtac]

 |    |- context [(Uminus ?x U0)] =>     

                  setoid_rewrite (Uminus_zero_right x)

 |    |- context [(Uminus ?x U1)] =>     

                  setoid_rewrite (Uminus_le_zero x U1);

                  [apply (Unit x)| idtac]

 |    |- context [(Uinv (Uinv ?x))] =>     

                  setoid_rewrite (Uinv_inv x)

 |    |- (Ule (Uplus ?x ?y) (Uplus ?x ?z)) => 

                  apply Uplus_le_compat_left

 |    |- (Ule (Uplus ?x ?z) (Uplus ?y ?z)) => 

                  apply Uplus_le_compat_right

 |    |- (Ule (Uplus ?x ?z) (Uplus ?z ?y)) => 

                  setoid_rewrite (Uplus_sym z y); apply Uplus_le_compat_right

 |    |- (Ule (Uplus ?x ?y) (Uplus ?z ?x)) => 

                  setoid_rewrite (Uplus_sym x y); apply Uplus_le_compat_right

 |    |- (Ueq (Uplus ?x ?y) (Uplus ?x ?z)) => 

                  apply Uplus_eq_compat_left

 |    |- (Ueq (Uplus ?x ?z) (Uplus ?y ?z)) => 

                  apply Uplus_eq_compat_right

 |    |- (Ueq (Uplus ?x ?z) (Uplus ?z ?y)) => 

                  setoid_rewrite (Uplus_sym z y); apply Uplus_eq_compat_right

 |    |- (Ueq (Uplus ?x ?y) (Uplus ?z ?x)) => 

                  setoid_rewrite (Uplus_sym x y); apply Uplus_eq_compat_right

 |    |- (Ule (Umult ?x ?y) (Umult ?x ?z)) => 

                  apply Umult_le_compat_left

 |    |- (Ule (Umult ?x ?z) (Umult ?y ?z)) => 

                  apply Umult_le_compat_right

 |    |- (Ule (Umult ?x ?z) (Umult ?z ?y)) => 

                  setoid_rewrite (Umult_sym z y); apply Umult_le_compat_right

 |    |- (Ule (Umult ?x ?y) (Umult ?z ?x)) => 

                  setoid_rewrite (Umult_sym x y); apply Umult_le_compat_right

 |    |- (Ueq (Umult ?x ?y) (Umult ?x ?z)) => 

                  apply Umult_eq_compat_left

 |    |- (Ueq (Umult ?x ?z) (Umult ?y ?z)) => 

                  apply Umult_eq_compat_right

 |    |- (Ueq (Umult ?x ?z) (Umult ?z ?y)) => 

                  setoid_rewrite (Umult_sym z y); apply Umult_eq_compat_right

 |    |- (Ueq (Umult ?x ?y) (Umult ?z ?x)) => 

                  setoid_rewrite (Umult_sym x y); apply Umult_eq_compat_right

end.




End Univ_prop.

This page has been generated by coqdoc

Library U_prop

Definition of

Left normal form with respect to associativity

Properties of

Properties of

disequality

strict order

More Properties

Definition of

Definition of

Definition of

Definition of max

Properties of generalized sums

Properties of Unth

mean of two numbers

Density

Properties of

Properties of least upper bounds

Properties of barycentre of two points

Product by an integer

Tactic for simplification of goals

Properties of `Unth`