nu type

nu-ty.v

Inductive LatticeExpr {T} :=
  | LAtom (t: T)
  | LTop
  | LIntersection (t0: LatticeExpr) (t1: LatticeExpr)
  | LBottom
  | LUnion (t0: LatticeExpr) (t1: LatticeExpr).
Arguments LatticeExpr T: clear implicits.

CoInductive ATy :=
  | TyNumber
  | TyArg (n: nat)
  | TyArrow (t0: LatticeExpr ATy) (t1: LatticeExpr ATy).
Definition Ty := LatticeExpr ATy.

Record TyEnv := {
  constraints: ATy -> ATy -> Prop;
}.

Inductive LatticeLe {T} (R: T -> T -> Prop): LatticeExpr T -> LatticeExpr T -> Prop :=
  | LRefl x: LatticeLe R x x
  | LTrans x y z: LatticeLe R x y -> LatticeLe R y z -> LatticeLe R x z
  | LAtomLe x y: R x y -> LatticeLe R (LAtom x) (LAtom y)
  | LTopLeR x: LatticeLe R x LTop
  | LIntersectionLeR x y0 y1: LatticeLe R x y0 -> LatticeLe R x y1 -> LatticeLe R x (LIntersection y0 y1)
  | LBottomLeL y: LatticeLe R LBottom y
  | LUnionLeL x0 x1 y: LatticeLe R x0 y -> LatticeLe R x1 y -> LatticeLe R (LUnion x0 x1) y
  | LIntersectionLeL0 x0 x1 y: LatticeLe R x0 y -> LatticeLe R (LIntersection x0 x1) y
  | LIntersectionLeL1 x0 x1 y: LatticeLe R x1 y -> LatticeLe R (LIntersection x0 x1) y
  | LUnionLeR0 x y0 y1: LatticeLe R x y0 -> LatticeLe R x (LUnion y0 y1)
  | LUnionLeR1 x y0 y1: LatticeLe R x y1 -> LatticeLe R x (LUnion y0 y1).

CoInductive ATyLe {Env: TyEnv}: ATy -> ATy -> Prop :=
  | TyLeNumber: ATyLe TyNumber TyNumber
  | TyLeArg n: ATyLe (TyArg n) (TyArg n)
  | TyLeArrow t00 t01 t10 t11:
      LatticeLe ATyLe t10 t00 ->
      LatticeLe ATyLe t01 t11 ->
      ATyLe (TyArrow t00 t01) (TyArrow t10 t11)
  | TyLeAxiom t0 t1: Env.(constraints) t0 t1 -> ATyLe t0 t1.

Definition TyLe {Env: TyEnv} := LatticeLe (@ATyLe Env).