Library time

Parameter Time: Type.
Parameter Zero: Time.
Parameter tadd: Time → Time → Time.
Notation "t1 @+ t2" := (tadd t1 t2) (at level 50).

Inductive tle t1 t2: Prop :=
  tleDiff: ∀ t, t1 @+ t = t2 → tle t1 t2.
Notation "t1 @<= t2" := (tle t1 t2) (at level 60).

Inductive tlt t1 t2: Prop :=
  istlt: t1 @<= t2 → t1 ≠ t2 → tlt t1 t2.
Notation "t1 @< t2" := (tlt t1 t2) (at level 60).

Parameter tplus_0_n: ∀ n, Zero @+ n = n.
Parameter tplus_n_0: ∀ n, n @+ Zero = n.
Parameter tplus_eq_0: ∀ n1 n2, Zero = n1 @+ n2 → n1 = Zero ∧ n2 = Zero.
Parameter tplus_assoc: ∀ n1 n2 n3, n1 @+ n2 @+ n3 = n1 @+ (n2 @+ n3).
Parameter tplus_opp_l: ∀ n n1 n2, n @+ n1 = n @+ n2 → n1 = n2.
Parameter tle_total: ∀ n1 n2, {n1 @<= n2}+{n2 @<= n1}.
Parameter teq_0_dec: ∀ (t:Time), {t=Zero}+{t ≠ Zero}.
Parameter tunb: ∀ (t:Time), ∃ t', t @< t'.

Lemma tlt_plus_nlt: ∀ t t', ¬t @+ t' @< t.
Proof.
  intros; intro.
  destruct H.
  destruct H.
  rewrite tplus_assoc in H.
  rewrite <- (tplus_n_0 t) in H.
  rewrite tplus_assoc in H.
  apply tplus_opp_l in H.
  rewrite tplus_0_n in H.
  apply eq_sym in H.
  apply tplus_eq_0 in H.
  destruct H.
  subst.
  apply H0; apply tplus_n_0.
Qed.

Lemma tle_trans: ∀ t1 t2 t3, t1 @<= t2 → t2 @<= t3 → t1 @<= t3.
Proof.
  intros.
  inversion_clear H.
  inversion_clear H0.
  rewrite <-H; clear H t3.
  rewrite <-H1; clear H1 t2.
  rewrite tplus_assoc.
  ∃ (t @+ t0).
  auto.
Qed.

Lemma tle_n_0: ∀ t, t @<= Zero → t=Zero.
Proof.
  intros.
  destruct H.
  apply sym_eq in H.
  apply tplus_eq_0 in H.
  apply (proj1 H).
Qed.

Lemma tle_refl: ∀ t, t @<= t.
Proof.
  intro.
  ∃ Zero.
  apply tplus_n_0.
Qed.

Lemma tle_mono_l: ∀ t t1 t2, t1 @<= t2 → t @+ t1 @<= t @+ t2.
Proof.
  intros.
  destruct H.
  ∃ t0.
  rewrite <-H; clear H.
  apply tplus_assoc.
Qed.

Lemma tle_lt_cases: ∀ d1 d2,
  (d1 @<= d2) ∨ (∃ t: Time, d1 = d2 @+ t ∧ t ≠ Zero).
Proof.
  intros.
  case (tle_total d1 d2); intro.
  left; apply t.
  destruct t.
  case (teq_0_dec t); intro.
  rewrite e in *; clear e t.
  rewrite tplus_n_0 in H.
  rewrite H in *; clear H d2.
  left; apply tle_refl.
  right; ∃ t.
  split; auto.
Qed.

Definition tmin d1 d2 := if tle_total d1 d2 then d1 else d2.

Lemma tmin_lel: ∀ d1 d2, tmin d1 d2 @<= d1.
Proof.
  intros.
  unfold tmin; case (tle_total d1 d2); simpl; intros; auto.
  apply tle_refl.
Qed.

Lemma tmin_ler: ∀ d1 d2, tmin d1 d2 @<= d2.
Proof.
  intros.
  unfold tmin; case (tle_total d1 d2); simpl; intros; auto.
  apply tle_refl.
Qed.

Lemma tmin_nz: ∀ d1 d2, d1 ≠ Zero → d2 ≠ Zero → tmin d1 d2 ≠ Zero.
Proof.
  intros.
  unfold tmin; case (tle_total d1 d2); simpl; intros; auto.
Qed.