VQCS.SI

Require Export Nunit.

Create a new scope, to manage the valid domain of symbols.

Declare Scope SI_scope.
Delimit Scope SI_scope with SI.
Open Scope SI.

Decimal multiples and sub-multiples of SI

Module SI_Prefix.

  Definition deca (u : Unit) : Unit := 1e1 * u.
  Definition hecto (u : Unit) : Unit := 1e2 * u.
  Definition kilo (u : Unit) : Unit := 1e3 * u.
  Definition mega (u : Unit) : Unit := 1e6 * u.
  Definition giga (u : Unit) : Unit := 1e9 * u.
  Definition tera (u : Unit) : Unit := 1e12 * u.
  Definition peta (u : Unit) : Unit := 1e15 * u.
  Definition exa (u : Unit) : Unit := 1e18 * u.
  Definition zetta (u : Unit) : Unit := 1e21 * u.
  Definition yotta (u : Unit) : Unit := 1e24 * u.
  Notation "'_da' x" :=
    (deca x) (at level 5, right associativity, format "'_da' x") : SI_scope.
  Notation "'_h' x" :=
    (hecto x) (at level 5, right associativity, format "'_h' x") : SI_scope.
  Notation "'_k' x" :=
    (kilo x) (at level 5, right associativity, format "'_k' x") : SI_scope.
  Notation "'_M' x" :=
    (mega x) (at level 5, right associativity, format "'_M' x") : SI_scope.
  Notation "'_G' x" :=
    (giga x) (at level 5, right associativity, format "'_G' x") : SI_scope.
  Notation "'_T' x" :=
    (tera x) (at level 5, right associativity, format "'_T' x") : SI_scope.
  Notation "'_P' x" :=
    (peta x) (at level 5, right associativity, format "'_P' x") : SI_scope.
  Notation "'_E' x" :=
    (exa x) (at level 5, right associativity, format "'_E' x") : SI_scope.
  Notation "'_Z' x" :=
    (zetta x) (at level 5, right associativity, format "'_Z' x") : SI_scope.
  Notation "'_Y' x" :=
    (yotta x) (at level 5, right associativity, format "'_Y' x") : SI_scope.

  Definition deci (u : Unit) : Unit := 1e-1 * u.
  Definition centi (u : Unit) : Unit := 1e-2 * u.
  Definition milli (u : Unit) : Unit := 1e-3 * u.
  Definition micro (u : Unit) : Unit := 1e-6 * u.
  Definition nano (u : Unit) : Unit := 1e-9 * u.
  Definition pico (u : Unit) : Unit := 1e-12 * u.
  Definition femto (u : Unit) : Unit := 1e-15 * u.
  Definition atto (u : Unit) : Unit := 1e-18 * u.
  Definition zepto (u : Unit) : Unit := 1e-21 * u.
  Definition yocto (u : Unit) : Unit := 1e-24 * u.
  Notation "'_d' x" :=
    (deci x) (at level 5, right associativity, format "'_d' x") : SI_scope.
  Notation "'_c' x" :=
    (centi x) (at level 5, right associativity, format "'_c' x") : SI_scope.
  Notation "'_m' x" :=
    (milli x) (at level 5, right associativity, format "'_m' x") : SI_scope.
  Notation "'_μ' x" :=
    (micro x) (at level 5, right associativity, format "'_μ' x") : SI_scope.
  Notation "'_n' x" :=
    (nano x) (at level 5, right associativity, format "'_n' x") : SI_scope.
  Notation "'_p' x" :=
    (pico x) (at level 5, right associativity, format "'_p' x") : SI_scope.
  Notation "'_f' x" :=
    (femto x) (at level 5, right associativity, format "'_f' x") : SI_scope.
  Notation "'_a' x" :=
    (atto x) (at level 5, right associativity, format "'_a' x") : SI_scope.
  Notation "'_z' x" :=
    (zepto x) (at level 5, right associativity, format "'_z' x") : SI_scope.
  Notation "'_y' x" :=
    (yocto x) (at level 5, right associativity, format "'_y' x") : SI_scope.

End SI_Prefix.

7 basic unit of SI.

Module SI_Basic.

Time

Definition second := BUTime.
Notation "'s" := (second) (at level 5) : SI_scope.

Length

