Name Term sublanguage of Typed Adapton

name_term_lang.v

(* The 'Name Term' sublanguage of Typed Adapton. *)
(* See: https://arxiv.org/pdf/1610.00097v2.pdf
        Figure 6 (top) 
    and Figure 8 (top) 
*)

Inductive sort : Set := 
  | Arr  : sort -> sort -> sort
  | Nm   : sort
  | Prod : sort -> sort -> sort
  | Unit : sort
.
Inductive var : Set := Z | S : var -> var.
Inductive tag : Set := One | Two.
Inductive ntm : Set :=
  | Lam  : var -> ntm -> ntm
  | Var  : var -> ntm
  | App  : ntm -> ntm -> ntm
  | Tag  : ntm -> tag -> ntm
  | Pair : ntm -> ntm -> ntm
  | Triv : ntm
.
Inductive ctx : Set :=
  | Ctx_emp : ctx
  | Ctx_var : ctx -> var -> sort -> ctx
.

Fixpoint vareq (x y:var) : bool :=
  match (x, y) with
   | (Z, Z)       => true
   | (S(x), S(y)) => vareq x y
   | _            => false
  end
.

Fixpoint ctx_find (Γ:ctx) (x:var) : (option sort) :=
  match Γ with
   | Ctx_emp      => None
   | Ctx_var Γ y γ => if vareq x y then Some γ else (ctx_find Γ x)
  end
.

(* Name-term Sorting Derivations *)
(* See: Figure 8, top *)
Inductive d_sort : ctx -> ntm -> sort -> Prop :=
 | Ds_Pair : forall Γ M N γ1 γ2,
    d_sort Γ M γ1
 -> d_sort Γ N γ2
 -> d_sort Γ (Pair M N) (Prod γ1 γ2)

 | Ds_Unit : forall Γ,
    d_sort Γ Triv Unit

 | Ds_Var : forall Γ x γ,
     (ctx_find Γ x = (Some γ))
 ->  d_sort Γ (Var x) γ

 | Ds_Lam : forall Γ M γ1 γ2 x,
    d_sort (Ctx_var Γ x γ1) M γ2
 -> d_sort Γ (Lam x M) (Arr γ1 γ2)

 | Ds_Tag : forall Γ t M,
    d_sort Γ M Nm
 -> d_sort Γ (Tag M t) Nm

 | Ds_App : forall Γ M N γ1 γ2,
    d_sort Γ M (Arr γ1 γ2)
 -> d_sort Γ N γ1
 -> d_sort Γ (App M N) γ2
.


Fixpoint subst (N:ntm) (x:var) (M:ntm) : ntm :=
 match M with
  | Triv       => Triv
  | Var y      => if vareq x y then N       else M
  | Lam y M    => if vareq x y then Lam y M else Lam y (subst N x M)
  | App M1 M2  => App  (subst N x M1) (subst N x M2)
  | Pair M1 M2 => Pair (subst N x M1) (subst N x M2)
  | Tag M t    => Tag  (subst N x M) t
 end
.

Inductive val : ntm -> Prop :=
 | V_Lam : forall M x,
    val (Lam x M)
 | V_Triv : val Triv
 | V_Pair : forall M N,
    val N
 -> val M
 -> val (Pair M N)
 | V_Tag : forall M t,
    val M
 -> val (Tag M t)
.

Inductive d_eval : ntm -> ntm -> Prop :=
 | De_App : forall M N x M' V,
    d_eval M (Lam x M')
 -> d_eval N V
 -> d_eval (App M N) (subst V x M')

 | De_Pair : forall M1 V1 M2 V2,
    d_eval M1 V1
 -> d_eval M2 V2
 -> d_eval (Pair M1 M2) (Pair V1 V2)

 | De_Tag : forall M V t,
     d_eval M V
 ->  d_eval (Tag M t) (Tag V t)

 | De_Val : forall M,
    val M
 -> d_eval M M
.

Theorem subst_lemma : forall Γ M γ1 x N γ2
  (S_M : d_sort Γ M γ1)
  (S_N : d_sort (Ctx_var Γ x γ1) N γ2),
  d_sort Γ (subst M x N) γ2.
Proof.
Admitted.


Theorem subjred : 
forall M γ, d_sort Ctx_emp M γ
->
forall V,   d_eval M V
-> 
            d_sort Ctx_emp V γ.
Proof.
intros M γ .
intro S.
induction S.
(* Pair *)
intros V E. inversion E. 
  apply Ds_Pair. auto. auto. 
  apply Ds_Pair. auto. auto.
(* Unit *)
intros V E. inversion E.
  apply Ds_Unit.
(* Var *)
intros V E. inversion E.
  apply Ds_Var. apply H.
(* Lam *)
intros V E. inversion E.
  apply Ds_Lam. apply S0.
(* Tag *)
intros V E. inversion E.
  apply Ds_Tag. auto. 
  apply Ds_Tag. apply S0.
(* App *)
intros V E. inversion E.
  apply IHS1 in H1.
  apply subst_lemma with (γ1 :=  γ1). auto.
  inversion H1. auto.
  apply Ds_App with (γ1 := γ1).
  auto. auto.
Qed.

(*
Inductive ectx : Set := 
  | Emp 
  | Equiv : ectx -> var -> var -> sort -> ectx
  | Disj  : ectx -> var -> var -> sort -> ectx
.
*)