Library f_env

Typing Environment Definition and Function Manipulation.

Require Import base f_term.

Require Import List.

Require Import Peano_dec.

Require Import Compare_dec.

Require Import Lt Le Gt Plus.

Module Type f_env_mod (X: term_sig) (TM: f_term_mod X).

Interactive Module Type f_env_mod started

Import TM.

Since we use de Bruijn indexes, Environment (or Context) are simply lists of terms: Γ,(x:A) is encoded as A::Γ.

Definition Env := list Term.

Env is defined

Some manipulation functions (mostly from Bruno Barras' PTS contrib):

how to find an item in the environment
how to truncate an environment
how to insert a new element (with correct de Bruijn update)
how to substitute something in the environment

Set Implicit Arguments.

  Inductive item (A:Type) (x:A): list A ->nat->Prop :=
  | item_hd: forall Γ :list A, (item x (cons x Γ) O)
  | item_tl: forall (Γ:list A)(n:nat)(y:A), item x Γ n -> item x (cons y Γ) (S n).

item is defined
item_ind is defined

Hint Constructors item.

In the list Γ, the nth item is syntacticaly x.

Notation " x ↓ n ∈ Γ " := (item x Γ n) (at level 80, no associativity) : F_scope.

Lemma fun_item: forall T (A B:T)(Γ:list T)(n:nat),
A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B.

1 subgoals, subgoal 1 (ID 7)
  
  ============================
   forall (T : Type) (A B : T) (Γ : list T) (n : nat),
   A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B

(dependent evars:)

intros T A B Γ n;revert T A B Γ.

1 subgoals, subgoal 1 (ID 14)
  
  n : nat
  ============================
   forall (T : Type) (A B : T) (Γ : list T), A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B

(dependent evars:)

induction n; intros.

2 subgoals, subgoal 1 (ID 26)
  
  T : Type
  A : T
  B : T
  Γ : list T
  H : A ↓ 0 ∈ Γ
  H0 : B ↓ 0 ∈ Γ
  ============================
   A = B

subgoal 2 (ID 32) is:
 A = B
(dependent evars:)

inversion H; inversion H0.

2 subgoals, subgoal 1 (ID 77)
  
  T : Type
  A : T
  B : T
  Γ : list T
  H : A ↓ 0 ∈ Γ
  H0 : B ↓ 0 ∈ Γ
  Γ0 : list T
  H1 : A :: Γ0 = Γ
  Γ1 : list T
  H2 : B :: Γ1 = Γ
  ============================
   A = B

subgoal 2 (ID 32) is:
 A = B
(dependent evars:)

rewrite <- H2 in H1; injection H1; trivial.

1 subgoals, subgoal 1 (ID 32)
  
  n : nat
  IHn : forall (T : Type) (A B : T) (Γ : list T),
        A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B
  T : Type
  A : T
  B : T
  Γ : list T
  H : A ↓ S n ∈ Γ
  H0 : B ↓ S n ∈ Γ
  ============================
   A = B

(dependent evars:)

inversion H; inversion H0; subst.

1 subgoals, subgoal 1 (ID 207)
  
  n : nat
  IHn : forall (T : Type) (A B : T) (Γ : list T),
        A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B
  T : Type
  A : T
  B : T
  Γ0 : list T
  y : T
  H3 : A ↓ n ∈ Γ0
  Γ1 : list T
  y0 : T
  H6 : B ↓ n ∈ Γ1
  H : A ↓ S n ∈ y :: Γ0
  H0 : B ↓ S n ∈ y :: Γ0
  H5 : y0 :: Γ1 = y :: Γ0
  ============================
   A = B

(dependent evars:)

injection H5; intros; subst.

1 subgoals, subgoal 1 (ID 228)
  
  n : nat
  IHn : forall (T : Type) (A B : T) (Γ : list T),
        A ↓ n ∈ Γ -> B ↓ n ∈ Γ -> A = B
  T : Type
  A : T
  B : T
  Γ0 : list T
  y : T
  H3 : A ↓ n ∈ Γ0
  H : A ↓ S n ∈ y :: Γ0
  H0 : B ↓ S n ∈ y :: Γ0
  H6 : B ↓ n ∈ Γ0
  H5 : y :: Γ0 = y :: Γ0
  ============================
   A = B

(dependent evars:)

apply IHn with (Γ:=Γ0); trivial.

No more subgoals.
(dependent evars:)

Qed.

fun_item is defined

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 Γ) Γ'.

trunc is defined
trunc_ind is defined

Hint Constructors trunc.

Lemma item_trunc: forall (T:Type) (n:nat) (Γ:list T) (t:T),
t ↓ n ∈ Γ -> exists Γ' , trunc (S n) Γ Γ'.

1 subgoals, subgoal 1 (ID 236)
  
  ============================
   forall (T : Type) (n : nat) (Γ : list T) (t : T),
   t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'

(dependent evars:)

intros T n; induction n; intros.

2 subgoals, subgoal 1 (ID 247)
  
  T : Type
  Γ : list T
  t : T
  H : t ↓ 0 ∈ Γ
  ============================
   exists Γ' : list T, trunc 1 Γ Γ'

subgoal 2 (ID 250) is:
 exists Γ' : list T, trunc (S (S n)) Γ Γ'
(dependent evars:)

inversion H.

2 subgoals, subgoal 1 (ID 265)
  
  T : Type
  Γ : list T
  t : T
  H : t ↓ 0 ∈ Γ
  Γ0 : list T
  H0 : t :: Γ0 = Γ
  ============================
   exists Γ' : list T, trunc 1 (t :: Γ0) Γ'

