Library env
Typing Environment for annotated terms .
As for Terms, we define contexts of "Annotated" terms, with the very safe function and tools as for the usual one.
Require Import base term.
Require Import List.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt Le Gt.
Module Type env_mod (X:term_sig) (TM:term_mod X).
Import TM.
Require Import List.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt Le Gt.
Module Type env_mod (X:term_sig) (TM:term_mod X).
Import TM.
Very naive definition of environment : list of term
be carefull, the usual written env Γ(x:A) is encoded in A::Γ
be carefull, the usual written env Γ(x:A) is encoded in A::Γ
Definition Env := list Term.
Inductive item (A:Type) (x:A): list A ->nat->Prop :=
| item_hd: forall l:list A, (item x (cons x l) O)
| item_tl: forall (l:list A)(n:nat)(y:A), item x l n -> item x (cons y l) (S n).
Hint Constructors item.
Notation " x ↓ n ∈ Γ " := (item x Γ n) (at level 80, no associativity) : Typ_scope.
Lemma fun_item: forall A (u v:A)(Γ:list A)(n:nat),
u ↓ n ∈ Γ -> v ↓ n ∈ Γ -> u=v.
Inductive trunc (A:Type) : nat->list A ->list A->Prop :=
trunc_O: forall (Γ:list A) , (trunc O Γ Γ)
| trunc_S: forall (k:nat)(Γ Γ':list A)(x:A), trunc k Γ Γ'
-> trunc (S k) (cons x Γ) Γ'.
Hint Constructors trunc.
Lemma item_trunc: forall (A:Type) (n:nat) (Γ:list A) (t:A),
t ↓ n ∈ Γ -> exists f , trunc (S n) Γ f.
insert a type d1 in an env Γ : BE CAREFULL d1 is not checked to be a valid type in Γ
it takes care of the DeBruijn lift when need
Inductive ins_in_env (Γ:Env ) (d1:Term): nat->Env -> Env ->Prop :=
| ins_O: ins_in_env Γ d1 O Γ (d1::Γ)
| ins_S: forall (n:nat)(Δ Δ':Env )(d:Term), (ins_in_env Γ d1 n Δ Δ')
-> ins_in_env Γ d1 (S n) (d::Δ) ( (d ↑ 1 # n)::Δ' ).
Hint Constructors ins_in_env.
Lemma ins_item_ge: forall (d':Term) (n:nat) (Γ Δ Δ':Env),
ins_in_env Γ d' n Δ Δ' ->
forall (v:nat), n<=v ->
forall (d:Term), d ↓ v ∈ Δ -> d ↓ (S v) ∈ Δ'.
Lemma gt_O: forall v, ~ 0 > v.
Lemma ins_item_lt: forall (d':Term)(n:nat)(Γ Δ Δ':Env),
ins_in_env Γ d' n Δ Δ' ->
forall (v:nat), n > v ->
forall (d:Term), d ↓ v ∈ Δ -> (d ↑ 1 # (n-S v)) ↓ v ∈ Δ' .
Definition item_lift (t:Term) (Γ:Env) (n:nat) :=
exists u , t= u ↑ (S n) /\ u ↓ n ∈ Γ .
Hint Unfold item_lift.
Notation " t ↓ n ⊂ Γ " := (item_lift t Γ n) (at level 80, no associativity): Typ_scope.
Lemma ins_item_lift_lt: forall (d':Term)(n:nat)(Γ Δ Δ':Env ),
ins_in_env Γ d' n Δ Δ' ->
forall (v:nat), n>v ->
forall (t:Term), t ↓ v ⊂ Δ -> (t ↑ 1 # n) ↓ v ⊂ Δ'.
| ins_O: ins_in_env Γ d1 O Γ (d1::Γ)
| ins_S: forall (n:nat)(Δ Δ':Env )(d:Term), (ins_in_env Γ d1 n Δ Δ')
-> ins_in_env Γ d1 (S n) (d::Δ) ( (d ↑ 1 # n)::Δ' ).
Hint Constructors ins_in_env.
Lemma ins_item_ge: forall (d':Term) (n:nat) (Γ Δ Δ':Env),
ins_in_env Γ d' n Δ Δ' ->
forall (v:nat), n<=v ->
forall (d:Term), d ↓ v ∈ Δ -> d ↓ (S v) ∈ Δ'.
Lemma gt_O: forall v, ~ 0 > v.
Lemma ins_item_lt: forall (d':Term)(n:nat)(Γ Δ Δ':Env),
ins_in_env Γ d' n Δ Δ' ->
forall (v:nat), n > v ->
forall (d:Term), d ↓ v ∈ Δ -> (d ↑ 1 # (n-S v)) ↓ v ∈ Δ' .
Definition item_lift (t:Term) (Γ:Env) (n:nat) :=
exists u , t= u ↑ (S n) /\ u ↓ n ∈ Γ .
Hint Unfold item_lift.
Notation " t ↓ n ⊂ Γ " := (item_lift t Γ n) (at level 80, no associativity): Typ_scope.
Lemma ins_item_lift_lt: forall (d':Term)(n:nat)(Γ Δ Δ':Env ),
ins_in_env Γ d' n Δ Δ' ->
forall (v:nat), n>v ->
forall (t:Term), t ↓ v ⊂ Δ -> (t ↑ 1 # n) ↓ v ⊂ Δ'.
if Γ == Γ1 (x:T) Γ2 and Γ1 ⊢ t:T and Γ1 as size n
then Γn← t = Γ1 (Γ2x ← t)
Inductive sub_in_env (Γ : Env) (t T:Term):
nat -> Env -> Env -> Prop :=
| sub_O : sub_in_env Γ t T 0 (T :: Γ) Γ
| sub_S :
forall Δ Δ' n B,
sub_in_env Γ t T n Δ Δ' ->
sub_in_env Γ t T (S n) (B :: Δ) ( B [n← t] :: Δ').
Hint Constructors sub_in_env.
Lemma nth_sub_sup :
forall n Γ Δ Δ' t T,
sub_in_env Γ t T n Δ Δ' ->
forall v : nat, n <= v ->
forall d , d ↓ (S v) ∈ Δ -> d ↓ v ∈ Δ'.
Lemma nth_sub_eq :
forall t T n Γ Δ Δ',
sub_in_env Γ t T n Δ Δ' ->
forall d , d↓ n ∈ Δ -> T = d.
Lemma nth_sub_inf :
forall t T n Γ Δ Δ',
sub_in_env Γ t T n Δ Δ' ->
forall v : nat,
n > v ->
forall d , d ↓ v ∈ Δ -> ( d [n - S v ← t] )↓ v ∈ Δ' .
Lemma nth_sub_item_inf :
forall t T n g e f , sub_in_env g t T n e f ->
forall v : nat, n > v ->
forall u , item_lift u e v -> item_lift (subst_rec t u n) f v.
End env_mod.