theorem CheckInvUnderAdd {x : Char} {m : Term} {nc : CurryType × TypeCtx} (pair pair' : PrincipalPair) (hxm : Term.var x ≠ m) (hl : pair'.ctx.lookup x = none) (hn : nc = next pair'.ctx) (hp : pair.ctx = add x nc.1 nc.2) (hp' : check pair'.ctx m = some pair'.ty) : check pair.ctx m = some pair'.ty

If a variable x is absent from pair'.ctx and pair.ctx extends pair'.ctx with a binding for x, then type-checking any term m (where Term.var x ≠ m) in pair.ctx yields the same result as in pair'.ctx. In other words, adding an unused variable to the context does not affect checking.

theorem LookupMap {x : Char} {y : CurryType} {xys : List (Char × CurryType)} (s : CurryType → CurryType) (hc : List.lookup x xys = some y) : List.lookup x (List.map (fun (xy : Char × CurryType) => (xy.1, s xy.2)) xys) = some (s y)

List.lookup commutes with mapping a function over the values: looking up x in a mapped list returns the mapped value.

theorem CheckSubst (t : Term) (ty : CurryType) (s : CurryType → CurryType) (ctx : TypeCtx) (hc : check ctx t = some ty) {h_arrow : ∀ (a b : CurryType), s (a.arrow b) = (s a).arrow (s b)} : check (applySubst s ctx) t = some (s ty)

Applying a type substitution s to every type in a context maps a successful check result covariantly: if check ctx t = some ty then check (applySubst s ctx) t = some (s ty).

theorem SubstComp (f g : CurryType → CurryType) (ctx : TypeCtx) : applySubst f (applySubst g ctx) = applySubst (f ∘ g) ctx

Composing two substitution applications is the same as applying their functional composition. That is, applySubst f (applySubst g ctx) = applySubst (f ∘ g) ctx.

theorem CheckInvUnderLabel (t : Term) (ctx ctx' : TypeCtx) (henv : ctx.env = ctx'.env) : check ctx t = check ctx' t

check depends only on the env field of TypeCtx and ignores the label (fresh-variable counter). Two contexts with equal environments yield identical check results for any term.

theorem CheckInvUnderNextSubst (ctx : TypeCtx) (f : CurryType → CurryType) (m : Term) : check (applySubst f ctx) m = check (applySubst f (next ctx).2) m

Applying a substitution to a context and then advancing to the next fresh variable yields the same check result as applying the substitution to the already-advanced context. In other words, applySubst and next commute as far as check is concerned. This is a corollary of CheckInvUnderLabel.

