Library UniMath.OrderTheory.DCPOs.Basis.Basis

Require Import UniMath.MoreFoundations.All.
Require Import UniMath.OrderTheory.Posets.
Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets.
Require Import UniMath.OrderTheory.DCPOs.Core.Basics.
Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous.
Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow.
Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous.

Local Open Scope dcpo.

Unset Universe Checking.

Section BasisInDCPO.
  Context {X : dcpo}.

1. Definition of a basis
  Definition dcpo_basis_data
    : UU
    := ∑ (B : UU), B → X.

  Coercion dcpo_basis_data_to_type
           (B : dcpo_basis_data)
    : UU
    := pr1 B.

  Definition dcpo_basis_data_to_dcpo
             (B : dcpo_basis_data)
             (b : B)
    : X
    := pr2 B b.

  Coercion dcpo_basis_data_to_dcpo : dcpo_basis_data >-> Funclass.

  Definition make_dcpo_basis_data
             (B : UU)
             (β : B → X)
    : dcpo_basis_data
    := B ,, β.

  Definition basis_below_element
             (B : dcpo_basis_data)
             (x : X)
    : UU
    := ∑ (b : B), B b ≪ x.

  Definition basis_below_map
             (B : dcpo_basis_data)
             (x : X)
    : basis_below_element B x → X
    := λ b, B(pr1 b).

  Definition dcpo_basis_laws
             (B : dcpo_basis_data)
    : UU
    := ∏ (x : X),
       is_directed X (basis_below_map B x)
       ×
       is_least_upperbound X (basis_below_map B x) x.

  Definition dcpo_basis
    : UU
    := ∑ (B : dcpo_basis_data), dcpo_basis_laws B.

2. Accessors and builders for bases
  Definition make_dcpo_basis
             (B : dcpo_basis_data)
             (HB : dcpo_basis_laws B)
    : dcpo_basis
    := B ,, HB.

  Coercion dcpo_basis_to_data
           (B : dcpo_basis)
    : dcpo_basis_data
    := pr1 B.

  Coercion dcpo_basis_to_laws
           (B : dcpo_basis)
    : dcpo_basis_laws B
    := pr2 B.

  Proposition is_directed_basis
              (B : dcpo_basis)
              (x : X)
    : is_directed X (basis_below_map B x).
  Show proof.
    exact (pr1 (pr2 B x)).

  Definition directed_set_from_basis
             (B : dcpo_basis)
             (x : X)
    : directed_set X.
  Show proof.
    use make_directed_set.
    - exact (basis_below_element B x).
    - exact (basis_below_map B x).
    - exact (is_directed_basis B x).

  Proposition is_least_upperbound_basis
              (B : dcpo_basis)
              (x : X)
    : is_least_upperbound X (basis_below_map B x) x.
  Show proof.
    exact (pr2 (pr2 B x)).

  Proposition approximating_basis_lub
              (B : dcpo_basis)
              (x : X)
    : ⨆ (directed_set_from_basis B x) = x.
  Show proof.
    use antisymm_dcpo.
    - use dcpo_lub_is_least.
      intro i.
      apply way_below_to_le.
      exact (pr2 i).
    - use (is_least_upperbound_is_least (is_least_upperbound_basis B x)).
      apply is_least_upperbound_is_upperbound.
      exact (is_least_upperbound_dcpo_lub (directed_set_from_basis B x)).
End BasisInDCPO.

Set Universe Checking.

Arguments dcpo_basis_data : clear implicits.
Arguments dcpo_basis_laws : clear implicits.
Arguments dcpo_basis : clear implicits.

3. Bases versus continuity
Definition continuous_struct_from_basis
           {X : dcpo}
           (B : dcpo_basis X)
  : continuous_dcpo_struct X.
Show proof.
  intro x.
  refine (directed_set_from_basis B x ,, _ ,, _).
  - intro i.
    exact (pr2 i).
  - apply is_least_upperbound_basis.

Definition basis_data_from_continuous_struct
           {X : dcpo}
           (CX : continuous_dcpo_struct X)
  : dcpo_basis_data X.