subgoal 2 (ID 250) is:
 exists Γ' : list T, trunc (S (S n)) Γ Γ'
(dependent evars:)

exists Γ0.

2 subgoals, subgoal 1 (ID 291)
  
  T : Type
  Γ : list T
  t : T
  H : t ↓ 0 ∈ Γ
  Γ0 : list T
  H0 : t :: Γ0 = Γ
  ============================
   trunc 1 (t :: Γ0) Γ0

subgoal 2 (ID 250) is:
 exists Γ' : list T, trunc (S (S n)) Γ Γ'
(dependent evars:)

apply trunc_S; apply trunc_O.

1 subgoals, subgoal 1 (ID 250)
  
  T : Type
  n : nat
  IHn : forall (Γ : list T) (t : T),
        t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
  Γ : list T
  t : T
  H : t ↓ S n ∈ Γ
  ============================
   exists Γ' : list T, trunc (S (S n)) Γ Γ'

(dependent evars:)

inversion H; subst.

1 subgoals, subgoal 1 (ID 348)
  
  T : Type
  n : nat
  IHn : forall (Γ : list T) (t : T),
        t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
  t : T
  Γ0 : list T
  y : T
  H2 : t ↓ n ∈ Γ0
  H : t ↓ S n ∈ y :: Γ0
  ============================
   exists Γ' : list T, trunc (S (S n)) (y :: Γ0) Γ'

(dependent evars:)

destruct (IHn Γ0 t H2).

1 subgoals, subgoal 1 (ID 355)
  
  T : Type
  n : nat
  IHn : forall (Γ : list T) (t : T),
        t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
  t : T
  Γ0 : list T
  y : T
  H2 : t ↓ n ∈ Γ0
  H : t ↓ S n ∈ y :: Γ0
  x : list T
  H0 : trunc (S n) Γ0 x
  ============================
   exists Γ' : list T, trunc (S (S n)) (y :: Γ0) Γ'

(dependent evars:)

exists x.

1 subgoals, subgoal 1 (ID 357)
  
  T : Type
  n : nat
  IHn : forall (Γ : list T) (t : T),
        t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
  t : T
  Γ0 : list T
  y : T
  H2 : t ↓ n ∈ Γ0
  H : t ↓ S n ∈ y :: Γ0
  x : list T
  H0 : trunc (S n) Γ0 x
  ============================
   trunc (S (S n)) (y :: Γ0) x

(dependent evars:)

apply trunc_S.

1 subgoals, subgoal 1 (ID 358)
  
  T : Type
  n : nat
  IHn : forall (Γ : list T) (t : T),
        t ↓ n ∈ Γ -> exists Γ' : list T, trunc (S n) Γ Γ'
  t : T
  Γ0 : list T
  y : T
  H2 : t ↓ n ∈ Γ0
  H : t ↓ S n ∈ y :: Γ0
  x : list T
  H0 : trunc (S n) Γ0 x
  ============================
   trunc (S n) Γ0 x

(dependent evars:)

apply H0.

No more subgoals.
(dependent evars:)

Qed.

item_trunc is defined

Lemma trunc_inj : forall n (Γ Δ Δ':Env),trunc n Γ Δ->trunc n Γ Δ'->Δ =Δ'.

1 subgoals, subgoal 1 (ID 363)
  
  ============================
   forall (n : nat) (Γ Δ Δ' : Env), trunc n Γ Δ -> trunc n Γ Δ' -> Δ = Δ'

(dependent evars:)

induction n;inversion 1;inversion 1;subst;[reflexivity|eapply IHn;eassumption].

No more subgoals.
(dependent evars: ?631 using ,)

Qed.

trunc_inj is defined

Lemma trunc_trans : forall m n (Γ Γ1 Γ2:Env), trunc n Γ Γ1->trunc m Γ1 Γ2->trunc (m +n) Γ Γ2.

1 subgoals, subgoal 1 (ID 639)
  
  ============================
   forall (m n : nat) (Γ Γ1 Γ2 : Env),
   trunc n Γ Γ1 -> trunc m Γ1 Γ2 -> trunc (m + n) Γ Γ2

(dependent evars:)

induction n;inversion 1;intros;subst;simpl.

2 subgoals, subgoal 1 (ID 778)
  
  m : nat
  Γ1 : Env
  Γ2 : Env
  H0 : trunc m Γ1 Γ2
  H : trunc 0 Γ1 Γ1
  ============================
   trunc (m + 0) Γ1 Γ2

subgoal 2 (ID 779) is:
 trunc (m + S n) (x :: Γ0) Γ2
(dependent evars:)

rewrite plus_comm;assumption.

1 subgoals, subgoal 1 (ID 779)
  
  m : nat
  n : nat
  IHn : forall Γ Γ1 Γ2 : Env,
        trunc n Γ Γ1 -> trunc m Γ1 Γ2 -> trunc (m + n) Γ Γ2
  Γ1 : Env
  Γ2 : Env
  Γ0 : list Term
  x : Term
  H1 : trunc n Γ0 Γ1
  H4 : trunc m Γ1 Γ2
  H : trunc (S n) (x :: Γ0) Γ1
  ============================
   trunc (m + S n) (x :: Γ0) Γ2

(dependent evars:)

rewrite plus_comm;simpl;constructor;rewrite plus_comm;eapply IHn;eassumption.

No more subgoals.
(dependent evars: ?787 using ,)

Qed.

trunc_trans is defined

This type describe how do we add an element in an environment: no type checking is done, this is just the mecanic way to do it.

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 )::Δ' ).

ins_in_env is defined
ins_in_env_ind is defined

Hint Constructors ins_in_env.

Some lemmas about inserting a new element. They explain how terms in the environment are lifted according to their original position and the position of insertion.

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 ) ∈ Δ'.

