Require String.
Require Import NumC.
Require Import DomainInterfaces.
Module Type AffItvSig (
N:
NumSig) <:
ItvSig N.
Parameter t:
Set.
Parameter sat:
t ->
N.t ->
Prop.
Build a singleton interval
Definition Mk1Spec (
n:
N.t) (
i:
t):
Prop
:=
forall n':
N.t,
n =
n' <->
sat i n'.
Parameter mk1Dep:
forall n:
N.t, {
i:
t |
Mk1Spec n i}.
Parameter mk1:
N.t ->
t.
Parameter Mk1_correct:
forall n:
N.t,
Mk1Spec n (
mk1 n).
Sum of two intervals
Definition AddSpec (
i1 i2 i:
t):
Prop
:=
forall n1 n2:
N.t,
sat i1 n1 /\
sat i2 n2 ->
sat i (
N.add n1 n2).
Parameter addDep:
forall i1 i2:
t, {
i:
t |
AddSpec i1 i2 i}.
Parameter add:
t ->
t ->
t.
Parameter Add_correct:
forall i1 i2:
t,
AddSpec i1 i2 (
add i1 i2).
Opposite of an interval
Definition OppSpec (
i1 i2:
t):
Prop
:=
forall n:
N.t,
sat i1 n <->
sat i2 (
N.opp n).
Parameter oppDep:
forall i0:
t, {
i:
t |
OppSpec i0 i}.
Parameter opp:
t ->
t.
Parameter Opp_correct:
forall i1:
t,
OppSpec i1 (
opp i1).
Multiplication by a constant
Definition MulcSpec (
i1:
t) (
n:
N.t) (
i2:
t):
Prop
:=
forall n':
N.t,
sat i1 n' ->
sat i2 (
N.mul n n').
Parameter mulcDep:
forall (
i0:
t) (
n:
N.t), {
i:
t |
MulcSpec i0 n i}.
Parameter mulc:
t ->
N.t ->
t.
Parameter Mulc_correct:
forall (
i1:
t) (
n:
N.t),
MulcSpec i1 n (
mulc i1 n).
Parameter pr:
t ->
String.string.
End AffItvSig.
Module StdItv (
N:
NumSig).
Inductive bndT:
Set
:=
|
Infty:
bndT
|
Open:
N.t ->
bndT
|
Closed:
N.t ->
bndT.
Inductive BndOk:
bndT ->
bndT ->
Prop
:=
|
BndInftyLow:
forall up:
bndT,
BndOk Infty up
|
BndInftyUp:
forall low:
bndT,
BndOk low Infty
|
BndClosed:
forall low up:
N.t,
N.Le low up ->
BndOk (
Closed low) (
Closed up)
|
BndOpen:
forall low up:
N.t,
N.Lt low up ->
BndOk (
Open low) (
Open up)
|
BndOpenClosed:
forall low up:
N.t,
N.Lt low up ->
BndOk (
Open low) (
Closed up)
|
BndClosedOpen:
forall low up:
N.t,
N.Lt low up ->
BndOk (
Closed low) (
Open up).
Inductive tInd:
Set
:=
Bot:
tInd |
NotBot:
forall low up:
bndT,
BndOk low up ->
tInd.
Definition t:
Set
:=
tInd.
Definition satLower (
b:
bndT) (
x:
N.t):
Prop :=
match b with
|
Infty =>
True
|
Open n =>
N.Lt n x
|
Closed n =>
N.Le n x
end.
Definition satUpper (
b:
bndT) (
x:
N.t):
Prop :=
match b with
|
Infty =>
True
|
Open n =>
N.Lt x n
|
Closed n =>
N.Le x n
end.
Definition sat (
i:
t) (
x:
N.t):
Prop
:=
match i with
|
Bot =>
False
|
NotBot low up _ =>
satLower low x /\
satUpper up x
end.
Definition MkSpec (
l u:
bndT) (
i:
t):
Prop
:=
forall x:
N.t,
satLower l x ->
satUpper u x ->
sat i x.
Definition mk (
l u:
bndT): {
i:
t |
MkSpec l u i}.
refine (
match l
return {
i:
t |
MkSpec l u i}
with
|
Infty =>
exist _ (
NotBot Infty u (
BndInftyLow _))
_
|
Open n1 =>
match u
return {
i:
t |
MkSpec (
Open n1)
u i}
with
|
Infty =>
exist _ (
NotBot (
Open n1)
Infty (
BndInftyUp _))
_
|
Open n2 =>
match N.ltLeDec n1 n2 with
|
left pf =>
exist _ (
NotBot (
Open n1) (
Open n2) (
BndOpen _ _ pf))
_
|
right pf =>
exist _ Bot _
end
|
Closed n2 =>
match N.ltLeDec n1 n2 with
|
left pf =>
exist _ (
NotBot (
Open n1) (
Closed n2) (
BndOpenClosed _ _ pf))
_
|
right pf =>
exist _ Bot _
end
end
|
Closed n1 =>
match u
return {
i:
t |
MkSpec (
Closed n1)
u i}
with
|
Infty =>
exist _ (
NotBot (
Closed n1)
Infty (
BndInftyUp _))
_
|
Open n2 =>
match N.ltLeDec n1 n2 with
|
left pf =>
exist _ (
NotBot (
Closed n1) (
Open n2) (
BndClosedOpen _ _ pf))
_
|
right pf =>
exist _ Bot _
end
|
Closed n2 =>
match N.ltLeDec n2 n1 with
|
left pf =>
exist _ Bot _
|
right pf =>
exist _ (
NotBot (
Closed n1) (
Closed n2) (
BndClosed _ _ pf))
_
end
end
end);
unfold MkSpec;
intros x hl hu;
simpl;
try intuition;
unfold satLower in hl;
unfold satUpper in hu;
(
apply N.LeNotLt in pf||
apply N.LtNotLe in pf);
try destruct pf;
[
apply N.LtTrans with (
n2 :=
x)
|
apply N.LtLeTrans with (
n2 :=
x)
|
apply N.LeLtTrans with (
n2 :=
x)
|
apply N.LeTrans with (
n2 :=
x)];
assumption.
Defined.
Proof.
Proof.