From Coq Require Import Unicode.Utf8.
From Equations Require Import Equations.
Require Import Notations.
Require Import Ltac.
Require Import Logic.
Require Import Specif.

(* 
This codes implements an implicitly typed version of the simple lambda calculus. 
Terms are identified with derivations. 
*)

(* We define simple types as follows *)
Inductive SimpleTypes:= 
  | base : SimpleTypes
  | arrow: SimpleTypes -> SimpleTypes -> SimpleTypes
.

(* We introduce some notation to make our lives easier. *)
Notation "$ A" := (base A) (at level 40).
Notation "A --> B" := (arrow A B) (at level 60, right associativity).

(* The next definition defines contexts, a context in our system is a list of 
simple types, which are identified with variables of that type *)
Inductive Context := 
  | empty : Context
  | append : Context -> SimpleTypes -> Context.

Notation "[]" := empty (at level 40).
Notation "Γ ,, A" := (append Γ A) (at level 60, right associativity).

(* We define a predicate InContext, which checks if a variable (type) is in a 
given context. Notation is A ∈ Γ *)
Inductive InContext : SimpleTypes -> Context -> Prop := 
  | Last: forall (A : SimpleTypes) (Γ: Context), InContext (A) (Γ ,,  A)
  | Middle : forall ( A B : SimpleTypes) (Γ: Context), 
              InContext (A) Γ -> InContext (A) (Γ ,,  B)
.

Notation "A ∈ Γ" := (InContext A Γ) (at level 60, right associativity).


(* We define a predicate for judgements, 
by which we can derive variables, lambda terms, and applications from our context.
We don't define terms explicitly, but identify them with the derivations. 
Notation we use for judgement is Γ ⊢ A *)
Inductive Judgment : SimpleTypes -> Context -> Prop := 
  | Var: forall (A : SimpleTypes) (Γ: Context),  A ∈ Γ -> Judgment A Γ
  | Abs: forall (A B : SimpleTypes) (Γ: Context), Judgment B (Γ ,, A) 
          -> Judgment (A --> B) Γ
  | App: forall (A B : SimpleTypes) (Γ: Context), Judgment (A --> B) Γ
          -> Judgment A Γ -> Judgment B Γ
. 

Notation "Γ ⊢ A" := (Judgment A Γ) (at level 70). 

(* ------------------------------- *)

(* The first lemma we prove is extension. Given a map from variables of one 
context to another, we can extend the map to an extended context. *)
Lemma ext (Γ  Δ: Context) : (forall A: SimpleTypes, ( (A∈Γ) -> (A∈Δ) )) -> 
(forall A B :SimpleTypes,  (A ∈(Γ,,B)) -> (A ∈(Δ,,B)) ).
Proof.
  intros.
  inversion_clear H0.
  - apply Last.
  - apply Middle.
    apply H.
    exact H1.
Qed.

(* Next we prove renaming, used to “rebase” a term from one context to another.
If we have a map from variables of one context to another, we can extend this map 
to all terms. *)
Lemma rename (Γ  Δ: Context) : (forall A: SimpleTypes,
 ( (A∈Γ) -> (A∈Δ) )) -> 
(forall A :SimpleTypes ,  ((Γ ⊢ A) -> (Δ ⊢ A) )).
Proof.
 intros.
  revert H.
  revert Δ.
  induction H0.
  - intros.
    apply Var.
    apply H0.
    exact H.
  - intros.
    apply Abs.
    apply IHJudgment.
    intros.
    revert H1.
    apply ext.
    exact H.
  - intros.
    apply App with (A := A).
    + apply IHJudgment1.
      exact H.
    + apply IHJudgment2.
      exact H.
Qed.

(* One consequence is a form of weakening *)
Lemma weakening (Γ: Context) : (forall B A : SimpleTypes, Γ ⊢ A -> Γ,,B ⊢ A).
Proof.
  intro.
  apply rename.
  intros.
  now apply Middle.
Qed.

(* Another consequence is permutation lemma of two variables in a context *)
Lemma permute (Γ: Context) : (forall A B C : SimpleTypes, (Γ,,A),,B ⊢ C 
                              -> (Γ,,B),,A ⊢ C).
Proof.
  intro; intro.
  apply rename.
  intros.
  inversion_clear H.
  - apply Middle.
    now apply Last.
  - inversion_clear H0.
    + apply Last.
    + now repeat apply Middle.
Qed.

(* The third lemma we prove is a slightly different extension. Given a map from 
variables of one context to terms in another another, we can extend the map to 
an extended context. We use the following auxiliary lemma. *)
Lemma lem01 (Δ: Context) : (forall A B: SimpleTypes,  (Δ ⊢ A) -> (Δ,,B ⊢ A) ).
Proof.
  intros.
  apply rename with (Γ:= Δ).
  - intros.
    now apply Middle.
  - auto.
