Section StepF_Functions.

Variable X:Setoid.

Step Functions over setoids

In this section we redevelop step functions over a setoid X. Here we shadow the old Step Function operations to operate over setoids.

Definition StepF := StepF X.

We lift the constructors and destructors to the setoid version
Definition constStepF : X -> StepF := (@constStepF X).

Definition glue : OpenUnit -> StepF -> StepF -> StepF := (@glue X).

Lemma StepF_ind : forall (P : StepF -> Prop),
       (forall x : X, P (constStepF x)) ->
       (forall (o : OpenUnit) (s : StepF),
        P s -> forall s0 : StepF, P s0 -> P (glue o s s0)) ->
       forall s : StepF, P s.

Definition StepFfold : forall Y, (X -> Y) -> (OpenUnit -> Y -> Y -> Y) -> StepF -> Y := (@StepFfold X).
Definition Mirror : StepF -> StepF := (@Mirror X).
Definition SplitL : StepF -> OpenUnit -> StepF := (@SplitL X).
Definition SplitR : StepF -> OpenUnit -> StepF := (@SplitR X).
End StepF_Functions.


We lift ap to the setoid version. Map is a notation calling ap so that all lemmas about ap automatically apply to ap
Definition Ap (X Y:Setoid) : (StepF (X --> Y))->(StepF X)->(StepF Y) := fun f x => (@Ap X Y (StepFunction.Map (@evalMorphism X Y) f) x).
Notation "f <@> x" := (Ap f x) (at level 15, left associativity) : sfstscope.
Notation "f ^@> x" := (Ap (constStepF f) x) (at level 15, left associativity) : sfstscope.
Notation "f <@^ x" := (Ap f (constStepF x)) (at level 15, left associativity) : sfstscope.


We lift lemmas about map, ap, mirror, and glue
Lemma MirrorGlue : forall (X : Setoid) (o : OpenUnit) (al ar : StepF X),
       Mirror (glue o al ar) = glue (OpenUnitDual o) (Mirror ar) (Mirror al).

Lemma MapGlue : forall (X Y : Setoid) (f : (X --> Y))
         (o : OpenUnit) (al ar : StepF X),
       f ^@> (glue o al ar) = glue o (f ^@> al) (f ^@> ar).

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

Lemma ApGlueGlue : forall (X Y : Setoid) (fl fr : StepF (X --> Y)) (o : OpenUnit) (l r : StepF X),
       (glue o fl fr) <@> (glue o l r) = glue o (fl <@> l) (fr <@> r).

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

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

