Library red
Beta reduction for annotated terms
As for the usual terms, we extend the definition of Beta to handle the two additional annotations. Since we want to prove that the typed version of the reduction is confluent, we don't care to prove it for this version.
Require Import Peano_dec.
Require Import Compare_dec.
Require Import Lt.
Require Import Le.
Require Import Gt.
Require Import Plus.
Require Import Minus.
Require Import Bool.
Require Import base.
Require Import term.
Module Type red_mod (X:term_sig) (TM:term_mod X).
Import TM.
Reserved Notation " A → B " (at level 80).
Inductive Beta : Term -> Term -> Prop :=
| Beta_head : forall A M N K L , (λ[ A ], M)·(K,L) N → M [← N]
| Beta_red1 : forall M M' N A B, M → M' -> M·(A,B) N → M'·(A,B) N
| Beta_red2 : forall M N N' A B, N → N' -> M·(A,B) N → M ·(A,B) N'
| Beta_red3 : forall M N A B B', B → B' -> M·(A,B) N → M ·(A,B') N
| Beta_red4 : forall M N A A' B, A → A' -> M·(A,B) N → M ·(A',B) 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) : Typ_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) : Typ_scope.
Hint Constructors Beta Betas.
Lemma Betas_App : forall M M' N N' A A' B B', M →→ M' -> N →→ N' -> A →→ A' -> B →→ B' ->
M·(A,B)N →→ M'·(A',B')N'.
Hint Resolve Betas_App.
Lemma Betas_La : forall A A' M M', A →→ A' -> M →→ M' -> λ[A],M →→ λ[A'],M'.
Hint Resolve Betas_La.
Lemma Betas_Pi : forall A A' B B', A →→ A' -> B →→ B' -> Π(A),B →→ Π(A'),B'.
Hint Resolve Betas_Pi.
Reserved Notation "M →' N" (at level 80).
Inductive Betap : Term -> Term -> Prop :=
| Betap_sort : forall s , !s →' !s
| Betap_var : forall v , #v →' #v
| 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' A A' B B', M →' M' -> N →' N' -> A →' A' -> B →' B' ->
M ·(A,B) N →' M'·(A',B') N'
| Betap_head : forall A M M' N N' K L , M →' M' -> N →' N' -> (λ[A],M)·(K,L) N →' M'[← N']
where "A →' B" := (Betap A B ) : Typ_scope.
Reserved Notation "M →→' N" (at level 80).
Inductive Betaps : Term -> Term -> Prop :=
| Betaps_intro : forall M N , M →' N -> M →→' N
| Betaps_trans : forall M N P, M →→' N -> N →→' P -> M →→' P
where "M →→' N" := (Betaps M N) : Typ_scope.
Hint Constructors Betap Betaps.
Lemma Betap_to_Betas : forall M N, M →' N -> M →→ N.
Lemma Betaps_to_Betas : forall M N, M →→' N -> M →→ N.
Lemma Betap_refl : forall M, M →' M.
Hint Resolve Betap_refl.
Lemma Betaps_Beta_closure : forall M N, M → N -> M →' N.
Lemma Betaps_Betas_closure : forall M N, M →→ N -> M →→' N.
End red_mod.
Require Import Compare_dec.
Require Import Lt.
Require Import Le.
Require Import Gt.
Require Import Plus.
Require Import Minus.
Require Import Bool.
Require Import base.
Require Import term.
Module Type red_mod (X:term_sig) (TM:term_mod X).
Import TM.
Reserved Notation " A → B " (at level 80).
Inductive Beta : Term -> Term -> Prop :=
| Beta_head : forall A M N K L , (λ[ A ], M)·(K,L) N → M [← N]
| Beta_red1 : forall M M' N A B, M → M' -> M·(A,B) N → M'·(A,B) N
| Beta_red2 : forall M N N' A B, N → N' -> M·(A,B) N → M ·(A,B) N'
| Beta_red3 : forall M N A B B', B → B' -> M·(A,B) N → M ·(A,B') N
| Beta_red4 : forall M N A A' B, A → A' -> M·(A,B) N → M ·(A',B) 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) : Typ_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) : Typ_scope.
Hint Constructors Beta Betas.
Lemma Betas_App : forall M M' N N' A A' B B', M →→ M' -> N →→ N' -> A →→ A' -> B →→ B' ->
M·(A,B)N →→ M'·(A',B')N'.
Hint Resolve Betas_App.
Lemma Betas_La : forall A A' M M', A →→ A' -> M →→ M' -> λ[A],M →→ λ[A'],M'.
Hint Resolve Betas_La.
Lemma Betas_Pi : forall A A' B B', A →→ A' -> B →→ B' -> Π(A),B →→ Π(A'),B'.
Hint Resolve Betas_Pi.
Reserved Notation "M →' N" (at level 80).
Inductive Betap : Term -> Term -> Prop :=
| Betap_sort : forall s , !s →' !s
| Betap_var : forall v , #v →' #v
| 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' A A' B B', M →' M' -> N →' N' -> A →' A' -> B →' B' ->
M ·(A,B) N →' M'·(A',B') N'
| Betap_head : forall A M M' N N' K L , M →' M' -> N →' N' -> (λ[A],M)·(K,L) N →' M'[← N']
where "A →' B" := (Betap A B ) : Typ_scope.
Reserved Notation "M →→' N" (at level 80).
Inductive Betaps : Term -> Term -> Prop :=
| Betaps_intro : forall M N , M →' N -> M →→' N
| Betaps_trans : forall M N P, M →→' N -> N →→' P -> M →→' P
where "M →→' N" := (Betaps M N) : Typ_scope.
Hint Constructors Betap Betaps.
Lemma Betap_to_Betas : forall M N, M →' N -> M →→ N.
Lemma Betaps_to_Betas : forall M N, M →→' N -> M →→ N.
Lemma Betap_refl : forall M, M →' M.
Hint Resolve Betap_refl.
Lemma Betaps_Beta_closure : forall M N, M → N -> M →' N.
Lemma Betaps_Betas_closure : forall M N, M →→ N -> M →→' N.
End red_mod.