Definition metre := BULength.
Notation "'m" := (metre) (at level 5) : SI_scope.

Mass

Definition killogram := BUMass.
Notation "'kg" := (killogram) (at level 5) : SI_scope.

Electric current

Definition ampere := BUElectricCurrent.
Notation "'A" := (ampere) (at level 5) : SI_scope.

Temperature

Definition kelvin := BUThermodynamicTemperature.
Notation "'K" := (kelvin) (at level 5) : SI_scope.

Amount of substance

Definition mole := BUAmountOfSubstance.
Notation "'mol" := (mole) (at level 5) : SI_scope.

Luminous intensity

Definition candela := BULuminousIntensity.
Notation "'cd" := (candela) (at level 5) : SI_scope.

End SI_Basic.

22 derived units of SI

Module SI_Derived.
  Export SI_Basic.

  Definition radian := 'm / 'm.
  Notation "'rad" := (radian) (at level 5) : SI_scope.

  Lemma radian_spec : 'rad == 1.
  Proof. ueq. Qed.

  Definition steradian := 'm ² / 'm ².
  Notation "'sr" := (steradian) (at level 5) : SI_scope.

  Lemma steradian_spec : 'sr == 1.
  Proof. ueq. Qed.

  Definition herz := / 's.
  Notation "'Hz" := (herz) (at level 5) : SI_scope.

  Definition herza := (2 * PI)%R / 's.
  Notation "'Hza" := (herza) (at level 5) : SI_scope.

  Definition newton := 'kg * 'm * (/'s ² ).
  Notation "'N" := (newton) (at level 5) : SI_scope.

  Definition pascal := 'kg * (/'m ) * (/'s ² ).
  Notation "'Pa" := (pascal) (at level 5) : SI_scope.

  Lemma pascal_spec : 'Pa == 'N / 'm ².
  Proof. ueq. Qed.

  Definition joule := 'kg * 'm ² * (/'s ² ).
  Notation "'J" := (joule) (at level 5) : SI_scope.

  Lemma joule_spec : 'J == 'N * 'm.
  Proof. ueq. Qed.

  Lemma pascal_spec2 : 'Pa == 'J / 'm ³.
  Proof. ueq. Qed.

  Definition watt := 'kg * 'm ² * (/'s ³ ).
  Notation "'W" := (watt) (at level 5) : SI_scope.

  Lemma power_spec : 'W == 'J * (/'s ).
  Proof. ueq. Qed.

  Definition coulomb := 'A * 's.
  Notation "'C" := (coulomb) (at level 5) : SI_scope.

  Definition volt := 'kg * 'm ² * (/'s ³ ) * (/'A ).
  Notation "'V" := (volt) (at level 5) : SI_scope.

  Lemma volt_spec : 'V == 'W / 'A.
  Proof. ueq. Qed.

  Example N_m_A_V_s : ('N * 'm ) / 'A == 'V * 's.
  Proof. ueq. Qed.

  Definition farad := (/'kg ) * (/'m ² ) * 's⁴ * 'A ².
  Notation "'F" := (farad) (at level 5) : SI_scope.

  Lemma farad_spec : 'F == 'C / 'V.
  Proof. ueq. Qed.

  Definition ohm := 'kg * 'm ² * (/'s ³ ) * (/'A ² ).
  Notation "'Ω" := (ohm) (at level 5) : SI_scope.

  Lemma ohm_spec : 'Ω == 'V / 'A.
  Proof. ueq. Qed.

  Definition siemens := (/'kg ) * (/'m ² ) * 's ³ * 'A ².
  Notation "'S" := (siemens) (at level 5) : SI_scope.

  Lemma siemens_spec : 'S == 'A / 'V.
  Proof. ueq. Qed.

  Definition weber := 'kg * 'm ² * (/'s ² ) * (/'A ).
  Notation "'Wb" := (weber) (at level 5) : SI_scope.

  Lemma weber_spec : 'Wb == 'V * 's.
  Proof. ueq. Qed.

  Definition tesla := 'kg * (/'s ² ) * (/'A ).
  Notation "'T" := (tesla) (at level 5) : SI_scope.

  Lemma tesla_spec : 'T == 'Wb / 'm ².
  Proof. ueq. Qed.

  Definition henry := 'kg * 'm ² * (/'s ² ) * (/'A ² ).
  Notation "'H" := (henry) (at level 5) : SI_scope.

  Lemma henry_spec : 'H == 'Wb / 'A.
  Proof. ueq. Qed.

  Definition lumen := 'cd * 'sr.
  Notation "'lm" := (lumen) (at level 5) : SI_scope.

  Definition lux := 'cd * 'sr * (/'m ² ).
  Notation "'lx" := (lux) (at level 5) : SI_scope.

  Lemma lux_spec : 'lx == 'lm / 'm ².
  Proof. ueq. Qed.

  Definition becquerel := /'s.
  Notation "'Bq" := (becquerel) (at level 5) : SI_scope.

  Definition gray := 'm ² / 's ².
  Notation "'Gy" := (gray) (at level 5) : SI_scope.

  Lemma gray_spec : 'Gy == 'J / 'kg.
  Proof. ueq. Qed.

  Definition sievert := 'm ² / 's ².
  Notation "'Sv" := (sievert) (at level 5) : SI_scope.

  Lemma sievert_spec : 'Sv == 'J / 'kg.
  Proof. ueq. Qed.

  Definition katal := 'mol / 's.
  Notation "'kat" := (katal) (at level 5) : SI_scope.

End SI_Derived.

Temperature and Temperature Difference

   Note that there are two types of temperature units:
   1. (Absolute) Temperature. The reference point is 0K (Absolute Zero).
      a. Kelvin, 1 K = 1 [K]
      b. Celsius, x ℃ = (273.15 + x) [K]
      c. Fahrenheit, x ℉ = ((x - 32) / 1.8 + 273.15) [K]
   2. Temperature Difference.
      a. Delta Kelvin, x DeltaK = x [K]
      b. Delta Celsius, x DeltaC = x [K]
      c. Delta Fahrenheit, x DeltaF = (x/1.8) [K]
   3. Conversion
	  kel2cel x := x - 273.15
	  cel2kel x := x + 273.15
      cel2fah x := x * 1.8 + 32
	  fah2cel x := (x - 32) / 1.8
	  fah2kel x := (x - 32) / 1.8 + 273.15
	  kel2fah x := (x - 273.15) * 1.8 + 32

Module Temperature_TemperatureDifference.
Export SI_Basic.

Conversion between temperature unit on `R` type

  Definition cel2kelR (x : R) : R := x + 273.15.
  Definition kel2celR (x : R) : R := x - 273.15.

  Definition cel2fahR (x : R) : R := x * 1.8 + 32.
  Definition fah2celR (x : R) : R := (x - 32) / 1.8.

  Definition kel2fahR (x : R) : R := (x - 273.15) * 1.8 + 32.
  Definition fah2kelR (x : R) : R := (x - 32) / 1.8 + 273.15.

  Local Ltac solve_tempUnit := intros; autounfold with unit; field; lra.

  Lemma kel2celR_cel2kelR_id : forall x, kel2celR (cel2kelR x) = x.
  Proof. intros; cbv; lra. Qed.
  Lemma cel2kelR_kel2celR_id : forall x, cel2kelR (kel2celR x) = x.
  Proof. intros; cbv; lra. Qed.

  Lemma fah2celR_cel2fahR_id : forall x, fah2celR (cel2fahR x) = x.
  Proof. intros; cbv; lra. Qed.
  Lemma cel2fahR_fah2celR_id : forall x, cel2fahR (fah2celR x) = x.
  Proof. intros; cbv; lra. Qed.

  Lemma fah2kelR_kel2fahR_id : forall x, fah2kelR (kel2fahR x) = x.
  Proof. intros; cbv; lra. Qed.
  Lemma kel2fahR_fah2kelR_id : forall x, kel2fahR (fah2kelR x) = x.
  Proof. intros; cbv; lra. Qed.

  Lemma kel2fahR_spec : forall x, kel2fahR x = cel2fahR (kel2celR x).
  Proof. intros; cbv; lra. Qed.
  Lemma fah2kelR_spec : forall x, fah2kelR x = cel2kelR (fah2celR x).
  Proof. intros; cbv; lra. Qed.

Definition of temperature difference unit on `R` type

  Definition deltaKel (x : R) : R := x.
  Definition deltaCel (x : R) : R := x.
  Definition deltaFah (x : R) : R := (x / 1.8).

  Lemma deltaKel_spec : forall x y, x + (deltaKel y ) = x + y.
  Proof. intros; cbv; lra. Qed.
  Lemma deltaCel_spec : forall x y, cel2kelR x + (deltaCel y ) = cel2kelR (x + y).
  Proof. intros; cbv; lra. Qed.
  Lemma deltaFah_spec : forall x y, fah2kelR x + (deltaFah y ) = fah2kelR (x + y).
  Proof. intros; cbv; lra. Qed.

Definition of temperature unit on `Unit` type

  Definition temperatureCel (x : R) : Unit := (cel2kelR x ) * 'K.
  Notation "x '℃" := (temperatureCel x) (at level 5) : SI_scope.

  Lemma temperatureCel_spec : forall x, ucoef (temperatureCel x) = cel2kelR x.
  Proof. intros; cbv; lra. Qed.

  Definition temperatureFah (x : R) : Unit := (fah2kelR x ) * 'K.
  Notation "'℉" := (temperatureFah) (at level 5) : SI_scope.

  Lemma temperatureFah_spec : forall x, ucoef (temperatureFah x) = fah2kelR x.
  Proof. intros; cbv; lra. Qed.

  Definition temperatureDiffKel (x : R) : Unit := (deltaKel x ) * 'K.
  Notation "x 'ΔK" := (temperatureDiffKel x) (at level 5) : SI_scope.

  Lemma temperatureDiffKel_spec : forall x, ucoef (temperatureDiffKel x) = deltaKel x.
  Proof. intros; cbv; lra. Qed.

  Definition temperatureDiffCel (x : R) : Unit := (deltaCel x ) * 'K.
  Notation "x 'Δ℃" := (temperatureDiffCel x) (at level 5) : SI_scope.

  Lemma temperatureDiffCel_spec : forall x, ucoef (temperatureDiffCel x) = deltaCel x.
  Proof. intros; cbv; lra. Qed.

  Definition temperatureDiffFah (x : R) : Unit := (deltaFah x ) * 'K.
  Notation "x 'Δ℉" := (temperatureDiffFah x) (at level 5) : SI_scope.

  Lemma temperatureDiffFah_spec : forall x, ucoef (temperatureDiffFah x) = deltaFah x.
  Proof. intros; cbv; lra. Qed.

  Section test.
    Local Lemma ex1 : 30 '℃ == 303.15 * 'K.
    Proof. ueq. Qed.

  End test.
End Temperature_TemperatureDifference.

Non-SI units that are accepted for use with the SI

Module SI_Accepted.
  Export SI_Derived.

  Definition millisecond := 1e-3 * 's.
  Notation "'ms" := (millisecond) (at level 5) : SI_scope.

  Lemma second_millisecond : 's == 1e3 * 'ms.
  Proof. ueq. Qed.

  Definition killometre := 1e3 * 'm.
  Notation "'km" := (killometre) (at level 5) : SI_scope.

  Definition millimetre := 1e-3 * 'm.
  Notation "'mm" := (millimetre) (at level 5) : SI_scope.

  Definition gram := 1e-3 * 'kg.
  Notation "'g" := (gram) (at level 5) : SI_scope.

  Definition milliampere := 1e-3 * 'A.
  Notation "'mA" := (milliampere) (at level 5) : SI_scope.

  Definition minute := 60 * 's.
  Notation "'min" := (minute) (at level 5) : SI_scope.

  Definition hour := 60 * 'min.
  Notation "'hrs" := (hour) (at level 5) : SI_scope.

  Lemma hour2second : 'hrs == 3600 * 's.
  Proof. ueq. Qed.

  Definition day := 24 * 'hrs.
  Notation "'d" := (day) (at level 5) : SI_scope.

  Lemma day2second : 'd == 86400 * 's.
  Proof. ueq. Qed.

  Lemma day2minute : 'd == 1440 * 'min.
  Proof. ueq. Qed.

astronomical Unit, 天文单位

Definition astronomicalUnit := 149_597_870_700 * 'm.
Notation "'au" := (astronomicalUnit) (at level 5) : SI_scope.

plane and phase angle, 平面角、相位角

Definition degree_angle := PI /180 * 'rad.
Notation "'ᵒ" := (degree_angle) (at level 5) : SI_scope.

area(hectare), 面积（公顷），=100m*100m

Definition hectare := 1e4 * 'm ².
Notation "'ha" := (hectare) (at level 5) : SI_scope.

volume(litre), 体积（升），= 1dm^3 = 10^3 cm^3 = 10^{-3} m^3

Definition litre := 1e-3 * 'm ³.
Notation "'L" := (litre) (at level 5) : SI_scope.

mass(tonne), 质量（吨）

Definition tonne := 1e3 * 'kg.
Notation "'t" := (tonne) (at level 5) : SI_scope.

mass(dalton), 质量（道尔顿）

Definition dalton := (1.660_539_066_60*(/10^27)) * 'kg.
Notation "'Da" := (dalton) (at level 5) : SI_scope.

energy(electronical voltage), 能量（电子伏）

Definition electronvolt := (1.602_176_634*(/10^27)) * 'J.
Notation "'eV" := (electronvolt) (at level 5) : SI_scope.

round speed, round per minute

  Definition round_per_minute := (2 * PI)%R /'min.
  Notation "'rpm" := (round_per_minute) (at level 5) : SI_scope.

  Example N_m_A_V_rpm : ('N * 'm ) / 'A == ((2*PI ) / 60) * ('V / 'rpm ).
  Proof. ueq. ra. Qed.

battery capacity

Definition milli_amper_hour := 'mA * 'hrs.
Notation "'mAh" := (milli_amper_hour) (at level 5) : SI_scope.

End SI_Accepted.

The 7 defining constants of SI

Module SI_Constants.
Export SI_Derived.

hyperfine transition frequency of Cs，铯原子能级跃迁辐射频率

Definition hyper_trans_freq_of_Cs := 9_192_631_770 * 'Hz.
Notation "'ΔV" := (hyper_trans_freq_of_Cs) (at level 5) : SI_scope.

speed of light in vaccum，真空中光速

Definition speed_of_light_in_vaccum := 299_792_458 * ('m /'s ).
Notation "'c" := (speed_of_light_in_vaccum) (at level 5) : SI_scope.

Planck constant，普朗克常量

Definition planck_constant := 6.626_070_15e-34 * ('J *'s ).
Notation "'h" := (planck_constant) (at level 5) : SI_scope.

elementary charge，元电荷

Definition elementary_charge := 1.602_176_634e-19 * 'C.
Notation "'e" := (elementary_charge) (at level 5) : SI_scope.

Boltzmann constant，玻尔兹曼常数

Definition boltzmann_constant := 1.380_649e-23 * ('J /'K ).
Notation "'k" := (boltzmann_constant) (at level 5) : SI_scope.

Avogadro constant，阿伏伽德罗常数

Definition avogadro_constant := 6.022_140_76e23 * (/'mol ).
Notation "'NA" := (avogadro_constant) (at level 5) : SI_scope.

luminous efficacy，最大发光效能

Definition luminous_efficacy := 683 * 'lm * (/'W ).
Notation "'Kcd" := (luminous_efficacy) (at level 5) : SI_scope.

End SI_Constants.

Verify consistency between defining constants and basic unit

Module SI_Constants_spec.
Export SI_Constants.

Tactic for proof unit approximate reletion.

  Ltac uapprox :=
    unfold unit_approx; simpl; split; auto;

    unfold Rapprox;
    match goal with
    | |- (Rabs ?r1 <= ?r2)%R => unfold Rabs; destruct Rcase_abs; lra
    end.

Properties about second

  Lemma Hz_def : 1 * 'Hz == 'ΔV / 9_192_631_770.
  Proof. ueq. Qed.

  Lemma s_def : 1 * 's == 9_192_631_770 / 'ΔV.
  Proof. ueq. Qed.

Properties about metre

  Lemma m_def1 : 1 * 'm == ('c / 299_792_458) * 's.
  Proof. ueq. Qed.

  Lemma m_def2 : 1 * 'm == (9_192_631_770 / 299_792_458) * ('c / 'ΔV ).
  Proof. ueq. Qed.

  Lemma m_def3 : unit_approx (1 * 'm) (30.663319 * ('c /'ΔV )) 1e-9.
  Proof. uapprox. Qed.

Properties about kilogram

  Lemma kg_def1 : 1 * 'kg ==
    ('h / (6.62607015e-34)) * ((/'m ² )*'s ).
  Proof. ueq. Qed.

  Lemma kg_def2 : 1 * 'kg ==
    ((299792458)² / (6.62607015e-34 * 9192631770)) *
    (('h * 'ΔV ) / ('c ² )).
  Proof. ueq. Qed.

  Lemma kg_def3 : unit_approx (1 * 'kg)
    ((1.4755214e40) * (('h * 'ΔV ) / ('c ² ))) 1e-9.
  Proof. uapprox. Qed.

Properties about ampere

  Lemma A_def1 : 1 * 'A == ('e / 1.602176634e-19) * (/'s ).
  Proof. ueq. Qed.

  Lemma A_def2 : 1 * 'A == (/(9192631770 * 1.602176634e-19)) * ('ΔV * 'e ).
  Proof. ueq. Qed.

  Lemma A_def3 : unit_approx (1 * 'A) (6.7896868e8 * ('ΔV * 'e )) 1e-8.
  Proof. uapprox. Qed.

Properties about kelvin

  Lemma kelvin_def1 : 1 * 'K == (1.380649e-23 /'k ) * ('kg * 'm ² * (/'s ² )).
  Proof. ueq. Qed.

  Lemma kelvin_def2 : 1 * 'K == (1.380649e-23 / (6.62607015e-34 * 9192631770))
                                * ('ΔV * 'h * (/'k )).
  Proof. ueq. Qed.

  Lemma kelvin_def3 : unit_approx (1*'K) (2.2666653 * ('ΔV * 'h * (/'k ))) 1e-7.
  Proof. uapprox. Qed.

Properties about mole

Lemma mol_def : 1 * 'mol == 6.02214076e23 / 'NA.
Proof. ueq. Qed.

Properties about candela

  Lemma cd_def1 : 1 * 'cd == ('Kcd /683) * ('kg * 'm ² * (/'s ³ ) * (/'sr )).
  Proof. ueq. Qed.

  Lemma cd_def2 : 1 * 'cd ==
    (/(6.62607015e-34 * 9192631770² * 683)) * ('ΔV ² * 'h * 'Kcd ).
  Proof. ueq. Qed.

  Lemma cd_def3 : unit_approx (1 * 'cd) (2.6148305e10 * ('ΔV ² * 'h * 'Kcd )) 1e-8.
  Proof. uapprox. Qed.

End SI_Constants_spec.

Section test.

  Import SI_Derived.
  Import SI_Accepted.
  Import SI_Prefix.
  Import SI_Constants.

  Section ex1.

    Let killoPa := _k 'Pa.
    Let bar := (1e5) * 'Pa.
    Notation "'bar" := (bar) (at level 5) : SI_scope.
    Let Ru1 : Unit := 'J / 'K / 'mol.
    Let Ru2 : Unit := 'm ³ * 'Pa / 'K / 'mol.
    Let Ru3 : Unit := 'kg * 'm ² / 's ² / 'K / 'mol.
    Let Ru4 : Unit := 1000 * 'L * 'Pa / 'K / 'mol.     Let Ru5 : Unit := 'L * _k 'Pa / 'K / 'mol.
    Let Ru6 : Unit := 0.01 * 'L * 'bar / 'K / 'mol.

    Goal Ru1 == Ru2. ueq. Qed.
    Goal Ru1 == Ru3. ueq. Qed.
    Goal Ru1 == Ru4. ueq. Qed.
    Goal Ru1 == Ru5. ueq. Qed.
    Goal Ru1 == Ru6. ueq. Qed.
  End ex1.

  Section ex2.

Test the ability that if Coq can handle large numbers. In astronomy, where there are some very large numbers involved, and Coq can check the equation or inequalities of these numbers

Local Lemma large_number_ex1 : (1.234567e200 * 2.345678e100 = 2.895896651426e300)%R.
Proof. lra. Qed.

天文学中的一个关系式：3.26 light-year <= parsec <= 3.27 light-year

    Let julian_year := 365.25 * day.
    Let light_year := 'c * julian_year.
    Let astronomical_unit := 149597870700 * 'm.
    Notation "'au" := astronomical_unit.

    Let parsec := (648000/PI ) * 'au.

  End ex2.

End test.