CoRN.metric2.StepFunctionSetoid
Require Export RSetoid.
Require Export StepFunction.
Require Import OpenUnit.
Require Import CornTac.
Require Import Qauto.
Require Import Qordfield.
Require Import COrdFields.
Set Implicit Arguments.
Set Automatic Introduction.
Open Local Scope Q_scope.
Section StepF_Functions.
Variable X : RSetoid.
Require Export StepFunction.
Require Import OpenUnit.
Require Import CornTac.
Require Import Qauto.
Require Import Qordfield.
Require Import COrdFields.
Set Implicit Arguments.
Set Automatic Introduction.
Open Local Scope Q_scope.
Section StepF_Functions.
Variable X : RSetoid.
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.
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 : ∀ (P : StepF → Prop),
(∀ x : X, P (constStepF x)) →
(∀ (o : OpenUnit) (s : StepF),
P s → ∀ s0 : StepF, P s0 → P (glue o s s0)) →
∀ s : StepF, P s.
Proof.
intros P H0 H1 s.
induction s.
apply H0.
apply H1; auto.
Qed.
Definition StepFfold : ∀ 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.
Open Local Scope setoid_scope.
Definition glue : OpenUnit → StepF → StepF → StepF := (@glue X).
Lemma StepF_ind : ∀ (P : StepF → Prop),
(∀ x : X, P (constStepF x)) →
(∀ (o : OpenUnit) (s : StepF),
P s → ∀ s0 : StepF, P s0 → P (glue o s s0)) →
∀ s : StepF, P s.
Proof.
intros P H0 H1 s.
induction s.
apply H0.
apply H1; auto.
Qed.
Definition StepFfold : ∀ 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.
Open Local Scope setoid_scope.
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 : RSetoid) : (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.
Open Local Scope sfstscope.
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.
Open Local Scope sfstscope.
We lift lemmas about map, ap, mirror, and glue
Lemma MirrorGlue : ∀ (X : RSetoid) (o : OpenUnit) (al ar : StepF X),
Mirror (glue o al ar) = glue (OpenUnitDual o) (Mirror ar) (Mirror al).
Proof.
reflexivity.
Qed.
Lemma MapGlue : ∀ (X Y : RSetoid) (f : (X --> Y))
(o : OpenUnit) (al ar : StepF X),
f ^@> (glue o al ar) = glue o (f ^@> al) (f ^@> ar).
Proof.
reflexivity.
Qed.
Lemma ApGlue : ∀ (X Y : RSetoid) (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)).
Proof.
intros X Y fl fr o b.
unfold Ap.
simpl (StepFunction.Map (@evalMorphism X Y) (glue o fl fr)).
rewrite ApGlue.
reflexivity.
Qed.
Lemma ApGlueGlue : ∀ (X Y : RSetoid) (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).
Proof.
intros X Y fl fr o l r.
unfold Ap.
simpl (StepFunction.Map (@evalMorphism X Y) (glue o fl fr)).
unfold glue.
rewrite ApGlueGlue.
reflexivity.
Qed.
Lemma SplitLGlue : ∀ (X : RSetoid) (x y : StepF X) (o : OpenUnit),
SplitL (glue o x y) o = x.
Proof.
intros X.
exact (@SplitLGlue X).
Qed.
Lemma SplitRGlue : ∀ (X : RSetoid) (x y : StepF X) (o : OpenUnit),
SplitR (glue o x y) o = y.
Proof.
intros X.
exact (@SplitRGlue X).
Qed.
Lemma SplitLR_glue_ind : ∀ (X : RSetoid) (s1 s2 : StepF X) (a b : OpenUnit)
(P : StepF X → StepF X → Prop),
(∀ H : a < b,
P (SplitL s1 (OpenUnitDiv a b H)) (glue (OpenUnitDualDiv b a H) (SplitR s1 (OpenUnitDiv a b H)) s2)) →
(∀ 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).
Proof.
intros X.
exact (@SplitLR_glue_ind X).
Qed.
Lemma SplitL_glue_ind : ∀ (X : RSetoid) (s1 s2 : StepF X) (a b : OpenUnit)
(P : StepF X → Prop),
(∀ H : a < b, P (SplitL s1 (OpenUnitDiv a b H))) →
(∀ 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).
Proof.
intros X.
exact (@SplitL_glue_ind X).
Qed.
Lemma SplitR_glue_ind : ∀ (X : RSetoid) (s1 s2 : StepF X) (a b : OpenUnit)
(P : StepF X → Prop),
(∀ H : a < b, P (glue (OpenUnitDualDiv b a H) (SplitR s1 (OpenUnitDiv a b H)) s2)) →
(∀ H : b < a, P (SplitR s2 (OpenUnitDualDiv a b H))) →
(a == b → P s2) → P (SplitR (glue b s1 s2) a).
Proof.
intros X.
exact (@SplitR_glue_ind X).
Qed.
Lemma SplitLMap : ∀ (X Y : RSetoid) (x : StepF X) (a : OpenUnit) (f : X --> Y),
SplitL (f ^@> x) a = f ^@> (SplitL x a).
Proof.
intros X Y x a f.
unfold Ap, SplitL.
simpl.
rewrite SplitLMap.
reflexivity.
Qed.
Lemma SplitRMap : ∀ (X Y : RSetoid) (x : StepF X) (a : OpenUnit) (f : X --> Y),
SplitR (f ^@> x) a = f ^@> (SplitR x a).
Proof.
intros X Y x a f.
unfold Ap, SplitR.
simpl.
rewrite SplitRMap.
reflexivity.
Qed.
Section EquivalenceA.
Variable X : RSetoid.
Mirror (glue o al ar) = glue (OpenUnitDual o) (Mirror ar) (Mirror al).
Proof.
reflexivity.
Qed.
Lemma MapGlue : ∀ (X Y : RSetoid) (f : (X --> Y))
(o : OpenUnit) (al ar : StepF X),
f ^@> (glue o al ar) = glue o (f ^@> al) (f ^@> ar).
Proof.
reflexivity.
Qed.
Lemma ApGlue : ∀ (X Y : RSetoid) (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)).
Proof.
intros X Y fl fr o b.
unfold Ap.
simpl (StepFunction.Map (@evalMorphism X Y) (glue o fl fr)).
rewrite ApGlue.
reflexivity.
Qed.
Lemma ApGlueGlue : ∀ (X Y : RSetoid) (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).
Proof.
intros X Y fl fr o l r.
unfold Ap.
simpl (StepFunction.Map (@evalMorphism X Y) (glue o fl fr)).
unfold glue.
rewrite ApGlueGlue.
reflexivity.
Qed.
Lemma SplitLGlue : ∀ (X : RSetoid) (x y : StepF X) (o : OpenUnit),
SplitL (glue o x y) o = x.
Proof.
intros X.
exact (@SplitLGlue X).
Qed.
Lemma SplitRGlue : ∀ (X : RSetoid) (x y : StepF X) (o : OpenUnit),
SplitR (glue o x y) o = y.
Proof.
intros X.
exact (@SplitRGlue X).
Qed.
Lemma SplitLR_glue_ind : ∀ (X : RSetoid) (s1 s2 : StepF X) (a b : OpenUnit)
(P : StepF X → StepF X → Prop),
(∀ H : a < b,
P (SplitL s1 (OpenUnitDiv a b H)) (glue (OpenUnitDualDiv b a H) (SplitR s1 (OpenUnitDiv a b H)) s2)) →
(∀ 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).
Proof.
intros X.
exact (@SplitLR_glue_ind X).
Qed.
Lemma SplitL_glue_ind : ∀ (X : RSetoid) (s1 s2 : StepF X) (a b : OpenUnit)
(P : StepF X → Prop),
(∀ H : a < b, P (SplitL s1 (OpenUnitDiv a b H))) →
(∀ 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).
Proof.
intros X.
exact (@SplitL_glue_ind X).
Qed.
Lemma SplitR_glue_ind : ∀ (X : RSetoid) (s1 s2 : StepF X) (a b : OpenUnit)
(P : StepF X → Prop),
(∀ H : a < b, P (glue (OpenUnitDualDiv b a H) (SplitR s1 (OpenUnitDiv a b H)) s2)) →
(∀ H : b < a, P (SplitR s2 (OpenUnitDualDiv a b H))) →
(a == b → P s2) → P (SplitR (glue b s1 s2) a).
Proof.
intros X.
exact (@SplitR_glue_ind X).
Qed.
Lemma SplitLMap : ∀ (X Y : RSetoid) (x : StepF X) (a : OpenUnit) (f : X --> Y),
SplitL (f ^@> x) a = f ^@> (SplitL x a).
Proof.
intros X Y x a f.
unfold Ap, SplitL.
simpl.
rewrite SplitLMap.
reflexivity.
Qed.
Lemma SplitRMap : ∀ (X Y : RSetoid) (x : StepF X) (a : OpenUnit) (f : X --> Y),
SplitR (f ^@> x) a = f ^@> (SplitR x a).
Proof.
intros X Y x a f.
unfold Ap, SplitR.
simpl.
rewrite SplitRMap.
reflexivity.
Qed.
Section EquivalenceA.
Variable X : RSetoid.
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.
Proof.
intros x.
∃ (st_eq x).
abstract ( intros x1 x2 Hx; simpl; rewrite → Hx; reflexivity).
Defined.
Definition st_eqS : X --> X --> iffSetoid.
Proof.
∃ (st_eqS0).
abstract ( intros x1 x2 Hx y; simpl; rewrite → Hx; reflexivity).
Defined.
Definition st_eqS0 : X → X --> iffSetoid.
Proof.
intros x.
∃ (st_eq x).
abstract ( intros x1 x2 Hx; simpl; rewrite → Hx; reflexivity).
Defined.
Definition st_eqS : X --> X --> iffSetoid.
Proof.
∃ (st_eqS0).
abstract ( intros x1 x2 Hx y; simpl; rewrite → Hx; reflexivity).
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).
(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:∀ (s:StepF X) (s1 s2:StepF X), ∀ a, s1 === (SplitL s a) → s2 === (SplitR s a) → (glue a s1 s2) === s.
Proof.
intros s s1 s2 a H0 H1.
unfold StepF_eq.
rewrite MapGlue.
rewrite ApGlue.
split; assumption.
Qed.
Lemma glue_eq_ind : ∀ (s1 s2 s:StepF X) a (P:Prop), (s1 === SplitL s a → s2 === SplitR s a → P) → (glue a s1 s2 === s) → P.
Proof.
intros s1 s2 s a P H H0.
unfold StepF_eq in ×.
rewrite → MapGlue in ×.
rewrite ApGlue in H0.
destruct H0.
auto.
Qed.
Proof.
intros s s1 s2 a H0 H1.
unfold StepF_eq.
rewrite MapGlue.
rewrite ApGlue.
split; assumption.
Qed.
Lemma glue_eq_ind : ∀ (s1 s2 s:StepF X) a (P:Prop), (s1 === SplitL s a → s2 === SplitR s a → P) → (glue a s1 s2 === s) → P.
Proof.
intros s1 s2 s a P H H0.
unfold StepF_eq in ×.
rewrite → MapGlue in ×.
rewrite ApGlue in H0.
destruct H0.
auto.
Qed.
The equivalence relation is reflexive
Lemma StepF_eq_refl:∀ x : StepF X, x === x.
Proof.
induction x using StepF_ind.
change (st_eq x x).
reflexivity.
apply glue_StepF_eq.
simpl; rewrite SplitLGlue; assumption.
simpl; rewrite SplitRGlue; assumption.
Qed.
Proof.
induction x using StepF_ind.
change (st_eq x x).
reflexivity.
apply glue_StepF_eq.
simpl; rewrite SplitLGlue; assumption.
simpl; rewrite SplitRGlue; assumption.
Qed.
StepF_Qeq is a refinement of any setoid equality
Lemma StepF_Qeq_eq : ∀ (s t:StepF X), (StepF_Qeq s t) → s === t.
Proof.
induction s using StepF_ind; induction t using StepF_ind; try contradiction; simpl.
intros H.
rewrite H.
auto with ×.
intros [H [H0 H1]].
apply glue_StepF_eq.
apply IHs1.
apply SplitL_glue_ind; intros H2; try (elim (Qlt_not_le _ _ H2); rewrite → H); auto with ×.
apply IHs2.
apply SplitR_glue_ind; intros H2; try (elim (Qlt_not_le _ _ H2); rewrite → H); auto with ×.
Qed.
Lemma glueSplit:∀ (s : StepF X), ∀ a, (glue a (SplitL s a) (SplitR s a)) === s.
Proof.
intros s a.
apply glue_StepF_eq; auto with ×.
Qed.
End EquivalenceA.
Notation "x == y" := (StepF_eq x y) (at level 70) : sfstscope.
Section EquivalenceB.
Variable X Y : RSetoid.
Lemma Map_resp_StepF_eq: ∀ f:X-->Y,
(∀ x y, (st_eq x y)-> (st_eq (f x) (f y))) →
∀ s t:(StepF X), s == t → (f ^@> s) == (f ^@> t).
Proof.
intros f H.
induction s using StepF_ind. induction t using StepF_ind.
unfold StepF_eq, Map2, StepFfoldProp ;simpl;auto with ×.
unfold StepF_eq, Map2, StepFfoldProp. simpl; intuition.
intros t H0.
unfold StepF_eq, Map2 in H0.
rewrite MapGlue in H0.
rewrite ApGlue in H0.
unfold StepF_eq, Map2.
repeat rewrite MapGlue.
rewrite ApGlue.
rewrite SplitLMap.
rewrite SplitRMap.
destruct H0 as [H0l H0R].
split.
apply IHs1; auto.
apply IHs2; auto.
Qed.
End EquivalenceB.
Lemma StepFfoldPropglue:∀ (y:StepF iffSetoid) o,
StepFfoldProp (glue o (SplitL y o) (SplitR y o)) ↔ StepFfoldProp y.
Proof.
induction y using StepF_ind.
unfold StepF_eq, StepFfoldProp.
simpl; tauto.
simpl.
intro o0.
apply SplitLR_glue_ind; intros H.
generalize (IHy1 (OpenUnitDiv o0 o H)).
unfold StepFfoldProp; simpl; tauto.
generalize (IHy2 (OpenUnitDualDiv o0 o H)).
unfold StepFfoldProp; simpl; tauto.
simpl.
reflexivity.
Qed.
Lemma StepFfoldProp_morphism:∀ x y:(StepF iffSetoid),
(StepF_eq x y) →
((StepFfoldProp x)<->(StepFfoldProp y)).
Proof.
induction x using StepF_ind. induction y using StepF_ind.
auto with ×.
unfold StepF_eq. simpl. unfold StepFfoldProp;simpl;intuition.
intros y H0.
unfold StepF_eq, Map2 in H0.
rewrite MapGlue in H0.
rewrite ApGlue in H0.
destruct H0 as [H0l H0r].
change ((StepFfoldProp x1 ∧ StepFfoldProp x2) ↔ StepFfoldProp y).
rewrite → (IHx1 (SplitL y o)); auto with ×.
rewrite → (IHx2 (SplitR y o)); auto with ×.
apply: StepFfoldPropglue.
Qed.
Lemma StepFfoldPropSplitR
: ∀ (s : StepF iffSetoid) (a : OpenUnit),
StepFfoldProp s → StepFfoldProp (SplitR s a).
Proof.
intros s a H.
rewrite <- (StepFfoldPropglue s a) in H.
destruct H; auto.
Qed.
Lemma StepFfoldPropSplitL
: ∀ (s : StepF iffSetoid) (a : OpenUnit),
StepFfoldProp s → StepFfoldProp (SplitL s a).
Proof.
intros s a H.
rewrite <- (StepFfoldPropglue s a) in H.
destruct H; auto.
Qed.
Section EquivalenceC.
Variable X : RSetoid.
Lemma StepF_eq_resp_Qeq : ∀ (s t : StepF X) u v, (StepF_Qeq s t) → (StepF_Qeq u v) → s == u → t == v.
Proof.
induction s using StepF_ind; induction t using StepF_ind; try contradiction.
intros u v Hst Huv Hsu.
simpl in Hst.
unfold StepF_eq in ×.
rewrite <- Hst.
rewrite <- (StepFfoldProp_morphism ((st_eqS X) ^@> constStepF x <@> u)); auto.
apply: (Map_resp_StepF_eq); auto with ×.
intros a b Hab.
simpl.
rewrite → Hab.
reflexivity.
intros u v [H [Hst0 Hst1]] Huv Hsu.
destruct Hsu as [Hsu1 Hsu2] using (glue_eq_ind s1).
apply glue_StepF_eq.
eapply IHs1.
assumption.
unfold SplitL; apply SplitL_resp_Qeq.
apply H.
apply Huv.
assumption.
eapply IHs2.
assumption.
unfold SplitR; apply SplitR_resp_Qeq.
apply H.
apply Huv.
assumption.
Qed.
Lemma Mirror_eq_Mirror : ∀ (s t : StepF X), Mirror s == Mirror t ↔ s == t.
Proof.
induction s using StepF_ind.
induction t using StepF_ind; simpl.
reflexivity.
change (constStepF x == (Mirror t2) ∧ constStepF x == (Mirror t1) ↔ constStepF x == t1 ∧ constStepF x == t2).
tauto.
intros t.
rewrite MirrorGlue.
split; apply (@glue_eq_ind X); intros H0 H1.
apply glue_StepF_eq.
rewrite <- IHs1.
eapply StepF_eq_resp_Qeq;[| |apply H1]; auto with ×.
apply StepF_Qeq_sym.
apply MirrorSplitL_Qeq; auto with ×.
rewrite <- IHs2.
eapply StepF_eq_resp_Qeq;[| |apply H0]; auto with ×.
apply StepF_Qeq_sym.
apply MirrorSplitR_Qeq; auto with ×.
apply glue_StepF_eq.
apply StepF_eq_resp_Qeq with (Mirror s2) (Mirror (SplitR t o)); auto.
apply MirrorSplitR_Qeq; apply Qeq_refl.
rewrite → IHs2.
assumption.
apply StepF_eq_resp_Qeq with (Mirror s1) (Mirror (SplitL t o)); auto.
apply MirrorSplitL_Qeq; apply Qeq_refl.
rewrite → IHs1.
assumption.
Qed.
Lemma SplitL_resp_Xeq : ∀ (s1 s2 : StepF X) a, s1 == s2 → SplitL s1 a == SplitL s2 a.
Proof.
induction s1 using StepF_ind.
intros s2 a H.
unfold StepF_eq in ×.
change (StepFfoldProp ((st_eqS X x:X-->iffSetoid) ^@> SplitL s2 a)).
rewrite <- SplitLMap.
apply StepFfoldPropSplitL.
assumption.
intros s2 a H.
destruct H using (glue_eq_ind s1_1).
apply SplitL_glue_ind; intros Hao.
apply StepF_eq_resp_Qeq with (SplitL s1_1 (OpenUnitDiv a o Hao)) (SplitL (SplitL s2 o) (OpenUnitDiv a o Hao)); auto.
apply SplitLSplitL.
simpl; field; auto with ×.
apply glue_StepF_eq.
apply StepF_eq_resp_Qeq with s1_1 (SplitL s2 o); auto.
apply StepF_Qeq_sym.
apply SplitLSplitL.
simpl; field; auto with ×.
apply StepF_eq_resp_Qeq with (SplitL s1_2 (OpenUnitDualDiv a o Hao)) (SplitL (SplitR s2 o) (OpenUnitDualDiv a o Hao)); auto.
apply SplitLSplitR; simpl; field; auto with ×.
apply StepF_eq_resp_Qeq with s1_1 (SplitL s2 o); auto with ×.
apply SplitL_resp_Qeq; auto.
symmetry.
assumption.
Qed.
Lemma SplitR_resp_Xeq : ∀ (s1 s2:StepF X) a, s1 == s2 → SplitR s1 a == SplitR s2 a.
Proof.
intros s1 s2 a H.
pose (b:=OpenUnitDual a).
apply StepF_eq_resp_Qeq with (Mirror (SplitL (Mirror s1) b)) (Mirror (SplitL (Mirror s2) b));
try (unfold Mirror, SplitR, SplitL, b;eapply StepF_Qeq_trans;[apply Mirror_resp_Qeq; apply StepF_Qeq_sym; apply MirrorSplitR_Qeq; reflexivity|apply MirrorMirror]).
rewrite → Mirror_eq_Mirror.
apply SplitL_resp_Xeq.
rewrite → Mirror_eq_Mirror.
assumption.
Qed.
Proof.
induction s using StepF_ind; induction t using StepF_ind; try contradiction; simpl.
intros H.
rewrite H.
auto with ×.
intros [H [H0 H1]].
apply glue_StepF_eq.
apply IHs1.
apply SplitL_glue_ind; intros H2; try (elim (Qlt_not_le _ _ H2); rewrite → H); auto with ×.
apply IHs2.
apply SplitR_glue_ind; intros H2; try (elim (Qlt_not_le _ _ H2); rewrite → H); auto with ×.
Qed.
Lemma glueSplit:∀ (s : StepF X), ∀ a, (glue a (SplitL s a) (SplitR s a)) === s.
Proof.
intros s a.
apply glue_StepF_eq; auto with ×.
Qed.
End EquivalenceA.
Notation "x == y" := (StepF_eq x y) (at level 70) : sfstscope.
Section EquivalenceB.
Variable X Y : RSetoid.
Lemma Map_resp_StepF_eq: ∀ f:X-->Y,
(∀ x y, (st_eq x y)-> (st_eq (f x) (f y))) →
∀ s t:(StepF X), s == t → (f ^@> s) == (f ^@> t).
Proof.
intros f H.
induction s using StepF_ind. induction t using StepF_ind.
unfold StepF_eq, Map2, StepFfoldProp ;simpl;auto with ×.
unfold StepF_eq, Map2, StepFfoldProp. simpl; intuition.
intros t H0.
unfold StepF_eq, Map2 in H0.
rewrite MapGlue in H0.
rewrite ApGlue in H0.
unfold StepF_eq, Map2.
repeat rewrite MapGlue.
rewrite ApGlue.
rewrite SplitLMap.
rewrite SplitRMap.
destruct H0 as [H0l H0R].
split.
apply IHs1; auto.
apply IHs2; auto.
Qed.
End EquivalenceB.
Lemma StepFfoldPropglue:∀ (y:StepF iffSetoid) o,
StepFfoldProp (glue o (SplitL y o) (SplitR y o)) ↔ StepFfoldProp y.
Proof.
induction y using StepF_ind.
unfold StepF_eq, StepFfoldProp.
simpl; tauto.
simpl.
intro o0.
apply SplitLR_glue_ind; intros H.
generalize (IHy1 (OpenUnitDiv o0 o H)).
unfold StepFfoldProp; simpl; tauto.
generalize (IHy2 (OpenUnitDualDiv o0 o H)).
unfold StepFfoldProp; simpl; tauto.
simpl.
reflexivity.
Qed.
Lemma StepFfoldProp_morphism:∀ x y:(StepF iffSetoid),
(StepF_eq x y) →
((StepFfoldProp x)<->(StepFfoldProp y)).
Proof.
induction x using StepF_ind. induction y using StepF_ind.
auto with ×.
unfold StepF_eq. simpl. unfold StepFfoldProp;simpl;intuition.
intros y H0.
unfold StepF_eq, Map2 in H0.
rewrite MapGlue in H0.
rewrite ApGlue in H0.
destruct H0 as [H0l H0r].
change ((StepFfoldProp x1 ∧ StepFfoldProp x2) ↔ StepFfoldProp y).
rewrite → (IHx1 (SplitL y o)); auto with ×.
rewrite → (IHx2 (SplitR y o)); auto with ×.
apply: StepFfoldPropglue.
Qed.
Lemma StepFfoldPropSplitR
: ∀ (s : StepF iffSetoid) (a : OpenUnit),
StepFfoldProp s → StepFfoldProp (SplitR s a).
Proof.
intros s a H.
rewrite <- (StepFfoldPropglue s a) in H.
destruct H; auto.
Qed.
Lemma StepFfoldPropSplitL
: ∀ (s : StepF iffSetoid) (a : OpenUnit),
StepFfoldProp s → StepFfoldProp (SplitL s a).
Proof.
intros s a H.
rewrite <- (StepFfoldPropglue s a) in H.
destruct H; auto.
Qed.
Section EquivalenceC.
Variable X : RSetoid.
Lemma StepF_eq_resp_Qeq : ∀ (s t : StepF X) u v, (StepF_Qeq s t) → (StepF_Qeq u v) → s == u → t == v.
Proof.
induction s using StepF_ind; induction t using StepF_ind; try contradiction.
intros u v Hst Huv Hsu.
simpl in Hst.
unfold StepF_eq in ×.
rewrite <- Hst.
rewrite <- (StepFfoldProp_morphism ((st_eqS X) ^@> constStepF x <@> u)); auto.
apply: (Map_resp_StepF_eq); auto with ×.
intros a b Hab.
simpl.
rewrite → Hab.
reflexivity.
intros u v [H [Hst0 Hst1]] Huv Hsu.
destruct Hsu as [Hsu1 Hsu2] using (glue_eq_ind s1).
apply glue_StepF_eq.
eapply IHs1.
assumption.
unfold SplitL; apply SplitL_resp_Qeq.
apply H.
apply Huv.
assumption.
eapply IHs2.
assumption.
unfold SplitR; apply SplitR_resp_Qeq.
apply H.
apply Huv.
assumption.
Qed.
Lemma Mirror_eq_Mirror : ∀ (s t : StepF X), Mirror s == Mirror t ↔ s == t.
Proof.
induction s using StepF_ind.
induction t using StepF_ind; simpl.
reflexivity.
change (constStepF x == (Mirror t2) ∧ constStepF x == (Mirror t1) ↔ constStepF x == t1 ∧ constStepF x == t2).
tauto.
intros t.
rewrite MirrorGlue.
split; apply (@glue_eq_ind X); intros H0 H1.
apply glue_StepF_eq.
rewrite <- IHs1.
eapply StepF_eq_resp_Qeq;[| |apply H1]; auto with ×.
apply StepF_Qeq_sym.
apply MirrorSplitL_Qeq; auto with ×.
rewrite <- IHs2.
eapply StepF_eq_resp_Qeq;[| |apply H0]; auto with ×.
apply StepF_Qeq_sym.
apply MirrorSplitR_Qeq; auto with ×.
apply glue_StepF_eq.
apply StepF_eq_resp_Qeq with (Mirror s2) (Mirror (SplitR t o)); auto.
apply MirrorSplitR_Qeq; apply Qeq_refl.
rewrite → IHs2.
assumption.
apply StepF_eq_resp_Qeq with (Mirror s1) (Mirror (SplitL t o)); auto.
apply MirrorSplitL_Qeq; apply Qeq_refl.
rewrite → IHs1.
assumption.
Qed.
Lemma SplitL_resp_Xeq : ∀ (s1 s2 : StepF X) a, s1 == s2 → SplitL s1 a == SplitL s2 a.
Proof.
induction s1 using StepF_ind.
intros s2 a H.
unfold StepF_eq in ×.
change (StepFfoldProp ((st_eqS X x:X-->iffSetoid) ^@> SplitL s2 a)).
rewrite <- SplitLMap.
apply StepFfoldPropSplitL.
assumption.
intros s2 a H.
destruct H using (glue_eq_ind s1_1).
apply SplitL_glue_ind; intros Hao.
apply StepF_eq_resp_Qeq with (SplitL s1_1 (OpenUnitDiv a o Hao)) (SplitL (SplitL s2 o) (OpenUnitDiv a o Hao)); auto.
apply SplitLSplitL.
simpl; field; auto with ×.
apply glue_StepF_eq.
apply StepF_eq_resp_Qeq with s1_1 (SplitL s2 o); auto.
apply StepF_Qeq_sym.
apply SplitLSplitL.
simpl; field; auto with ×.
apply StepF_eq_resp_Qeq with (SplitL s1_2 (OpenUnitDualDiv a o Hao)) (SplitL (SplitR s2 o) (OpenUnitDualDiv a o Hao)); auto.
apply SplitLSplitR; simpl; field; auto with ×.
apply StepF_eq_resp_Qeq with s1_1 (SplitL s2 o); auto with ×.
apply SplitL_resp_Qeq; auto.
symmetry.
assumption.
Qed.
Lemma SplitR_resp_Xeq : ∀ (s1 s2:StepF X) a, s1 == s2 → SplitR s1 a == SplitR s2 a.
Proof.
intros s1 s2 a H.
pose (b:=OpenUnitDual a).
apply StepF_eq_resp_Qeq with (Mirror (SplitL (Mirror s1) b)) (Mirror (SplitL (Mirror s2) b));
try (unfold Mirror, SplitR, SplitL, b;eapply StepF_Qeq_trans;[apply Mirror_resp_Qeq; apply StepF_Qeq_sym; apply MirrorSplitR_Qeq; reflexivity|apply MirrorMirror]).
rewrite → Mirror_eq_Mirror.
apply SplitL_resp_Xeq.
rewrite → Mirror_eq_Mirror.
assumption.
Qed.
equalitiy is transitive
Lemma StepF_eq_trans:∀ x y z : StepF X, x == y → y == z → x == z.
Proof.
induction x using StepF_ind. intros.
unfold StepF_eq in ×.
set (A:=((st_eqS X:X-->X-->iffSetoid) ^@> constStepF x)) in ×.
rewrite <- (StepFfoldProp_morphism (A <@> y)); auto with ×.
apply: (Map_resp_StepF_eq); auto with ×.
intros a b Hab.
simpl.
rewrite → Hab.
reflexivity.
intros.
destruct H using (glue_eq_ind x1).
apply glue_StepF_eq.
eapply IHx1.
apply H.
apply SplitL_resp_Xeq.
assumption.
eapply IHx2.
apply H1.
apply SplitR_resp_Xeq.
assumption.
Qed.
Lemma glue_resp_StepF_eq:∀ (x x' y y':StepF X) o,
(x==x')->(y==y')->
(glue o x y)==(glue o x' y').
Proof.
intros.
unfold StepF_eq.
rewrite MapGlue.
rewrite ApGlueGlue.
split; assumption.
Qed.
Proof.
induction x using StepF_ind. intros.
unfold StepF_eq in ×.
set (A:=((st_eqS X:X-->X-->iffSetoid) ^@> constStepF x)) in ×.
rewrite <- (StepFfoldProp_morphism (A <@> y)); auto with ×.
apply: (Map_resp_StepF_eq); auto with ×.
intros a b Hab.
simpl.
rewrite → Hab.
reflexivity.
intros.
destruct H using (glue_eq_ind x1).
apply glue_StepF_eq.
eapply IHx1.
apply H.
apply SplitL_resp_Xeq.
assumption.
eapply IHx2.
apply H1.
apply SplitR_resp_Xeq.
assumption.
Qed.
Lemma glue_resp_StepF_eq:∀ (x x' y y':StepF X) o,
(x==x')->(y==y')->
(glue o x y)==(glue o x' y').
Proof.
intros.
unfold StepF_eq.
rewrite MapGlue.
rewrite ApGlueGlue.
split; assumption.
Qed.
equality is symmetric
Lemma StepF_eq_sym :∀ x y: StepF X, x == y → y == x.
Proof.
intros x y.
revert x.
induction y using StepF_ind.
unfold StepF_eq. simpl. intro x0. induction x0.
unfold StepFfoldProp. simpl. intros. symmetry; assumption.
simpl. unfold StepFfoldProp; simpl; intuition; auto with ×.
intros x H.
assert (H0:=(SplitL_resp_Xeq _ _ o H)).
rewrite SplitLGlue in H0.
assert (H1:=(SplitR_resp_Xeq _ _ o H)).
rewrite SplitRGlue in H1.
apply glue_StepF_eq;auto with ×.
Qed.
End EquivalenceC.
Lemma StepF_Sth (X : RSetoid) : (Setoid_Theory (StepF X) (@StepF_eq X)).
split; unfold Reflexive, Symmetric, Transitive; eauto with sfarith.
Qed.
Proof.
intros x y.
revert x.
induction y using StepF_ind.
unfold StepF_eq. simpl. intro x0. induction x0.
unfold StepFfoldProp. simpl. intros. symmetry; assumption.
simpl. unfold StepFfoldProp; simpl; intuition; auto with ×.
intros x H.
assert (H0:=(SplitL_resp_Xeq _ _ o H)).
rewrite SplitLGlue in H0.
assert (H1:=(SplitR_resp_Xeq _ _ o H)).
rewrite SplitRGlue in H1.
apply glue_StepF_eq;auto with ×.
Qed.
End EquivalenceC.
Lemma StepF_Sth (X : RSetoid) : (Setoid_Theory (StepF X) (@StepF_eq X)).
split; unfold Reflexive, Symmetric, Transitive; eauto with sfarith.
Qed.
Common subdivision view
This lemma allows to do induction over two step function as if the functions had the same subdivisions.
Lemma StepF_ind2 : ∀ (X Y : RSetoid) (P : StepF X → StepF Y → Prop),
(∀ (s s0 : StepF X) (t t0 : StepF Y),
(s==s0) → (t==t0) → P s t → P s0 t0) →
(∀ (x:X) (y:Y), P (constStepF x) (constStepF y)) →
(∀ (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)) →
∀ (s:StepF X) (t:StepF Y), P s t.
Proof.
intros X Y P wd c0 c1.
induction s using StepF_ind.
induction t using StepF_ind.
apply c0.
apply wd with (s:=(glue o (constStepF x) (constStepF x))) (t:=glue o t1 t2); try reflexivity.
apply (glueSplit (constStepF x) o).
apply c1; assumption.
intros t.
eapply wd.
reflexivity.
apply glueSplit with (a:=o).
apply c1; auto.
Qed.
Lemma glue_injl X :∀ o (x y x1 y1:StepF X),
(glue o x y)==(glue o x1 y1) → (x==x1).
Proof.
intros.
destruct H as [H _] using (glue_eq_ind x).
rewrite SplitLGlue in H.
assumption.
Qed.
Lemma glue_injr X :∀ o (x y x1 y1:StepF X),
(glue o x y)==(glue o x1 y1) → (y==y1).
Proof.
intros.
destruct H as [_ H] using (glue_eq_ind x).
rewrite SplitRGlue in H.
assumption.
Qed.
(∀ (s s0 : StepF X) (t t0 : StepF Y),
(s==s0) → (t==t0) → P s t → P s0 t0) →
(∀ (x:X) (y:Y), P (constStepF x) (constStepF y)) →
(∀ (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)) →
∀ (s:StepF X) (t:StepF Y), P s t.
Proof.
intros X Y P wd c0 c1.
induction s using StepF_ind.
induction t using StepF_ind.
apply c0.
apply wd with (s:=(glue o (constStepF x) (constStepF x))) (t:=glue o t1 t2); try reflexivity.
apply (glueSplit (constStepF x) o).
apply c1; assumption.
intros t.
eapply wd.
reflexivity.
apply glueSplit with (a:=o).
apply c1; auto.
Qed.
Lemma glue_injl X :∀ o (x y x1 y1:StepF X),
(glue o x y)==(glue o x1 y1) → (x==x1).
Proof.
intros.
destruct H as [H _] using (glue_eq_ind x).
rewrite SplitLGlue in H.
assumption.
Qed.
Lemma glue_injr X :∀ o (x y x1 y1:StepF X),
(glue o x y)==(glue o x1 y1) → (y==y1).
Proof.
intros.
destruct H as [_ H] using (glue_eq_ind x).
rewrite SplitRGlue in H.
assumption.
Qed.
Decompose an equality over glue into two parts
Lemma eq_glue_ind X : ∀ (s1 s2 s : StepF X) (a : OpenUnit) (P : Prop),
((SplitL s a) == s1 → (SplitR s a) == s2 → P) →
s == (glue a s1 s2) → P.
Proof.
intros s1 s2 s a P H H0.
symmetry in H0.
destruct H0 as [H0l H0r] using (glue_eq_ind s1).
symmetry in H0l, H0r.
auto.
Qed.
Lemma MirrorSplitR X : ∀ (s : StepF X) (a b : OpenUnit),
(b == OpenUnitDual a)%Q →
(Mirror (SplitR s a)) == (SplitL (Mirror s) b).
Proof.
intros.
apply StepF_Qeq_eq; auto with ×.
apply MirrorSplitR_Qeq; auto with ×.
Qed.
Lemma MirrorSplitL X : ∀ (s : StepF X) (a b : OpenUnit),
(b == OpenUnitDual a)%Q →
(Mirror (SplitL s a)) == (SplitR (Mirror s) b).
Proof.
intros.
apply StepF_Qeq_eq; auto with ×.
apply MirrorSplitL_Qeq; auto with ×.
Qed.
((SplitL s a) == s1 → (SplitR s a) == s2 → P) →
s == (glue a s1 s2) → P.
Proof.
intros s1 s2 s a P H H0.
symmetry in H0.
destruct H0 as [H0l H0r] using (glue_eq_ind s1).
symmetry in H0l, H0r.
auto.
Qed.
Lemma MirrorSplitR X : ∀ (s : StepF X) (a b : OpenUnit),
(b == OpenUnitDual a)%Q →
(Mirror (SplitR s a)) == (SplitL (Mirror s) b).
Proof.
intros.
apply StepF_Qeq_eq; auto with ×.
apply MirrorSplitR_Qeq; auto with ×.
Qed.
Lemma MirrorSplitL X : ∀ (s : StepF X) (a b : OpenUnit),
(b == OpenUnitDual a)%Q →
(Mirror (SplitL s a)) == (SplitR (Mirror s) b).
Proof.
intros.
apply StepF_Qeq_eq; auto with ×.
apply MirrorSplitL_Qeq; auto with ×.
Qed.
Lift the distribution lemmas between ap and split to work over step
functions
Lemma SplitRAp :∀ (X Y : RSetoid) (f : StepF (Y --> X)) (s : StepF Y) (o : OpenUnit),
(SplitR (f <@> s) o) == (SplitR f o <@> SplitR s o).
Proof.
intros X Y f s o.
apply StepF_Qeq_eq; auto with ×.
unfold Ap, SplitR.
rewrite <- StepFunction.SplitRMap.
apply SplitRAp_Qeq.
Qed.
Lemma SplitLAp :∀ (X Y : RSetoid) (f : StepF (Y --> X)) (s : StepF Y) (o : OpenUnit),
(SplitL (f <@> s) o) == (SplitL f o <@> SplitL s o).
Proof.
intros X Y f s o.
apply StepF_Qeq_eq; auto with ×.
unfold Ap, SplitL.
rewrite <- StepFunction.SplitLMap.
apply SplitLAp_Qeq.
Qed.
Lemma GlueAp : ∀ (X Y : RSetoid) (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).
Proof.
intros X Y f o l r.
set (A:= ((SplitL f o)<@>l)).
set (B:= ((SplitR f o)<@>r)).
rewrite <- (glueSplit f o).
rewrite ApGlueGlue.
reflexivity.
Qed.
(SplitR (f <@> s) o) == (SplitR f o <@> SplitR s o).
Proof.
intros X Y f s o.
apply StepF_Qeq_eq; auto with ×.
unfold Ap, SplitR.
rewrite <- StepFunction.SplitRMap.
apply SplitRAp_Qeq.
Qed.
Lemma SplitLAp :∀ (X Y : RSetoid) (f : StepF (Y --> X)) (s : StepF Y) (o : OpenUnit),
(SplitL (f <@> s) o) == (SplitL f o <@> SplitL s o).
Proof.
intros X Y f s o.
apply StepF_Qeq_eq; auto with ×.
unfold Ap, SplitL.
rewrite <- StepFunction.SplitLMap.
apply SplitLAp_Qeq.
Qed.
Lemma GlueAp : ∀ (X Y : RSetoid) (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).
Proof.
intros X Y f o l r.
set (A:= ((SplitL f o)<@>l)).
set (B:= ((SplitR f o)<@>r)).
rewrite <- (glueSplit f o).
rewrite ApGlueGlue.
reflexivity.
Qed.
Lemma Map_homomorphism (X Y : RSetoid) : ∀ (f:X-->Y) (a:X),
(f ^@> constStepF a) == (constStepF (f a)).
Proof.
reflexivity.
Qed.
Lemma Map_identity X : ∀ (a:StepF X),
(@id X) ^@> a == a.
Proof.
intros a.
now rewrite <-(Map_identity a) at 2.
Qed.
Lemma Map_composition X Y Z: ∀ (a:StepF (Y-->Z)) (b:StepF (X-->Y)) (c:StepF X),
((@compose X Y Z) ^@> a <@> b <@> c) == (a <@> (b <@> c)).
Proof.
induction a using StepF_ind.
simpl.
apply StepF_ind2; auto with ×.
intros s s0 t t0 Hs Ht.
rewrite → Hs, Ht.
auto.
intros o s s0 t t0 H H0.
rewrite → Map_homomorphism.
rewrite ApGlueGlue.
do 2 rewrite MapGlue.
rewrite ApGlueGlue.
rewrite <- H.
rewrite <- H0.
reflexivity.
intros b c.
rewrite MapGlue.
repeat rewrite ApGlue.
apply glue_resp_StepF_eq.
rewrite → IHa1.
rewrite → SplitLAp.
reflexivity.
rewrite → IHa2.
rewrite → SplitRAp.
reflexivity.
Qed.
(f ^@> constStepF a) == (constStepF (f a)).
Proof.
reflexivity.
Qed.
Lemma Map_identity X : ∀ (a:StepF X),
(@id X) ^@> a == a.
Proof.
intros a.
now rewrite <-(Map_identity a) at 2.
Qed.
Lemma Map_composition X Y Z: ∀ (a:StepF (Y-->Z)) (b:StepF (X-->Y)) (c:StepF X),
((@compose X Y Z) ^@> a <@> b <@> c) == (a <@> (b <@> c)).
Proof.
induction a using StepF_ind.
simpl.
apply StepF_ind2; auto with ×.
intros s s0 t t0 Hs Ht.
rewrite → Hs, Ht.
auto.
intros o s s0 t t0 H H0.
rewrite → Map_homomorphism.
rewrite ApGlueGlue.
do 2 rewrite MapGlue.
rewrite ApGlueGlue.
rewrite <- H.
rewrite <- H0.
reflexivity.
intros b c.
rewrite MapGlue.
repeat rewrite ApGlue.
apply glue_resp_StepF_eq.
rewrite → IHa1.
rewrite → SplitLAp.
reflexivity.
rewrite → IHa2.
rewrite → SplitRAp.
reflexivity.
Qed.
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 : ∀ (a:StepF X) (b:StepF Y),
((@const _ _) ^@> a <@> b == a).
Proof.
apply StepF_ind2; auto with ×.
intros s s0 t t0 Hs Ht.
rewrite → Hs, Ht; auto.
intros o s s0 t t0 H0 H1.
rewrite MapGlue.
rewrite ApGlueGlue.
rewrite → H0, H1;reflexivity.
Qed.
Lemma Map_commutative W X Y : ∀ (f:StepF (W --> X --> Y)) (x:StepF X) (w:StepF W),
((@flip _ _ _) ^@> f <@> x <@> w) == (f <@> w <@> x).
Proof.
induction f using StepF_ind.
simpl.
apply StepF_ind2; auto with ×.
intros s s0 t t0 Hs Ht.
rewrite → Hs, Ht;auto.
intros o s s0 t t0 H0 H1.
rewrite → Map_homomorphism.
do 2 rewrite MapGlue.
do 2 rewrite ApGlueGlue.
rewrite → H0, H1; reflexivity.
intros x w.
rewrite MapGlue.
do 4 rewrite ApGlue.
apply glue_resp_StepF_eq; auto.
Qed.
Lemma Map_copyable X Y : ∀ (f:StepF (X --> X --> Y)) (x:StepF X),
((@join _ _) ^@> f <@> x) == (f <@> x <@> x).
Proof.
apply StepF_ind2; auto with ×.
intros s s0 t t0 Hs Ht.
rewrite → Hs, Ht; auto.
intros o s s0 t t0 H0 H1.
rewrite MapGlue.
do 3 rewrite ApGlueGlue.
rewrite → H0, H1;reflexivity.
Qed.
((@const _ _) ^@> a <@> b == a).
Proof.
apply StepF_ind2; auto with ×.
intros s s0 t t0 Hs Ht.
rewrite → Hs, Ht; auto.
intros o s s0 t t0 H0 H1.
rewrite MapGlue.
rewrite ApGlueGlue.
rewrite → H0, H1;reflexivity.
Qed.
Lemma Map_commutative W X Y : ∀ (f:StepF (W --> X --> Y)) (x:StepF X) (w:StepF W),
((@flip _ _ _) ^@> f <@> x <@> w) == (f <@> w <@> x).
Proof.
induction f using StepF_ind.
simpl.
apply StepF_ind2; auto with ×.
intros s s0 t t0 Hs Ht.
rewrite → Hs, Ht;auto.
intros o s s0 t t0 H0 H1.
rewrite → Map_homomorphism.
do 2 rewrite MapGlue.
do 2 rewrite ApGlueGlue.
rewrite → H0, H1; reflexivity.
intros x w.
rewrite MapGlue.
do 4 rewrite ApGlue.
apply glue_resp_StepF_eq; auto.
Qed.
Lemma Map_copyable X Y : ∀ (f:StepF (X --> X --> Y)) (x:StepF X),
((@join _ _) ^@> f <@> x) == (f <@> x <@> x).
Proof.
apply StepF_ind2; auto with ×.
intros s s0 t t0 Hs Ht.
rewrite → Hs, Ht; auto.
intros o s s0 t t0 H0 H1.
rewrite MapGlue.
do 3 rewrite ApGlueGlue.
rewrite → H0, H1;reflexivity.
Qed.
This tactic is usefully for symbolically evaluating functions written
in (BCKWI) combinator form that are ap'ed to step functions
Ltac evalStepF := progress
(repeat rewrite <- Map_homomorphism; autorewrite with StepF_eval).
Lemma Ap_interchange (X Y : RSetoid) : ∀ (f:StepF (X-->Y)) (a:X),
(f <@^ a) == (flip id a) ^@> f.
Proof.
intros f a.
evalStepF.
reflexivity.
Qed.
(repeat rewrite <- Map_homomorphism; autorewrite with StepF_eval).
Lemma Ap_interchange (X Y : RSetoid) : ∀ (f:StepF (X-->Y)) (a:X),
(f <@^ a) == (flip id a) ^@> f.
Proof.
intros f a.
evalStepF.
reflexivity.
Qed.
Map'ing the S combinator (which is also called ap)
Lemma Map_ap X Y Z : ∀ (f:StepF (X --> Y --> Z)) (x:StepF (X --> Y)) (a:StepF X),
((@ap _ _ _) ^@> f <@> x <@> a) == (f <@> a <@> (x <@> a)).
Proof.
intros f x a.
unfold ap.
evalStepF.
reflexivity.
Qed.
Ltac rewriteStepF := autorewrite with StepF_rew.
Lemma StepFfoldPropForall_Ap :
∀ X (f:StepF (X --> iffSetoid)) (x:StepF X), (∀ y, StepFfoldProp (f <@> constStepF y)) → StepFfoldProp (f <@> x).
Proof.
intros X f x H.
revert f H.
induction x using StepF_ind.
intros f H.
apply H.
intros f H.
rewrite <- (glueSplit f o).
rewrite ApGlueGlue.
split.
apply IHx1.
intros y.
assert (H0:=H y).
rewrite <- (glueSplit f o) in H0.
rewrite ApGlue in H0.
destruct H0 as [H0 _].
assumption.
apply IHx2.
intros y.
assert (H0:=H y).
rewrite <- (glueSplit f o) in H0.
rewrite ApGlue in H0.
destruct H0 as [_ H0].
assumption.
Qed.
((@ap _ _ _) ^@> f <@> x <@> a) == (f <@> a <@> (x <@> a)).
Proof.
intros f x a.
unfold ap.
evalStepF.
reflexivity.
Qed.
Ltac rewriteStepF := autorewrite with StepF_rew.
Lemma StepFfoldPropForall_Ap :
∀ X (f:StepF (X --> iffSetoid)) (x:StepF X), (∀ y, StepFfoldProp (f <@> constStepF y)) → StepFfoldProp (f <@> x).
Proof.
intros X f x H.
revert f H.
induction x using StepF_ind.
intros f H.
apply H.
intros f H.
rewrite <- (glueSplit f o).
rewrite ApGlueGlue.
split.
apply IHx1.
intros y.
assert (H0:=H y).
rewrite <- (glueSplit f o) in H0.
rewrite ApGlue in H0.
destruct H0 as [H0 _].
assumption.
apply IHx2.
intros y.
assert (H0:=H y).
rewrite <- (glueSplit f o) in H0.
rewrite ApGlue in H0.
destruct H0 as [_ H0].
assumption.
Qed.
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 :
∀ X (f:X --> iffSetoid) (x:StepF X), (∀ a, f a) → StepFfoldProp (f ^@> x).
Proof.
intros X f x H.
apply StepFfoldPropForall_Ap.
assumption.
Qed.
Lemma StepFfoldPropForall_Map2 :
∀ X Y (f:X --> Y --> iffSetoid) x y, (∀ a b, f a b) → StepFfoldProp (f ^@> x <@> y).
Proof.
intros X Y f x y H.
apply StepFfoldPropForall_Ap.
intros b.
rewrite <- (Map_commutative (constStepF f) (constStepF b)).
rewriteStepF.
apply StepFfoldPropForall_Map.
intros a.
apply: H.
Qed.
Lemma StepFfoldPropForall_Map3 :
∀ X Y Z (f:X --> Y --> Z --> iffSetoid) x y z, (∀ a b c, f a b c) → StepFfoldProp (f ^@> x <@> y <@> z).
Proof.
intros X Y Z f x y z H.
apply StepFfoldPropForall_Ap.
intros c.
rewrite <- (Map_commutative ((constStepF f) <@> x) (constStepF c)).
rewrite <- Map_composition.
rewriteStepF.
rewrite <- (Map_commutative (constStepF (compose flip f)) (constStepF c)).
rewriteStepF.
apply StepFfoldPropForall_Map2.
intros a b.
apply: H.
Qed.
∀ X (f:X --> iffSetoid) (x:StepF X), (∀ a, f a) → StepFfoldProp (f ^@> x).
Proof.
intros X f x H.
apply StepFfoldPropForall_Ap.
assumption.
Qed.
Lemma StepFfoldPropForall_Map2 :
∀ X Y (f:X --> Y --> iffSetoid) x y, (∀ a b, f a b) → StepFfoldProp (f ^@> x <@> y).
Proof.
intros X Y f x y H.
apply StepFfoldPropForall_Ap.
intros b.
rewrite <- (Map_commutative (constStepF f) (constStepF b)).
rewriteStepF.
apply StepFfoldPropForall_Map.
intros a.
apply: H.
Qed.
Lemma StepFfoldPropForall_Map3 :
∀ X Y Z (f:X --> Y --> Z --> iffSetoid) x y z, (∀ a b c, f a b c) → StepFfoldProp (f ^@> x <@> y <@> z).
Proof.
intros X Y Z f x y z H.
apply StepFfoldPropForall_Ap.
intros c.
rewrite <- (Map_commutative ((constStepF f) <@> x) (constStepF c)).
rewrite <- Map_composition.
rewriteStepF.
rewrite <- (Map_commutative (constStepF (compose flip f)) (constStepF c)).
rewriteStepF.
apply StepFfoldPropForall_Map2.
intros a b.
apply: H.
Qed.
The implication operation can be lifted to work on characteristic
functions
Definition imp0:Prop→iffSetoid-->iffSetoid.
Proof.
intro A.
∃ (fun B:Prop=>(A→B)).
simpl. unfold canonical_names.equiv. intuition.
Defined.
Definition imp:iffSetoid-->iffSetoid-->iffSetoid.
Proof.
∃ imp0.
simpl. unfold canonical_names.equiv, extEq. intuition.
simpl. intuition.
Defined.
Definition StepF_imp (f g:StepF iffSetoid):Prop:=
(StepFfoldProp (imp ^@> f <@> g)).
Lemma StepFfoldPropglue_rew:(∀ o x y, (StepFfoldProp (glue o x y))<->((StepFfoldProp x)/\StepFfoldProp y)).
Proof.
auto with ×.
Qed.
Lemma StepF_imp_imp:∀ x y:(StepF iffSetoid),
(StepF_imp x y) →
((StepFfoldProp x)->(StepFfoldProp y)).
Proof.
induction x using StepF_ind. induction y using StepF_ind.
auto with ×.
unfold StepF_imp. unfold StepFfoldProp;simpl;intuition.
intros y.
unfold StepF_imp, Map2.
rewriteStepF.
intros.
rewrite <- (StepFfoldPropglue y o).
rewriteStepF.
intuition.
Qed.
Proof.
intro A.
∃ (fun B:Prop=>(A→B)).
simpl. unfold canonical_names.equiv. intuition.
Defined.
Definition imp:iffSetoid-->iffSetoid-->iffSetoid.
Proof.
∃ imp0.
simpl. unfold canonical_names.equiv, extEq. intuition.
simpl. intuition.
Defined.
Definition StepF_imp (f g:StepF iffSetoid):Prop:=
(StepFfoldProp (imp ^@> f <@> g)).
Lemma StepFfoldPropglue_rew:(∀ o x y, (StepFfoldProp (glue o x y))<->((StepFfoldProp x)/\StepFfoldProp y)).
Proof.
auto with ×.
Qed.
Lemma StepF_imp_imp:∀ x y:(StepF iffSetoid),
(StepF_imp x y) →
((StepFfoldProp x)->(StepFfoldProp y)).
Proof.
induction x using StepF_ind. induction y using StepF_ind.
auto with ×.
unfold StepF_imp. unfold StepFfoldProp;simpl;intuition.
intros y.
unfold StepF_imp, Map2.
rewriteStepF.
intros.
rewrite <- (StepFfoldPropglue y o).
rewriteStepF.
intuition.
Qed.