syn_lemmas.v

(** * Free-variable lemmas for DOT.
To limit compile times, do not load this file in unary_lr. *)
From D.Dot Require Import syn.

Implicit Types
         (L T U : ty) (v : vl) (e : tm) (d : dm) (ds : dms)
         (Γ : ctx) (ρ : vls).

(** Here is a manual proof of [fv_vabs_inv], with explanations, as
documentation for [solve_inv_fv_congruence]. *)
Lemma fv_vabs_inv_manual e n : nclosed_vl (vabs e) n → nclosed e n.+1.
Proof.
  rewrite /nclosed_vl /nclosed => /= Hfv s1 s2 HsEq.

  (* From [Hfv], we only learn that [e.|[up s1] = e.|[up s2]], for arbitrary
  [s1] and [s2], but substitutions in our thesis [e.|[s1] = e.|[s2]] are not
  of form [up ?]. Hence, we rewrite it using [decomp_s] / [decomp_s_vl] to
  get a substitution of form [up ?], then rewrite with [e.|[up (stail s1)] =
  e.|[up (stail s2)]] (got from [Hfv]), and conclude.
      *)
  rewrite ?(decomp_s _ s1) ?(decomp_s _ s2) ?(decomp_s_vl _ s1) ?(decomp_s_vl _ s2) (eq_n_s_heads HsEq); last lia.
  injection (Hfv _ _ (eq_n_s_tails HsEq)); rewritePremises; reflexivity.
Qed.

(** The following ones are "direct" lemmas: deduce that an expression is closed
    by knowing that its subexpression are closed. *)

Lemma fv_vabs_inv e n : nclosed_vl (vabs e) n → nclosed e n.+1.
Proof. solve_inv_fv_congruence. Qed.