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

    ereal_of_itv_bound : forall [T : Type], itv_bound T -> \bar T ereal_of_itv_bound is not universe polymorphic Arguments ereal_of_itv_bound [T]%_type_scope !b ereal_of_itv_bound is a coercion The reduction tactics unfold ereal_of_itv_bound when the 2nd argument evaluates to a constructor ereal_of_itv_bound is transparent Expands to: Constant mathcomp.reals.real_interval.ereal_of_itv_bound Declared in library mathcomp.reals.real_interval, line 161, characters 9-27

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

    [Loading ML file rocq-runtime.plugins.nsatz_core ... done]

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

    [Loading ML file rocq-runtime.plugins.nsatz ... done]

    Source code
     (
    x
    Source code
    y
    Source code
     : T) := (x + y)%R.
    Definition
    Nsatz_realType_mul
    Source code
     (
    x
    Source code
    y
    Source code
     : T) := (x * y)%R.
    Definition
    Nsatz_realType_sub
    Source code
     (
    x
    Source code
    y
    Source code
     : T) := (x - y)%R.
    Definition
    Nsatz_realType_opp
    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