namespace http://hku.hk/PL❚

/T The SEDEL type theory (simple type theory with distributive intersection types).
   Formalized with Bruno Oliveira's students during Florian Rabe's March 2019 visit at Hongkong University.
   
   See also https://i.cs.hku.hk/~bruno/papers/nested.pdf and https://i.cs.hku.hk/~bruno/papers/traits.pdf
❚

// define some namespace prefixes❚

import lfx http://gl.mathhub.info/MMT/LFX/Subtyping❚
import lfrules scala://lf.mmt.kwarc.info/❚
import stdlit scala://uom.api.mmt.kwarc.info/❚

theory SEDEL : lfx:?LFSubtyped =
  # Syntactic Categories❙
  
  /T types and terms of simple type theory❙
  tp : type❙
  tm : tp ⟶ type❘# tm 1 prec -5❙

  # Judgments❙
  
  ## Equality of terms❙
  
  equal : {A} tm A ⟶ tm A ⟶ type ❘ # 2 ≡ 1 3 prec -5❘role Eq❙
  refl  : {A,X: tm A} X ≡ A X❘# refl 2❙ 
  // admissible rule (admissibility proof by logical relation)❙
  cong  : {A,B,X,Y: tm A, F: tm A ⟶ tm B} X ≡ A Y ⟶ (F X) ≡ B (F Y)❙

  ## Subtyping❙
  sbt : tp ⟶ tp ⟶ type❘# 1 < 2 prec -5❙
  spt : tp ⟶ tp ⟶ type❘= [A,B] B < A❘# 1 > 2 prec -5❙
  
  /T proof irrelevance for subtyping proofs❙
  rule lfrules?TermIrrelevanceRule sbt❙

  st_refl: {A} A < A❙
  st_trans: {A,B,C} A < B ⟶ B < C ⟶ A < C❙

  /T embed SEDEL subtyping into LF subtyping❙
  st_shallow : {A,B} A < B ⟶ tm A <* tm B❙

  ## Relationship between Equality and Subtyping❙

  /T equality depends on the type at which terms are compared.
     Equality is preserved when going to larger types.
     But not necessarily the other way round, e.g., all terms are equal at unit type.❙ 
  // TODO: this should type-check❙
  // equal_st : {A,B,s:tm A, t: tm A} A < B ⟶ s ≡ A t ⟶ s ≡ B t❙  
  
  # Syntax❙

  ## Function Types❙
  
  fun : tp ⟶ tp ⟶ tp❘# 1 → 2❙
  fun_st : {A,B,C,D} A > C ⟶ B < D ⟶ A → B < C → D❙
  lambda : {A,B} (tm A ⟶ tm B) ⟶ tm (A → B)❘# λ 3❙
  apply : {A,B} tm (A → B) ⟶ tm A ⟶ tm B ❘# 3 @ 4 prec 10❙
  
  beta : {A,B, F: tm A ⟶ tm B, a} (λ [x] F x) @ a ≡ B (F a)❘ role Simplify❘# beta 3 4❙
  cong_apply : {A,B,F: tm (A → B), G, X, Y}
                 (F ≡ (A → B) G) ⟶ X ≡ A Y ⟶ (F @ X) ≡ B (G@Y)❙
  cong_lambda : {A,B,F: tm A ⟶ tm B,G} ({x} (F x) ≡ B (G x)) ⟶ (λ F) ≡ (A → B) (λ G)❙

  ## Top type❙

  /T The top type can be seen as the common supertype of all types, the unit type, and the neutral element of intersection.❙
  
  top : tp❘# ⊤❙
  unit : tm ⊤❙
  st_top : {A} A < ⊤❙
  eq_top: {x: tm ⊤} x ≡ ⊤ unit❙

  ## Bottom type❙
  
  bottom : tp❘# ⊥❙
  st_bottom: {A} ⊥ < A❙
  
  ## Intersection types❙
  
  inter : tp ⟶ tp ⟶ tp❘# 1 & 2 prec 10❙
  inter_st_left  : {A,B} A & B < A❙
  inter_st_right : {A,B} A & B < B❙
  inter_glb : {A,B,C} C < A ⟶ C < B ⟶ C < A & B❙
  
  disjoint: tp ⟶ tp ⟶ type❘# 1 * 2❙
  rule lfrules?TermIrrelevanceRule disjoint❙

  disjointIntro: {A,B} ({C} C > A ⟶ C > B ⟶ C > ⊤) ⟶ A * B❙
  disjointElim : {A,B} A * B ⟶ {C} C > A ⟶ C > B ⟶ C > ⊤❙
  
  // TODO: these definitions should type-check❙
  inter_left  : {A,B} tm A & B ⟶ tm A❘// = [A,B,x] x❘❙
  inter_right : {A,B} tm A & B ⟶ tm B❘// = [A,B,x] x❘❙
  inter_in    : {A,B} {a:tm A} {b: tm B} A * B ⟶ tm A & B❘# 3 ,, 4 %I5❙
  // TODO: this must solve the proof term (which is in the context) as an implicit argument❙
  // cong_inter_in : {A,B} A * B ⟶ {a1,a2: tm A, b1,b2: tm B}
                  a1 ≡ A a2 ⟶ b1 ≡ B b2 ⟶ (a1 ,,h b1) ≡ (A & B) (a2 ,, b2)❙ 
  
  /T Distributivity is natural but makes it harder to devise algorithms for subtyping.❙
  st_distrib: {A,B,C} (A → B) & (A → C) < A → (B & C)❙
  st_distrib_0 : {A} ⊤ < (A → ⊤)❙

  top_arrow : ⊤ < (⊤ → ⊤)❘= st_distrib_0 ⊤❙
  
  ## Literals❙

  nat  : tp❙
  zero : tm nat❙
  succ : tm nat ⟶ tm nat❙

  /T import lexing and computation rules for literals❙ 
  
  rule lfrules?Realize (tm nat) stdlit?StandardNat❙
  rule lfrules?Realize zero stdlit?Arithmetic/Zero❙
  rule lfrules?Realize succ stdlit?Arithmetic/Succ❙

  # Testing❙
  
  identity : {A} tm A → A ❘ = [A] λ [x] x❘# id 1❙
  compose  : {A,B,C} tm A → B ⟶ tm B → C ⟶ tm A → C❘
           = [A,B,C,f,g] λ[x] g @ (f @ x)❙
    
  test: (id nat) @ (succ 1) ≡ nat 2❘= beta ([x] x) 2❙

❚