Files

  • mathcomp

    • Top

    Module mathcomp.reals_stdlib.nsatz_realtype

    From Stdlib Require Import Nsatz.
    From mathcomp Require Import all_ssreflect_compat 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.

    Local Open Scope ring_scope.

    Section Nsatz_realType.
    Variable T : realType.

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

    Definition
    Nsatz_realType0

    Nsatz_realType0 : forall T : realType, T Nsatz_realType0 is not universe polymorphic Arguments Nsatz_realType0 T Nsatz_realType0 is transparent Expands to: Constant mathcomp.reals_stdlib.nsatz_realtype.Nsatz_realType0 Declared in library mathcomp.reals_stdlib.nsatz_realtype, line 27, characters 11-26

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

    Nsatz_realType1 : forall T : realType, T Nsatz_realType1 is not universe polymorphic Arguments Nsatz_realType1 T Nsatz_realType1 is transparent Expands to: Constant mathcomp.reals_stdlib.nsatz_realtype.Nsatz_realType1 Declared in library mathcomp.reals_stdlib.nsatz_realtype, line 28, characters 11-26

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

    Nsatz_realType_add : forall T : realType, T -> T -> T Nsatz_realType_add is not universe polymorphic Arguments Nsatz_realType_add T (x y)%_ring_scope Nsatz_realType_add is transparent Expands to: Constant mathcomp.reals_stdlib.nsatz_realtype.Nsatz_realType_add Declared in library mathcomp.reals_stdlib.nsatz_realtype, line 29, characters 11-29

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

    Nsatz_realType_mul : forall T : realType, T -> T -> T Nsatz_realType_mul is not universe polymorphic Arguments Nsatz_realType_mul T (x y)%_ring_scope Nsatz_realType_mul is transparent Expands to: Constant mathcomp.reals_stdlib.nsatz_realtype.Nsatz_realType_mul Declared in library mathcomp.reals_stdlib.nsatz_realtype, line 30, characters 11-29

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

    Nsatz_realType_sub : forall T : realType, T -> T -> T Nsatz_realType_sub is not universe polymorphic Arguments Nsatz_realType_sub T (x y)%_ring_scope Nsatz_realType_sub is transparent Expands to: Constant mathcomp.reals_stdlib.nsatz_realtype.Nsatz_realType_sub Declared in library mathcomp.reals_stdlib.nsatz_realtype, line 31, characters 11-29

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

    Nsatz_realType_opp : forall T : realType, T -> T Nsatz_realType_opp is not universe polymorphic Arguments Nsatz_realType_opp T x%_ring_scope Nsatz_realType_opp is transparent Expands to: Constant mathcomp.reals_stdlib.nsatz_realtype.Nsatz_realType_opp Declared in library mathcomp.reals_stdlib.nsatz_realtype, line 32, characters 11-29

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

    #[global]
    Instance Nsatz_realType_Ring_ops:
       (@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 : (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: (Cring.Cring (Rr:=Nsatz_realType_Ring)).
    Proof.
    exact: mulrC. Defined.

    #[global]
    Instance Nsatz_realType_Integral_domain :
       (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