1 subgoals, subgoal 1 (ID 795)
  
  ============================
   forall (d' : Term) (n : nat) (Γ Δ Δ' : Env),
   ins_in_env Γ d' n Δ Δ' ->
   forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'

(dependent evars:)

induction n; intros.

2 subgoals, subgoal 1 (ID 811)
  
  d' : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' 0 Δ Δ'
  v : nat
  H0 : 0 <= v
  d : Term
  H1 : d ↓ v ∈ Δ
  ============================
   d ↓ S v ∈ Δ'

subgoal 2 (ID 819) is:
 d ↓ S v ∈ Δ'
(dependent evars:)

inversion H; subst.

2 subgoals, subgoal 1 (ID 873)
  
  d' : Term
  Δ : Env
  v : nat
  H0 : 0 <= v
  d : Term
  H1 : d ↓ v ∈ Δ
  H : ins_in_env Δ d' 0 Δ (d' :: Δ)
  ============================
   d ↓ S v ∈ d' :: Δ

subgoal 2 (ID 819) is:
 d ↓ S v ∈ Δ'
(dependent evars:)

apply item_tl.

2 subgoals, subgoal 1 (ID 874)
  
  d' : Term
  Δ : Env
  v : nat
  H0 : 0 <= v
  d : Term
  H1 : d ↓ v ∈ Δ
  H : ins_in_env Δ d' 0 Δ (d' :: Δ)
  ============================
   d ↓ v ∈ Δ

subgoal 2 (ID 819) is:
 d ↓ S v ∈ Δ'
(dependent evars:)

exact H1.

1 subgoals, subgoal 1 (ID 819)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' (S n) Δ Δ'
  v : nat
  H0 : S n <= v
  d : Term
  H1 : d ↓ v ∈ Δ
  ============================
   d ↓ S v ∈ Δ'

(dependent evars:)

inversion H; subst.

1 subgoals, subgoal 1 (ID 937)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↓ S v ∈ d0 ↑  1 # n :: Δ'0

(dependent evars:)

apply item_tl.

1 subgoals, subgoal 1 (ID 938)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↓ v ∈ Δ'0

(dependent evars:)

destruct v.

2 subgoals, subgoal 1 (ID 948)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  H0 : S n <= 0
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ 0 ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↓ 0 ∈ Δ'0

subgoal 2 (ID 954) is:
 d ↓ S v ∈ Δ'0
(dependent evars:)

elim (le_Sn_O n H0).

1 subgoals, subgoal 1 (ID 954)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↓ S v ∈ Δ'0

(dependent evars:)

apply IHn with (Γ:=Γ) (Δ:=Δ0).

3 subgoals, subgoal 1 (ID 955)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   ins_in_env Γ d' n Δ0 Δ'0

subgoal 2 (ID 956) is:
 n <= v
subgoal 3 (ID 957) is:
 d ↓ v ∈ Δ0
(dependent evars:)

trivial.

2 subgoals, subgoal 1 (ID 956)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   n <= v

subgoal 2 (ID 957) is:
 d ↓ v ∈ Δ0
(dependent evars:)

apply le_S_n ; trivial.

1 subgoals, subgoal 1 (ID 957)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↓ v ∈ Δ0

(dependent evars:)

inversion H1.

1 subgoals, subgoal 1 (ID 1028)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat, n <= v -> forall d : Term, d ↓ v ∈ Δ -> d ↓ S v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n <= S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  Γ0 : list Term
  n0 : nat
  y : Term
  H4 : d ↓ v ∈ Δ0
  H2 : y = d0
  H5 : Γ0 = Δ0
  H6 : n0 = v
  ============================
   d ↓ v ∈ Δ0

(dependent evars:)

exact H4.

No more subgoals.
(dependent evars:)

Qed.

ins_item_ge is defined

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 ∈ Δ' .

1 subgoals, subgoal 1 (ID 1035)
  
  ============================
   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 ∈ Δ'

(dependent evars:)

induction n; intros.

2 subgoals, subgoal 1 (ID 1051)
  
  d' : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' 0 Δ Δ'
  v : nat
  H0 : 0 > v
  d : Term
  H1 : d ↓ v ∈ Δ
  ============================
   d ↑  1 # (0 - S v) ↓ v ∈ Δ'

subgoal 2 (ID 1059) is:
 d ↑  1 # (S n - S v) ↓ v ∈ Δ'
(dependent evars:)

inversion H0.

1 subgoals, subgoal 1 (ID 1059)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' (S n) Δ Δ'
  v : nat
  H0 : S n > v
  d : Term
  H1 : d ↓ v ∈ Δ
  ============================
   d ↑  1 # (S n - S v) ↓ v ∈ Δ'

(dependent evars:)

inversion H; subst.

1 subgoals, subgoal 1 (ID 1150)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↑  1 # (S n - S v) ↓ v ∈ d0 ↑  1 # n :: Δ'0

(dependent evars:)

destruct v.

