Library Lambda.JRussell.Freevars


Require
 Import
 Lambda.Terms.

Require
 Import
 Lambda.LiftSubst.

Require
 Import
 Lambda.Reduction.

Require
 Import
 Lambda.Conv.

Require
 Import
 Lambda.Env.

Require
 Import
 Lambda.JRussell.Types.







Implicit
 Types
 i
 k
 m
 n
 p
 : nat.

Implicit
 Type
 s
 : sort.

Implicit
 Types
 A
 B
 M
 N
 T
 t
 u
 v
 : term.




Lemma
 free_db_lift1_rec : ∀ n
 t
, free_db n
 t
 → ∀ k
, free_db (S n
) (lift_rec 1 t
 k
).




Lemma
 free_db_lift1 : ∀ n
 t
, free_db n
 t
 → free_db (S n
) (lift 1 t
).




Hint
 Resolve
 free_db_lift1 : coc
.




Lemma
 free_db_lift_rec : ∀ n
 t
, free_db n
 t
 → ∀ n'
 k
, free_db (n'
 + n
) (lift_rec n'
 t
 k
).




Require
 Import
 Omega.

Require
 Import
 Arith.




Lemma
 term_free_db : ∀ e
 t
 T
, e
 |-= t
 : T
 → free_db (length e
) t
.




Hint
 Resolve
 term_free_db : coc
.




  Lemma
 free_db_subst_rec : ∀ t
 n
, free_db (S n
) t
 → 

    ∀ m
 t'
, free_db m
 t'
 → n
 ≥ m
 → free_db n
 (subst_rec t'
 t
 (n
 - m
)).




Lemma
 free_db_subst : ∀ t
 n
, free_db (S n
) t
 → 

 ∀ t'
, free_db n
 t'
→ free_db n
 (subst t'
 t
).




Lemma
 type_free_db : 

  (∀ e
 t
 T
, e
 |-= t
 : T
 → free_db (length e
) T
) ∧

  (∀ e
 U
 V
 s
, e
 |-= U
 >> V
 : s
 → free_db (length e
) U
 ∧ free_db (length e
) V
) ∧

  (∀ e
 U
 V
 T
, e
 |-= U
 = V
 : T
 → free_db (length e
) U
 ∧ free_db (length e
) V
).




Lemma
 typ_free_db : ∀ e
 t
 T
, e
 |-= t
 : T
 → free_db (length e
) T
.




Lemma
 coerce_free_db : ∀ e
 T
 U
 s
, e
 |-= T
 >> U
 : s
 → free_db (length e
) T
 ∧ free_db (length e
) U
.




Lemma
 jeq_free_db : ∀ e
 U
 V
 T
 , e
 |-= U
 = V
 : T
 → free_db (length e
) U
 ∧ free_db (length e
) V
.