RefinementTypes.SyntacticSubtyping

Syntactic Subtyping (Figure 10)

Inductive subtyping judgment Γ ⊢ A <: B mirroring the semantic subtyping rules; each constructor corresponds to a rule of Figure 10 and to the lemma of the same name in SemanticSubtyping. Adequacy is Theorem 3.2, proved in Adequacy. Note that the S-Refine premise uses the semantic implication judgment sem_implies, which has no syntactic counterpart.

From Stdlib Require Import Lists.List.
Import ListNotations.
Require Import RefinementTypes.Syntax.
Require Import RefinementTypes.Subst.
Require Import RefinementTypes.Wf.
Require Import RefinementTypes.WfLemmas.
Require Import RefinementTypes.Positivity.
Require Import RefinementTypes.SemanticImplies.

Inductive syn_subtype (tbounds: TBounds) (tenv: list Ty)
  (facts: list ((nat × Term ) × (nat × Term ))) : Ty → Ty → Prop :=

  | SSub_Refl : ∀ A,
      syn_subtype tbounds tenv facts A A

  | SSub_Trans : ∀ A B C,
      syn_subtype tbounds tenv facts A B →
      syn_subtype tbounds tenv facts B C →
      syn_subtype tbounds tenv facts A C

  | SSub_Fun : ∀ A1 A2 B1 B2,
      syn_subtype tbounds tenv facts B1 A1 →
      syn_subtype (tbounds_shift_term tbounds) (A1 :: tenv) facts A2 B2 →
      syn_subtype tbounds tenv facts (TFun A1 A2) (TFun B1 B2)

  | SSub_Forall : ∀ L1 U1 L2 U2 A B,
      syn_subtype tbounds tenv facts L1 L2 →
      syn_subtype tbounds tenv facts U2 U1 →
      syn_subtype ((L2 , U2 ) :: tbounds) (tenv_shift_type tenv) facts A B →
      syn_subtype tbounds tenv facts (TForall L1 U1 A) (TForall L2 U2 B)

  | SSub_Sigma : ∀ A1 A2 B1 B2,
      syn_subtype tbounds tenv facts A1 B1 →
      syn_subtype (tbounds_shift_term tbounds) (A1 :: tenv) facts A2 B2 →
      syn_subtype tbounds tenv facts (TSigma A1 A2) (TSigma B1 B2)

  | SSub_Or_L : ∀ A B,
      syn_subtype tbounds tenv facts A (TOr A B)

  | SSub_Or_R : ∀ A B,
      syn_subtype tbounds tenv facts B (TOr A B)

  | SSub_Or : ∀ A B C,
      syn_subtype tbounds tenv facts A C →
      syn_subtype tbounds tenv facts B C →
      syn_subtype tbounds tenv facts (TOr A B) C

  | SSub_And_L : ∀ A B,
      syn_subtype tbounds tenv facts (TAnd A B) A

  | SSub_And_R : ∀ A B,
      syn_subtype tbounds tenv facts (TAnd A B) B

  | SSub_And : ∀ A B C,
      syn_subtype tbounds tenv facts C A →
      syn_subtype tbounds tenv facts C B →
      syn_subtype tbounds tenv facts C (TAnd A B)

  | SSub_Refine_Base : ∀ A p,
      syn_subtype tbounds tenv facts (TRefine A p) A

  | SSub_Refine : ∀ A B p1 p2,
      syn_subtype tbounds tenv facts A B →
      sem_implies (tbounds_shift_term tbounds) (A :: tenv) facts p1 p2 →
      syn_subtype tbounds tenv facts (TRefine A p1) (TRefine B p2)

  | SSub_Top : ∀ A,
      syn_subtype tbounds tenv facts A TTop

  | SSub_Bot : ∀ A,
      syn_subtype tbounds tenv facts TBot A

  | SSub_TVar_Upper : ∀ i L U,
      nth_error tbounds i = Some (L , U ) →
      syn_subtype tbounds tenv facts (TVar i) (ren_ty (fun n ⇒ n + S i) id U)

  | SSub_TVar_Lower : ∀ i L U,
      nth_error tbounds i = Some (L , U ) →
      syn_subtype tbounds tenv facts (ren_ty (fun n ⇒ n + S i) id L) (TVar i)

  | SSub_Mu_Unfold : ∀ A,
      spos 0 A = true →
      syn_subtype tbounds tenv facts (TMuAll A) (ty_subst A (TMuAll A))

  | SSub_Mu_Fold : ∀ A,
      spos 0 A = true →
      syn_subtype tbounds tenv facts (ty_subst A (TMuAll A)) (TMuAll A).