2 subgoals, subgoal 1 (ID 1160)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  H0 : S n > 0
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ 0 ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↑  1 # (S n - 1) ↓ 0 ∈ d0 ↑  1 # n :: Δ'0

subgoal 2 (ID 1166) is:
 d ↑  1 # (S n - S (S v)) ↓ S v ∈ d0 ↑  1 # n :: Δ'0
(dependent evars:)

inversion H1; subst.

2 subgoals, subgoal 1 (ID 1235)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  H0 : S n > 0
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  H1 : d0 ↓ 0 ∈ d0 :: Δ0
  ============================
   d0 ↑  1 # (S n - 1) ↓ 0 ∈ d0 ↑  1 # n :: Δ'0

subgoal 2 (ID 1166) is:
 d ↑  1 # (S n - S (S v)) ↓ S v ∈ d0 ↑  1 # n :: Δ'0
(dependent evars:)

replace (S n -1) with n by intuition.

2 subgoals, subgoal 1 (ID 1239)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  H0 : S n > 0
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  H1 : d0 ↓ 0 ∈ d0 :: Δ0
  ============================
   d0 ↑  1 # n ↓ 0 ∈ d0 ↑  1 # n :: Δ'0

subgoal 2 (ID 1166) is:
 d ↑  1 # (S n - S (S v)) ↓ S v ∈ d0 ↑  1 # n :: Δ'0
(dependent evars:)

apply item_hd.

1 subgoals, subgoal 1 (ID 1166)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↑  1 # (S n - S (S v)) ↓ S v ∈ d0 ↑  1 # n :: Δ'0

(dependent evars:)

apply item_tl.

1 subgoals, subgoal 1 (ID 1255)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↑  1 # (S n - S (S v)) ↓ v ∈ Δ'0

(dependent evars:)

replace (S n - S (S v)) with (n -S v) by intuition.

1 subgoals, subgoal 1 (ID 1259)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↑  1 # (n - S v) ↓ v ∈ Δ'0

(dependent evars:)

apply IHn with (Γ:=Γ) (Δ:=Δ0).

3 subgoals, subgoal 1 (ID 1262)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   ins_in_env Γ d' n Δ0 Δ'0

subgoal 2 (ID 1263) is:
 n > v
subgoal 3 (ID 1264) is:
 d ↓ v ∈ Δ0
(dependent evars:)

exact H3.

2 subgoals, subgoal 1 (ID 1263)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   n > v

subgoal 2 (ID 1264) is:
 d ↓ v ∈ Δ0
(dependent evars:)

intuition.

1 subgoals, subgoal 1 (ID 1264)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  ============================
   d ↓ v ∈ Δ0

(dependent evars:)

inversion H1.

1 subgoals, subgoal 1 (ID 1350)
  
  d' : Term
  n : nat
  IHn : forall Γ Δ Δ' : Env,
        ins_in_env Γ d' n Δ Δ' ->
        forall v : nat,
        n > v -> forall d : Term, d ↓ v ∈ Δ -> d ↑  1 # (n - S v) ↓ v ∈ Δ'
  Γ : Env
  v : nat
  H0 : S n > S v
  d : Term
  Δ0 : Env
  Δ'0 : Env
  d0 : Term
  H3 : ins_in_env Γ d' n Δ0 Δ'0
  H1 : d ↓ S v ∈ d0 :: Δ0
  H : ins_in_env Γ d' (S n) (d0 :: Δ0) (d0 ↑  1 # n :: Δ'0)
  Γ0 : list Term
  n0 : nat
  y : Term
  H4 : d ↓ v ∈ Δ0
  H2 : y = d0
  H5 : Γ0 = Δ0
  H6 : n0 = v
  ============================
   d ↓ v ∈ Δ0

(dependent evars:)

exact H4.

No more subgoals.
(dependent evars:)

Qed.

ins_item_lt is defined

Lemma ins_item : forall Δ A v Γ Γ',ins_in_env Δ A v Γ Γ'->A ↓ v ∈ Γ'.

