Library Top.equiv
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.
Require Export reduction.
Require Import Coq.Program.Equality.
Inductive lsa_d_ret (u :term) (i:nat): term→term→Prop:=
| LSA_Var1 :
lsa_d_ret u i (TVar i) (lift (S i) u)
| LSA_Lam1 : ∀ t t':term,
lsa_d_ret (u) (S i) t t' →
lsa_d_ret u i (\t) (\t')
| LSA_AppLeft1 : ∀ t t' s:term,
lsa_d_ret u i t t' →
lsa_d_ret u i (t @ s) (t' @ s)
| LSA_AppRight1 : ∀ t t' s:term,
lsa_d_ret u i t t' →
lsa_d_ret u i (s @ t) (s @ t')
| LSA_SubExt1 : ∀ t t' s:term,
lsa_d_ret u i t t' →
lsa_d_ret u i (s[t]) (s[t'])
| LSA_SubInt1 : ∀ t t' s:term,
lsa_d_ret (u) (S i) t t' →
lsa_d_ret u i (t[s]) (t'[s]).
Hint Resolve LSA_Var1 LSA_Lam1 LSA_AppLeft1 LSA_AppRight1 LSA_SubExt1 LSA_SubInt1 :IE.
Autre définition de ls qui retarde la réindexation des
variables libres
Inductive lsa_ret (i:nat) : term → term → Prop :=
| LSA_RET : ∀ t t' u,
lsa_d_ret u i t t' → lsa_ret i (t[u]) (t'[u]).
Equivalence entre les deux ls
Lemma ls_equivalence: ∀ t t' u,∀ i,
lsa_def (lift i u) i t t' ↔ lsa_d_ret u i t t'.
Lemma lsa_Hyp1:
∀ t t' u,∀ i, lsa_ret i (t[u]) (t'[u]) ↔ lsa_d_ret u i t t'.
Lemma no_subst_gen: ∀ t u :term, ∀ i j k:nat,
j ≤ k < i+j →
(lift_rec (i) t j){k := u} =
(lift_rec (i) t j).
Lemma lsa_red' :
∀ t t' u :term, ∀ i,
lsa_d_ret u i t t' →
t'{i:= (lift (S i) u)} = t {i:= (lift (S i) u)}.
Lemma lsa_red :
∀ t t' u :term,
lsa_def u 0 t t' →
t'{0:= (shift u)} = t {0:= (shift u)}.