VQCS.Nconv

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

Open Scope Unit_scope.

#[global] Opaque n2u.

Conversion between normalized units

Two Nunits are convertible only when they have same dimensions

Definition ncvtble (n1 n2 : Nunit) : Prop := ndims n1 = ndims n2.

ncvtble is equivalence relation

Lemma ncvtble_refl : forall n, ncvtble n n.
Proof. intros. hnf. auto. Qed.

Lemma ncvtble_sym : forall n1 n2, ncvtble n1 n2 -> ncvtble n2 n1.
Proof. intros. hnf. auto. Qed.

Lemma ncvtble_trans : forall n1 n2 n3, ncvtble n1 n2 -> ncvtble n2 n3 -> ncvtble n1 n3.
Proof. intros. hnf. rewrite H. auto. Qed.

#[export] Instance ncvtble_equiv : Equivalence ncvtble.
Proof.
constructor; hnf; intros; auto.
apply ncvtble_refl. apply ncvtble_sym; auto. apply ncvtble_trans with y; auto.
Qed.

Two normalized units are similar only when they have same dimensions (bool version)

Definition ncvtbleb (n1 n2 : Nunit) : bool := deqb (ndims n1) (ndims n2).

Lemma ncvtbleb_refl : forall n, ncvtbleb n n = true.
Proof. intros. unfold ncvtbleb. rewrite deqb_refl. auto. Qed.

Lemma ncvtbleb_true_iff : forall n1 n2, ncvtbleb n1 n2 = true <-> ncvtble n1 n2.
Proof. intros. unfold ncvtbleb, ncvtble. rewrite deqb_true_iff. simpl. easy. Qed.

Lemma ncvtbleb_false_iff : forall n1 n2, ncvtbleb n1 n2 = false <-> ~(ncvtble n1 n2 ).
Proof. intros. rewrite <- ncvtbleb_true_iff. split; solve_bool. Qed.

Lemma ncvtbleb_reflect : forall n1 n2, reflect (ncvtble n1 n2) (ncvtbleb n1 n2).
Proof.
intros. destruct (ncvtbleb n1 n2) eqn:E1; constructor.
apply ncvtbleb_true_iff; auto. apply ncvtbleb_false_iff; auto.
Qed.

#[export] Hint Resolve ncvtbleb_reflect : bdestruct.

Get ratio factor from Nunit `src` to Nunit `ref`

Definition nconvRate (src ref : Nunit) : option R :=
  if ncvtbleb src ref
  then Some (ncoef src / ncoef ref)%R
  else None.

Lemma nconvRate_eq : forall n, ncoef n <> 0 -> nconvRate n n = Some 1.
Proof. intros. unfold nconvRate. rewrite ncvtbleb_refl. f_equal. ra. Qed.

Convert a Nunit `src` to Nunit `ref`

Definition nconv (src ref : Nunit) : option (R * Nunit) :=
  if ncvtbleb src ref
  then Some ((ncoef src / ncoef ref)%R, ref )
  else None.

Section test.

  Goal nconvRate (u2n 'hrs ) (u2n 'min ) = Some 60.
  Proof. cbv. f_equal. lra. Qed.

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