Library Top.list_subst

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 Terme.
Require Export List.
Require Import Coq.Sorting.Mergesort.
Require Import Orders.

merge, sort et tri décroissant

Module NatOrderInv <: TotalLeBool.

Definition t := nat.

Fixpoint leb x y :=
    match x, y with
    | _, 0 ⇒ true
    | 0, _ ⇒ false
    | S x', S y' ⇒ leb x' y'
    end.
  Infix "<=?" := leb (at level 70).

Theorem leb_total : ∀ a1 a2, a1 <=? a2 ∨ a2 <=? a1.
End NatOrderInv.

Module Import NatSort := Sort NatOrderInv.

fv détermine un liste de variable libre dans t {i0...in}

Fixpoint fv_rec t{struct t}: nat → list nat:=
fun k ⇒
  match t with
  |TVar i ⇒match le_gt_dec k i with
              | left _ ⇒ i :: nil
              | right _ ⇒ nil
            end
  | \u ⇒ sort (fv_rec u (S k))
  | u @ v ⇒ merge (sort (fv_rec u k)) (sort (fv_rec v k))
  | TSub u v ⇒ merge (sort (fv_rec u (S k))) (sort (fv_rec v k))
  end.

Definition fv t := fv_rec t 0.

Fixpoint list_substV t l {struct l} :=
  match l with
    | nil ⇒ t
    |(u,i)::l' ⇒ list_substV (t {i := TVar u}) l'
  end.

Fixpoint build_list l k :=
match l with
  | nil ⇒ nil
  | i::l' ⇒ ((i+k ), i)::(build_list l' k )
end.

Définition de la fonction list_subst t{i0+k/i0}..{in+k/in}

Fixpoint list_substT t l i k :=
  match t with
    |TVar i ⇒ list_substV (TVar i) l
    |\u ⇒ \(list_substT u (build_list (fv_rec u (S i)) k) (S i) k)
    | u @ v ⇒ (list_substT u (build_list (fv_rec u i) k) i k ) @ (list_substT v (build_list (fv_rec v i) k) i k )
    |TSub u v ⇒ TSub (list_substT u (build_list (fv_rec u (S i)) k) (S i) k) (list_substT v (build_list (fv_rec v i) k) i k)
  end.

Lift_subst permet de voir un terme lifté comme une la substitution de toutes les variables libres de u par (in + j) où in est la n-ème variable libre de u.

lift_rec j u k = u{i0+j/i0}....{in+j/in} et {i0...in} = (fv u)

Lemma lift_subst: ∀ u:term, ∀ j k:nat,∀ l:list nat,
l = (fv_rec u k ) →lift_rec j u k = list_substT u (build_list l j) k j.

Lemma shift_subst: ∀ u:term, ∀ j k:nat,∀ l:list nat,
l = (fv u ) → shift u = list_substT u (build_list l 1) 0 1.

Lemme de commutativité auxiliaire

Lemma commut_lift_subst_list_aux : ∀ t k k' j, k'≤ k →
(list_substT (lift_rec 1 t k') (build_list (fv_rec (lift_rec 1 t k') (S k)) j) (S k) j )
= (lift_rec 1 (list_substT t (build_list (fv_rec t k) j) k j) k').

Lemme de commutativité de list_subst et lift

Lemma commut_lift_subst_list : ∀ t k j,
list_substT (shift t) (build_list (fv_rec (shift t) (S k)) j) (S k) j =
shift (list_substT t (build_list (fv_rec t k) j) k j).