1 subgoals, subgoal 1 (ID 1361)
  
  ============================
   forall (Δ : Env) (A : Term) (v : nat) (Γ Γ' : Env),
   ins_in_env Δ A v Γ Γ' -> A ↓ v ∈ Γ'

(dependent evars:)

induction v;inversion 1;subst;constructor;eapply IHv;eassumption.

No more subgoals.
(dependent evars: ?1497 using ,)

Qed.

ins_item is defined

Lemma ins_trunc : forall v Δ A Γ Γ',ins_in_env Δ A v Γ Γ'->trunc (S v) Γ' Δ.

1 subgoals, subgoal 1 (ID 1505)
  
  ============================
   forall (v : nat) (Δ : Env) (A : Term) (Γ Γ' : Env),
   ins_in_env Δ A v Γ Γ' -> trunc (S v) Γ' Δ

(dependent evars:)

induction v;inversion 1;subst;econstructor;try econstructor;eapply IHv;eassumption.

No more subgoals.
(dependent evars: ?1648 using , ?1649 using ,)

Qed.

ins_trunc is defined

In the list Γ, t is nth element correctly lifted according to Γ: e.g.: if t ↓ n ⊂ Γ and we insert something in Γ, then we can still speak about t without think of the lift hidden by the insertion.

Definition item_lift (t:Term) (Γ:Env) (n:nat) :=
exists u , t = u ↑ (S n ) /\ u ↓ n ∈ Γ .

item_lift is defined

Hint Unfold item_lift.

Notation " t ↓ n ⊂ Γ " := (item_lift t Γ n) (at level 80, no associativity): F_scope.

Properties of the item_lift notation.

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 ⊂ Δ'.

1 subgoals, subgoal 1 (ID 1654)
  
  ============================
   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 ⊂ Δ'

(dependent evars:)

intros.

1 subgoals, subgoal 1 (ID 1664)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  H1 : t ↓ v ⊂ Δ
  ============================
   t ↑  1 # n ↓ v ⊂ Δ'

(dependent evars:)

destruct H1 as [u [ P Q]].

1 subgoals, subgoal 1 (ID 1672)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑  (S v)
  Q : u ↓ v ∈ Δ
  ============================
   t ↑  1 # n ↓ v ⊂ Δ'

(dependent evars:)

rewrite P.

1 subgoals, subgoal 1 (ID 1673)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑  (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑  (S v) ↑  1 # n ↓ v ⊂ Δ'

(dependent evars:)

exists (u ↑ 1 # (n - S v) ); split.

2 subgoals, subgoal 1 (ID 1677)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑  (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑  (S v) ↑  1 # n = u ↑  1 # (n - S v) ↑  (S v)

subgoal 2 (ID 1678) is:
 u ↑  1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)

replace n with ( S v + (n - S v)) by intuition .

2 subgoals, subgoal 1 (ID 1682)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑  (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑  (S v) ↑  1 # (S v + (n - S v)) =
   u ↑  1 # (S v + (n - S v) - S v) ↑  (S v)

subgoal 2 (ID 1678) is:
 u ↑  1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)

destruct liftP2 as (HH&HH0);rewrite HH.

3 subgoals, subgoal 1 (ID 1706)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑  (S v)
  Q : u ↓ v ∈ Δ
  HH : forall (M : Term) (i j k n : nat),
       i <= n -> M ↑  j # i ↑  k # (j + n) = M ↑  k # n ↑  j # i
  HH0 : forall (H : Prf) (i j k n : nat),
        i <= n -> H ↑h j # i ↑h k # (j + n) = H ↑h k # n ↑h j # i
  ============================
   u ↑  1 # (n - S v) ↑  (S v) = u ↑  1 # (S v + (n - S v) - S v) ↑  (S v)

subgoal 2 (ID 1707) is:
 0 <= n - S v
subgoal 3 (ID 1678) is:
 u ↑  1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)

replace (S v+(n-S v)-S v) with (n-S v) by intuition.

3 subgoals, subgoal 1 (ID 1711)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑  (S v)
  Q : u ↓ v ∈ Δ
  HH : forall (M : Term) (i j k n : nat),
       i <= n -> M ↑  j # i ↑  k # (j + n) = M ↑  k # n ↑  j # i
  HH0 : forall (H : Prf) (i j k n : nat),
        i <= n -> H ↑h j # i ↑h k # (j + n) = H ↑h k # n ↑h j # i
  ============================
   u ↑  1 # (n - S v) ↑  (S v) = u ↑  1 # (n - S v) ↑  (S v)

subgoal 2 (ID 1707) is:
 0 <= n - S v
subgoal 3 (ID 1678) is:
 u ↑  1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)

reflexivity.

2 subgoals, subgoal 1 (ID 1707)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑  (S v)
  Q : u ↓ v ∈ Δ
  HH : forall (M : Term) (i j k n : nat),
       i <= n -> M ↑  j # i ↑  k # (j + n) = M ↑  k # n ↑  j # i
  HH0 : forall (H : Prf) (i j k n : nat),
        i <= n -> H ↑h j # i ↑h k # (j + n) = H ↑h k # n ↑h j # i
  ============================
   0 <= n - S v

subgoal 2 (ID 1678) is:
 u ↑  1 # (n - S v) ↓ v ∈ Δ'
(dependent evars:)

intuition.

1 subgoals, subgoal 1 (ID 1678)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  t : Term
  u : Term
  P : t = u ↑  (S v)
  Q : u ↓ v ∈ Δ
  ============================
   u ↑  1 # (n - S v) ↓ v ∈ Δ'

(dependent evars:)

clear t P.

1 subgoals, subgoal 1 (ID 1746)
  
  d' : Term
  n : nat
  Γ : Env
  Δ : Env
  Δ' : Env
  H : ins_in_env Γ d' n Δ Δ'
  v : nat
  H0 : n > v
  u : Term
  Q : u ↓ v ∈ Δ
  ============================
   u ↑  1 # (n - S v) ↓ v ∈ Δ'

(dependent evars:)

inversion H; subst.

2 subgoals, subgoal 1 (ID 1813)
  
  d' : Term
  Δ : Env
  v : nat
  u : Term
  Q : u ↓ v ∈ Δ
  H0 : 0 > v
  H : ins_in_env Δ d' 0 Δ (d' :: Δ)
  ============================
   u ↑  1 # (0 - S v) ↓ v ∈ d' :: Δ

subgoal 2 (ID 1830) is:
 u ↑  1 # (S n0 - S v) ↓ v ∈ d ↑  1 # n0 :: Δ'0
(dependent evars:)

inversion H0.

1 subgoals, subgoal 1 (ID 1830)
  
  d' : Term
  Γ : Env
  v : nat
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  Q : u ↓ v ∈ d :: Δ0
  H0 : S n0 > v
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑  1 # n0 :: Δ'0)
  ============================
   u ↑  1 # (S n0 - S v) ↓ v ∈ d ↑  1 # n0 :: Δ'0

(dependent evars:)

inversion Q; subst.

2 subgoals, subgoal 1 (ID 1935)
  
  d' : Term
  Γ : Env
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑  1 # n0 :: Δ'0)
  H0 : S n0 > 0
  Q : d ↓ 0 ∈ d :: Δ0
  ============================
   d ↑  1 # (S n0 - 1) ↓ 0 ∈ d ↑  1 # n0 :: Δ'0

subgoal 2 (ID 1943) is:
 u ↑  1 # (S n0 - S (S n)) ↓ S n ∈ d ↑  1 # n0 :: Δ'0
(dependent evars:)

replace (S n0 -1) with n0 by intuition.

2 subgoals, subgoal 1 (ID 1947)
  
  d' : Term
  Γ : Env
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑  1 # n0 :: Δ'0)
  H0 : S n0 > 0
  Q : d ↓ 0 ∈ d :: Δ0
  ============================
   d ↑  1 # n0 ↓ 0 ∈ d ↑  1 # n0 :: Δ'0

subgoal 2 (ID 1943) is:
 u ↑  1 # (S n0 - S (S n)) ↓ S n ∈ d ↑  1 # n0 :: Δ'0
(dependent evars:)

apply item_hd.

1 subgoals, subgoal 1 (ID 1943)
  
  d' : Term
  Γ : Env
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑  1 # n0 :: Δ'0)
  n : nat
  H5 : u ↓ n ∈ Δ0
  Q : u ↓ S n ∈ d :: Δ0
  H0 : S n0 > S n
  ============================
   u ↑  1 # (S n0 - S (S n)) ↓ S n ∈ d ↑  1 # n0 :: Δ'0

(dependent evars:)

apply item_tl.

1 subgoals, subgoal 1 (ID 1962)
  
  d' : Term
  Γ : Env
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑  1 # n0 :: Δ'0)
  n : nat
  H5 : u ↓ n ∈ Δ0
  Q : u ↓ S n ∈ d :: Δ0
  H0 : S n0 > S n
  ============================
   u ↑  1 # (S n0 - S (S n)) ↓ n ∈ Δ'0

(dependent evars:)

replace (S n0 - S (S n)) with (n0 -S n) by intuition.

1 subgoals, subgoal 1 (ID 1966)
  
  d' : Term
  Γ : Env
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑  1 # n0 :: Δ'0)
  n : nat
  H5 : u ↓ n ∈ Δ0
  Q : u ↓ S n ∈ d :: Δ0
  H0 : S n0 > S n
  ============================
   u ↑  1 # (n0 - S n) ↓ n ∈ Δ'0

(dependent evars:)

apply ins_item_lt with d' Γ Δ0; trivial.

1 subgoals, subgoal 1 (ID 1970)
  
  d' : Term
  Γ : Env
  u : Term
  n0 : nat
  Δ0 : Env
  Δ'0 : Env
  d : Term
  H1 : ins_in_env Γ d' n0 Δ0 Δ'0
  H : ins_in_env Γ d' (S n0) (d :: Δ0) (d ↑  1 # n0 :: Δ'0)
  n : nat
  H5 : u ↓ n ∈ Δ0
  Q : u ↓ S n ∈ d :: Δ0
  H0 : S n0 > S n
  ============================
   n0 > n

