Library Top.Terme
This file is part of the IE library
Copyright (C) El Ouraoui, Mayero, Mazza
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Les termes
Inductive term : Set :=
| TVar : nat → term
| TAbs : term → term
| TApp : term → term → term
| TSub : term → term → term.
Notation "t [ u ]" := (TSub t u)(at level 70).
Notation "\" := (TAbs ) (at level 66).
Notation "u @ v" := (TApp u v) (at level 66).
Mise à jours des indices de de Bruijn
Fixpoint lift_rec n t {struct t} : nat → term :=
fun k ⇒
match t with
| TVar i ⇒
match le_gt_dec k i with
| left _ ⇒ TVar (n + i)
| right _ ⇒ TVar i
end
| \u ⇒ \(lift_rec n u (S k))
| u @ v ⇒ (lift_rec n u k) @ (lift_rec n v k)
| u [v] ⇒ (lift_rec n u (S k))[(lift_rec n v k)]
end.
Definition lift n t := lift_rec n t 0.
Definition shift t := lift 1 t.
Définition de la substitution explicite M{k/N}
Fixpoint subst_rec u t {struct t} : nat → term :=
fun k ⇒
match t with
| TVar i ⇒
match eq_nat_dec k i with
| left _ ⇒ u
| right _ ⇒ TVar i
end
| \v ⇒ \(subst_rec (shift u) v (S k))
| w@v ⇒ (subst_rec u w k)@(subst_rec u v k)
| w[v] ⇒ (subst_rec (shift u) w (S k))[(subst_rec u v k)]
end.
Definition subs_recbis u x t:= subst_rec u t x.
Notation " t { x := u } " := (subs_recbis u x t)(at level 0).
Lemma subst_nothing' :
∀ u u', ∀ j n, n > 0 →
(lift_rec n u j) { j := u'} = (lift_rec n u j).
Lemma subst_nothing :
∀ u u',
(shift u) { 0 := u'} = (shift u).
Lemma lift_rec0 : ∀ t k, lift_rec 0 t k = t.
Lemma lift0 : ∀ t, lift 0 t = t.
Fixpoint is_free k t :=
match t with
| TVar j ⇒ k ≠ j
| \u ⇒ is_free (S k) u
| u@v ⇒ is_free k u ∧ is_free k v
| u[v] ⇒ is_free (S k) u ∧ is_free k v
end.
Quelques lemmes élémentaires concernant lift et subst
Lemma lift_var_ge :
∀ k n p, p ≤ n → lift_rec k (TVar n) p = TVar (k + n).
Lemma lift_var_lt : ∀ k n p, p > n → lift_rec k (TVar n) p = TVar n.
Lemma subst_var_diff : ∀ u n k, k ≠ n → (TVar n){k := u} = TVar n.
Lemme de simplification du lift
Lemma simpl_lift_rec :
∀ t n k p i,
i ≤ k + n →
k ≤ i → lift_rec p (lift_rec n t k) i = lift_rec (p + n) t k.
Lemma simpl_lift : ∀ t n, lift (S n) t = shift (lift n t).
Lemme de commutativité des indices pour lift
Lemma lift_commut: ∀ a k i j p, k ≤ p →
lift_rec i (lift_rec j a p) k = lift_rec j (lift_rec i a k) (i + p).
Lemma shift_commut: ∀ u j, lift j (shift u) = shift (lift j u).
Lemma lift_commut_of_succ:
∀ u n k,
lift_rec n (lift_rec 1 u k) (k+1) = lift_rec 1 (lift_rec n u k) k.
Lemma commut_lift_subst_rec :
∀ t u n k h,
k ≤ h →
lift_rec n (t {h := u}) k = (lift_rec n t k) {(n+h) := (lift_rec n u k)}.
Commutativité entre lift et substitution
Lemmes pour le prédicat gc de la réduction
Lemma substFree_eq:
∀ t u x, is_free x t → t{x := u} = t.
Fixpoint num_occ t n :nat :=
match t with
|TVar x ⇒ if n =? x then 1
else 0
|\u ⇒
num_occ u (S n)
|u @ v ⇒
num_occ u n + num_occ v n
| u [v] ⇒
num_occ u (S n) + num_occ v n
end.
Lemma var_occ :
∀ n i,
num_occ (TVar n) i = 0 → n ≠ i.
Lemma no_occ_of_x :
∀ t u u',∀ i,
num_occ t i = 0 → t{i := u} = t{i := u'}.
Lemma free_lift :
∀ u:term, ∀ n k j:nat,
0 ≤ j → j ≤ k < n+j →
num_occ (lift_rec n u j) k = 0.