Section StepFunction.

Variable X:Type.

Step Functions

We represent step functions from [0,1] to X inductively as a tree structure. In the base case a costant function is a step function. Given two step functions f and g, then they can be scaled and glued together at a point o yeilding the step function which is f(x/o) for x in [0,o], and g((x-o)/(1-o)) for x in [o,1].

Step functions are not functions. They could be interpreted as functions; however, we don't give any particular interpretation to how the step functions ought to behave at the glue points in between step. Because our primary purpose for introducing step functions is to implement integration, this ambiguity is not a problem.

Inductive StepF :Type:=
|constStepF:X-> StepF
|glue:OpenUnit-> StepF -> StepF -> StepF.

Fixpoint StepFfold (Y : Type) (f : X -> Y) (g : OpenUnit -> Y -> Y -> Y)
              (s : StepF) {struct s} : Y :=
  match s with
  | constStepF x => f x
  | glue b t1 t2 => g b (StepFfold f g t1) (StepFfold f g t2)
  end.

If f is a step function, so is f(1-x). This symmetry operation is useful reasoning about step functions because of the symetric nature of the glue constructor.

Definition Mirror :StepF -> StepF :=
StepFfold constStepF (fun a l r => glue (OpenUnitDual a) r l).

Split decomposes (and scales) a step function at a point o. It is essentially an inverse operation of glue

Definition Split : StepF -> OpenUnit -> StepF*StepF.

Defined.

Definition SplitL (s:StepF) (o:OpenUnit) : StepF :=
fst (Split s o).

Definition SplitR (s:StepF) (o:OpenUnit) : StepF :=
snd (Split s o).

Induction principles for reasoning about Split, SplitR, and SplitL

Lemma Split_ind : forall s a (P:StepF*StepF -> Prop),
(P (SplitL s a,SplitR s a)) -> P (Split s a).

Lemma SplitLR_glue_ind : forall s1 s2 (a b:OpenUnit) (P:StepF -> StepF -> Prop),
(forall (H:a < b), P (SplitL s1 (OpenUnitDiv a b H)) (glue (OpenUnitDualDiv b a H) (SplitR s1 (OpenUnitDiv a b H)) s2)) ->
(forall (H:b < a), P (glue (OpenUnitDiv b a H) s1 (SplitL s2 (OpenUnitDualDiv a b H))) (SplitR s2 (OpenUnitDualDiv a b H))) ->
(a == b -> P s1 s2) ->
P (SplitL (glue b s1 s2) a) (SplitR (glue b s1 s2) a).

Lemma SplitL_glue_ind : forall s1 s2 (a b:OpenUnit) (P:StepF -> Prop),
(forall (H:a < b), P (SplitL s1 (OpenUnitDiv a b H))) ->
(forall (H:b < a), P (glue (OpenUnitDiv b a H) s1 (SplitL s2 (OpenUnitDualDiv a b H)))) ->
(a == b -> P (s1)) ->
P (SplitL (glue b s1 s2) a).

Lemma SplitR_glue_ind : forall s1 s2 (a b:OpenUnit) (P:StepF -> Prop),
(forall (H:a < b), P (glue (OpenUnitDualDiv b a H) (SplitR s1 (OpenUnitDiv a b H)) s2)) ->
(forall (H:b < a), P (SplitR s2 (OpenUnitDualDiv a b H))) ->
(a == b -> P (s2)) ->
P (SplitR (glue b s1 s2) a).

Lemma SplitGlue : forall x y:StepF, forall o,
  (Split (glue o x y) o)=(x, y).

Lemma SplitLGlue : forall x y:StepF, forall o,
  (SplitL (glue o x y) o)=x.

Lemma SplitRGlue : forall x y:StepF, forall o,
  (SplitR (glue o x y) o)=y.

As stepping point to a proper setoid equality on step functions, StepF_Qeq specifies equality of step function upto Qeq on rational glue points

Fixpoint StepF_Qeq (s1 s2: StepF) : Prop :=
match s1, s2 with
|constStepF x, constStepF y => x = y
|glue a x1 x2, glue b y1 y2 => a == b /\ (StepF_Qeq x1 y1) /\ (StepF_Qeq x2 y2)
|_, _ => ⊥
end.

Lemma StepF_Qeq_refl : forall (s: StepF), StepF_Qeq s s.

Lemma StepF_Qeq_sym : forall (s t: StepF), StepF_Qeq s t -> StepF_Qeq t s.

Lemma StepF_Qeq_trans : forall (s t u: StepF), StepF_Qeq s t -> StepF_Qeq t u -> StepF_Qeq s u.

Mirror behaves well with respect to this equality

Lemma Mirror_resp_Qeq : forall (s t:StepF), StepF_Qeq s t -> StepF_Qeq (Mirror s) (Mirror t).
Lemma MirrorMirror : forall (s:StepF), (StepF_Qeq (Mirror (Mirror s)) s).

Splits interacts with Mirror in the way you expect

Lemma SplitR_resp_Qeq : forall (s t:StepF) (a b:OpenUnit), a == b -> StepF_Qeq s t -> StepF_Qeq (SplitR s a) (SplitR t b).
Lemma MirrorSplitL_Qeq : forall (s:StepF) (a b:OpenUnit), b == (OpenUnitDual a) -> (StepF_Qeq (Mirror (SplitL s a)) (SplitR (Mirror s) b)).

Lemma MirrorSplitR_Qeq: forall (s:StepF) (a b:OpenUnit), b == (OpenUnitDual a) -> (StepF_Qeq (Mirror (SplitR s a)) (SplitL (Mirror s) b)).

