Library Top.reduction

This file is part of the IE library

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 list_subst.
Require Export Decidable.

Règle de réduction db

Inductive db : term → term → Prop :=
  | DB_Lam : ∀ t u:term, db ((\t )@u) (t [u ])
  | DB_App : ∀ t u r s, db (t@u) r →
                                  db ((shift t [s ])@u) (shift r [s ]).
Hint Resolve DB_Lam DB_App:IE.
Notation " t -->db t'" := (db t t') (at level 66).

Lemme de db partiel de lemme 2 de l'article

Lemma db_to_subst : ∀ t t' a x,
t -->db t' → (t {x := a }) -->db (t' {x := a }).

Réduction ls définissant la substitution linéaire

Inductive lsa_def (u :term): nat →term →term →Prop:=
  | LSA_Var :∀ i,
      lsa_def u i (TVar i) (shift u)
  | LSA_Lam : ∀ t t':term,∀ i :nat,
                 lsa_def (shift u) (S i) t t' →
                 lsa_def u i (\t) (\t')
  | LSA_AppLeft : ∀ t t' s:term,∀ i:nat,
                    lsa_def u i t t' →
                    lsa_def u i (t@s) (t'@s)
  | LSA_AppRight : ∀ t t' s:term,∀ i:nat,
                     lsa_def u i t t' →
                     lsa_def u i (s@t) (s@t')
  | LSA_SubExt : ∀ t t' s:term,∀ i:nat,
                  lsa_def u i t t' →
                  lsa_def u i (s [t ]) (s [t'])
  | LSA_SubInt : ∀ t t' s:term,∀ i:nat,
                  lsa_def (shift u) (S i) t t' →
                  lsa_def u i (t [s ]) (t'[s ]).

Hint Resolve LSA_Var LSA_Lam LSA_AppLeft LSA_AppRight LSA_SubExt LSA_SubInt :IE.

Définition de ls

Inductive lsa (i:nat) : term → term → Prop :=
| LSA : ∀ t t' u, lsa_def u i t t' → lsa i (t [u ]) (t'[u ]).

Lemma lsa_Hyp:
∀ t t' u,∀ i, lsa i (t [u ]) (t'[u ]) ↔ lsa_def u i t t'.

lemme de ls partiel de lemme 2 de l'article

Lemma lsa_to_subst :
  ∀ t t',
  ∀ j:nat,
    lsa 0 t t' →
    ∀ a :term,
      lsa 0 t {(0+j ) := a } t'{(0+j ) := a }.

Definition ls := lsa 0 .
Notation " t -->ls t'" := (ls t t') (at level 66).

Lemma ls_to_subst : ∀ t t' ,∀ j:nat, t -->ls t' → ∀ a,
                                               t { j := a } -->ls t' { j := a }.

Règle gc

Inductive gc : term → term → Prop :=
| GC_Term : ∀ t u:term,
gc ((shift t )[u ]) t.
Hint Resolve GC_Term: IE.
Notation " t -->gc t'" := (gc t t') (at level 66).

Lemme de gc partiel du lemme 2 de l'article

Lemma gc_to_subst : ∀ t t' a, t -->gc t' →∀ k,
(t {k := a }) -->gc (t'{k := a }).

Réduction complète

Inductive red : term → term → Prop :=
  | DB : ∀ t t':term, t -->db t' → red t t'
  | LS : ∀ t t':term, t -->ls t' → red t t'
  | GC : ∀ t t':term, t -->gc t' → red t t'

  | RedContextTAbs:
      ∀ t t':term,
      red t t' →
      red (\t) (\t')
  | RedContextTAppLeft:
      ∀ t t' v:term,
      red t t' →
      red (t @ v) (t' @ v)
  | RedContextTAppRight:
      ∀ v v' t:term,
      red v v' →
      red (t @ v) (t @ v')
  | RedContextSubExt :
      ∀ t t' u:term,
      red t t' →
      red (t [u ]) (t'[u ])
  | RedContextSubInt :
      ∀ t u u':term,
      red u u' →
      red (t [u ]) (t [u']).

Notation " t --> t'" := (red t t') (at level 66).

Réduction star

Inductive red_star: term → term → Prop :=
  | red_star_eq: ∀ t:term, red_star t t
  | red_star_step: ∀ t u v:term,
                     red t u → red_star u v → red_star t v.

Notation " t -->* t'" := (red_star t t') (at level 66).

Hint Resolve DB LS GC RedContextTAbs RedContextTAppLeft RedContextTAppRight RedContextSubExt GC_Term: IE.

Theorem red_to_star:
  ∀ t u:term, (t --> u ) → (t -->* u ).

Theorem red_star_db:
  ∀ t t': term, t -->db t' → t -->* t'.

Theorem red_star_ls:
  ∀ t t': term,
    t -->ls t' → t -->* t'.

Theorem red_star_gc:
  ∀ t t': term,
    t -->gc t' → t -->* t'.

Theorem red_star_ContextTAbs:
  ∀ t t': term, t -->* t' → (\t ) -->* (\t').

Theorem red_star_RedContextTAppLeft:
  ∀ t t' u: term, t -->* t' → (t @ u ) -->* (t' @ u ).

Theorem red_star_RedContextTAppRight:
  ∀ w w' t: term, w -->* w' → (t @ w ) -->* (t @ w').

Theorem red_star_RedContextSubExt:
  ∀ t t' u: term, t -->* t' → (t [u ]) -->* (t'[u ]).

Theorem red_star_RedContextSubInt:
  ∀ w w' u:term, w -->* w' → (u [w ]) -->* (u [w']).

Lemma red_app : ∀ t1 t1' t2 t2' ,
                  t1 -->* t1' → t2 -->* t2' → (t1 @ t2 ) -->* (t1' @ t2').

Lemma red_sub : ∀ t1 t1' t2 t2' ,
                  t1 -->* t1' → t2 -->* t2' → (t1 [t2 ]) -->* (t1'[t2']).

Le lemme 2 de l'article : si t -> t' => t{k/u} -> t'{k/u}

Lemma lemme2' : ∀ t t', t --> t' → ∀ u k, t {k := u } --> t'{k := u }.
Lemma lemme2 : ∀ t t' u, t --> t' → t {0 := u } --> t'{0 := u }.

Lemma db_to_list_substT :
  ∀ u u' j k,
    u -->db u' → (list_substT u (build_list (fv_rec u k) j) k j ) -->db (list_substT u' (build_list (fv_rec u' k) j) k j ).

Lemma lsa_to_list_substT :
  ∀ t1 t2 j k,
    lsa 0 t1 t2 → lsa 0 (list_substT t1 (build_list (fv_rec t1 (0+k)) j) (0+k) j) (list_substT t2 (build_list (fv_rec t2 (0+k)) j) (0+k) j).

Lemma ls_to_list_subst :
  ∀ t1 t2 j,∀ k:nat, t1 -->ls t2 →
                               (list_substT t1 (build_list (fv_rec t1 k) j) (k) j ) -->ls
                               (list_substT t2 (build_list (fv_rec t2 k) j) (k) j ).

Lemma gc_to_list_substT : ∀ t1 t2, t1 -->gc t2 →∀ k j,
                          (list_substT t1 (build_list (fv_rec t1 k) j) k j ) -->gc
                          (list_substT t2 (build_list (fv_rec t2 k) j) k j ).

Lemma red_to_list_substT :
  ∀ j u u', u --> u' →
                  ∀ k, (list_substT u (build_list (fv_rec u k) j) k j ) -->
                            (list_substT u' (build_list (fv_rec u' k) j) k j ).

Le lemme 1 de l'article: si u -> u' => t{k/u} -> t{k/u'}

Lemma lemme1 : ∀ t x u u', u --> u' → t {x := u } -->* t {x := u'}.