Library ut_red

Beta-reduction definition and properties.

Require Import base ut_term.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt Plus.

Module Type ut_red_mod (X:term_sig) (TM : ut_term_mod X).
 Import TM.

Usual Beta-reduction:

  • one step
  • multi step (reflexive, transitive closure)
  • converesion (reflexive, symetric, transitive closure)
Reserved Notation " A → B " (at level 80).

Inductive Beta : Term -> Term -> Prop :=
 | Beta_head : forall A M N , (λ[A], M)· N → M [← N]
 | Beta_red1 : forall M M' N , M → M' -> M · N → M'· N
 | Beta_red2 : forall M N N', N → N' -> M · N → M · N'
 | Beta_lam : forall A M M', M → M' -> λ[A],M → λ[A ],M'
 | Beta_lam2 : forall A A' M , A → A' -> λ[A],M → λ[A'],M
 | Beta_pi : forall A B B', B → B' -> Π(A),B → Π(A ),B'
 | Beta_pi2 : forall A A' B , A → A' -> Π(A),B → Π(A'),B
where "M → N" := (Beta M N) : UT_scope.

Reserved Notation " A →→ B " (at level 80).

Inductive Betas : Term -> Term -> Prop :=
 | Betas_refl : forall M , M →→ M
 | Betas_Beta : forall M N , M → N -> M →→ N
 | Betas_trans : forall M N P, M →→ N -> N →→ P -> M →→ P
where " A →→ B " := (Betas A B) : UT_scope.

Reserved Notation " A ≡ B " (at level 80).

Inductive Betac : Term -> Term -> Prop :=
 | Betac_Betas : forall M N , M →→ N -> M ≡ N
 | Betac_sym : forall M N , M ≡ N -> N ≡ M
 | Betac_trans : forall M N P, M ≡ N -> N ≡ P -> M ≡ P
where " A ≡ B " := (Betac A B) : UT_scope.

Hint Constructors Beta.
Hint Constructors Betas.
Hint Constructors Betac.

Facts about Betas and Betac: Congruence.
Lemma Betac_refl : forall M, M ≡ M.

Hint Resolve Betac_refl.

Lemma Betas_App : forall M M' N N',M →→ M' -> N →→ N' -> M · N →→ M' · N'.

Hint Resolve Betas_App.

Lemma Betac_App : forall M M' N N' , M ≡ M' -> N ≡ N' -> M · N ≡ M' · N'.

Hint Resolve Betac_App.

Lemma Betas_La : forall A A' M M', A →→ A' -> M →→ M' -> λ[A],M →→ λ[A'],M'.

Hint Resolve Betas_La.

Lemma Betac_La: forall A A' M M', A ≡ A' -> M ≡ M' -> λ[A],M ≡ λ[A'],M'.

Hint Resolve Betac_La.

Lemma Betas_Pi : forall A A' B B', A →→ A' -> B →→ B' -> Π(A),B →→ Π(A'),B'.

Hint Resolve Betas_Pi.

Lemma Betac_Pi : forall A A' B B', A ≡ A' -> B ≡ B' -> Π(A),B ≡ Π(A'),B'.

Hint Resolve Betac_Pi.

Lemma Beta_beta : forall M N P n, M → N -> M[n←P] → N[n←P] .

Some "inversion" lemmas :
  • a variable/sort cannot reduce at all
  • a pi/lam can only reduce to another pi/lam
  • ...
Lemma Betas_V : forall x N, #x →→ N -> N = #x.

Lemma Betas_S : forall s N, !s →→ N -> N = !s.

Lemma Betas_Pi_inv : forall A B N, Π(A), B →→ N ->
  exists C, exists D, N = Π(C), D /\ A →→ C /\ B →→ D.

Lift properties.
Lemma Beta_lift: forall M N n m, M → N -> M ↑ n # m → N ↑ n # m .

Lemma Betas_lift : forall M N n m , M →→ N -> M ↑ n # m →→ N ↑ n # m .

Lemma Betac_lift : forall M N n m, M ≡ N -> M ↑ n # m ≡ N ↑ n # m .

Hint Resolve Beta_lift Betas_lift Betac_lift.

Subst properties.
Lemma Betas_subst : forall M P P' n, P →→ P' -> M [n←P] →→ M[n← P'].

Hint Resolve Betas_subst.

Lemma Betas_subst2 : forall M N P n, M →→ N -> M [n← P] →→ N [n ← P].

Hint Resolve Betas_subst2.

Lemma Betac_subst : forall M P P' n, P ≡ P' -> M[n←P] ≡ M [n←P'].

Lemma Betac_subst2 : forall M N P n,
  M ≡ N -> M[n←P] ≡ N[n← P] .

Hint Resolve Betac_subst Betac_subst2.

Parallel Reduction

We use the parallel reduction to prove that Beta is confluent.
Reserved Notation "M →' N" (at level 80).

Beta parallel definition.
Inductive Betap : Term -> Term -> Prop :=
 | Betap_sort : forall s , !s →' !s
 | Betap_var : forall x , #x →' #x
 | Betap_lam : forall A A' M M' , A →' A' -> M →' M' -> λ[A],M →' λ[A'],M'
 | Betap_pi : forall A A' B B' , A →' A' -> B →' B' -> Π(A),B →' Π(A'),B'
 | Betap_app : forall M M' N N' , M →' M' -> N →' N' -> M · N →' M' · N'
 | Betap_head : forall A M M' N N', M →' M' -> N →' N' -> (λ[A],M)· N →' M'[← N']
where "M →' N" := (Betap M N) : UT_scope.

Notation "m →' n" := (Betap m n) (at level 80) : UT_scope.

Hint Constructors Betap.

Lemma Betap_refl : forall M, M →' M.

Hint Resolve Betap_refl.

Lift and Subst property of Betap.
Lemma Betap_lift: forall M N n m, M →' N -> M ↑ n # m →' N ↑ n # m .

Hint Resolve Betap_lift.

Lemma Betap_subst:forall M M' N N' n, M →' M' -> N →' N' -> M[n←N] →' M'[n←N'].

Hint Resolve Betap_subst.

Betap has the diamond property.
Lemma Betap_diamond : forall M N P,
   M →' N -> M →' P -> exists Q, N →' Q /\ P →' Q.

Reflexive Transitive closure of Betap.
Reserved Notation " x →→' y " (at level 80).

Inductive Betaps : Term -> Term -> Prop :=
 | Betaps_refl : forall M , M →→' M
 | Betaps_trans : forall M N P, M →' N -> N →→' P -> M →→' P
where " x →→' y " := (Betaps x y) : UT_scope.

Hint Constructors Betaps.

Closure properties to relate Betaps and Betas.
Lemma Betas_Betap_closure : forall M N , M →' N -> M →→ N.

Local Hint Resolve Betas_Betap_closure.

Lemma Betas_Betaps_closure : forall M N, M →→' N -> M →→ N.

Lemma Betap_Beta_closure : forall M N, M → N -> M →' N.

Local Hint Resolve Betas_Betaps_closure Betap_Beta_closure.

Lemma Betaps_Beta_closure :forall M N, M → N -> M →→' N.

Local Hint Resolve Betaps_Beta_closure.

Lemma Betaps_trans2 : forall M N P, M →→' N -> N →→' P -> M →→' P.

Local Hint Resolve Betaps_trans2.

Lemma Betaps_Betas_closure : forall M N , M →→ N -> M →→' N.

Local Hint Resolve Betaps_Betas_closure.

Betas inherites its diamond property from Betaps.
Lemma sub_diamond_Betaps :
( forall M N P, M →' N -> M →' P -> exists Q, N →' Q /\ P →' Q )
 -> forall M N P, M →' N -> M →→' P -> exists Q, N →→' Q /\ P →' Q .

Lemma diamond_Betaps :
( forall M N P, M →' N -> M →' P -> exists Q, N →' Q /\ P →' Q) ->
  forall M N P, M →→' N -> M →→' P -> exists Q, N →→' Q /\ P →→' Q .

Theorem Betas_diamond:
  forall M N P, M →→ N -> M →→ P -> exists Q, N →→ Q /\ P →→ Q.

So Beta is confluent.
Theorem Betac_confl : forall M N, M ≡ N -> exists Q, M →→ Q /\ N →→ Q.

Some consequences:
  • convertible sorts are equals
  • converitble vars are equals
  • Pi-types are Injective
  • Pi and sorts are not convertible
Lemma conv_sort : forall s t, !s ≡ !t -> s = t.

Lemma conv_to_sort : forall s T, !s ≡ T -> T →→ !s.

Lemma conv_var : forall x y, #x ≡ #y -> x = y.

Lemma conv_to_var : forall x T , #x ≡ T -> T →→ #x.

Theorem PiInj : forall A B C D, Π(A), B ≡ Π(C), D -> A ≡ C /\ B ≡ D.

Lemma Betac_not_Pi_sort : forall A B s, ~ (Π(A), B ≡ !s ).

End ut_red_mod.