Module SemiLattice
Require Import CoqlibC.
Require Import MapsC.
Require Import FinFun.
Set Implicit Arguments.
Local Open Scope nat_scope.
Definition greatest A (
le:
A ->
A ->
Prop) (
P:
A ->
Prop) (
max:
A):
Prop :=
<<
PROP:
P max>> /\ <<
MAX:
forall a (
PROP:
P a),
le a max>>
.
Module TRIAL1.
Class FSL:
Type := {
t:
Type;
finite:
Finite t;
le:
t ->
t ->
Prop;
le_PreOrder :>
PreOrder le;
lub:
t ->
t ->
t;
lub_spec:
forall x y ,
(<<
LE:
le x (
lub x y)>>) /\ (<<
LE:
le y (
lub x y)>>);
greatest P :=
greatest le P;
}.
Section SemiLatticeProps.
Context `{
FSL}.
Variable P:
t ->
Prop.
Hypothesis CLOSED:
forall x y
(
PX:
P x)
(
PY:
P y),
<<
PXY:
P (
lub x y)>>.
Let find_greatest_aux:
forall l
(
INHAB:
exists inhab,
P inhab),
exists max,
(<<
PROP:
P max>>) /\
(<<
LE:
forall x
(
PROP:
P x)
(
IN:
List.In x l),
<<
LE:
le x max>>>>).
Proof.
intros.
induction l;
ii;
ss.
{
des.
esplits;
eauto.
ii.
ss. }
des.
destruct (
classic (
P a));
cycle 1.
{
esplits;
eauto.
ii.
des;
clarify.
eapply LE;
eauto. }
exists (
lub max a).
esplits;
eauto.
{
eapply CLOSED;
eauto. }
ii.
des;
clarify.
{
eapply lub_spec;
eauto. }
etrans;
try eapply LE;
eauto.
eapply lub_spec;
eauto.
Qed.
Lemma find_greatest
(
INHAB:
exists inhab,
P inhab):
exists max, <<
MAX:
greatest P max>>.
Proof.
hexpl finite FIN.
rr in FIN.
des.
exploit (@
find_greatest_aux l);
eauto.
i;
des.
esplits;
eauto.
rr.
esplits;
eauto.
ii.
eapply LE;
eauto.
Qed.
End SemiLatticeProps.
End TRIAL1.
Module FSL.
Class class (
t:
Type) (
le:
t ->
t ->
Prop) (
lub:
t ->
t ->
t):
Type := {
le_PreOrder :>
PreOrder le;
lub_spec:
forall x y,
(<<
LE:
le x (
lub x y)>>) /\ (<<
LE:
le y (
lub x y)>>);
greatest P :=
greatest le P;
}.
Section SemiLatticeProps.
Variable t:
Type.
Variable le:
t ->
t ->
Prop.
Variable lub:
t ->
t ->
t.
Context `{
class t le lub}.
Variable P:
t ->
Prop.
Hypothesis FIN:
Finite t.
Hypothesis CLOSED:
forall x y
(
PX:
P x)
(
PY:
P y),
<<
PXY:
P (
lub x y)>>.
Let find_greatest_aux:
forall l
(
INHAB:
exists inhab,
P inhab),
exists max,
(<<
PROP:
P max>>) /\
(<<
LE:
forall x
(
PROP:
P x)
(
IN:
List.In x l),
<<
LE:
le x max>>>>).
Proof.
intros.
induction l;
ii;
ss.
{
des.
esplits;
eauto.
ii.
ss. }
des.
destruct (
classic (
P a));
cycle 1.
{
esplits;
eauto.
ii.
des;
clarify.
eapply LE;
eauto. }
exists (
lub max a).
esplits;
eauto.
{
eapply CLOSED;
eauto. }
ii.
des;
clarify.
{
eapply lub_spec;
eauto. }
etrans;
try eapply LE;
eauto.
eapply lub_spec;
eauto.
Qed.
Lemma find_greatest
(
INHAB:
exists inhab,
P inhab):
exists max, <<
MAX:
greatest P max>>.
Proof.
rr in FIN.
destruct FIN as [
l ?].
exploit (@
find_greatest_aux l);
eauto.
i;
des.
esplits;
eauto.
rr.
esplits;
eauto.
ii.
eapply LE;
eauto.
Qed.
End SemiLatticeProps.
End FSL.
Section SemiLatticeProps.
Variable t:
Type.
Variable le:
t ->
t ->
Prop.
Variable lub:
t ->
t ->
option t.
Variable P:
t ->
Prop.
Hypothesis LEORD:
PreOrder le.
Hypothesis LUBSUCC:
forall x y
(
PX:
P x)
(
PY:
P y),
exists z,
lub x y =
Some z.
Hypothesis LUBSPEC:
forall x y z
(
LUB:
lub x y =
Some z),
(<<
LE:
le x z>>) /\ (<<
LE:
le y z>>).
Hypothesis FIN:
exists l,
forall x (
PROP:
P x),
In x l.
Hypothesis CLOSED:
forall x y z
(
PX:
P x)
(
PY:
P y)
(
LUB:
lub x y =
Some z),
<<
PXY:
P z>>.
Let find_greatest_aux:
forall l
(
INHAB:
exists inhab,
P inhab) ,
exists max,
(<<
PROP:
P max>>) /\
(<<
LE:
forall x
(
PROP:
P x)
(
IN:
List.In x l),
<<
LE:
le x max>>>>).
Proof.
intros.
induction l;
ii;
ss.
{
des.
esplits;
eauto.
ii.
ss. }
des.
destruct (
classic (
P a));
cycle 1.
{
esplits;
eauto.
ii.
des;
clarify.
eapply LE;
eauto. }
exploit (@
LUBSUCC max a);
eauto.
i;
des.
exploit (@
CLOSED max a);
eauto.
i;
des.
exists z.
esplits;
eauto.
ii.
exploit LUBSPEC;
eauto.
i;
des_safe.
etrans;
try eapply LE;
eauto.
Qed.
Lemma find_greatest
(
INHAB:
exists inhab,
P inhab):
exists max, <<
MAX:
greatest le P max>>.
Proof.
rr in FIN.
destruct FIN as [
l ?].
des.
exploit (@
find_greatest_aux l);
eauto.
i;
des.
esplits;
eauto.
rr.
esplits;
eauto.
ii.
eapply LE;
eauto.
Qed.
End SemiLatticeProps.
Section GRLE.
Variable t:
Type.
Variable le:
t ->
t ->
Prop.
Variable lub:
t ->
t ->
option t.
Variable P:
t ->
Prop.
Hypothesis LEORD:
PreOrder le.
Hypothesis LUBSUCC:
forall su0 x y
(
PX:
le su0 x /\
P x)
(
PY:
le su0 y /\
P y),
exists z,
lub x y =
Some z.
Hypothesis LUBSPEC:
forall x y z
(
LUB:
lub x y =
Some z),
(<<
LE:
le x z>>) /\ (<<
LE:
le y z>>).
Hypothesis FIN:
exists l,
forall x (
PROP:
P x),
In x l.
Hypothesis CLOSED:
forall su0 x y z
(
PX:
le su0 x /\
P x)
(
PY:
le su0 y /\
P y)
(
LUB:
lub x y =
Some z),
<<
PXY:
P z>>.
Lemma greatest_le_irr
a0 a1 max
(
LE:
le a0 a1)
(
P1:
P a1)
(
GR:
greatest le (
fun a =>
le a1 a /\
P a)
max):
<<
GR:
greatest le (
fun a =>
le a0 a /\
P a)
max>>.
Proof.
r in GR.
rr.
des.
esplits;
eauto.
{
etrans;
eauto. }
ii.
des.
exploit LUBSUCC.
{
esplits;
cycle 1.
eapply P1.
eauto. }
{
esplits;
cycle 1.
eapply PROP2.
eauto. }
intro LUB;
des.
exploit LUBSPEC;
eauto.
i;
des.
exploit CLOSED;
try apply LUB;
eauto.
i;
des.
specialize (
MAX z).
exploit MAX;
eauto.
i;
des.
etrans;
eauto.
Qed.
End GRLE.