Show proof.
  use make_dcpo_basis_data.
  - exact X.
  - exact (λ x, x).

Proposition basis_laws_from_continuous_struct
            {X : dcpo}
            (CX : continuous_dcpo_struct X)
  : dcpo_basis_laws X (basis_data_from_continuous_struct CX).
Show proof.
  intro x.
  split.
  - split.
    + exact (nullary_interpolation CX x).
    + intros i j.
      unfold basis_below_element, basis_data_from_continuous_struct in i, j.
      cbn -[way_below] in i, j.
      assert (H := binary_interpolation CX (pr2 i) (pr2 j)).
      revert H.
      use factor_through_squash.
      {
        apply propproperty.
      }
      intros z.
      induction z as [ z [ p₁ [ p₂ p₃ ]]].
      refine (hinhpr ((z ,, p₃) ,, _ ,, _)).
      * apply way_below_to_le.
        exact p₁.
      * apply way_below_to_le.
        exact p₂.
  - split.
    + intros i.
      induction i as [ i p ].
      apply way_below_to_le.
      exact p.
    + intros y Hy.
      rewrite <- (approximating_family_lub CX x).
      use dcpo_lub_is_least.
      intro i.
      use (Hy (approximating_family CX x i ,, _)).
      cbn -[way_below].
      apply approximating_family_way_below.

Definition basis_from_continuous_struct
           {X : dcpo}
           (CX : continuous_dcpo_struct X)
  : dcpo_basis X.
Show proof.
  use make_dcpo_basis.
  - exact (basis_data_from_continuous_struct CX).
  - exact (basis_laws_from_continuous_struct CX).

Section BasisProperties.
  Context {X : dcpo}
          (B : dcpo_basis X).

4. Approximation via bases
We can characterize the order of the DCPO using the way-below relation and the basis
  Proposition dcpo_basis_le_via_approximation
              (x y : X)
    : x ⊑ y
      ≃
      ∀ (z : B), (B z ≪ x ⇒ B z ≪ y)%logic.
  Show proof.
    use weqimplimpl.
    - intros p z q.
      exact (trans_way_below_le q p).
    - intros H.
      rewrite <- (approximating_basis_lub B x).
      use dcpo_lub_is_least.
      intro i.
      apply way_below_to_le.
      apply (H (pr1 i) (pr2 i)).
    - apply propproperty.
    - apply propproperty.

  Let CX : continuous_dcpo_struct X := continuous_struct_from_basis B.

5. Interpolation using bases
  Proposition basis_nullary_interpolation
              (x : X)
    : ∃ (i : B), B i ≪ x.
  Show proof.
    assert (H := nullary_interpolation CX x).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intro y.
    induction y as [ y p ].
    assert (H := directed_set_el (directed_set_from_basis B y)).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intro i.
    induction i as [ i q ].
    refine (hinhpr (i ,, _)).
    exact (trans_way_below q p).

  Proposition basis_unary_interpolation
              {x y : X}
              (p : x ≪ y)
    : ∃ (i : B), x ≪ B i ∧ B i ≪ y.
  Show proof.
    assert (H := unary_interpolation CX p).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intro z.
    induction z as [ z [ q₁ q₂ ] ].
    assert (r : y ⊑ ⨆ directed_set_from_basis B y).
    {
      rewrite approximating_basis_lub.
      apply refl_dcpo.
    }
    assert (H := q₂ (directed_set_from_basis B y) r).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intro i.
    induction i as [ [ i s₁ ] s₂ ].
    refine (hinhpr (i ,, _ ,, _)).
    - exact (trans_way_below_le q₁ s₂).
    - exact s₁.

  Proposition basis_binary_interpolation
              {x₁ x₂ y : X}
              (p₁ : x₁ ≪ y)
              (p₂ : x₂ ≪ y)
    : ∃ (i : B), x₁ ≪ B i ∧ x₂ ≪ B i ∧ B i ≪ y.
  Show proof.
    assert (H := binary_interpolation CX p₁ p₂).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intro z.
    induction z as [ z [ q₁ [ q₂ q₃ ] ] ].
    assert (H := basis_unary_interpolation q₃).
    revert H.
    use factor_through_squash.
    {
      apply propproperty.
    }
    intro i.
    induction i as [ i [ r₁ r₂ ]].
    refine (hinhpr (i ,, _ ,, _ ,, _)).
    - exact (trans_way_below q₁ r₁).
    - exact (trans_way_below q₂ r₁).
    - exact r₂.

