Module mathcomp.classical.mathcomp_extra

From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.

# MathComp extra This files contains lemmas and definitions recently added in mathcomp, in order to be able to compile analysis with older versions of mathcomp. ``` proj i f == f i, where f : forall i, T i dfwith f x == fun j => x if j = i, and f j otherwise given x : T i ```

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

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

MathComp 2.3 additions

Module .
Import Order.
Definition : disp_t.

Proof.

exact: Disp tt tt. Defined.

End Order.

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

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

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

Lemma : dfwith x i = x.

Proof.

by rewrite /dfwith; case: eqP => // ii; rewrite eq_axiomK. Qed.

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

Proof.

by rewrite /dfwith; case: eqP. Qed.

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

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

Proof.

by case: (eqVneq i j) => [<-|nij];
[rewrite dfwithin|rewrite dfwithout//]; constructor.
Qed.

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

Proof.

by move=> z; rewrite /proj dfwithin. Qed.

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

MathComp 2.4 additions

MathComp 2.5 additions

Section ssralg.
Lemma { : zmodType} ( : V) : x + (y - x) = y.

Proof.

by rewrite addrC subrK. Qed.

End ssralg.

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

Proof.

by move=> F0; elim/big_rec : _ => // i x Pi; apply/ler_wnDl/F0. Qed.

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

Proof.

by rewrite big_seq_fsetE/= sum1_card cardfE. Qed.

Lemma { : Order.disp_t} { : porderType disp}
[ : T] ( : bool) : (x < y)%O -> (x < y ?<= if C)%O.

Proof.

by case: C => //= /ltW. Qed.

MathComp 2.6 additions

Lemma { : pzRingType} ( : int) : (i + 1)%:~R = i%:~R + 1 :> R.

Proof.

by rewrite intrD. Qed.

Lemma { : pzRingType} ( : int) : (1 + i)%:~R = 1 + i%:~R :> R.

Proof.

by rewrite intrD. Qed.

Files

Module mathcomp.classical.mathcomp_extra