VQCS.test_PropulsionSystem.Basic
Defined as Q.
Notice that, T_0, T_t, we use 'K instead ℃, it is correct in such case.
Definition T_0 : QuR := u2qR val_T_0 'K.
Definition h : QuR := u2qR val_h 'm.
Definition p_0 : QuR := u2qR val_p_0 'Pa.
Definition rho_0 : QuR := u2qR val_rho_0 ('kg / 'm³)%U.
Definition T_t : QuR := u2qR val_T_t 'K. Definition G : QuR := u2qR val_G 'N. Definition I_other : QuR := u2qR val_I_other 'A.
Definition p : QuR := p_0 * (qpower (1 - value_0_0065 * (h / (T_0 + T_t))) val_5_2561).
Parameter val_rho : R.
Definition rho : QuR := u2qR val_rho ('kg/('m³))%U.
Definition n_r : QuR := val_n_r.
Definition h : QuR := u2qR val_h 'm.
Definition p_0 : QuR := u2qR val_p_0 'Pa.
Definition rho_0 : QuR := u2qR val_rho_0 ('kg / 'm³)%U.
Definition T_t : QuR := u2qR val_T_t 'K. Definition G : QuR := u2qR val_G 'N. Definition I_other : QuR := u2qR val_I_other 'A.
Definition p : QuR := p_0 * (qpower (1 - value_0_0065 * (h / (T_0 + T_t))) val_5_2561).
Parameter val_rho : R.
Definition rho : QuR := u2qR val_rho ('kg/('m³))%U.
Definition n_r : QuR := val_n_r.
Parameters
val_D_p
val_H_p
val_B_p
val_G_p
val_PP_A
val_PP_epsilon
val_PP_lambda
val_PP_zeta
val_PP_e
val_PP_K0
val_PP_alpha0
val_C_fd
: R.
Definition val_PP_alpha_ab : R :=
(val_PP_epsilon * (atan (val_H_p / (PI * val_D_p))) - val_PP_alpha0).
Parameter val_C_T : R.
Parameter val_C_d : R.
Parameter val_C_M : R.
Definition D_p : QuR := u2qR val_D_p 'm.
Definition H_p : QuR := u2qR val_H_p 'm.
Definition C_T : QuR := val_C_T.
Definition C_d : QuR := val_C_d.
Definition C_M : QuR := val_C_M.
val_D_p
val_H_p
val_B_p
val_G_p
val_PP_A
val_PP_epsilon
val_PP_lambda
val_PP_zeta
val_PP_e
val_PP_K0
val_PP_alpha0
val_C_fd
: R.
Definition val_PP_alpha_ab : R :=
(val_PP_epsilon * (atan (val_H_p / (PI * val_D_p))) - val_PP_alpha0).
Parameter val_C_T : R.
Parameter val_C_d : R.
Parameter val_C_M : R.
Definition D_p : QuR := u2qR val_D_p 'm.
Definition H_p : QuR := u2qR val_H_p 'm.
Definition C_T : QuR := val_C_T.
Definition C_d : QuR := val_C_d.
Definition C_M : QuR := val_C_M.
Parameters
val_K_V0
val_I_mMax
val_U_m0
val_I_m0
val_R_m
val_G_m : R.
Definition I_mMax : QuR := u2qR val_I_mMax 'A.
Definition U_m0 : QuR := u2qR val_U_m0 'V.
Definition I_m0 : QuR := u2qR val_I_m0 'A.
Definition R_m : QuR := u2qR val_R_m 'Ω.
Definition G_m : QuR := u2qR val_G_m 'g.
Definition K_E : QuR := (U_m0 - I_m0 * R_m) / (val_K_V0 * U_m0).
Definition K_T : QuR := val_9_55 * K_E.
val_K_V0
val_I_mMax
val_U_m0
val_I_m0
val_R_m
val_G_m : R.
Definition I_mMax : QuR := u2qR val_I_mMax 'A.
Definition U_m0 : QuR := u2qR val_U_m0 'V.
Definition I_m0 : QuR := u2qR val_I_m0 'A.
Definition R_m : QuR := u2qR val_R_m 'Ω.
Definition G_m : QuR := u2qR val_G_m 'g.
Definition K_E : QuR := (U_m0 - I_m0 * R_m) / (val_K_V0 * U_m0).
Definition K_T : QuR := val_9_55 * K_E.
Parameters
val_I_eMax
val_R_e
val_G_e : R.
Definition I_eMax : QuR := u2qR val_I_eMax 'A.
Definition R_e : QuR := u2qR val_R_e 'Ω.
Definition G_e : QuR := u2qR val_G_e 'g.
val_I_eMax
val_R_e
val_G_e : R.
Definition I_eMax : QuR := u2qR val_I_eMax 'A.
Definition R_e : QuR := u2qR val_R_e 'Ω.
Definition G_e : QuR := u2qR val_G_e 'g.
Parameters
val_C_b
val_C_min
val_K_b
val_R_b
val_U_b : R.
Definition C_b : QuR := u2qR val_C_b ('mAh).
Definition C_min : QuR := u2qR val_C_min 'mAh.
Definition K_b : QuR := val_K_b.
Definition R_b : QuR := u2qR val_R_b 'Ω.
Definition U_b : QuR := u2qR val_U_b 'V.
val_C_b
val_C_min
val_K_b
val_R_b
val_U_b : R.
Definition C_b : QuR := u2qR val_C_b ('mAh).
Definition C_min : QuR := u2qR val_C_min 'mAh.
Definition K_b : QuR := val_K_b.
Definition R_b : QuR := u2qR val_R_b 'Ω.
Definition U_b : QuR := u2qR val_U_b 'V.
Check the unit of the input Quantity q with reference Unit u,
if they are equal return q, otherwise return !!
Definition CHK_UNIT (q : QuR) (u : Unit) : QuR :=
if qsameub q u then q else !!.
Hint Unfold CHK_UNIT : Q.
if qsameub q u then q else !!.
Hint Unfold CHK_UNIT : Q.
Convert the unit of the input Quantity q with reference Unit u,
if it is convertible then return a proper q', otherwise return !!
Definition CVT_UNIT (q : QuR) (u : Unit) : QuR := q2quR q u.
Hint Unfold CVT_UNIT : Q.
Module demo1.
Hint Unfold CVT_UNIT : Q.
Module demo1.
The input parameter `N` could be any unit, and the output could be any unit.
we can check the unit of the input parameter
Definition get_T_by_N_CHECK_INPUT (N : QuR) : QuR :=
let N := CHK_UNIT N 'rpm in
rho * C_T * (D_p ^ 4) * ((N / 60) ^ 2).
Goal get_T_by_N_CHECK_INPUT (u2qR 1 'rpm) <> !!. qeqR. Qed.
Goal get_T_by_N_CHECK_INPUT (u2qR 60 'Hz) = !!. qeqR. Qed.
Goal get_T_by_N_CHECK_INPUT (u2qR 1 'A) = !!. qeqR. Qed.
let N := CHK_UNIT N 'rpm in
rho * C_T * (D_p ^ 4) * ((N / 60) ^ 2).
Goal get_T_by_N_CHECK_INPUT (u2qR 1 'rpm) <> !!. qeqR. Qed.
Goal get_T_by_N_CHECK_INPUT (u2qR 60 'Hz) = !!. qeqR. Qed.
Goal get_T_by_N_CHECK_INPUT (u2qR 1 'A) = !!. qeqR. Qed.
we can convert the unit of the input parameter
Definition get_T_by_N_CONVERT_INPUT N :=
let N := CVT_UNIT N 'rpm in
rho * C_T * (D_p ^ 4) * ((N / 60) ^ 2).
Goal get_T_by_N_CONVERT_INPUT (u2qR 1 'rpm) <> !!. qeqR. Qed.
Goal get_T_by_N_CONVERT_INPUT (u2qR 60 'Hz) <> !!. qeqR. Qed.
Goal get_T_by_N_CONVERT_INPUT (u2qR 1 'A) = !!. qeqR. Qed.
let N := CVT_UNIT N 'rpm in
rho * C_T * (D_p ^ 4) * ((N / 60) ^ 2).
Goal get_T_by_N_CONVERT_INPUT (u2qR 1 'rpm) <> !!. qeqR. Qed.
Goal get_T_by_N_CONVERT_INPUT (u2qR 60 'Hz) <> !!. qeqR. Qed.
Goal get_T_by_N_CONVERT_INPUT (u2qR 1 'A) = !!. qeqR. Qed.
we can convert the unit of the output parameter
1. the output has a fixed unit, which is beneficial for caller which need
exactly unit.
2. the function itself also accept any convertible units
3. any not convertible units will be rejected.
Definition get_T_by_N_CONVERT_OUTPUT N :=
CVT_UNIT (rho * C_T * (D_p ^ 4) * ((N / 60) ^ 2)) 'N.
End demo1.
CVT_UNIT (rho * C_T * (D_p ^ 4) * ((N / 60) ^ 2)) 'N.
End demo1.
Definition get_T_by_N N :=
let N := CHK_UNIT N 'rpm in
let _ret := rho * C_T * (D_p ^ 4) * ((N / 60) ^ 2) in
CVT_UNIT _ret 'N.
Hint Unfold get_T_by_N : Q.
Lemma get_T_by_N_unit : forall N, qsameu N 'rpm -> qsameu (get_T_by_N N) 'N.
Proof.
intros. autounfold with Q. lazy [qsameu q2quR q2qu q2qn] in *.
destruct N; auto. rewrite H. simpl.
rewrite neqb_refl. simpl. auto.
Qed.
Definition get_M_by_N N :=
let N := CHK_UNIT N 'rpm in
CVT_UNIT (C_M * rho * ((N / 60) ^ 2) * (D_p ^ 5)) ('N*'m)%U.
Definition get_E_a_by_N N :=
let N := CHK_UNIT N 'rpm in
CVT_UNIT (K_E * N) 'V.
Definition get_M_by_I_m I_m :=
let I_m := CHK_UNIT I_m 'A in
CVT_UNIT (K_T * (I_m - I_m0)) ('N*'m)%U.
Definition get_U_m_by_E_a_and_I_m E_a I_m :=
let E_a := CHK_UNIT E_a 'V in
let I_m := CHK_UNIT I_m 'A in
CVT_UNIT (E_a + R_m * I_m) 'V.
Section test.
Variable E_a I_m : R.
Goal qsameub (get_U_m_by_E_a_and_I_m (u2qR E_a 'V) (u2qR I_m 'A)) 'V = true.
Proof. qeqR. Qed.
Goal qsameub (get_U_m_by_E_a_and_I_m (u2qR E_a 'V) (u2qR I_m 'mA)) 'V = false.
Proof. qeqR. Qed.
Goal qsameub (get_U_m_by_E_a_and_I_m (u2qR E_a 'V) (u2qR I_m 'A)) (_m 'V) = false.
Proof. qeqR. Qed.
End test.
Definition get_U_eo_by_U_m_and_I_m U_m I_m :=
let U_m := CHK_UNIT U_m 'V in
let I_m := CHK_UNIT I_m 'A in
CVT_UNIT (U_m + I_m * R_e) 'V.
Definition get_U_eo_by_sigma_e sigma_e :=
let sigma_e := CHK_UNIT sigma_e 1 in
CVT_UNIT (sigma_e * U_b) 'V.
Definition get_I_e_by_sigma_e_and_I_m sigma_e I_m :=
let sigma_e := CHK_UNIT sigma_e 1 in
let I_m := CHK_UNIT I_m 'A in
CVT_UNIT (sigma_e * I_m) 'A.
Definition get_I_b_by_I_e I_e :=
let I_e := CHK_UNIT I_e 'A in
CVT_UNIT (n_r * I_e + I_other) 'A.
Definition get_U_e_by_I_b I_b :=
let I_b := CHK_UNIT I_b 'A in
CVT_UNIT (U_b - I_b * R_b) 'V.
Definition get_T_b_by_I_b I_b :=
let I_b := CHK_UNIT I_b 'A in
CVT_UNIT ((C_b - C_min) / I_b * val_0_06) 'min.
Module T_b_ex.
Extract Constant val_0_06 => "0.06".
Extract Constant val_C_b => "4000.".
Extract Constant val_C_min => "800.".
Example val_T_b_1 := qval (get_T_b_by_I_b (u2qR 15 'A)).
Example val_T_b_2 := qval (get_T_b_by_I_b (u2qR 15 'mA)).
Extraction "test_T_b.ml" val_T_b_1 val_T_b_2.
End T_b_ex.
Definition get_G_maxload_by_T T :=
let T := CHK_UNIT T 'N in
CVT_UNIT (n_r * T - G) 'N.
Definition get_theta_max_by_T T :=
let T := CHK_UNIT T 'N in
CVT_UNIT ('acos (G / (n_r * T))) 1.
Definition get_eta_by_M_and_N_and_I_b M N I_b :=
let M := CHK_UNIT M ('N*'m)%U in
let N := CHK_UNIT N 'rpm in
let I_b := CHK_UNIT I_b 'A in
CVT_UNIT (((2 * PI) / 60) * n_r * M * N / (U_b * I_b)) 1.
let N := CHK_UNIT N 'rpm in
let _ret := rho * C_T * (D_p ^ 4) * ((N / 60) ^ 2) in
CVT_UNIT _ret 'N.
Hint Unfold get_T_by_N : Q.
Lemma get_T_by_N_unit : forall N, qsameu N 'rpm -> qsameu (get_T_by_N N) 'N.
Proof.
intros. autounfold with Q. lazy [qsameu q2quR q2qu q2qn] in *.
destruct N; auto. rewrite H. simpl.
rewrite neqb_refl. simpl. auto.
Qed.
Definition get_M_by_N N :=
let N := CHK_UNIT N 'rpm in
CVT_UNIT (C_M * rho * ((N / 60) ^ 2) * (D_p ^ 5)) ('N*'m)%U.
Definition get_E_a_by_N N :=
let N := CHK_UNIT N 'rpm in
CVT_UNIT (K_E * N) 'V.
Definition get_M_by_I_m I_m :=
let I_m := CHK_UNIT I_m 'A in
CVT_UNIT (K_T * (I_m - I_m0)) ('N*'m)%U.
Definition get_U_m_by_E_a_and_I_m E_a I_m :=
let E_a := CHK_UNIT E_a 'V in
let I_m := CHK_UNIT I_m 'A in
CVT_UNIT (E_a + R_m * I_m) 'V.
Section test.
Variable E_a I_m : R.
Goal qsameub (get_U_m_by_E_a_and_I_m (u2qR E_a 'V) (u2qR I_m 'A)) 'V = true.
Proof. qeqR. Qed.
Goal qsameub (get_U_m_by_E_a_and_I_m (u2qR E_a 'V) (u2qR I_m 'mA)) 'V = false.
Proof. qeqR. Qed.
Goal qsameub (get_U_m_by_E_a_and_I_m (u2qR E_a 'V) (u2qR I_m 'A)) (_m 'V) = false.
Proof. qeqR. Qed.
End test.
Definition get_U_eo_by_U_m_and_I_m U_m I_m :=
let U_m := CHK_UNIT U_m 'V in
let I_m := CHK_UNIT I_m 'A in
CVT_UNIT (U_m + I_m * R_e) 'V.
Definition get_U_eo_by_sigma_e sigma_e :=
let sigma_e := CHK_UNIT sigma_e 1 in
CVT_UNIT (sigma_e * U_b) 'V.
Definition get_I_e_by_sigma_e_and_I_m sigma_e I_m :=
let sigma_e := CHK_UNIT sigma_e 1 in
let I_m := CHK_UNIT I_m 'A in
CVT_UNIT (sigma_e * I_m) 'A.
Definition get_I_b_by_I_e I_e :=
let I_e := CHK_UNIT I_e 'A in
CVT_UNIT (n_r * I_e + I_other) 'A.
Definition get_U_e_by_I_b I_b :=
let I_b := CHK_UNIT I_b 'A in
CVT_UNIT (U_b - I_b * R_b) 'V.
Definition get_T_b_by_I_b I_b :=
let I_b := CHK_UNIT I_b 'A in
CVT_UNIT ((C_b - C_min) / I_b * val_0_06) 'min.
Module T_b_ex.
Extract Constant val_0_06 => "0.06".
Extract Constant val_C_b => "4000.".
Extract Constant val_C_min => "800.".
Example val_T_b_1 := qval (get_T_b_by_I_b (u2qR 15 'A)).
Example val_T_b_2 := qval (get_T_b_by_I_b (u2qR 15 'mA)).
Extraction "test_T_b.ml" val_T_b_1 val_T_b_2.
End T_b_ex.
Definition get_G_maxload_by_T T :=
let T := CHK_UNIT T 'N in
CVT_UNIT (n_r * T - G) 'N.
Definition get_theta_max_by_T T :=
let T := CHK_UNIT T 'N in
CVT_UNIT ('acos (G / (n_r * T))) 1.
Definition get_eta_by_M_and_N_and_I_b M N I_b :=
let M := CHK_UNIT M ('N*'m)%U in
let N := CHK_UNIT N 'rpm in
let I_b := CHK_UNIT I_b 'A in
CVT_UNIT (((2 * PI) / 60) * n_r * M * N / (U_b * I_b)) 1.
Definition get_N_by_T T :=
let T := CHK_UNIT T 'N in
CVT_UNIT (60 * qsqrt (T /(rho * C_T * (D_p ^ 4)))) 'rpm.
Definition get_N_by_M M :=
let M := CHK_UNIT M ('N*'m)%U in
CVT_UNIT (60 * (qsqrt (M / (rho * (D_p ^ 5) * C_M)))) 'rpm.
Axiom const_val_0_0065 : val_0_0065 = 0.0065.
Axiom const_val_5_2561 : val_5_2561 = 5.2561.
Axiom const_val_0_8 : val_0_8 = 0.8.
Axiom const_val_0_25 : val_0_25 = 0.0065.
Axiom const_val_9_55 : val_9_55 = 9.55.
Axiom const_val_0_06 : val_0_06 = 0.0065.
Axiom const_val_5_2561 : val_5_2561 = 5.2561.
Axiom const_val_0_8 : val_0_8 = 0.8.
Axiom const_val_0_25 : val_0_25 = 0.0065.
Axiom const_val_9_55 : val_9_55 = 9.55.
Axiom const_val_0_06 : val_0_06 = 0.0065.
These assumptions should be checked by expert carefully.
Axiom const_val_T_0 : val_T_0 = 273.15.
Axiom gt0_val_p_0 : (0 < val_p_0)%R.
Axiom gt0_val_rho_0 : (0 < val_rho_0)%R.
Axiom gt0_val_T_t : (0 < val_T_t)%R.
Axiom gt0_val_n_r : (0 < val_n_r)%R.
Axiom gt0_val_G : (0 < val_G)%R.
Temperature and Height assumption
1. max flight height is [0~9200] meter, that means [0~30000] ft. 2. environment temperature is [-60,60] ℃
Axiom condL_val_h : (0 < val_h)%R.
Axiom condH_val_h : (val_h < 9200)%R.
Axiom condL_val_T_t : (-60 < val_T_t)%R.
Axiom condH_val_T_t : (val_T_t < 60)%R.
Axiom gt0_val_D_p : (0 < val_D_p)%R.
Axiom gt0_val_B_p : (0 < val_B_p)%R.
Axiom gt0_val_PP_A : (0 < val_PP_A)%R.
Axiom gt0_val_PP_K0 : (0 < val_PP_K0)%R.
Axiom gt0_val_PP_epsilon : (0 < val_PP_epsilon)%R.
Axiom gt0_val_PP_lambda : (0 < val_PP_lambda)%R.
Axiom gt0_val_PP_zeta : (0 < val_PP_zeta)%R.
Axiom gt0_val_PP_e : (0 < val_PP_e)%R.
Axiom gt0_val_C_fd : (0 < val_C_fd)%R.
Axiom gt0_val_C_T : (0 < val_C_T)%R. Axiom gt0_val_C_M : (0 < val_C_M)%R. Axiom gt0_val_R_b : (0 < val_R_b)%R.
Axiom gt0_val_R_m : (0 < val_R_m)%R.
Axiom gt0_val_R_e : (0 < val_R_e)%R.
Axiom gt0_val_PP_alpha_ab : (0 < val_PP_alpha_ab)%R.
Axiom gt0_val_U_b : (0 < val_U_b)%R.
Axiom gt0_val_C_b_minus_C_min : 0 < val_C_b - val_C_min. Axiom gt0_val_U_m0 : (0 < val_U_m0)%R. Axiom gt0_val_K_V0 : (0 < val_K_V0)%R.
Axiom condH_val_h : (val_h < 9200)%R.
Axiom condL_val_T_t : (-60 < val_T_t)%R.
Axiom condH_val_T_t : (val_T_t < 60)%R.
Axiom gt0_val_D_p : (0 < val_D_p)%R.
Axiom gt0_val_B_p : (0 < val_B_p)%R.
Axiom gt0_val_PP_A : (0 < val_PP_A)%R.
Axiom gt0_val_PP_K0 : (0 < val_PP_K0)%R.
Axiom gt0_val_PP_epsilon : (0 < val_PP_epsilon)%R.
Axiom gt0_val_PP_lambda : (0 < val_PP_lambda)%R.
Axiom gt0_val_PP_zeta : (0 < val_PP_zeta)%R.
Axiom gt0_val_PP_e : (0 < val_PP_e)%R.
Axiom gt0_val_C_fd : (0 < val_C_fd)%R.
Axiom gt0_val_C_T : (0 < val_C_T)%R. Axiom gt0_val_C_M : (0 < val_C_M)%R. Axiom gt0_val_R_b : (0 < val_R_b)%R.
Axiom gt0_val_R_m : (0 < val_R_m)%R.
Axiom gt0_val_R_e : (0 < val_R_e)%R.
Axiom gt0_val_PP_alpha_ab : (0 < val_PP_alpha_ab)%R.
Axiom gt0_val_U_b : (0 < val_U_b)%R.
Axiom gt0_val_C_b_minus_C_min : 0 < val_C_b - val_C_min. Axiom gt0_val_U_m0 : (0 < val_U_m0)%R. Axiom gt0_val_K_V0 : (0 < val_K_V0)%R.
Global Hint Unfold
get_E_a_by_N
get_G_maxload_by_T
get_I_b_by_I_e
get_I_e_by_sigma_e_and_I_m
get_M_by_N
get_M_by_I_m
get_N_by_M
get_N_by_T
get_T_by_N
: Q.
Global Hint Resolve
gt0_val_p_0
gt0_val_rho_0
gt0_val_T_t
gt0_val_G
gt0_val_n_r
condL_val_h
condH_val_h
condL_val_T_t
condH_val_T_t
gt0_val_D_p
gt0_val_B_p
gt0_val_PP_A
gt0_val_PP_K0
gt0_val_PP_epsilon
gt0_val_PP_lambda
gt0_val_PP_zeta
gt0_val_PP_e
gt0_val_C_fd
gt0_val_C_T
gt0_val_C_M
gt0_val_R_b
gt0_val_R_m
gt0_val_R_e
gt0_val_PP_alpha_ab
gt0_val_U_b
gt0_val_C_b_minus_C_min
gt0_val_U_m0
gt0_val_K_V0
: Q.
Hint Rewrite
const_val_0_0065
const_val_5_2561
const_val_0_8
const_val_0_25
const_val_9_55
const_val_0_06
const_val_T_0
: Q.