6. Equality of maps via bases
Two maps from a continuous DCPO to any DCPO are equal if they are equal on the basis elements.
  Proposition scott_continuous_map_eq_on_basis
              {Y : dcpo}
              {f g : scott_continuous_map X Y}
              (p : ∏ (i : B), f (B i) = g (B i))
    : f = g.
  Show proof.
    use eq_scott_continuous_map.
    intro x.
    refine (maponpaths f (!((approximating_basis_lub B x))) @ _).
    refine (_ @ maponpaths g (approximating_basis_lub B x)).
    rewrite !scott_continuous_map_on_lub.
    use antisymm_dcpo.
    - use dcpo_lub_is_least ; cbn.
      intro i.
      use less_than_dcpo_lub ; cbn.
      + exact i.
      + unfold basis_below_map.
        rewrite p.
        apply refl_dcpo.
    - use dcpo_lub_is_least ; cbn.
      intro i.
      use less_than_dcpo_lub ; cbn.
      + exact i.
      + unfold basis_below_map.
        rewrite p.
        apply refl_dcpo.

  Proposition map_eq_on_basis_if_scott_continuous
              {Y : dcpo}
              {f g : X → Y}
              (p : ∏ (i : B), f (B i) = g (B i))
              (Hf : is_scott_continuous X Y f)
              (Hg : is_scott_continuous X Y g)
              (x : X)
    : f x = g x.
  Show proof.
    exact (maponpaths
             (λ z, pr1 z x)
             (@scott_continuous_map_eq_on_basis Y (f ,, Hf) (g ,, Hg) p)).

7. The order on maps via basis elements
  Proposition scott_continuous_map_le_on_basis
              {Y : dcpo}
              {f g : scott_continuous_map X Y}
              (p : ∏ (i : B), f (B i) ⊑ g (B i))
              (x : X)
    : f x ⊑ g x.
  Show proof.
    rewrite (maponpaths f (!((approximating_basis_lub B x)))).
    rewrite (maponpaths g (!(approximating_basis_lub B x))).
    rewrite !scott_continuous_map_on_lub.
    use dcpo_lub_is_least ; cbn.
    intro i.
    use less_than_dcpo_lub ; cbn.
    - exact i.
    - unfold basis_below_map.
      apply p.

  Proposition map_le_on_basis_if_scott_continuous
              {Y : dcpo}
              {f g : X → Y}
              (p : ∏ (i : B), f (B i) ⊑ g (B i))
              (Hf : is_scott_continuous X Y f)
              (Hg : is_scott_continuous X Y g)
              (x : X)
    : f x ⊑ g x.
  Show proof.
    exact (@scott_continuous_map_le_on_basis Y (f ,, Hf) (g ,, Hg) p x).

