Top

Module mathcomp.classical.mathcomp_extra

Require Import BinPos.
From mathcomp Require choice.
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
From mathcomp Require Import finset interval.


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.

MathComp 2.1 additions  

From mathcomp Require Import poly.

Definition coefE :=
  (coef0, coef1, coefC, coefX, coefXn,
   coefZ, coefMC, coefCM, coefXnM, coefMXn, coefXM, coefMX, coefMNn, coefMn,
   coefN, coefB, coefD,
   coef_cons, coef_Poly, coef_poly,
   coef_deriv, coef_nderivn, coef_derivn, coef_map, coef_sum,
   coef_comp_poly).

Module Export Pdeg2.

Module Export Field.

Section Pdeg2Field.
Variable F : fieldType.
Hypothesis nz2 : 2%:R != 0 :> F.

Variable p : {poly F}.
Hypothesis degp : size p = 3%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Let pneq0 : p != 0
Let aneq0 : a != 0.
Let a2neq0 : 2%:R * a != 0
Let sqa2neq0 : (2%:R * a) ^+ 2 != 0

Let aa4 : 4%:R * a * a = (2%:R * a)^+2.

Let splitr (x : F) : x = x / 2%:R + x / 2%:R.

Let pE : p = a *: 'X^2 + b *: 'X + c%:P.

Let delta := b ^+ 2 - 4%:R * a * c.

Lemma deg2_poly_canonical :
  p = a *: (('X + (b / (2%:R * a))%:P)^+2 - (delta / (4%:R * a ^+ 2))%:P).

Variable r : F.
Hypothesis r_sqrt_delta : r ^+ 2 = delta.

Let r1 := (- b - r) / (2%:R * a).
Let r2 := (- b + r) / (2%:R * a).

Lemma deg2_poly_factor : p = a *: ('X - r1%:P) * ('X - r2%:P).

End Pdeg2Field.
End Field.

Module Real.

Section Pdeg2Real.

Variable F : realFieldType.

Section Pdeg2RealConvex.

Variable p : {poly F}.
Hypothesis degp : size p = 3%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Hypothesis age0 : 0 <= a.

Let delta := b ^+ 2 - 4%:R * a * c.

Let pneq0 : p != 0
Let aneq0 : a != 0.
Let agt0 : 0 < a
Let a4gt0 : 0 < 4%:R * a

Lemma deg2_poly_min x : p.[- b / (2%:R * a)] <= p.[x].

Lemma deg2_poly_minE : p.[- b / (2%:R * a)] = - delta / (4%:R * a).

Lemma deg2_poly_ge0 : reflect (forall x, 0 <= p.[x]) (delta <= 0).

End Pdeg2RealConvex.

End Pdeg2Real.

Section Pdeg2RealClosed.

Variable F : rcfType.

Section Pdeg2RealClosedConvex.

Variable p : {poly F}.
Hypothesis degp : size p = 3%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Let nz2 : 2%:R != 0 :> F

Let delta := b ^+ 2 - 4%:R * a * c.

Let r1 := (- b - Num.sqrt delta) / (2%:R * a).
Let r2 := (- b + Num.sqrt delta) / (2%:R * a).

Lemma deg2_poly_factor : 0 <= delta -> p = a *: ('X - r1%:P) * ('X - r2%:P).

End Pdeg2RealClosedConvex.

End Pdeg2RealClosed.
End Real.

End Pdeg2.

Section Degle2PolyRealConvex.

Variable (F : realFieldType) (p : {poly F}).
Hypothesis degp : (size p <= 3)%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Let delta := b ^+ 2 - 4%:R * a * c.

Lemma deg_le2_poly_delta_ge0 : 0 <= a -> (forall x, 0 <= p.[x]) -> delta <= 0.

End Degle2PolyRealConvex.

Section Degle2PolyRealClosedConvex.

Variable (F : rcfType) (p : {poly F}).
Hypothesis degp : (size p <= 3)%N.

Let a := p`_2.
Let b := p`_1.
Let c := p`_0.

Let delta := b ^+ 2 - 4%:R * a * c.

Lemma deg_le2_poly_ge0 : (forall x, 0 <= p.[x]) -> delta <= 0.

End Degle2PolyRealClosedConvex.

Lemma natr1 (R : ringType) (n : nat) : (n%:R + 1 = n.+1%:R :> R)%R.

Lemma nat1r (R : ringType) (n : nat) : (1 + n%:R = n.+1%:R :> R)%R.

MathComp 2.2 additions  

Notation "f \min g" := (Order.min_fun f g) : function_scope.
Notation "f \max g" := (Order.max_fun f g) : function_scope.

Lemma ler_sqrt {R : rcfType} (a b : R) :
  (0 <= b -> (Num.sqrt a <= Num.sqrt b) = (a <= b))%R.

MathComp 2.3 additions  

Lemma invf_plt (F : numFieldType) :
  {in Num.pos &, forall x y : F, (x^-1 < y)%R = (y^-1 < x)%R}.

not yet backported  

Lemma deg_le2_ge0 (F : rcfType) (a b c : F) :
  (forall x, 0 <= a * x ^+ 2 + b * x + c)%R -> (b ^+ 2 - 4%:R * a * c <= 0)%R.

Section dependent_choice_Type.
Context X (R : X -> X -> Prop).

Lemma dependent_choice_Type : (forall x, {y | R x y}) ->
  forall x0, {f | f 0%N = x0 /\ forall n, R (f n) (f n.+1)}.
End dependent_choice_Type.

Section max_min.
Variable R : realFieldType.

Let nz2 : 2%:R != 0 :> R

Lemma maxr_absE (x y : R) : Num.max x y = (x + y + `|x - y|) / 2%:R.

Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.

End max_min.

Notation trivial := (ltac:(done)).

Section bigmax_seq.
Context d {T : orderType d} {x : T} {I : eqType}.
Variables (r : seq I) (i0 : I) (P : pred I).

Lemma le_bigmax_seq F :
  i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_(i <- r | P i) F i)%O.