(dependent evars:)

intuition.

No more subgoals.
(dependent evars:)

Qed.

ins_item_lift_lt is defined

This type describe how do we do substitution inside a context. As previously, no type checking is done at this point.

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] :: Δ').

sub_in_env is defined
sub_in_env_ind is defined

Hint Constructors sub_in_env.

Some ins / subst related facts: what happens to term when we do a substitution in a context.

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 ∈ Δ'.

1 subgoals, subgoal 1 (ID 2004)
  
  ============================
   forall (n : nat) (Γ Δ Δ' : Env) (t T : Term),
   sub_in_env Γ t T n Δ Δ' ->
   forall v : nat, n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'

(dependent evars:)

intros n Γ Δ Δ' t T H; induction H; intros.

2 subgoals, subgoal 1 (ID 2031)
  
  Γ : Env
  t : Term
  T : Term
  v : nat
  H : 0 <= v
  d : Term
  H0 : d ↓ S v ∈ T :: Γ
  ============================
   d ↓ v ∈ Γ

subgoal 2 (ID 2035) is:
 d ↓ v ∈ B [n ←  t] :: Δ'
(dependent evars:)

inversion H0; subst.

2 subgoals, subgoal 1 (ID 2112)
  
  Γ : Env
  t : Term
  T : Term
  v : nat
  H : 0 <= v
  d : Term
  H0 : d ↓ S v ∈ T :: Γ
  H2 : d ↓ v ∈ Γ
  ============================
   d ↓ v ∈ Γ

subgoal 2 (ID 2035) is:
 d ↓ v ∈ B [n ←  t] :: Δ'
(dependent evars:)

trivial.

1 subgoals, subgoal 1 (ID 2035)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : S n <= v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  ============================
   d ↓ v ∈ B [n ←  t] :: Δ'

(dependent evars:)

inversion H1; subst.

1 subgoals, subgoal 1 (ID 2189)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : S n <= v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  H3 : d ↓ v ∈ Δ
  ============================
   d ↓ v ∈ B [n ←  t] :: Δ'

(dependent evars:)

destruct v.

2 subgoals, subgoal 1 (ID 2199)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  H0 : S n <= 0
  d : Term
  H1 : d ↓ 1 ∈ B :: Δ
  H3 : d ↓ 0 ∈ Δ
  ============================
   d ↓ 0 ∈ B [n ←  t] :: Δ'

subgoal 2 (ID 2205) is:
 d ↓ S v ∈ B [n ←  t] :: Δ'
(dependent evars:)

elim (le_Sn_O n H0).

1 subgoals, subgoal 1 (ID 2205)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : S n <= S v
  d : Term
  H1 : d ↓ S (S v) ∈ B :: Δ
  H3 : d ↓ S v ∈ Δ
  ============================
   d ↓ S v ∈ B [n ←  t] :: Δ'

(dependent evars:)

apply item_tl.

1 subgoals, subgoal 1 (ID 2206)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : S n <= S v
  d : Term
  H1 : d ↓ S (S v) ∈ B :: Δ
  H3 : d ↓ S v ∈ Δ
  ============================
   d ↓ v ∈ Δ'

(dependent evars:)

apply le_S_n in H0.

1 subgoals, subgoal 1 (ID 2208)
  
  Γ : Env
  t : Term
  T : Term
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n <= v -> forall d : Term, d ↓ S v ∈ Δ -> d ↓ v ∈ Δ'
  v : nat
  H0 : n <= v
  d : Term
  H1 : d ↓ S (S v) ∈ B :: Δ
  H3 : d ↓ S v ∈ Δ
  ============================
   d ↓ v ∈ Δ'

(dependent evars:)

apply IHsub_in_env; trivial.

No more subgoals.
(dependent evars:)

Qed.

nth_sub_sup is defined

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 ∈ Δ' .

1 subgoals, subgoal 1 (ID 2220)
  
  ============================
   forall (t T : Term) (n : nat) (Γ Δ Δ' : Env),
   sub_in_env Γ t T n Δ Δ' ->
   forall v : nat,
   n > v -> forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'

(dependent evars:)

intros t T n Γ Δ Δ' H; induction H; intros.

2 subgoals, subgoal 1 (ID 2247)
  
  t : Term
  T : Term
  Γ : Env
  v : nat
  H : 0 > v
  d : Term
  H0 : d ↓ v ∈ T :: Γ
  ============================
   d [(0 - S v) ←  t] ↓ v ∈ Γ

subgoal 2 (ID 2251) is:
 d [(S n - S v) ←  t] ↓ v ∈ B [n ←  t] :: Δ'
(dependent evars:)

inversion H.

1 subgoals, subgoal 1 (ID 2251)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > v
  d : Term
  H1 : d ↓ v ∈ B :: Δ
  ============================
   d [(S n - S v) ←  t] ↓ v ∈ B [n ←  t] :: Δ'

(dependent evars:)

destruct v.

2 subgoals, subgoal 1 (ID 2288)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  H0 : S n > 0
  d : Term
  H1 : d ↓ 0 ∈ B :: Δ
  ============================
   d [(S n - 1) ←  t] ↓ 0 ∈ B [n ←  t] :: Δ'

subgoal 2 (ID 2293) is:
 d [(S n - S (S v)) ←  t] ↓ S v ∈ B [n ←  t] :: Δ'
(dependent evars:)

inversion H1; subst.

2 subgoals, subgoal 1 (ID 2362)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  H0 : S n > 0
  H1 : B ↓ 0 ∈ B :: Δ
  ============================
   B [(S n - 1) ←  t] ↓ 0 ∈ B [n ←  t] :: Δ'

subgoal 2 (ID 2293) is:
 d [(S n - S (S v)) ←  t] ↓ S v ∈ B [n ←  t] :: Δ'
(dependent evars:)

replace (S n -1) with n by intuition.

2 subgoals, subgoal 1 (ID 2366)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  H0 : S n > 0
  H1 : B ↓ 0 ∈ B :: Δ
  ============================
   B [n ←  t] ↓ 0 ∈ B [n ←  t] :: Δ'

subgoal 2 (ID 2293) is:
 d [(S n - S (S v)) ←  t] ↓ S v ∈ B [n ←  t] :: Δ'
(dependent evars:)

apply item_hd.

1 subgoals, subgoal 1 (ID 2293)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > S v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  ============================
   d [(S n - S (S v)) ←  t] ↓ S v ∈ B [n ←  t] :: Δ'

(dependent evars:)

replace (S n - S (S v)) with (n - S v) by intuition.

1 subgoals, subgoal 1 (ID 2385)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > S v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  ============================
   d [(n - S v) ←  t] ↓ S v ∈ B [n ←  t] :: Δ'

(dependent evars:)

inversion H1; subst.

1 subgoals, subgoal 1 (ID 2464)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > S v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  H3 : d ↓ v ∈ Δ
  ============================
   d [(n - S v) ←  t] ↓ S v ∈ B [n ←  t] :: Δ'

(dependent evars:)

apply item_tl.

1 subgoals, subgoal 1 (ID 2465)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  v : nat
  H0 : S n > S v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  H3 : d ↓ v ∈ Δ
  ============================
   d [(n - S v) ←  t] ↓ v ∈ Δ'

(dependent evars:)

apply gt_S_n in H0.

1 subgoals, subgoal 1 (ID 2467)
  
  t : Term
  T : Term
  Γ : Env
  Δ : Env
  Δ' : Env
  n : nat
  B : Term
  H : sub_in_env Γ t T n Δ Δ'
  IHsub_in_env : forall v : nat,
                 n > v ->
                 forall d : Term, d ↓ v ∈ Δ -> d [(n - S v) ←  t] ↓ v ∈ Δ'
  v : nat
  H0 : n > v
  d : Term
  H1 : d ↓ S v ∈ B :: Δ
  H3 : d ↓ v ∈ Δ
  ============================
   d [(n - S v) ←  t] ↓ v ∈ Δ'

(dependent evars:)

apply IHsub_in_env; trivial.

No more subgoals.
(dependent evars:)

Qed.

nth_sub_inf is defined

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.

1 subgoals, subgoal 1 (ID 2477)
  
  ============================
   forall (t T : Term) (n : nat) (g e f : Env),
   sub_in_env g t T n e f ->
   forall v : nat, n > v -> forall u : Term, u ↓ v ⊂ e -> u [n ←  t] ↓ v ⊂ f

(dependent evars:)

intros.

1 subgoals, subgoal 1 (ID 2488)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  u : Term
  H1 : u ↓ v ⊂ e
  ============================
   u [n ←  t] ↓ v ⊂ f

(dependent evars:)

destruct H1 as [y [K L]].

1 subgoals, subgoal 1 (ID 2496)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  u : Term
  y : Term
  K : u = y ↑  (S v)
  L : y ↓ v ∈ e
  ============================
   u [n ←  t] ↓ v ⊂ f

(dependent evars:)

exists (subst_rec t y (n-S v)); split.

2 subgoals, subgoal 1 (ID 2500)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  u : Term
  y : Term
  K : u = y ↑  (S v)
  L : y ↓ v ∈ e
  ============================
   u [n ←  t] = y [(n - S v) ←  t] ↑  (S v)

subgoal 2 (ID 2501) is:
 y [(n - S v) ←  t] ↓ v ∈ f
(dependent evars:)

rewrite K; clear u K.

2 subgoals, subgoal 1 (ID 2503)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  y : Term
  L : y ↓ v ∈ e
  ============================
   y ↑  (S v) [n ←  t] = y [(n - S v) ←  t] ↑  (S v)

subgoal 2 (ID 2501) is:
 y [(n - S v) ←  t] ↓ v ∈ f
(dependent evars:)

pattern n at 1 .

2 subgoals, subgoal 1 (ID 2504)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  y : Term
  L : y ↓ v ∈ e
  ============================
   (fun n0 : nat => y ↑  (S v) [n0 ←  t] = y [(n - S v) ←  t] ↑  (S v)) n

subgoal 2 (ID 2501) is:
 y [(n - S v) ←  t] ↓ v ∈ f
(dependent evars:)

replace n with (S v + ( n - S v)) by intuition.

2 subgoals, subgoal 1 (ID 2508)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  y : Term
  L : y ↓ v ∈ e
  ============================
   y ↑  (S v) [(S v + (n - S v)) ←  t] = y [(n - S v) ←  t] ↑  (S v)

subgoal 2 (ID 2501) is:
 y [(n - S v) ←  t] ↓ v ∈ f
(dependent evars:)

apply substP2; intuition.

1 subgoals, subgoal 1 (ID 2501)
  
  t : Term
  T : Term
  n : nat
  g : Env
  e : Env
  f : Env
  H : sub_in_env g t T n e f
  v : nat
  H0 : n > v
  u : Term
  y : Term
  K : u = y ↑  (S v)
  L : y ↓ v ∈ e
  ============================
   y [(n - S v) ←  t] ↓ v ∈ f

(dependent evars:)

apply nth_sub_inf with T g e; trivial.

No more subgoals.
(dependent evars:)

Qed.

nth_sub_item_inf is defined

Lemma subst_item : forall n Δ T A Γ1 Γ2,sub_in_env Δ T A n Γ1 Γ2->A ↓ n ∈ Γ1.

1 subgoals, subgoal 1 (ID 2552)
  
  ============================
   forall (n : nat) (Δ : Env) (T A : Term) (Γ1 Γ2 : Env),
   sub_in_env Δ T A n Γ1 Γ2 -> A ↓ n ∈ Γ1

(dependent evars:)

induction 1;constructor;assumption.

No more subgoals.
(dependent evars:)

Qed.

subst_item is defined

Lemma subst_trunc : forall n Δ T A Γ1 Γ2,sub_in_env Δ T A n Γ1 Γ2->trunc (S n) Γ1 Δ.

1 subgoals, subgoal 1 (ID 2587)
  
  ============================
   forall (n : nat) (Δ : Env) (T A : Term) (Γ1 Γ2 : Env),
   sub_in_env Δ T A n Γ1 Γ2 -> trunc (S n) Γ1 Δ

(dependent evars:)

induction 1;constructor;constructor||assumption.

No more subgoals.
(dependent evars:)

Qed.

subst_trunc is defined

Lemma subst_trunc2 : forall n Δ T A Γ1 Γ2,sub_in_env Δ T A n Γ1 Γ2->trunc n Γ2 Δ.

1 subgoals, subgoal 1 (ID 2627)
  
  ============================
   forall (n : nat) (Δ : Env) (T A : Term) (Γ1 Γ2 : Env),
   sub_in_env Δ T A n Γ1 Γ2 -> trunc n Γ2 Δ

(dependent evars:)

induction 1;constructor;constructor||assumption.

No more subgoals.
(dependent evars:)

Qed.

subst_trunc2 is defined

End f_env_mod.

Module Type f_env_mod is defined

Index

This page has been generated by coqdoc