Require Import base
  protype ordtype clat frame
  mono adj cont.

Section PairProType.
  Variable (A B : proType).
  Implicit Types (p q r : A * B).

  Definition pair_le p q := (p.1 ≤ q.1) /\ (p.2 ≤ q.2).

  Lemma pair_le_refl : reflexive pair_le.
  Proof. by []. Qed.

  Lemma pair_le_trans : transitive pair_le.
  Proof.
    move=> p q r [l11 l12] [l21 l22]. split; by [rewrite l11|rewrite l12].
  Qed.

  Canonical pair_proMixin := ProMixin pair_le_refl pair_le_trans.
  Canonical pair_proType := Eval hnf in ProType (A * B) pair_proMixin.
End PairProType.

Section PairOrdType.
  Variable (A B : ordType).
  Implicit Types (p q : A * B).

  Lemma pair_le_eq p q : p ≤ q -> q ≤ p -> p = q.
  Proof.
    move: p q => -[p1 p2] [q1 q2] [/=h11 h12] [/=h21 h22].
    congr pair; exact: le_eq.
  Qed.

  Canonical pair_ordMixin := OrdMixin pair_le_eq.
  Canonical pair_ordType := Eval hnf in OrdType (A * B) pair_ordMixin.
End PairOrdType.

Section PairCLat.
  Variable (A B : clat).
  Implicit Types (p q r : A * B).

  Definition pair_inf I (G : I -> A * B) : A * B :=
    (inf (fst \o G), inf (snd \o G)).

  Lemma pair_infP I (G : I -> A * B) : is_glb G (pair_inf G).
  Proof.
    apply: mk_glb => [i|f h] /=. split=>/=; exact: allE (i) _.
    split=>/=; focus=> i; by case: (h i).
  Qed.

  Canonical pair_clatMixin := CLatMixin pair_infP.
  Canonical pair_clat := Eval hnf in CLat (A * B) pair_clatMixin.

  Lemma pair_topE : (⊤ : A * B) = (⊤, ⊤).
  Proof. apply: top_def. split; exact: topI. Qed.

  Lemma pair_botE : (⊥ : A * B) = (⊥,⊥).
  Proof. apply: bot_def. split; exact: botE. Qed.

  Lemma pair_joinE p q : (p ∨ q) = (p.1 ∨ q.1, p.2 ∨ q.2).
  Proof.
    apply: join_def. split; exact: joinIl. split; exact: joinIr.
    move=> [x y] [/=l11 l12] [/=l21 l22]. split=>/=; by focus.
  Qed.

  Lemma pair_meetE p q : (p ∧ q) = (p.1 ∧ q.1, p.2 ∧ q.2).
  Proof.
    apply: meet_def. split; exact: meetEl. split; exact: meetEr.
    move=> [x y] [/=l11 l12] [/=l21 l22]. split=>/=; by focus.
  Qed.

  Lemma pair_exE I (G : I -> A * B) :
    (∃ i, G i) = (∃ i, (G i).1, ∃ i, (G i).2).
  Proof.
    apply: ex_def => [i|[x y] h]. split; exact: exI.
    split=>/=; focus=> i; by case: (h i).
  Qed.

  Lemma pair_allE I (G : I -> A * B) : (∀ i, G i) = (∀ i, (G i).1, ∀ i, (G i).2).
  Proof. by []. Qed.
End PairCLat.

Section PairFrame.
  Variables (A B : frame).
  Implicit Types (p q : A * B).

  Lemma pair_frameP I (G : I -> A * B) p :
    p ∧ sup G ≤ ∃ i, p ∧ G i.
  Proof.
    rewrite pair_meetE pair_exE !meetxE pair_exE.
    (* FIXME: make meet/join/etc globally opaque! *)
    Opaque meet. split=>/=; focus=> i; apply: exI (i) _; by rewrite pair_meetE.
  Qed.

  Canonical pair_frameMixin := FrameMixin pair_frameP.
  Canonical pair_frame := Eval hnf in Frame (A * B) pair_frameMixin.

  Lemma pair_impE p q : (p → q) = (p.1 → q.1, p.2 → q.2).
  Proof.
    apply: imp_def. rewrite pair_meetE /=. split; exact: impEr.
    move=> [x y]. rewrite pair_meetE => -[/=l1 l2]. split; exact: impI.
  Qed.
