(** * 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'.
assert (forall a b c A B , b →→ c ->  a·(A,B)b →→ a·(A,B)c).
induction 1; eauto. 
assert (forall a b c A B, b→→c -> b·(A,B) a →→ c·(A,B) a).
induction 1; eauto.
assert (forall a b A B B', B →→ B' -> a·(A,B) b →→ a·(A,B') b).
induction 1; eauto.
assert (forall a b A A' B, A →→ A' -> a·(A,B) b →→ a·(A',B) b).
induction 1; eauto.
intros. eapply Betas_trans. apply H. apply H4. eapply Betas_trans. apply H0. apply H3. eauto.
Qed.

Hint Resolve Betas_App.

Lemma Betas_La : forall A A' M M', A →→ A' -> M →→ M' -> λ[A],M →→ λ[A'],M'.
assert (forall a b c , a →→ b -> λ[c],  a →→ λ[c], b).
induction 1; eauto.
assert (forall a b c, a →→ b -> λ[a], c →→ λ[b], c).
induction 1; eauto.
eauto.
Qed.


Hint Resolve Betas_La.


Lemma Betas_Pi : forall A A' B B', A →→ A' -> B →→ B' -> Π(A),B →→ Π(A'),B'.
assert (forall a b c , a →→ b -> Π (c), a →→ Π(c), b).
induction 1; eauto.
assert (forall a b c, a →→ b -> Π(a), c →→ Π(b), c).
induction 1; eauto.
eauto.
Qed.

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.
induction 1; intuition.
eapply Betas_trans. eapply Betas_App. eapply Betas_La. apply Betas_refl.
apply IHBetap1. apply IHBetap2. apply Betas_refl. apply Betas_refl.
constructor. econstructor.
Qed.

Lemma Betaps_to_Betas : forall M N, M →→' N -> M →→ N.
induction 1; eauto. apply Betap_to_Betas in H; trivial.
Qed.

Lemma Betap_refl : forall M, M →' M.
induction M; intuition.
Qed.

Hint Resolve Betap_refl.

Lemma Betaps_Beta_closure : forall M N,  M → N -> M →' N.
induction 1; intuition.
Qed.

Lemma Betaps_Betas_closure :  forall M N, M →→ N -> M →→' N.
induction 1. intuition.
apply Betaps_Beta_closure in  H; intuition.
eauto.
Qed.

End red_mod.