Lemma bigmax_sup_seq (m : T) (F : I -> T) :
  i0 \in r -> P i0 -> (m <= F i0)%O ->
  (m <= \big[Order.max/x]_(i <- r | P i) F i)%O.

End bigmax_seq.
Arguments le_bigmax_seq {d T} x {I r} i0 P.

Lemma gerBl {R : numDomainType} (x y : R) : 0 <= y -> x - y <= x.

Section normr.
Variable R : realDomainType.

Definition Rnpos : qualifier 0 R := [qualify x : R | x <= 0].
Lemma nposrE x : (x \is Rnpos) = (x <= 0)

Lemma ger0_le_norm :
  {in Num.nneg &, {mono (@Num.Def.normr _ R) : x y / x <= y}}.

Lemma gtr0_le_norm :
  {in Num.pos &, {mono (@Num.Def.normr _ R) : x y / x <= y}}.

Lemma ler0_ge_norm :
  {in Rnpos &, {mono (@Num.Def.normr _ R) : x y / x <= y >-> x >= y}}.

Lemma ltr0_ge_norm :
  {in Num.neg &, {mono (@Num.Def.normr _ R) : x y / x <= y >-> x >= y}}.

End normr.

Lemma leq_ltn_expn m : exists n, (2 ^ n <= m.+1 < 2 ^ n.+1)%N.

Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) :=
  {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}.

Section path_lt.
Context d {T : orderType d}.
Implicit Types (a b c : T) (s : seq T).

Lemma last_filterP a (P : pred T) s :
  P a -> P (last a [seq x <- s | P x]).

Lemma path_lt_filter0 a s : path <%O a s -> [seq x <- s | (x < a)%O] = [::].

Lemma path_lt_filterT a s : path <%O a s -> [seq x <- s | (a < x)%O] = s.

Lemma path_lt_head a b s : (a < b)%O -> path <%O b s -> path <%O a s.

Lemma path_lt_last_filter a b c s :
  (a < c)%O -> (c < b)%O -> path <%O a s -> last a s = b ->
  last c [seq x <- s | (c < x)%O] = b.

Lemma path_lt_le_last a s : path <%O a s -> (a <= last a s)%O.

End path_lt.
Arguments last_filterP {d T a} P s.

Lemma sumr_le0 (R : numDomainType) I (r : seq I) (P : pred I) (F : I -> R) :
  (forall i, P i -> F i <= 0)%R -> (\sum_(i <- r | P i) F i <= 0)%R.

