Library Top.Sn_Axiomatic

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 equiv.

Axiomatisation de la normalisation forte

Eta représente la longueur de la plus longue réduction de t
Parameter eta : term → nat.

Require Import NPeano.
Infix "=?" := Nat.eqb.

Ltac inv := inversion 1; subst; simpl; auto.

Definition SN := term → Prop.
Parameter sn : SN.

Axiom Ax1 : ∀ t : term,
              (∀ t': term, t --> t' → sn t' ) →
              sn t.

Axiom Ax2 : ∀ t t': term,
              sn t → t --> t' →
              (sn t' ∧ eta t' < eta t).

Axiom Ax2_stars : ∀ t t':term,
              sn(t) → t -->* t' →
              ((sn t') ∧ (eta t' ≤ eta t) ).

Axiom renommage :
  ∀ t u : term,
    sn (u ) ↔ sn ((shift u)).

Axiom renommage_subst :
  ∀ t u : term, ∀ i,
    sn (t { i := u }) ↔ sn (t {i := (shift u)}).

Axiom eta_subst_eq :
  ∀ t u : term, ∀ i,
    eta (t {i := u}) = eta (t {i := (shift u)}).

Théorèmes issus de l'axiomatisation

Theorem Ax2_stars_sn : ∀ t t':term,
                 sn(t) → t -->* t' → (sn t').

Theorem Ax2_stars_eta : ∀ t t': term,
                 sn (t) → t -->* t' → eta t' ≤ eta t .

Theorem Th2 : ∀ t t': term,
              sn t → t --> t' → (sn t').
Theorem Th3 : ∀ t t': term,
              sn t → t --> t' → (eta t' < eta t).

Lemma sn_and_eta :
  ∀ t u : term,
    sn (t {0 := u}) → sn (t {0 := (shift u)}) ∧
    eta (t {0 := u}) = eta (t {0 := (shift u)}).

Theorem Ax2_bisl :∀ t t' u u': term,
                 sn (t {0 := u}) →
                 t {0 := u} --> t' {0 := u} →
                 (sn (t' {0 := u }) ∧
                  eta t' {0 := u } + eta u < eta t {0 := u} + eta u).