order.v

From mathcomp Require Import classical_sets eqtype boolp seq order topology choice ssrfun.
Require Import ssreflect ssrbool.
Open Scope classical_set_scope.


Module SetOrder.
Section SetOrder.


Context {T: Type}.
Implicit Types (X Y : set T).

Definition asboolsubset X Y :=
`[< X `<=`Y >].

Definition proper_asboolsubset X Y :=
    ~~(Y == X) && asboolsubset X Y.

Lemma setI_meet X Y:
asboolsubset X Y = (setI X Y == X).
Admitted.

Fact tmp x y:
proper_asboolsubset x y = ~~ (y == x) && asboolsubset x y.
Admitted.


Fact subset_C: @commutative (set T) (set T) setI.
Admitted.

Fact setUC: @commutative (set T) (set T) setU.
Admitted.

Fact tmp2: @associative (set T)  setI.
Admitted.
Fact tmp3: @associative (set T)  setU.
Admitted.

Fact joinP:
       (forall y x : arrow_choiceType T Prop_choiceType, x `&` (x `|` y) = x).
Admitted.

Fact meetP:
       (forall y x : arrow_choiceType T Prop_choiceType, x `|` x `&` y = x).
Admitted.

Fact ldist:
       @left_distributive (set T) (set T) setI setU.
Admitted.

Fact idemp:
       @idempotent (set T) setI.
Admitted.


Definition orderMixin :=
@MeetJoinMixin _ asboolsubset proper_asboolsubset setI setU setI_meet tmp subset_C setUC tmp2 tmp3 joinP meetP ldist idemp.

Canonical porderType := POrderType total_display (set T) orderMixin.
Canonical latticeType := LatticeType (set T) orderMixin.
Canonical distrLatticeType := DistrLatticeType (set T) orderMixin.

End SetOrder.
Module Exports.
Canonical porderType.
Canonical latticeType.
Canonical distrLatticeType.
Definition asboolsubset {T}:=@asboolsubset T.
End Exports.
End SetOrder.

Import SetOrder.Exports.


Variable T: Type.

Local Open Scope order_scope.

Example test (A B: set T):
asboolsubset A B.
Proof.
Fail apply: Order.POrderTheory.ltW.
apply: (@Order.POrderTheory.ltW _ _ A B ).

asboolsubset A B.

Use A <= B