Section QS.

Definition QabsS : QS-->QS.
Defined.

Definition Qplus0 : QS -> QS --> QS.
Defined.

Definition QplusS : QS --> QS --> QS.
Defined.

Definition QoppS : QS --> QS.
Defined.

Definition Qminus0 : QS -> QS --> QS.
Defined.

Definition QminusS : QS --> QS --> QS.
Defined.

Definition QscaleS : QS -> QS --> QS.
Defined.

Definition QmultS : QS --> QS --> QS.
Defined.

Definition Qle0 : QS -> QS --> iffSetoid.
Defined.

Definition QleS : QS --> QS --> iffSetoid.
Defined.

End QS.

Notation "'StepQ'" := (StepF QS) : StepQ_scope.



Definition StepQplus (s t:StepQ) : StepQ := QplusS ^@> s <@> t.
Definition StepQopp (s:StepQ) : StepQ := QoppS ^@> s.
Definition StepQminus (s t:StepQ) : StepQ := QminusS ^@> s <@> t.
Definition StepQmult (s t:StepQ) : StepQ := QmultS ^@> s <@> t.
Notation "x + y" := (StepQplus x y) : StepQ_scope.
Notation "- x" := (StepQopp x) : StepQ_scope.
Notation "x - y" := (StepQminus x y) : StepQ_scope.
Notation "x * y" := (StepQmult x y) : StepQ_scope.

Add Morphism StepQplus with signature (@StepF_eq QS) ==> (@StepF_eq QS) ==> (@StepF_eq QS) as StepQplus_wd.

Add Morphism StepQopp with signature (@StepF_eq QS) ==> (@StepF_eq QS) as StepQopp_wd.

Add Morphism StepQminus with signature (@StepF_eq QS) ==> (@StepF_eq QS) ==> (@StepF_eq QS) as StepQminus_wd.

Add Morphism StepQmult with signature (@StepF_eq QS) ==> (@StepF_eq QS) ==> (@StepF_eq QS) as StepQmult_wd.

Definition StepQsrt : (@ring_theory (StepQ) (constStepF (0:QS)) (constStepF (1:QS)) StepQplus StepQmult StepQminus StepQopp (@StepF_eq QS)).









Qed.

Definition StepQisZero:(StepQ)->bool:=(StepFfold (fun (x:QS) => Qeq_bool x 0) (fun _ x y => x && y)).

Definition StepQeq_bool (x y:StepQ) : bool := StepQisZero (x-y).

Lemma StepQeq_bool_correct : forall x y, StepQeq_bool x y = true -> x == y.

Lemma StepQRing_Morphism : ring_eq_ext StepQplus StepQmult StepQopp (@StepF_eq QS).



Add Ring StepQRing : StepQsrt
 (decidable StepQeq_bool_correct,
  setoid (StepF_Sth QS) StepQRing_Morphism,
  constants [StepQcst]).

Definition StepQabs (s:StepQ) : StepQ := QabsS ^@> s.

Add Morphism StepQabs with signature (@StepF_eq QS) ==> (@StepF_eq QS) as StepQabs_wd.



A Partial Order on Step Functions.

Definition StepQ_le x y := (StepFfoldProp (QleS ^@> x <@> y)).
Notation "x <= y" := (StepQ_le x y) (at level 70) : sfstscope.

Lemma StepQ_le_refl:forall x, (x <= x).

Lemma StepQ_le_trans:forall x y z,
 (x <= y)-> (y <= z) ->(x <= z).


Lemma StepQabsOpp : forall x, StepQabs (-x) == StepQabs (x).

Lemma StepQabs_triangle : forall x y, StepQabs (x+y) <= StepQabs x + StepQabs y.