Library strict_utils


Require Import String.
Require Import List.
Require Import Setoid.

Require Import basics.
Require Import preord.
Require Import categories.
Require Import sets.
Require Import finsets.
Require Import esets.
Require Import effective.
Require Import directed.
Require Import plotkin.
Require Import joinable.
Require Import approx_rels.
Require Import cpo.
Require Import profinite.
Require Import profinite_adj.
Require Import flat.

Strict functions and applications lifted into PLT

We give operators for strict functions and applications in PLT. This takes two forms: a direct one and another one with lifted functions.

Definition strict_app (A B:PLT)
  : U (A B) × U A U B

  := U·(apply PLT.pair_map ε ε lift_prod') η.

Definition strict_curry (Γ:PLT) (A B:PLT)
  (f:Γ×U A U B) : Γ U (A B)

  := U·(Λ( ε L·f lift_prod PLT.pair_map id γ)) η.

Definition strict_app' (A B:PLT)
  : U (colift (A B)) × U A U B

  := strict_app A B PLT.pair_map (U·ε) id.

Definition strict_curry' (Γ:PLT) (A B:PLT)
  (f:Γ × U A U B) : Γ U (colift (A B))

  := η strict_curry Γ A B f.



Definition semvalue (Γ:PLT) (A:PLT) (f:Γ U A) :=
  forall g, exists a, (g,Some a) PLT.hom_rel f.

Lemma semvalue_le : forall Γ A (f f':Γ U A),
  f f' -> semvalue f -> semvalue f'.

Lemma semvalue_equiv : forall Γ A (f f':Γ U A),
  f f' -> semvalue f -> semvalue f'.

Add Parametric Morphism Γ A :
  (@semvalue Γ A)
  with signature (eq_op _) ==> iff
    as semvalue_eq_morphism.

Lemma eta_semvalue A B (f:A B) :
  semvalue (η f).

Bottom is not a semantic value.
Lemma plt_semvalue_bot (Γ:PLT) (A:PLT) (x:Γ) :
  semvalue ( : Γ U A) -> False.

Lemma strict_curry_app2 D (Γ:PLT) (A B:PLT)
  (f : Γ×U A U B) (g : D U A) (h:D Γ)
  (Hg : semvalue g) :

  strict_app strict_curry f h, g f h, g.

Lemma strict_curry_app_converse (Γ:PLT) (A:PLT)
  (g : Γ U A) :
  (forall B (f : Γ×U A U B),
    strict_app strict_curry f, g f id, g) ->
  semvalue g.

Lemma strict_curry_app (Γ:PLT) (A B:PLT)
  (f : Γ×U A U B) (g : Γ U A)
  (Hg: semvalue g) :
  strict_app strict_curry f, g f id, g.

Lemma strict_curry_app2' D (Γ:PLT) (A B:PLT)
  (f : Γ×U A U B) (g : D U A) (h:D Γ)
  (Hg : semvalue g) :

  strict_app' strict_curry' f h, g f h, g.

Lemma strict_curry_app' (Γ:PLT) (A B:PLT)
  (f : Γ×U A U B) (g : Γ U A) (Hg : semvalue g) :

  strict_app' strict_curry' f, g f id, g.

Lemma strict_curry_monotone Γ A B (f f':Γ×U A U B) :
  f f' -> strict_curry f strict_curry f'.

Lemma strict_curry'_monotone Γ A B (f f':Γ×U A U B) :
  f f' -> strict_curry' f strict_curry' f'.

Lemma strict_curry_eq Γ A B (f f':Γ×U A U B) :
  f f' -> strict_curry f strict_curry f'.

Lemma strict_curry'_eq Γ A B (f f':Γ×U A U B) :
  f f' -> strict_curry' f strict_curry' f'.

Add Parametric Morphism Γ A B :
  (@strict_curry Γ A B)
    with signature (Preord.ord_op _) ==> (Preord.ord_op _)
    as strict_curry_le_morphism.

Add Parametric Morphism Γ A B :
  (@strict_curry' Γ A B)
    with signature (Preord.ord_op _) ==> (Preord.ord_op _)
    as strict_curry'_le_morphism.

Add Parametric Morphism Γ A B :
  (@strict_curry Γ A B)
    with signature (eq_op _) ==> (eq_op _)
    as strict_curry_morphism.

Add Parametric Morphism Γ A B :
  (@strict_curry' Γ A B)
    with signature (eq_op _) ==> (eq_op _)
    as strict_curry'_morphism.

Lemma strict_curry_compose_commute Γ Γ' A B (f:Γ×U A U B) (h:Γ' Γ) :
  strict_curry f h strict_curry (f PLT.pair_map h id).

Lemma strict_curry_compose_commute' Γ Γ' A B (f:Γ×U A U B) (h:Γ' Γ) :
  strict_curry' f h strict_curry' (f PLT.pair_map h id).

Lemma plt_strict_compose : forall (A B C:PLT) (f:B C),
  f (: A B) .

Lemma strict_app_bot (Γ:PLT) (A B:PLT) (f:Γ U (A B)) :
  strict_app f, .

Lemma strict_app_bot' (Γ:PLT) (A B:PLT) (f:Γ U (colift (A B))) :
  strict_app' f, .

Lemma strict_curry'_semvalue Γ A B f :
  semvalue (@strict_curry' Γ A B f).

Lemma strict_curry'_semvalue2 Γ A B C f (g:C Γ) :
  semvalue (@strict_curry' Γ A B f g).

Lemma semvalue_strict_app_out1 A B C (f:C U (A B)) (x:C U A) :
  semvalue (strict_app f, x) ->
  semvalue f.

Lemma semvalue_strict_app_out2 A B C (f:C U (A B)) (x:C U A) :
  semvalue (strict_app f, x) ->
  semvalue x.

Lemma semvalue_app_out1' A B C (f:C U (colift (A B))) (x:C U A) :
  semvalue (strict_app' f, x) ->
  semvalue f.

Lemma semvalue_app_out2' A B C (f:C U (colift (A B))) (x:C U A) :
  semvalue (strict_app' f, x) ->
  semvalue x.

Lift the case analysis and element function for flat domains into PLT.
Definition flat_cases' (X:enumtype) (Γ:PLT) (B:PLT) (f:X -> Γ U B)
  : (Γ × U (flat X))%plt U B
  := U·(flat_cases (fun x => ε L·(f x)) PLT.pair_map id ε lift_prod') η.

Definition flat_elem' (X:enumtype) (Γ:PLT) (x:X) : Γ U (flat X)
  := U·(flat_elem x PLT.terminate _ _) η.

Lemma flat_cases_elem' (X:enumtype) (Γ D:PLT) (B:PLT)
  (f:X -> Γ U B) (x:X) (h:D Γ) :
  flat_cases' f h, flat_elem' x f x h.

Lemma flat_cases'_strict (X:enumtype) (Γ:PLT) (B:PLT)
  (f:X -> Γ U B) a x b :
  (a,x,b) PLT.hom_rel (flat_cases' f) -> x = None -> b = None.

Lemma flat_cases'_semvalue (X:enumtype) A (Γ:PLT) (B:PLT)
  (f:X -> Γ U B) (g : A Γ) h :
  semvalue (flat_cases' f g,h) ->
  semvalue h.

Lemma flat_cases_univ' (X:enumtype) (A:PLT) (B:PLT) (f:X -> A U B)
  (q: A × U (flat X) U B) :
  (forall a x b, (a,x,b) PLT.hom_rel q -> x = None -> b = None) ->
  (forall x, f x q id, flat_elem' x ) ->
  flat_cases' f q.

Lemma flat_cases_commute : forall (X : enumtype) (A C : PLT) (B:PLT)
  (f : X -> A U B) (g:C A) (h:C U (flat X)),
  flat_cases' f g, h flat_cases' (fun x => f x g) id, h.

Lemma flat_elem'_ignores_arg (X:enumtype) A B (x:X) (h:A B) :
  flat_elem' x flat_elem' x h.

Lemma flat_elem'_semvalue : forall (X:enumtype) Γ (x:X),
  @semvalue Γ (flat X) (flat_elem' x).

Lemma flat_elem_canon : forall (X:enumtype) (g:1 U (flat X)),
  semvalue g -> exists x, g flat_elem' x.

Lemma flat_elem'_inj (X:enumtype) (x x':X) (A:PLT) (a:A) :
  @flat_elem' X A x flat_elem' x' -> x = x'.