Lemma SplitLR_glue_ind : forall (X : Setoid) (s1 s2 : StepF X) (a b : OpenUnit)
         (P : StepF X -> StepF X -> 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 (X : Setoid) (s1 s2 : StepF X) (a b : OpenUnit)
         (P : StepF X -> 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 (X : Setoid) (s1 s2 : StepF X) (a b : OpenUnit)
         (P : StepF X -> 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 SplitLMap : forall (X Y : Setoid) (x : StepF X) (a : OpenUnit) (f : X --> Y),
       SplitL (f ^@> x) a = f ^@> (SplitL x a).

Lemma SplitRMap : forall (X Y : Setoid) (x : StepF X) (a : OpenUnit) (f : X --> Y),
       SplitR (f ^@> x) a = f ^@> (SplitR x a).

Section EquivalenceA.
Variable X:Setoid.
A step function over Prop, a characteristic function, can be folded into Prop, which holds for the always true characteristic function
Definition StepFfoldProp : StepF iffSetoid -> Prop := (StepFfold (X:=iffSetoid) (fun x => x ) (fun _ a b => a /\ b )).

Definition st_eqS0 : X -> X --> iffSetoid.
Defined.

Definition st_eqS : X --> X --> iffSetoid.
Defined.

Equivalence

An equivalence relation on step functions is implemented by lifiting the equivalence relation on the underlying setoid to step functions. The results is a characteristic function saying where two step functions are equivalent. The step functions are considered equivalent if this characteristic function says they are equivalent everywhere.
Definition StepF_eq (f g:StepF X):Prop:=
(StepFfoldProp (st_eqS ^@> f <@> g)).

Notation "x === y" := (StepF_eq x y) (at level 70).

With equality defined we can complete the proof that split is the opposite of glue
Lemma glue_StepF_eq:forall (s:StepF X) (s1 s2:StepF X), forall a, s1 === (SplitL s a) -> s2 === (SplitR s a) -> (glue a s1 s2) === s.

Lemma glue_eq_ind : forall (s1 s2 s:StepF X) a (P:Prop), (s1 === SplitL s a -> s2 === SplitR s a -> P) -> (glue a s1 s2 === s) -> P.
The equivalence relation is reflexive
Lemma StepF_eq_refl:forall x : StepF X, x === x.
StepF_Qeq is a refinement of any setoid equality
Lemma StepF_Qeq_eq : forall (s t:StepF X), (StepF_Qeq s t) -> s === t.

Lemma glueSplit:forall (s : StepF X), forall a, (glue a (SplitL s a) (SplitR s a)) === s.

End EquivalenceA.
Notation "x == y" := (StepF_eq x y) (at level 70) : sfstscope.

Section EquivalenceB.
Variable X Y:Setoid.

Lemma Map_resp_StepF_eq: forall f:X-->Y,
    (forall x y, (st_eq x y)-> (st_eq (f x) (f y))) ->
    forall s t:(StepF X), s == t -> (f ^@> s) == (f ^@> t).



End EquivalenceB.

Lemma StepFfoldPropglue:forall (y:StepF iffSetoid) o,
 StepFfoldProp (glue o (SplitL y o) (SplitR y o)) <-> StepFfoldProp y.

Lemma StepFfoldProp_morphism:forall x y:(StepF iffSetoid),
  (StepF_eq x y) ->
  ((StepFfoldProp x)<->(StepFfoldProp y)).



Lemma StepFfoldPropSplitR
     : forall (s : StepF iffSetoid) (a : OpenUnit),
       StepFfoldProp s -> StepFfoldProp (SplitR s a).

Lemma StepFfoldPropSplitL
     : forall (s : StepF iffSetoid) (a : OpenUnit),
       StepFfoldProp s -> StepFfoldProp (SplitL s a).

Section EquivalenceC.

Variable X:Setoid.
Lemma StepF_eq_resp_Qeq : forall (s t : StepF X) u v, (StepF_Qeq s t) -> (StepF_Qeq u v) -> s == u -> t == v.

Lemma Mirror_eq_Mirror : forall (s t : StepF X), Mirror s == Mirror t <-> s == t.

Lemma SplitL_resp_Xeq : forall (s1 s2 : StepF X) a, s1 == s2 -> SplitL s1 a == SplitL s2 a.

Lemma SplitR_resp_Xeq : forall (s1 s2:StepF X) a, s1 == s2 -> SplitR s1 a == SplitR s2 a.

equalitiy is transitive
Lemma StepF_eq_trans:forall x y z : StepF X, x == y -> y == z -> x == z.


Lemma glue_resp_StepF_eq:forall (x x' y y':StepF X) o,
  (x==x')->(y==y')->
  (glue o x y)==(glue o x' y').

equality is symmetric
Lemma StepF_eq_sym :forall x y: StepF X, x == y -> y == x.




End EquivalenceC.
Lemma StepF_Sth (X:Setoid) : (Setoid_Theory (StepF X) (@StepF_eq X)).

Common subdivision view

This lemma allows to do induction over two step function as if the functions had the same subdivisions.
Lemma StepF_ind2 : forall (X Y : Setoid) (P : StepF X -> StepF Y -> Prop),
       (forall (s s0 : StepF X) (t t0 : StepF Y),
        (s==s0) -> (t==t0) -> P s t -> P s0 t0) ->
       (forall (x:X) (y:Y), P (constStepF x) (constStepF y)) ->
       (forall (o : OpenUnit) (s s0 : StepF X) (t t0 : StepF Y),
        P s t -> P s0 t0 -> P (glue o s s0) (glue o t t0)) ->
       forall (s:StepF X) (t:StepF Y), P s t.

Lemma glue_injl X :forall o (x y x1 y1:StepF X),
(glue o x y)==(glue o x1 y1) -> (x==x1).

Lemma glue_injr X :forall o (x y x1 y1:StepF X),
(glue o x y)==(glue o x1 y1) -> (y==y1).

Decompose an equality over glue into two parts
Lemma eq_glue_ind X : forall (s1 s2 s : StepF X) (a : OpenUnit) (P : Prop),
       ((SplitL s a) == s1 -> (SplitR s a) == s2 -> P) ->
       s == (glue a s1 s2) -> P.

Lemma MirrorSplitR X : forall (s : StepF X) (a b : OpenUnit),
  (b == OpenUnitDual a)%Q ->
  (Mirror (SplitR s a)) == (SplitL (Mirror s) b).

Lemma MirrorSplitL X : forall (s : StepF X) (a b : OpenUnit),
  (b == OpenUnitDual a)%Q ->
  (Mirror (SplitL s a)) == (SplitR (Mirror s) b).

Lift the distribution lemmas between ap and split to work over step functions
Lemma SplitRAp :forall (X Y:Setoid) (f : StepF (Y --> X)) (s : StepF Y) (o : OpenUnit),
  (SplitR (f <@> s) o) == (SplitR f o <@> SplitR s o).

Lemma SplitLAp :forall (X Y:Setoid) (f : StepF (Y --> X)) (s : StepF Y) (o : OpenUnit),
  (SplitL (f <@> s) o) == (SplitL f o <@> SplitL s o).
Lemma GlueAp : forall (X Y : Setoid) (f : StepF (X --> Y)) (o : OpenUnit) (l r : StepF X),
       f <@> (glue o l r) == glue o ((SplitL f o) <@> l) ((SplitR f o) <@> r).

Applicative Functor

Here we prove the axioms of an applicative functor.
Lemma Map_homomorphism (X Y:Setoid) : forall (f:X-->Y) (a:X),
 (f ^@> constStepF a) == (constStepF (f a)).

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

Lemma Map_composition X Y Z: forall (a:StepF (Y-->Z)) (b:StepF (X-->Y)) (c:StepF X),
 ((@compose X Y Z) ^@> a <@> b <@> c) == (a <@> (b <@> c)).

Here we show that the rest of the BCKW combinators lift to step functions. Hence all of the lambda calculus lifts to operate over step functions. Step functions form about a nice of an applicative functor as is possible.
Lemma Map_discardable X Y : forall (a:StepF X) (b:StepF Y),
 ((@const _ _) ^@> a <@> b == a).

Lemma Map_commutative W X Y : forall (f:StepF (W --> X --> Y)) (x:StepF X) (w:StepF W),
 ((@flip _ _ _) ^@> f <@> x <@> w) == (f <@> w <@> x).

Lemma Map_copyable X Y : forall (f:StepF (X --> X --> Y)) (x:StepF X),
 ((@join _ _) ^@> f <@> x) == (f <@> x <@> x).
This tactic is usefully for symbolically evaluating functions written in (BCKWI) combinator form that are ap'ed to step functions

Lemma Ap_interchange (X Y:Setoid) : forall (f:StepF (X-->Y)) (a:X),
 (f <@^ a) == (flip id a) ^@> f.

Map'ing the S combinator (which is also called ap)
Lemma Map_ap X Y Z : forall (f:StepF (X --> Y --> Z)) (x:StepF (X --> Y)) (a:StepF X),
 ((@ap _ _ _) ^@> f <@> x <@> a) == (f <@> a <@> (x <@> a)).

Lemma StepFfoldPropForall_Ap :
 forall X (f:StepF (X --> iffSetoid)) (x:StepF X), (forall y, StepFfoldProp (f <@> constStepF y)) -> StepFfoldProp (f <@> x).

A common case that we will encounter is that a predicate holds for all step functions when it is define via map (or map2 or map3) and the underlying function holds for all X.
Lemma StepFfoldPropForall_Map :
 forall X (f:X --> iffSetoid) (x:StepF X), (forall a, f a) -> StepFfoldProp (f ^@> x).

Lemma StepFfoldPropForall_Map2 :
 forall X Y (f:X --> Y --> iffSetoid) x y, (forall a b, f a b) -> StepFfoldProp (f ^@> x <@> y).

Lemma StepFfoldPropForall_Map3 :
 forall X Y Z (f:X --> Y --> Z --> iffSetoid) x y z, (forall a b c, f a b c) -> StepFfoldProp (f ^@> x <@> y <@> z).

The implication operation can be lifted to work on characteristic functions
Definition imp0:Prop->iffSetoid-->iffSetoid.
Defined.

Definition imp:iffSetoid-->iffSetoid-->iffSetoid.
Defined.

Definition StepF_imp (f g:StepF iffSetoid):Prop:=
(StepFfoldProp (imp ^@> f <@> g)).

Lemma StepFfoldPropglue_rew:(forall o x y, (StepFfoldProp (glue o x y))<->((StepFfoldProp x)/\StepFfoldProp y)).
Lemma StepF_imp_imp:forall x y:(StepF iffSetoid),
  (StepF_imp x y) ->
  ((StepFfoldProp x)->(StepFfoldProp y)).