Lemma SplitL_resp_Qeq : forall (s t:StepF) (a b:OpenUnit), a == b -> StepF_Qeq s t -> StepF_Qeq (SplitL s a) (SplitL t b).

The following three lemmas are the key lemmas about Splits. They characterise how Splits distribute across each other.

Lemma SplitLSplitL : forall (s:StepF) (a b c:OpenUnit), (a*b==c) ->
(StepF_Qeq (SplitL (SplitL s a) b) (SplitL s c)).

Lemma SplitRSplitR : forall (s:StepF) (a b c:OpenUnit), (a+b-a*b==c) ->
(StepF_Qeq (SplitR (SplitR s a) b) (SplitR s c)).

Lemma SplitLSplitR : forall (s:StepF) (a b c d:OpenUnit), (a+b-a*b==c) -> (d*c==a) ->
(StepF_Qeq (SplitL (SplitR s a) b) (SplitR (SplitL s c) d)).

End StepFunction.

Step functions are a functor

Definition Map(X Y:Type):(X->Y)->(StepF X)->(StepF Y).

Defined.

Notation "f ^@> x" := (Map f x) (at level 15, left associativity) : sfscope.

Step functions are an applicative functor

Fixpoint Ap (X Y:Type) (f:StepF (X->Y)) (a:StepF X) : StepF Y :=
match f with
|constStepF f0 => f0 ^@> a
|glue o f0 f1 => let (l,r):=Split a o in (glue o (Ap f0 l) (Ap f1 r))
end.

Notation "f <@> x" := (Ap f x) (at level 15, left associativity) : sfscope.

Definition Map2 (X Y Z:Type) (f:(X->Y->Z)) a b :=
f ^@> a <@> b.

Add Parametric Morphism X Y f : (@Map X Y f) with signature (@StepF_Qeq X) ==> (@StepF_Qeq Y) as Map_resp_Qeq.

These lemmas show how ap distributes over glue

Lemma ApGlue : forall X Y (fl fr:StepF (X -> Y)) o b, (glue o fl fr) <@> b = glue o (fl <@> (SplitL b o)) (fr <@> (SplitR b o)).

Lemma ApGlueGlue : forall X Y (fl fr:StepF (X -> Y)) o l r, (glue o fl fr) <@> (glue o l r) = glue o (fl <@> l) (fr <@> r).
Add Parametric Morphism X Y : (@Ap X Y) with signature (@StepF_Qeq (X->Y)) ==> (@StepF_Qeq X) ==> (@StepF_Qeq Y) as Ap_resp_Qeq.
Section Ap.

Splits commute with maps

Lemma SplitMap (X Y:Type):forall x:(StepF X), forall a, forall f:X->Y,
    (Split (Map f x) a) = let (l,r) := Split x a in (Map f l,Map f r).

Lemma SplitLMap (X Y:Type): forall x:(StepF X), forall a, forall f:X->Y,
    SplitL (Map f x) a = Map f (SplitL x a).

Lemma SplitRMap(X Y:Type): forall x:(StepF X), forall a, forall f:X->Y,
    SplitR (Map f x) a = Map f (SplitR x a).

These lemmas show how ap distributes over split and uses mirror properties to get the symetric cases

Lemma SplitLAp_Qeq (X Y:Type) : forall (f: StepF (X -> Y)) s o,
StepF_Qeq (SplitL (f <@> s) o) ((SplitL f o) <@> (SplitL s o)).

Lemma MirrorMap (X Y:Type) : forall (f: X -> Y) s,
(Mirror (Map f s)) = (Map f (Mirror s)).

Lemma MirrorAp_Qeq (X Y: Type) : forall (f: StepF (X -> Y)) s,
StepF_Qeq (Mirror (f <@> s)) ((Mirror f) <@> (Mirror s)).

Lemma SplitRAp_Qeq (X Y:Type) : forall (f: StepF (X -> Y)) s o,
StepF_Qeq (SplitR (f <@> s) o) ((SplitR f o) <@> (SplitR s o)).

End Ap.

Section ApplicativeFunctor.

These are the laws of an applicative functor

Lemma Ap_identity : forall X (a:StepF X), constStepF (fun x => x) <@> a = a.

Lemma Map_identity : forall X (a:StepF X), (fun x => x) ^@> a = a.

Let compose X Y Z (x : Y ->Z) (y:X -> Y) z := x (y z).

Lemma Ap_composition_Qeq : forall X Y Z (a:StepF (Y->Z)) (b:StepF (X->Y)) (c:StepF X),
StepF_Qeq (constStepF (@compose X Y Z) <@> a <@> b <@> c) (a <@> (b <@> c)).

Lemma Map_composition_Qeq : forall X Y Z (a:StepF (Y->Z)) (b:StepF (X->Y)) (c:StepF X),
StepF_Qeq ((fun x y z => x (y z)) ^@> a <@> b <@> c) (a <@> (b <@> c)).

Lemma Ap_homomorphism : forall X Y (f:X->Y) (a:X),
(constStepF f <@> constStepF a) = (constStepF (f a)).

Lemma Map_homomorphism : forall X Y (f:X->Y) (a:X),
(f ^@> constStepF a) = (constStepF (f a)).

Lemma Ap_interchange : forall X Y (f:StepF (X->Y)) (a:X),
(f <@> constStepF a) = (constStepF (fun g => g a)) <@> f.

Lemma Map_interchange : forall X Y (f:StepF (X->Y)) (a:X),
(f <@> constStepF a) = (fun g => g a) ^@> f.

Lemma Map_compose_Map : forall X Y Z (f:Y->Z) (g:X -> Y) a,
StepF_Qeq ((fun a => f (g a)) ^@> a) (f ^@> (g ^@> a)).

End ApplicativeFunctor.