End PairFrame.

Section IProdProType.
  Variables (T : Type) (F : T -> proType).
  Implicit Types (f g h : iprod F).

  Definition iprod_le f g := forall x, f x ≤ g x.

  Lemma iprod_le_refl f : iprod_le f f.
  Proof. by []. Qed.

  Lemma iprod_le_trans f g h : iprod_le f g -> iprod_le g h -> iprod_le f h.
  Proof. move=> h1 h2 x. exact: le_trans (h1 x) (h2 x). Qed.

  Canonical iprod_proMixin := ProMixin iprod_le_refl iprod_le_trans.
  Canonical iprod_proType := Eval hnf in ProType (iprod F) iprod_proMixin.
End IProdProType.

Section IProdOrdType.
  Variables (T : Type) (F : T -> ordType).
  Implicit Types (f g : iprod F).

  Lemma iprod_le_eq f g : f ≤ g -> g ≤ f -> f = g.
  Proof. move=> le_f_g le_g_f. fext=> x. exact: le_eq. Qed.

  Canonical iprod_ordMixin := OrdMixin iprod_le_eq.
  Canonical iprod_ordType := Eval hnf in OrdType (iprod F) iprod_ordMixin.
End IProdOrdType.

Section IProdCLat.
  Variables (T : Type) (F : T -> clat).
  Implicit Types (f g : iprod F) (x : T).

  Definition iprod_inf I (G : I -> iprod F) : iprod F :=
    fun t => inf (G^~ t).

  Lemma iprod_infP I (G : I -> iprod F) : is_glb G (iprod_inf G).
  Proof.
    apply: mk_glb => [i x|f h x] /=. exact: allE. apply: allI => i. exact: h.
  Qed.

  Canonical iprod_clatMixin := CLatMixin iprod_infP.
  Canonical iprod_clat := Eval hnf in CLat (iprod F) iprod_clatMixin.

  Lemma iprod_topE x : (⊤ : iprod F) x = ⊤.
  Proof.
    suff->: ⊤ = (fun _ => ⊤) :> (iprod F). by [].
    apply: top_def; hnf=> y. exact: topI.
  Qed.

  Lemma iprod_botE x : (⊥ : iprod F) x = ⊥.
  Proof.
    suff->: ⊥ = (fun _ => ⊥) :> (iprod F). by [].
    apply: bot_def; hnf=> y. exact: botE.
  Qed.

  Lemma iprod_joinE f g x : (f ∨ g) x = (f x ∨ g x).
  Proof.
    suff->: (f ∨ g) = (fun x => f x ∨ g x) :> (iprod F). by [].
    apply: join_def; try (hnf=> y; cauto). move=> h h1 h2; hnf=> y /=.
    rewrite (h1 y) (h2 y). by focus.
  Qed.

  Lemma iprod_meetE f g x : (f ∧ g) x = (f x ∧ g x).
  Proof.
    suff->: (f ∧ g) = (fun x => f x ∧ g x) :> (iprod F). by [].
    apply: meet_def; try (hnf=> y; cauto). move=> h h1 h2; hnf=> y /=.
    rewrite -(h1 y) -(h2 y). by focus.
  Qed.

  Lemma iprod_exE I (G : I -> iprod F) x : (∃ i, G i) x = ∃ i, G i x.
  Proof.
    suff->: sup G = (fun x => ∃ i, G i x) :> (iprod F). by [].
    apply: ex_def => [i|/= g h]; hnf=> y /=. exact: exI. focus=> i. exact: h.
  Qed.

  Lemma iprod_allE I (G : I -> iprod F) x : (∀ i, G i) x = ∀ i, G i x.
  Proof. by []. Qed.