theorem EnvInvUnderSubst (ctx ctx' : TypeCtx) (fce : ctx.env = ctx'.env) (f : CurryType → CurryType) : (applySubst f ctx).env = (applySubst f ctx').env

applySubst preserves the env field of a context (up to value substitution), so two contexts with equal environments produce equal environments after the same substitution.

theorem UnifySound (t1 t2 : CurryType) (s : Subst t1 t2) : unify t1 t2 = some s → s.apply t1 = s.apply t2

Soundness of unify: if unify t1 t2 returns a substitution s, then s is indeed a unifier, i.e. s.apply t1 = s.apply t2.

theorem SubstMap {α β : CurryType} {ctx1 ctx2 : TypeCtx} {ab a b : CurryType} (s1 : Subst α β) (s2 : CtxSubst ctx1 ctx2) (hs : s1.apply ab = (s1.apply a).arrow (s1.apply b)) : (s2.apply ∘ s1.apply) ab = ((s2.apply ∘ s1.apply) a).arrow ((s2.apply ∘ s1.apply) b)

If a Subst s1 distributes over arrows (i.e. s1.apply ab = (s1.apply a).arrow (s1.apply b)), then composing with a CtxSubst s2 preserves this arrow structure.

theorem InferenceSubsetMap (ctx ctx' : TypeCtx) (m : Term) (ty : CurryType) (hpp : pp' ctx m = some { ctx := ctx', ty := ty }) : ∃ (f : CurryType → CurryType), (applySubst f ctx).env ⊆ ctx'.env

If pp' ctx m = some ⟨ctx', ty⟩, then there exists a substitution f such that (applySubst f ctx).env ⊆ ctx'.env. In other words, the inference output context contains the input context (up to substitution).

theorem NextFresh (x y : Char) (ty : CurryType) (ctx : TypeCtx) {hxy : x ≠ y} : ctx.lookup x = some ty ↔ (add y (next ctx).1 (next ctx).2).lookup x = some ty

theorem SubstLookup (f : CurryType → CurryType) (ctx : TypeCtx) (x : Char) (ty : CurryType) : ctx.lookup x = some ty → (applySubst f ctx).lookup x = some (f ty)

SubstLookup: applying a substitution to a context preserves lookup results up to f. This is a convenience wrapper around LookupMap.

def distributes (f : CurryType → CurryType) : Prop

distributes f: predicate asserting that f distributes over arrow types, i.e. f (a → b) = f(a) → f(b). Required by CheckSubst.

Equations

• distributes f = ∀ (a b : CurryType), f (a.arrow b) = (f a).arrow (f b)

def lookup_inv (f : CurryType → CurryType) (ctx ctx' : TypeCtx) : Prop

lookup_inv f ctx ctx': predicate asserting that f is a lookup invariant from ctx to ctx', i.e. for every variable x with type ty in ctx, ctx' assigns f ty to x.

Equations

• lookup_inv f ctx ctx' = ∀ (x : Char) (ty : CurryType), ctx.lookup x = some ty → ctx'.lookup x = some (f ty)

def check_inv (f : CurryType → CurryType) (ctx ctx' : TypeCtx) : Prop

check_inv f ctx ctx': predicate asserting that f is a check invariant from ctx to ctx', i.e. for every term t with type ty under ctx, ctx' assigns f ty to t.

Equations

• check_inv f ctx ctx' = ∀ (t : Term) (ty : CurryType), check ctx t = some ty → check ctx' t = some (f ty)

def equiv_lookup_on (f g : CurryType → CurryType) (ctx : TypeCtx) : Prop

equiv_lookup_on f g ctx: f and g agree on types of variables actually occurring in ctx, i.e. for all x with ctx.lookup x = some ty, g ty = f ty.

Equations

• equiv_lookup_on f g ctx = ∀ (x : Char) (ty : CurryType), ctx.lookup x = some ty → g ty = f ty

def equiv_check_on (f g : CurryType → CurryType) (ctx : TypeCtx) : Prop

equiv_check_on f g ctx: f and g agree on types of terms that type-check under ctx, i.e. for all t with check ctx t = some ty, g ty = f ty.

Equations

• equiv_check_on f g ctx = ∀ (x : Term) (ty : CurryType), check ctx x = some ty → g ty = f ty

theorem InferenceLookupInv {_ty : CurryType} (ctx ctx' : TypeCtx) (m : Term) (hpp : pp' ctx m = some { ctx := ctx', ty := _ty }) : ∃ (f : CurryType → CurryType), lookup_inv f ctx ctx' ∧ distributes f ∧ ∀ (g : CurryType → CurryType), lookup_inv g ctx ctx' → equiv_lookup_on f g ctx

InferenceLookupInv: if pp' ctx m = some ⟨ctx', _⟩, then there exists a canonical substitution f (distributing over arrows) that is a lookup invariant from ctx to ctx', and it is unique in the sense that any other lookup invariant g agrees with f on types occurring in ctx.

theorem InferenceCheckInv {_ty : CurryType} (ctx ctx' : TypeCtx) (m : Term) (hpp : pp' ctx m = some { ctx := ctx', ty := _ty }) : ∃ (f : CurryType → CurryType), check_inv f ctx ctx' ∧ distributes f ∧ ∀ (g : CurryType → CurryType), check_inv g ctx ctx' → equiv_check_on f g ctx

InferenceCheckInv: if pp' ctx m = some ⟨ctx', _⟩, then there exists a canonical substitution f (distributing over arrows) that is a check invariant from ctx to ctx', and it is unique among check invariants in that any other g agrees with f on types of terms typeable under ctx.

def occursInTerm (x : Char) : Term → Prop

occursInTerm x t: proposition that variable x occurs (free or bound as a name) in term t.

Equations

• occursInTerm x (Term.var y) = (x = y)
• occursInTerm x (Term.abs y m) = (x = y ∨ occursInTerm x m)
• occursInTerm x (m.app n) = (occursInTerm x m ∨ occursInTerm x n)

theorem CheckEqIfOccursInv (t : Term) (ctx1 ctx2 : TypeCtx) : (∀ (x : Char), occursInTerm x t → ctx1.lookup x = ctx2.lookup x) → check ctx1 t = check ctx2 t

CheckEqIfOccursInv: if two contexts agree on the types of all variables occurring in t, then check ctx1 t = check ctx2 t.

theorem CheckSuccessLookupSome (t : Term) (ctx : TypeCtx) (ty : CurryType) : check ctx t = some ty → ∀ (x : Char), occursInTerm x t → ∃ (ty' : CurryType), ctx.lookup x = some ty'

CheckSuccessLookupSome: if check ctx t = some ty, then every variable occurring in t has a type in ctx.

theorem LookupThenIn {α β : Type} [BEq α] [LawfulBEq α] {x : α} {y : β} {l : List (α × β)} (h : List.lookup x l = some y) : (x, y) ∈ l

theorem FoldlInv (es : List ExSubst) (f : CurryType → CurryType) (a b : CurryType) (h : f a = f b) : List.foldl (fun (acc : CurryType → CurryType) (ex : ExSubst) => ex.cast ∘ acc) f es a = List.foldl (fun (acc : CurryType → CurryType) (ex : ExSubst) => ex.cast ∘ acc) f es b

theorem UnifyCtxSound (l : List (Char × CurryType × CurryType)) (exs : List ExSubst) : unifyCtx' l = some exs → ∀ (x : Char) (a b : CurryType), (x, a, b) ∈ l → have F := List.foldl (fun (acc : CurryType → CurryType) (ex : ExSubst) => ex.cast ∘ acc) id exs; F a = F b

theorem UnifyCtxMapCommon {ctx1 ctx2 : TypeCtx} {s : CtxSubst ctx1 ctx2} (h : unifyCtx ctx1 ctx2 = some s) (x : Char) (ty1 ty2 : CurryType) (h1 : ctx1.lookup x = some ty1) (h2 : ctx2.lookup x = some ty2) : s.apply ty1 = s.apply ty2

UnifyCtxMapCommon: if unifyCtx ctx1 ctx2 = some s, then for any variable x whose type is ty1 in ctx1 and ty2 in ctx2, the substitution s unifies them: s.apply ty1 = s.apply ty2. This is the soundness property of unifyCtx.

theorem InferenceSound' (t : Term) (ctx : TypeCtx) (pair : PrincipalPair) : pp' ctx t = some pair → WellTyped pair.ctx t pair.ty

Soundness of the principal-type algorithm helper pp': if pp' ctx t = some pair, then t is well-typed in pair.ctx with type pair.ty, i.e. check pair.ctx t = some pair.ty.

theorem InferenceSound (t : Term) (pair : PrincipalPair) : pp t = some pair → WellTyped pair.ctx t pair.ty

Soundness of the principal-type algorithm pp: if pp t = some pair, then t is well-typed in pair.ctx with type pair.ty. This is the top-level soundness statement.