Annotated typ_open_types

typ_open_types.md

Annotated:

Lemma typ_open_types : forall T Us,
  typ_body (length Us) T ->

Definition typ_body n T := exists L, forall Xs, fresh L n Xs -> type (typ_open_vars T Xs).

  types (length Us) Us ->

Definition types := list_for_n type.

Definition list_for_n (A : Set) (P : A -> Prop) (n : nat) (L : list A) := n = length L /\ list_forall P L.

  type (typ_open T Us).
Proof.
  introv [L K] WT.

L : vars (a.k.a. FinSet)

K : forall Xs, fresh L (length Us) Xs -> type (typ_open_vars T Xs)

WT : types (length Us) Us

  pick_freshes (length Us) Xs.

Creates an assumption named Fr defined as the union of all finite sets of variables in the context for some list. That is, because destruct (var_freshes L n) as [Y Fr] and Lemma var_freshes : forall L n, { xs : list var | fresh L n xs }., we have:

Fr : fresh (...) (length Us) Xs

where (...) is the union of all finite sets of variables.

  poses Fr' Fr.

Copies Fr to Fr'.

  rewrite (fresh_length _ _ _  Fr) in WT, Fr'.

Lemma fresh_length : forall xs L n, fresh L n xs -> n = length xs.

fresh_length _ _ _ Fr : length Us = length Xs

WT : types (length Xs) Us

Fr' : fresh (...) (length Xs) Xs

  rewrite* (@typ_substs_intro Xs).

Lemma typ_substs_intro : forall Xs Us T,

fresh (typ_fv T \u typ_fv_list Us) (length Xs) Xs ->

• Resolved by Fr'.

types (length Xs) Us ->

• Resolved by WT.

(typ_open T Us) = typ_substs Xs Us (typ_open_vars T Xs).

• New goal: type (typ_substs Xs Us (typ_open_vars T Xs))

  apply* typ_substs_types.

Lemma typ_substs_types : forall Xs Us T,

types (length Xs) Us ->

• Resolved by WT.

type T ->

• Expected: type (typ_open_vars T Xs). Resolved by K.
• Subgoal for K: fresh L n Xs. Resolved by Fr.

type (typ_substs Xs Us T).

Qed.