(** This file models a very simple functional language known as the 
    simply-typed lambda calculus (with nat's).  *)
Require Import String.
Require Import List.

(** We only have two kinds of types:  natural numbers and functions. *)
Inductive type : Type := 
| Nat_t : type
| Arrow_t : type -> type -> type.

(** We will represent variables as strings -- later, we'll discuss 
    alternative representations and the problems that arise when 
    using simple first-order data structures to represent and reason
    about variables. *)
Definition var := string.

(** Expressions have only 4 forms:  variables, constants, functions, 
    and function calls. *)
Inductive exp : Type := 
| Var_e : var -> exp
| Num_e : nat -> exp
| Lam_e : var -> exp -> exp
| App_e : exp -> exp -> exp.

(** When we evaluate a program, we get out a [value].  Values are 
    a subset of the expressions and include just numbers and functions. *)
Definition value(e:exp) : Prop := 
  match e with 
    | Num_e _ => True
    | Lam_e _ _ => True
    | _ => False
  end.

(** We'll model function call using substitution.  Note that this is
    not a form of capture-avoiding substitution, so it assumes that 
    the free variables of [v] do not conflict with the bound variables
    in [e].  Here, we're only going to consider substituting closed
    expressions (those with no free variables) so this won't be an 
    issue. *)
Fixpoint subst(v:exp)(x:var)(e:exp) := 
  match e with 
    | Var_e y => if string_dec x y then v else Var_e y
    | Num_e n => Num_e n
    | Lam_e y e => if string_dec x y then Lam_e y e else Lam_e y (subst v x e)
    | App_e e1 e2 => App_e (subst v x e1) (subst v x e2)
  end.

(** A little notation for substitution. *)
Notation "e @ [ x '|->' v ] " := (subst v x e) (at level 60).


(** We reserve some notation for use in the definition below.  This
    will be our big-step semantics for expressions and is intended
    to mean that expression [e] evaluates to value [v].   Notice that
    here we are modeling call-by-name, whereas most languages use 
    call-by-value.  In particular, we don't evaluate the argument before
    substituting it for a formal parameter.  In a call-by-value setting,
    we evaluate the argument before substitution.  In a call-by-need
    setting (e.g., Haskell) we have to do something much more complicated. *)
Reserved Notation "e ==> v" (at level 70).

Inductive cbn_evals : exp -> exp -> Prop := 
| Num_cbn : forall n, Num_e n ==> Num_e n
| Lam_cbn : forall x e, Lam_e x e ==> Lam_e x e
| App_cbn : forall e1 e2 x e1' v, 
  e1 ==> Lam_e x e1' -> 
  e1' @ [ x |-> e2 ] ==> v ->
    App_e e1 e2 ==> v
where "e ==> v" := (cbn_evals e v).

Lemma evals_value : forall e1 e2, cbn_evals e1 e2 -> value e2.
Proof.
  induction 1 ; subst ; simpl ; auto.
Qed.
 
(** Let us now define a small-step semantics for our language. We begin
    by defining the notion of a single step. *)
Reserved Notation "e1 --> e2" (at level 70).

Inductive cbn_step : exp -> exp -> Prop := 
| Beta_cbn : forall x e1 e2, 
  App_e (Lam_e x e1) e2 --> e1 @ [ x |-> e2 ]
| App_steps : forall e1 e2 e1', 
  e1 --> e1' -> 
  App_e e1 e2 --> App_e e1' e2
where "e1 --> e2" := (cbn_step e1 e2).

(** We then extend this to a reflexive, transitive closure of the
    single-step relation. *)
Reserved Notation "e1 '-->*' e2" (at level 70).
Inductive cbn_steps : exp -> exp -> Prop := 
| Refl_cbn : forall e, e -->* e
| Step_cbn : forall e1 e2 e3, e1 --> e2 -> e2 -->* e3 -> e1 -->* e3
where "e1 '-->*' e2" := (cbn_steps e1 e2).

Lemma steps_append : forall e1 e2 e3,
  e1 -->* e2 -> 
  e2 -->* e3 ->
  e1 -->* e3.
Proof.
  Hint Constructors cbn_steps. (* tells auto to try constructors *)
  induction 1 ; eauto.
  (* Full proof
  induction 1.
  auto.
  intro.
  eapply Step_cbn.
  apply H.
  apply IHcbn_steps.
  auto. *)
Qed.

Lemma steps_app : forall e1 e2 e1',
  e1 -->* e1' ->
  App_e e1 e2 -->* App_e e1' e2.
Proof.
  induction 1.
  constructor.
  assert (App_e e1 e2 --> App_e e0 e2).
  econstructor. auto.
  econstructor. eauto. auto.
Qed.

(** We can argue that the two semantics are equivalent. *)
Lemma cbn_eval_equiv_cbn_steps : 
  forall e v, value v -> (e ==> v <-> e -->* v).
Proof.
  intros. split.
  induction 1 ; try constructor. simpl in *.
  specialize (IHcbn_evals1 I).
  specialize (IHcbn_evals2 H).
  assert (App_e e1 e2 -->* App_e (Lam_e x e1') e2).
  apply steps_app ; auto.
  assert (App_e (Lam_e x e1') e2 -->* v).
  econstructor. econstructor. auto.
  eapply steps_append. eauto. auto.

  induction 1.
  destruct e ; simpl in H ; try contradiction ; constructor.
  specialize (IHcbn_steps H).
  Lemma big_cons e1 e2 e3 :
    e1 --> e2 ->
    e2 ==> e3 ->
    e1 ==> e3.
  Proof.
    induction 1. intros.
    econstructor. econstructor. auto.
    intro.
    Lemma big_app e1 e2 e1' e3 :
      e1 --> e1' ->
      App_e e1' e2 ==> e3 ->
      App_e e1 e2 ==> e3.
      Admitted.
    apply (big_app e1 e2 e1' e3) ; auto.
Qed.

(** Now we're going to consider a well-formedeness (typing) relation on
    terms.  The basic idea is that we want to rule out "stuck" expressions
    where e.g., we have an unbound variable, or we pass an argument of
    the wrong type to a function, or we try to "apply" a number instead
    of a function.  *)

(** We begin by defining contexts as lists of variables and types -- these
    are our assumptions.  If you like, this is a kind of symbol table. *)
Definition context := list (var * type).

(** We use a last-in-first-out lookup to lookup a variable's type. *)
Fixpoint lookup (x:var) (G:context) : option type := 
  match G with 
    | nil => None
    | p::rest => if string_dec x (fst p) then Some (snd p) else lookup x rest
  end.

(** Our typing relation can be read:  Under the assumptions in context [G], 
    expression [e] has type [t].  That is, when evaluated, [e] will not get
    stuck and will produce a value of type [t]. *)
Reserved Notation "G '|-' e ';' t" (at level 70).

Inductive hasType : context -> exp -> type -> Prop := 
| Nat_ht : forall G n, G |- Num_e n ; Nat_t
| Var_ht : forall G x t, lookup x G = Some t -> G |- Var_e x ; t
| App_ht : forall G e1 e2 t2 t, 
  G |- e1 ; Arrow_t t2 t -> 
    G |- e2 ; t2 -> 
      G |- App_e e1 e2 ; t
| Lam_ht : forall G x e t1 t2, 
  (x,t1)::G |- e ; t2 -> 
    G |- Lam_e x e ; Arrow_t t1 t2
where "G |- e ';' t" := (hasType G e t).

(** Next, we want to prove that well-typed programs won't get stuck.  
   Alternatively, we can argue that every well-typed program is already
   a (well-typed) value, or else it can take a step to a well-typed
   program.  That's the positive way of saying it won't get stuck. 
   Notice that we can't easily talk about this using the big-step
   semantics because it doesn't differentiate getting stuck from 
   possible divergence.  So we'll use the small-step semantics to
   argue this.
*)

(** Our proof will break into two lemmas.  One is a lemma that says
    well-formedness is preserved when taking a step.  The other argues
    that if we're well-formed, then we are either a value or can take
    a step.  Then soundness follows by induction on the number of steps
    we take. *)

Lemma progress : forall e t, 
  nil |- e ; t -> 
    value e \/ (exists e', e --> e').
Proof.
  intros.
  remember (@nil (var * type)) as g'.
  induction H ; try (left ; constructor). subst. simpl in *. congruence.
  subst. simpl in *.
  right ; destruct IHhasType1 ; auto ; destruct IHhasType2 ; auto. 
  destruct e1 ; destruct H1 ; inversion H ; econstructor ; econstructor.
  destruct e1 ; destruct H1 ; inversion H ; econstructor ; econstructor.
  destruct e1 ; destruct H1 ; inversion H ; econstructor ; econstructor ; apply H1.
  destruct e1 ; destruct H1 ; inversion H ; econstructor ; econstructor ; apply H1.
Qed.

(*Lemma value_stop : forall v e, (value v) -> v --> e -> False.
Proof.
  intros ; destruct H0 ; simpl in * ; auto.
Qed.*)

Lemma weaken : forall G1 e t,
  G1 |- e ; t -> 
  forall G2, 
    (forall x t2, lookup x G1 = Some t2 -> lookup x G2 = Some t2) ->
     G2 |- e ; t.
Proof.
  induction 1 ; intros ; econstructor ; eauto.
  eapply IHhasType. simpl in *.
  intros.
  destruct (string_dec x0 x). auto.
  apply H0.
  auto.
Qed.

Corollary weaken_closed : forall G e t, 
  nil |- e ; t -> G |- e ; t.
Proof.
  intros.
  eapply weaken.
  eauto.
  intros. simpl in *.
  congruence.
Qed.

Lemma preservation : forall e1 e2,
  e1 --> e2 ->
  forall t,
    nil |- e1 ; t ->
    nil |- e2 ; t.
Proof.
  induction 1 ; intros. Focus 2.
  inversion H0 ; subst ; clear H0.
  econstructor. eapply IHcbn_step ; eauto ; auto. auto.
  inversion H ; subst ; clear H.
  inversion H3 ; subst ; clear H3.
  Lemma preservation_subst : forall e2 t2 G e t x,
    nil |- e2 ; t2 ->
    G |- e ; t ->
      forall G1,
        lookup x G1 = None ->
        G = G1 ++ (x,t2) :: nil ->
        G1 |- e @ [x |-> e2] ; t.
  Proof.
    induction 2 ; simpl ; intros ; subst. constructor.
    destruct string_dec. subst.
    Lemma lookup_weaken : forall x (G1 G2:context),
      lookup x (G1 ++ G2) =
      match lookup x G1 with
        | None => lookup x G2
        | Some t => Some t
      end.
    Admitted.
    rewrite lookup_weaken in H0.
    rewrite H1 in H0. simpl in H0. destruct string_dec ; try congruence.
    injection H0 ; intros ; subst.
    apply weaken_closed. auto.
    Lemma foo : forall G1 x0 x t2 t, lookup x0 (G1 ++ (x, t2)::nil) = Some t ->
      x <> x0 -> lookup x0 G1 = Some t.
    Proof.
      induction G1 ; simpl ; intros. destruct string_dec ; simpl in * ; try congruence.
      destruct a. simpl in *. destruct string_dec ; simpl in *.
      auto. eapply IHG1 ; eauto.
    Qed.
    constructor.
    eapply foo. eauto. auto.
    econstructor.
    eauto.
    eapply (IHhasType2). eauto. auto.
    destruct string_dec.
    Admitted.
  Admitted.

Theorem soundness : forall e t e', 
  nil |- e ; t -> 
    e -->* e' -> value e' \/ (exists e'', e' --> e'').
Proof.
  intros e t e' H1 H2. induction H2. apply (progress _ _ H1). 
  apply IHcbn_steps. eapply preservation ; eauto.
Qed.