Inductive boxed T := Box of T.

Reserved Notation "`1- r" (format "`1- r", at level 2).
Reserved Notation "f \^-1" (at level 3, format "f \^-1", left associativity).


Lemma fset_nat_maximum (X : choiceType) (A : {fset X})
    (f : X -> nat) : A != fset0 ->
  (exists i, i \in A /\ forall j, j \in A -> f j <= f i)%nat.

Lemma image_nat_maximum n (f : nat -> nat) :
  (exists i, i <= n /\ forall j, j <= n -> f j <= f i)%N.

Lemma card_fset_sum1 (T : choiceType) (A : {fset T}) :
  #|` A| = (\sum_(i <- A) 1)%N.

Arguments big_rmcond {R idx op I r} P.
Arguments big_rmcond_in {R idx op I r} P.

Reserved Notation "`1- x" (format "`1- x", at level 2).

Section onem.
Variable R : numDomainType.
Implicit Types r : R.

Definition onem r := 1 - r.
Local Notation "`1- r" := (onem r).

Lemma onem0 : `1-0 = 1

Lemma onem1 : `1-1 = 0

Lemma onemK r : `1-(`1-r) = r.

Lemma add_onemK r : r + `1- r = 1.

Lemma onem_gt0 r : r < 1 -> 0 < `1-r

Lemma onem_ge0 r : r <= 1 -> 0 <= `1-r.

Lemma onem_le1 r : 0 <= r -> `1-r <= 1.

Lemma onem_lt1 r : 0 < r -> `1-r < 1.

Lemma onemX_ge0 r n : 0 <= r -> r <= 1 -> 0 <= `1-(r ^+ n).

Lemma onemX_lt1 r n : 0 < r -> `1-(r ^+ n) < 1.

Lemma onemD r s : `1-(r + s) = `1-r - s.

Lemma onemMr r s : s * `1-r = s - s * r.

Lemma onemM r s : `1-(r * s) = `1-r + `1-s - `1-r * `1-s.

End onem.
Notation "`1- r" := (onem r) : ring_scope.

Lemma onemV (F : numFieldType) (x : F) : x != 0 -> `1-(x^-1) = (x - 1) / x.

Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N.

Lemma ler_gtP (R : numFieldType) (x y : R) :
  reflect (forall z, z > y -> x <= z) (x <= y).

Lemma ler_ltP (R : numFieldType) (x y : R) :
  reflect (forall z, z < x -> z <= y) (x <= y).

Definition inv_fun T (R : unitRingType) (f : T -> R) x := (f x)^-1%R.
Notation "f \^-1" := (inv_fun f) : ring_scope.
Arguments inv_fun {T R} _ _ /.

Definition bound_side d (T : porderType d) (c : bool) (x : itv_bound T) :=
  if x is BSide c' _ then c == c' else false.

Lemma real_ltr_distlC [R : numDomainType] [x y : R] (e : R) :
  x - y \is Num.real -> (`|x - y| < e) = (x - e < y < x + e).

Definition proj {I} {T : I -> Type} i (f : forall i, T i) := f i.

Section DFunWith.
Variables (I : eqType) (T : I -> Type) (f : forall i, T i).

Definition dfwith i (x : T i) (j : I) : T j :=
  if (i =P j) is ReflectT ij then ecast j (T j) ij x else f j.

Lemma dfwithin i x : dfwith x i = x.

Lemma dfwithout i (x : T i) j : i != j -> dfwith x j = f j.

Variant dfwith_spec i (x : T i) : forall j, T j -> Type :=
  | DFunWithin : dfwith_spec x x
  | DFunWithout j : i != j -> dfwith_spec x (f j).

Lemma dfwithP i (x : T i) (j : I) : dfwith_spec x (dfwith x j).

Lemma projK i (x : T i) : cancel (@dfwith i) (proj i).

End DFunWith.
Arguments dfwith {I T} f i x.

Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).

Section order_min.
Variables (d : unit) (T : orderType d).

Lemma lt_min_lt (x y z : T) : (Order.min x z < Order.min y z)%O -> (x < y)%O.

End order_min.