Require Import Setoid.
Require Import Coq.Program.Program.
Require Import List.

Instance [ ! Morphism (iff ==> iff ==> iff) R ] =>
  lift_pointwise_morphism :
  Morphism (@predicate_equivalence l ==> @predicate_equivalence l ==> iff) (@pointwise_lifting R l).
Proof.
  simpl_relation.
  induction l.
  simpl in *.

  rewrite H. rewrite H0. reflexivity.

  simpl.
  split ; intros.
  rewrite <- (IHl _ _ (H x1) _ _ (H0 x1)).
  apply H1.
  rewrite (IHl _ _ (H x1) _ _ (H0 x1)).
  apply H1.
Qed.

Program Instance subpredicate_partial_order :
  ! PartialOrder (predicate l) predicate_equivalence predicate_implication.

  Next Obligation.
  Proof.
    induction l. firstorder.
    unfold predicate_equivalence, RelationClasses.relation_equivalence, predicate_implication in *.
    simpl pointwise_lifting.
    setoid_rewrite IHl at 1.
    firstorder.
  Qed.

Require Import Order.Lattice.

Print true_predicate.

Instance predicate_infimum : Infimum _ (@false_predicate l).
Proof. induction l; firstorder. Qed.

Instance predicate_supremum : Supremum _ (@true_predicate l).
Proof. induction l; firstorder. Qed.

Instance and_glb : BinaryGlb subpredicate_partial_order (@predicate_intersection l).
Proof.
  reduce. 
  unfold le, predicate_intersection, predicate_implication.
  induction l.
  
    simpl. firstorder.

    simpl in *. 
    setoid_rewrite IHl. firstorder.
Qed.

Instance or_lub : BinaryLub subpredicate_partial_order (@predicate_union l).
Proof.
  reduce. unfold flip, le, predicate_union, predicate_implication. 
  induction l. simpl. firstorder.
  simpl in *. 
  setoid_rewrite IHl. firstorder.
Qed.

Program Instance meet_semi : MeetSemiLattice _ (@predicate_intersection l) :=
  meet_glb := and_glb.

  Next Obligation.
  Proof.
    induction l. firstorder.
    simpl in *.
    intro. fold pointwise_lifting.
    apply IHl ; firstorder.
  Qed.

Program Instance join_semi : JoinSemiLattice _ (@predicate_union l).

  Next Obligation.
  Proof.
    constructor. obligations_tactic.
    
    induction l. firstorder.
    simpl in *. intro ; fold pointwise_lifting. apply IHl ; firstorder.

    apply @or_lub.
  Qed.

Program Instance predicates_lattice : Lattice _ (@meet_semi l) (@join_semi l).

Open Local Scope predicate_scope.

Instance bounded_meet : BoundedMeetSemiLattice (@meet_semi l) ∙⊤∙.
Proof. auto with typeclass_instances.
  induction l; firstorder.
Qed.

Instance bounded_join : BoundedJoinSemiLattice (@join_semi l) ∙⊥∙.
Proof.
  induction l; firstorder.
Qed.

Instance bounded_lattice : BoundedLattice (@predicates_lattice l) _ _.

Instance bounded_predicates_lattice : Bounded (@subpredicate_partial_order l) := 
  top := ∙⊤∙ ; 
  bottom := ∙⊥∙ ; 
  is_top := @predicate_supremum l ;
  is_bottom := @predicate_infimum l.

Fixpoint predicate_subset_union {l} : forall (s : subset (predicate l)), predicate l :=
  match l with
    | [] => fun (s : subset Prop) => exists u, u ∈ s /\ u
    | A :: l' => fun s =>
      fun x => predicate_subset_union 
        (fun r =>
          exists r' : predicate (A :: l'),
            s r' /\ (r <∙> r' x))
  end.

Lemma union_lub : forall l (s : subset (predicate l)), least_upper_bound s (predicate_subset_union s).
Proof.
  unfold least_upper_bound, upper_bound. simpl in *.
  unfold le, predicate_implication, impl in * ; simpl in *.
  induction l; simpl in *; intros.

  (* predicate Prop *)
    split ; intros.
    destruct H0 ; destruct_conjs.
    apply (H (exist s _ H0)). simpl. assumption.

    apply H.
    destruct y ; simpl in *.
    exists x. intuition.

  (* predicate (A :: l) *)
    split ; intros.
    rewrite <- IHl.
    intros {r, r', Hr', Hr}.
    simpl.
    setoid_rewrite Hr.
    apply (H (exist s r' Hr')).

    destruct y ; simpl in *.
    pose (H x) as p.
    rewrite <- IHl in p.
    assert(exists r', s r' /\ (x0 x <∙> r' x)).
    exists x0. split ; order.
    apply (p (exist _ (x0 x) H0)).
Qed.

Instance predicate_complete_lattice : ! CompleteLattice (predicate l) _ _ _ _.
Proof.
  reduce. 
  exists (predicate_subset_union s).
  apply union_lub.
Qed.

Definition subpredicate_infjoin {l} : InfJoinSemiLattice (@subpredicate_partial_order l) least_upper_bound.
  intros.
  eapply @subset_lub_join.
  intros.
  exists (predicate_subset_union s). 
  apply union_lub.
Qed.