Files

  • mathcomp

    • Top source

    Module mathcomp.reals_stdlib.nsatz_realtype

    From Stdlib Require Import Nsatz.
    From mathcomp Require Import boot order ssralg ssrint ssrnum.
    From mathcomp Require Import boolp reals constructive_ereal.

    # nsatz for realType This file registers the ring corresponding to the MathComp-Analysis type realType to the tactic nsatz of Coq. This enables some automation used for example in the file trigo.v. Reference: - https://coq.inria.fr/refman/addendum/nsatz.html

    Import GRing.Theory Num.Theory.

    Unset SsrOldRewriteGoalsOrder.

    Local Open Scope ring_scope.

    Section Nsatz_realType.
    Variable
    T
    Source code
     : realType.

    Lemma
    Nsatz_realType_Setoid_Theory
    Source code
     : Setoid.Setoid_Theory T (@eq T).
    Proof.
    by constructor => [x //|x y //|x y z ->]. Qed.

    Definition
    Nsatz_realType0

    expand : forall [R : realFieldType], R -> \bar R expand is not universe polymorphic Arguments expand [R] r%_ring_scope expand is transparent Expands to: Constant mathcomp.reals.constructive_ereal.expand Declared in library mathcomp.reals.constructive_ereal, line 4590, characters 11-17

    Source code
     := (0%:R : T).
    Definition
    Nsatz_realType1

    lt_contract : forall [R : realFieldType], {mono contract (R:=R) : x y / (x < y)%E >-> (x < y)%R} lt_contract is not universe polymorphic Arguments lt_contract [R] x y lt_contract is transparent Expands to: Constant mathcomp.reals.constructive_ereal.lt_contract Declared in library mathcomp.reals.constructive_ereal, line 4654, characters 11-22

    Source code
     := (1%:R : T).
    Definition
    Nsatz_realType_add

    contract_inj : forall [R : realFieldType], injective (contract (R:=R)) contract_inj is not universe polymorphic Expanded type for implicit arguments contract_inj : forall [R : realFieldType] [x1 x2 : constructive_ereal_extended__canonical__Order_POrder], contract (R:=R) x1 = contract (R:=R) x2 -> x1 = x2 Arguments contract_inj [R x1 x2] _ contract_inj is transparent Expands to: Constant mathcomp.reals.constructive_ereal.contract_inj Declared in library mathcomp.reals.constructive_ereal, line 4655, characters 11-23

    Source code
     (
    x
    Source code
    y
    Source code
     : T) := (x + y)%R.
    Definition
    Nsatz_realType_mul

    lt_expand : forall [R : realFieldType], {in [pred r | (`|r| <= 1)%R] &, {mono expand (R:=R) : x y / (x < y)%R >-> (x < y)%E}} lt_expand is not universe polymorphic Expanded type for implicit arguments lt_expand : forall [R : realFieldType] [x y : R], x \in [pred r | (`|r| <= 1)%R] -> y \in [pred r | (`|r| <= 1)%R] -> (fun x0 : constructive_ereal_extended__canonical__Order_Preorder => [eta (> x0)%O]) (expand (R:=R) x) (expand (R:=R) y) = (fun x0 : R => [eta (> x0)%R]) x y Arguments lt_expand [R x y] _ _ lt_expand is transparent Expands to: Constant mathcomp.reals.constructive_ereal.lt_expand Declared in library mathcomp.reals.constructive_ereal, line 4661, characters 11-20

    Source code
     (
    x
    Source code
    y
    Source code
     : T) := (x * y)%R.
    Definition
    Nsatz_realType_sub

    expand_inj : forall [R : realFieldType], {in [pred r | (`|r| <= 1)%R] &, injective (expand (R:=R))} expand_inj is not universe polymorphic Expanded type for implicit arguments expand_inj : forall [R : realFieldType] [x y : R], x \in [pred r | (`|r| <= 1)%R] -> y \in [pred r | (`|r| <= 1)%R] -> expand (R:=R) x = expand (R:=R) y -> x = y Arguments expand_inj [R x y] _ _ _ expand_inj is transparent Expands to: Constant mathcomp.reals.constructive_ereal.expand_inj Declared in library mathcomp.reals.constructive_ereal, line 4662, characters 11-21

    Source code
     (
    x
    Source code
    y
    Source code
     : T) := (x - y)%R.
    Definition
    Nsatz_realType_opp

    ereal_ball : forall {R : realFieldType}, \bar R -> R -> \bar R -> bool ereal_ball is not universe polymorphic Arguments ereal_ball {R} x%_ereal_scope r%_ring_scope y%_ereal_scope ereal_ball is transparent Expands to: Constant mathcomp.reals.constructive_ereal.ereal_ball Declared in library mathcomp.reals.constructive_ereal, line 4696, characters 11-21

    Source code
     (
    x
    Source code
     : T) := (- x)%R.

    #[global]
    Instance
    Nsatz_realType_Ring_ops
    Source code
    :
       (@Ncring.Ring_ops T Nsatz_realType0 Nsatz_realType1
      Nsatz_realType_add
      Nsatz_realType_mul
      Nsatz_realType_sub
      Nsatz_realType_opp (@eq T)).
    Proof.
    Defined.

    #[global]
    Instance
    Nsatz_realType_Ring
    Source code
     : (Ncring.Ring (Ro:=Nsatz_realType_Ring_ops)).
    Proof.
    constructor => //.
    - exact: Nsatz_realType_Setoid_Theory.
    - by move=> x y -> x1 y1 ->.
    - by move=> x y -> x1 y1 ->.
    - by move=> x y -> x1 y1 ->.
    - by move=> x y ->.
    - exact: add0r.
    - exact: addrC.
    - exact: addrA.
    - exact: mul1r.
    - exact: mulr1.
    - exact: mulrA.
    - exact: mulrDl.
    - move=> x y z; exact: mulrDr.
    - exact: subrr.
    Defined.

    #[global]
    Instance
    Nsatz_realType_Cring
    Source code
    : (Cring.Cring (Rr:=Nsatz_realType_Ring)).
    Proof.
    exact: mulrC. Defined.

    #[global]
    Instance
    Nsatz_realType_Integral_domain
    Source code
     :
       (Integral_domain.Integral_domain (Rcr:=Nsatz_realType_Cring)).
    Proof.
    constructor.
      move=> x y.
      rewrite -[_ _ Algebra_syntax.zero]/(x * y = 0)%R => /eqP.
      by rewrite mulf_eq0 => /orP[] /eqP->; [left | right].
    rewrite -[_ _ Algebra_syntax.zero]/(1 = 0)%R; apply/eqP.
    by rewrite (eqr_nat T 1 0).
    Defined.

    End Nsatz_realType.

    Tactic Notation "nsatz" := nsatz_default.
    Generated by rocqnavi