VQCS.Uconv


Require Export Unit Nunit.
Require Import SI.
Import SI_Accepted.

Open Scope Unit_scope.

Conversion between Unit


Two units are convertible

Two units are convertible only when they have same dimensions
Definition ucvtble (u1 u2 : Unit) : Prop := ndims (u2n u1) = ndims (u2n u2).

ucvtble is equivalence relation
Lemma ucvtble_refl : forall u, ucvtble u u.
Proof. intros. hnf. auto. Qed.

Lemma ucvtble_sym : forall u1 u2, ucvtble u1 u2 -> ucvtble u2 u1.
Proof. intros. hnf. auto. Qed.

Lemma ucvtble_trans : forall u1 u2 u3, ucvtble u1 u2 -> ucvtble u2 u3 -> ucvtble u1 u3.
Proof. intros. hnf. rewrite H. auto. Qed.

#[export] Instance ucvtble_equiv : Equivalence ucvtble.
Proof.
  constructor; hnf; intros; auto.
  apply ucvtble_refl. apply ucvtble_sym; auto. apply ucvtble_trans with y; auto.
Qed.


Two units are similar only when they have same dimensions (bool version)
Definition ucvtbleb (u1 u2 : Unit) : bool := deqb (ndims (u2n u1)) (ndims (u2n u2)).

Lemma ucvtbleb_true_iff : forall u1 u2, ucvtbleb u1 u2 = true <-> ucvtble u1 u2.
Proof. intros. unfold ucvtbleb, ucvtble. rewrite deqb_true_iff. simpl. easy. Qed.

Lemma ucvtbleb_false_iff : forall u1 u2, ucvtbleb u1 u2 = false <-> ~(ucvtble u1 u2).
Proof. intros. rewrite <- ucvtbleb_true_iff. split; solve_bool. Qed.

Lemma ucvtbleb_reflect : forall u1 u2, reflect (ucvtble u1 u2) (ucvtbleb u1 u2).
Proof.
  intros. destruct (ucvtbleb u1 u2) eqn:E1; constructor.
  apply ucvtbleb_true_iff; auto. apply ucvtbleb_false_iff; auto.
Qed.

#[export] Hint Resolve ucvtbleb_reflect : bdestruct.

Get ratio factor from Unit `src` to Unit `ref`
Definition uconvRate (src ref : Unit) : option R :=
  if ucvtbleb src ref
  then Some (ncoef (u2n src) / ncoef (u2n ref))%R
  else None.

Convert a Unit `src` to Unit `ref`
Definition uconv (src ref : Unit) : option (R * Unit) :=
  if ucvtbleb src ref
  then Some ((ncoef (u2n src) / ncoef (u2n ref))%R, ref)
  else None.

Section test.

  Goal uconvRate 'hrs 'min = Some 60.
  Proof. cbv. f_equal. lra. Qed.

  Goal uconv 'hrs 's = Some (3600, Ubu 's).
  Proof. cbv. f_equal. f_equal. lra. Qed.
End test.

Convert a unit with given reference unit.

  For example:
    src = 2*hours, ref = 30*minutes, return (4, 30*minutes).
  Conversion step
  1. check that src and ref is convertible
  2. calc coefficient
    src == (coef_src, dims)
    ref == (coef_ref, dims)
    coef = coef_src / coef_ref
  3. return result
    dst = (coef, ref)






Unify two Units

  For example:
    src = 2*hours, ref = 30*minutes, return (7200, 1800, secons)
  Steps:
  1. normalize
     u1 == (c1, d1), u2 == (c2, d2)
  2. check if `u1` and `u2` are convertible, that is `d1 =? d2`.
     If not return None, otherwise retrun (c1,c2,d).
     Here, d == (1, d1) = (1, d2)