8. Constructing maps from their action on the basis
  Section ScottContinuousFromBasis.
    Context {Y : dcpo}
            (f : B → Y)
            (Hf : ∏ (i₁ i₂ : B), B i₁ ≪ B i₂ → f i₁ ⊑ f i₂).

    Proposition is_directed_map_from_basis
                (x : X)
      : is_directed Y (λ (i : basis_below_element B x), f (pr1 i)).
    Show proof.
      split.
      - assert (H := directed_set_el (directed_set_from_basis B x)).
        revert H.
        use factor_through_squash.
        {
          apply propproperty.
        }
        intro i.
        exact (hinhpr i).
      - intros i j.
        induction i as [i Hix].
        induction j as [j Hjx].
        assert (H := basis_binary_interpolation Hix Hjx).
        revert H.
        use factor_through_squash.
        {
          apply propproperty.
        }
        intro k.
        induction k as [ k [ p [ q r ]]].
        refine (hinhpr ((k ,, r) ,, _ ,, _)).
        + apply Hf.
          exact p.
        + apply Hf.
          exact q.

    Definition map_directed_set_from_basis
               (x : X)
      : directed_set Y.
    Show proof.
      use make_directed_set.
      - exact (basis_below_element B x).
      - exact (λ i, f (pr1 i)).
      - exact (is_directed_map_from_basis x).

    Definition map_from_basis
               (x : X)
      : Y
      := ⨆ (map_directed_set_from_basis x).

    Proposition map_from_basis_monotone
                (x₁ x₂ : X)
                (p : x₁ ⊑ x₂)
      : map_from_basis x₁ ⊑ map_from_basis x₂.
    Show proof.
      unfold map_from_basis.
      use dcpo_lub_is_least ; cbn.
      intro i.
      use less_than_dcpo_lub.
      - refine (pr1 i ,, _).
        exact (trans_way_below_le (pr2 i) p).
      - cbn.
        apply refl_dcpo.

    Proposition map_from_basis_lub
                (D : directed_set X)
      : map_from_basis (⨆ D)
        =
        ⨆_{ D} (map_from_basis ,, map_from_basis_monotone).
    Show proof.
      unfold map_from_basis.
      use antisymm_dcpo.
      - unfold map_from_basis.
        use dcpo_lub_is_least ; cbn.
        intro i.
        induction i as [ i p ] ; cbn.
        assert (H := unary_interpolation CX p).
        revert H.
        use factor_through_squash.
        {
          apply propproperty.
        }
        intro H.
        induction H as [ j [ q₁ q₂ ]].
        assert (H := q₂ D (refl_dcpo _)).
        revert H.
        use factor_through_squash.
        {
          apply propproperty.
        }
        intro k.
        induction k as [ k r ].
        use less_than_dcpo_lub.
        + exact k.
        + cbn.
          use less_than_dcpo_lub.
          * refine (i ,, _).
            exact (trans_way_below_le q₁ r).
          * cbn.
            apply refl_dcpo.
      - unfold map_from_basis.
        use dcpo_lub_is_least ; cbn.
        intro i.
        use dcpo_lub_is_least ; cbn.
        intro j.
        induction j as [ j p ] ; cbn.
        use less_than_dcpo_lub.
        + refine (j ,, _).
          refine (trans_way_below_le p _).
          use less_than_dcpo_lub.
          * exact i.
          * apply refl_dcpo.
        + cbn.
          apply refl_dcpo.

    Proposition is_scott_continuous_map_from_basis
      : is_scott_continuous (pr2 X) (pr2 Y) map_from_basis.
    Show proof.
      use make_is_scott_continuous.
      - exact map_from_basis_monotone.
      - exact map_from_basis_lub.

    Definition scott_continuous_map_from_basis
      : scott_continuous_map X Y
      := map_from_basis ,, is_scott_continuous_map_from_basis.

    Proposition scott_continuous_map_from_basis_le
                (i : B)
      : scott_continuous_map_from_basis (B i) ⊑ f i.
    Show proof.
      use dcpo_lub_is_least ; cbn.
      intro j.
      induction j as [ j p ] ; cbn.
      apply Hf.
      exact p.

    Proposition scott_continuous_map_from_basis_greatest
      (g : scott_continuous_map X Y)
      (Hg : ∏ (i : B), g (B i) ⊑ f i)
      (x : X)
      : g x ⊑ scott_continuous_map_from_basis x.
    Show proof.
      assert (g x ⊑ g (⨆ directed_set_from_basis B x)) as p.
      {
        apply (is_monotone_scott_continuous_map g).
        rewrite (approximating_basis_lub B x).
        apply refl_dcpo.
      }
      refine (trans_dcpo p _).
      rewrite scott_continuous_map_on_lub.
      cbn ; unfold map_from_basis.
      use dcpo_lub_is_least.
      intro i.
      cbn in i.
      use less_than_dcpo_lub.
      - exact i.
      - apply Hg.

  End ScottContinuousFromBasis.
End BasisProperties.