This notation allows one to easily write closed expressions for
OpenUnit (e.g. ou (1#2)). The typechecker verifies that the close
term is inside (0,1) by computation.
Notation "'ou' x":=(@Build_OpenUnit x (conj (refl_equal Lt) (refl_equal Lt))) (at level 60, no associativity) : ou_scope.
Basic propertirs about a:OpenUnit and its dual value 1-a.
Lemma OpenUnit_0_lt : forall (a:OpenUnit), 0 < a.
Lemma OpenUnit_lt_1 : forall (a:OpenUnit), a < 1.
Lemma OpenUnit_0_lt_Dual : forall (a:OpenUnit), 0 < 1-a.
Lemma OpenUnit_Dual_lt_1 : forall (a:OpenUnit), 1-a < 1.
Lemma OpenUnit_lt_1 : forall (a:OpenUnit), a < 1.
Lemma OpenUnit_0_lt_Dual : forall (a:OpenUnit), 0 < 1-a.
Lemma OpenUnit_Dual_lt_1 : forall (a:OpenUnit), 1-a < 1.
Multiplication
Definition OpenUnitMult (a b:OpenUnit):OpenUnit.
Defined.
Notation "x * y":=(OpenUnitMult x y) : ou_scope.
Defined.
Notation "x * y":=(OpenUnitMult x y) : ou_scope.
Division
The dual of a is 1-a
The dual of multipliation: 1 - (1-a)*(1-b) or a + b - a*b
The dual of division: 1 - (1-b)/(1-a) or (b-a)/(1-a)
Definition ou_eq (x y:OpenUnit) := Qeq x y.
Lemma ou_eq_refl : forall x, ou_eq x x.
Lemma ou_eq_sym : forall x y, ou_eq x y -> ou_eq y x.
Lemma ou_eq_trans : forall x y z, ou_eq x y -> ou_eq y z -> ou_eq x z.
Add Relation OpenUnit ou_eq
reflexivity proved by ou_eq_refl
symmetry proved by ou_eq_sym
transitivity proved by ou_eq_trans
as ou_st.
Lemma ou_eq_refl : forall x, ou_eq x x.
Lemma ou_eq_sym : forall x y, ou_eq x y -> ou_eq y x.
Lemma ou_eq_trans : forall x y z, ou_eq x y -> ou_eq y z -> ou_eq x z.
Add Relation OpenUnit ou_eq
reflexivity proved by ou_eq_refl
symmetry proved by ou_eq_sym
transitivity proved by ou_eq_trans
as ou_st.
One cheif use of OpenUnit is to make strict affine combinations.
Definition affineCombo (o:OpenUnit) (a b:Q) := o*a + (1-o)*b.
Add Morphism affineCombo with signature ou_eq ==> Qeq ==> Qeq ==> Qeq as affineCombo_wd.
Add Morphism affineCombo with signature ou_eq ==> Qeq ==> Qeq ==> Qeq as affineCombo_wd.
Properties of an affine combination.
Lemma affineCombo_gt : forall o a b (H:a < b), a < affineCombo o a b.
Lemma affineCombo_lt : forall o a b (H:a < b), affineCombo o a b < b.
Lemma affineAffine_l : forall a b o1 o2,
(affineCombo o1 a (affineCombo o2 a b)==affineCombo (OpenUnitDualMult o1 o2) a b)%Q.
Lemma affineAffine_r : forall a b o1 o2,
(affineCombo o1 (affineCombo o2 a b) b==affineCombo (o1*o2) a b)%Q.
Lemma affineCombo_lt : forall o a b (H:a < b), affineCombo o a b < b.
Lemma affineAffine_l : forall a b o1 o2,
(affineCombo o1 a (affineCombo o2 a b)==affineCombo (OpenUnitDualMult o1 o2) a b)%Q.
Lemma affineAffine_r : forall a b o1 o2,
(affineCombo o1 (affineCombo o2 a b) b==affineCombo (o1*o2) a b)%Q.