Qed.


Lemma exts (Γ  Δ: Context) : (forall A: SimpleTypes, ( (A∈Γ) -> (Δ ⊢ A) )) -> 
(forall A B :SimpleTypes,  (A ∈(Γ,,B)) -> ((Δ,,B)⊢ A) ).
Proof.
  intros.
  inversion_clear H0.
  - apply Var.
    apply Last.
  - apply lem01.
    now apply H.
Qed.

(* The next lemma proves simultaneous substitution *)
Lemma subst (Γ  Δ: Context) : (forall A: SimpleTypes, ( (A∈Γ) -> (Δ ⊢ A) )) -> 
(forall A B :SimpleTypes,  (Γ ⊢ A) -> (Δ ⊢ A) ).
Proof.
  intros.
  revert H.
  revert Δ.
  induction H0.
  - intros.
now apply H0.
  - intros.
apply Abs.
apply IHJudgment.
intros.
    apply exts with (Γ:=Γ).
    + auto.
    + auto.
  - intros.
    apply App with (A:=A).
    + now apply IHJudgment1.
    + now apply IHJudgment2.
Qed.

(* As a special instance we get single substitution, using one auxiliary lemma. *)
Lemma lem02 (Γ: Context) (B : SimpleTypes) (M : Γ ⊢ B) : (forall A : SimpleTypes,
  A∈(Γ,,B) -> Γ ⊢ A).
Proof.
  intros.
  inversion_clear H.
  - exact M.
  - now apply Var.
Qed.

Lemma single_subst (Γ: Context) (A B: SimpleTypes) :
                  ( Γ,,B ⊢ A) -> (Γ ⊢ B)  -> (Γ ⊢ A).
Proof.
  intros.
  apply subst with (Γ:=(Γ,,B)) (Δ := Γ).
  - now apply lem02.
  - auto.
  - exact H.
Qed.

(* With single substitution, we are ready to prove one-step beta reduction *)
Inductive Reduction {Γ: Context} : forall A: SimpleTypes, 
                (Γ ⊢ A) -> (Γ ⊢ A) -> Prop :=
  | xi_1: forall (A B: SimpleTypes) (L L': Γ ⊢ A --> B) (M: Γ ⊢ A),
          Reduction (A-->B) L L' -> Reduction B (App A B Γ L M)   (App A B Γ L' M)
  | xi_2: forall (A B: SimpleTypes) (V : Γ ⊢ A --> B) (M M': Γ ⊢ A),
          Reduction A M M' 
                -> Reduction B (App A B Γ V M) (App A B Γ V M')
  | xi_3 : forall (A B : SimpleTypes) (M N : Γ,,A ⊢ B), Reduction B M N ->
           Reduction (A --> B) (Abs A B Γ M) (Abs A B Γ N)
  | beta: forall (A B: SimpleTypes) (N : (Γ,,A) ⊢ B) (W: Γ ⊢ A),
          Reduction B (App A B Γ (Abs A B Γ N) W) (single_subst Γ B A N W)
.

(* We define the reflexive transitive closure, in n steps *)
Inductive Reduces {Γ : Context} {A : SimpleTypes} : (Γ ⊢ A) → (Γ ⊢ A) → Prop := 
  | refl: forall (M : Γ ⊢ A), Reduces M M
  | trans: forall (L : Γ ⊢ A) (M N : Γ ⊢ A), (Reduction A L M) -> (Reduces  M N) -> 
          Reduces L N 
. 

(* The next definition defines values, namely exactly terms of the form lambda.M *)
Inductive Value {Δ: Context} : forall C:SimpleTypes, (Δ ⊢ C) -> Prop := 
  | Value_lam : forall (A B: SimpleTypes) (N: ((Δ,,A) ⊢ B)),
                Value (A-->B) (Abs A B Δ N)
.

(* Using this, we can give an inductive definition of normal forms *)
Inductive NF {Γ : Context} : forall (A : SimpleTypes), (Γ ⊢ A) → Prop := 
  | var_nf : forall (A : SimpleTypes) (x : A∈Γ), NF A (Var A Γ x)
  | abs_nf : forall (A B : SimpleTypes) (M : Γ,,A ⊢ B), NF B M 
                -> NF (A --> B) (Abs A B Γ M)
  | app_nf : forall (A B : SimpleTypes) (M : Γ ⊢ A --> B) (N : Γ ⊢ A), NF (A --> B) M 
                -> NF A N -> ~ Value (A --> B) M -> NF B (App A B Γ M N)
.

(* Finally, we can state weak normalization theorem *)
Theorem weak_normalization {Γ : Context} {A : SimpleTypes} : forall (M : Γ ⊢ A), 
        exists (N : Γ ⊢ A), NF A N /\ (Reduces M N)
.