End IProdCLat.

Section IProdFrame.
  Variables (T : Type) (F : T -> frame).
  Implicit Types (f g : iprod F) (x : T).

  Lemma iprod_frameP I (G : I -> iprod F) f :
    f ∧ sup G ≤ ∃ i, f ∧ G i.
  Proof.
    move=> x. rewrite iprod_meetE !iprod_exE meetxE.
    focus=> i. apply: exI (i) _. by rewrite iprod_meetE.
  Qed.

  Canonical iprod_frameMixin := FrameMixin iprod_frameP.
  Canonical iprod_frame := Eval hnf in Frame (iprod F) iprod_frameMixin.

  Lemma iprod_impE f g x : (f → g) x = (f x → g x).
  Proof.
    suff->: (f → g) = (fun x => f x → g x). by [].
    apply: imp_def => [|h H]; hnf=> y /=. rewrite iprod_meetE. exact/impP.
    apply/impP. by rewrite -(H y) iprod_meetE.
  Qed.
End IProdFrame.

Arguments iprod_le {T F} f g /.

Lemma iprod_leE (T : Type) (F : T -> proType) (f g : forall x, F x) :
  (f ≤ g :> iprod _) = (forall x, f x ≤ g x).
Proof. by []. Qed.

Canonical prod_proType (T : Type) (X : proType) :=
  Eval hnf in ProType (T -> X) (@iprod_proMixin T (fun _ => X)).

Lemma prod_leE (T : Type) (X : proType) (f g : T -> X) :
  (f ≤ g) = (forall x, f x ≤ g x).
Proof. by []. Qed.

Canonical prod_ordType (T : Type) (X : ordType) :=
  Eval hnf in OrdType (T -> X) (@iprod_ordMixin T (fun _ => X)).

Canonical prod_clat (T : Type) (X : clat) :=
  Eval hnf in CLat (T -> X) (@iprod_clatMixin T (fun _ => X)).

Section ProdCLat.
  Variables (T : Type) (X : clat).
  Implicit Types (f g : T -> X) (x : T).

  Lemma prod_topE x : (⊤ : T -> X) x = ⊤.
  Proof. by rewrite iprod_topE. Qed.

  Lemma prod_botE x : (⊥ : T -> X) x = ⊥.
  Proof. by rewrite iprod_botE. Qed.

  Lemma prod_joinE f g x : (f ∨ g) x = (f x ∨ g x).
  Proof. by rewrite iprod_joinE. Qed.

  Lemma prod_meetE f g x : (f ∧ g) x = (f x ∧ g x).
  Proof. by rewrite iprod_meetE. Qed.

  Lemma prod_exE I (F : I -> T -> X) x : (∃ i, F i) x = ∃ i, F i x.
  Proof. by rewrite iprod_exE. Qed.

  Lemma prod_allE I (F : I -> T -> X) x : (∀ i, F i) x = ∀ i, F i x.
  Proof. by rewrite iprod_allE. Qed.
End ProdCLat.

Canonical prod_frame (T : Type) (X : frame) :=
  Eval hnf in Frame (T -> X) (@iprod_frameMixin T (fun _ => X)).

Lemma prod_impE (T : Type) (X : frame) (f g : T -> X) (x : T) :
  (f → g) x = (f x → g x).
Proof. by rewrite iprod_impE. Qed.

(*Instance prod_le_pointwise {T : Type} {X : proType} :
  subrelation (@ord_op (prod_proType T X)) (eq ++> ord_op)*)

Global Instance prod_pointwise_subrelation (T : Type) (X : proType) :
  subrelation (@ord_op (prod_proType T X)) (pointwise_relation T ord_op).
Proof. by []. Qed.