Require Import List.
Require Import String.
Open Scope string_scope.

Definition var := string.

Inductive Expr : Set :=
| Var : var -> Expr
| App : Expr -> Expr -> Expr
| Lam : var -> Expr -> Expr.

Notation "'V' x" := (Var x) (at level 48).
Notation "e1 @ e2" := (App e1 e2) (at level 49).
Notation "\ x , t" := (Lam x t) (at level 50).

Check (\"x", \"y", V"x").
Check (\"x", \"y", V"y").
Check ((\"x", V"x" @ V"x") @ (\"x", V"x" @ V"x")).

Inductive Subst : Expr -> Expr -> var ->
                  Expr -> Prop :=
| SubstVar_same : forall e x,
  Subst (V x) e x e
| SubstVar_diff : forall e x1 x2,
  x1 <> x2 ->
  Subst (V x1) e x2 (V x1)
| SubstApp : forall eA eB e x eA' eB',
  Subst eA e x eA' ->
  Subst eB e x eB' ->
  Subst (eA @ eB) e x (eA' @ eB')
| SubstLam_same : forall eA e x,
  Subst (\x, eA) e x (\x, eA)
| SubstLam_diff : forall eA e x1 x2 eA',
  x1 <> x2 ->
  Subst eA e x2 eA' ->
  Subst (\x1, eA) e x2 (\x1, eA').

Lemma subst_test_1:
  Subst (\"x", V"y") (V"z") "y" (\"x", V"z").
Proof.
  constructor.
  { discriminate. }
  { constructor. }
Qed.

Lemma subst_test_2:
  Subst (\"x", V"x") (V"z") "x"
        (\"x", V"x").
Proof.
  constructor.
Qed.

       e1 --> e1'
  ---------------------
    e1 e2 --> e1' e2

  -----------------------------
    (\x. e1) e2 --> e1[e2/x]

Inductive SStep : Expr -> Expr -> Prop :=
| Scrunch : forall e1 e1' e2,
  SStep e1 e1' ->
  SStep (e1 @ e2) (e1' @ e2)
| Ssubst : forall x e1 e2 e1',
  Subst e1 e2 x e1' ->
  SStep ((\x, e1) @ e2) e1'.

Notation "e1 --> e2" := (SStep e1 e2) (at level 51).

Lemma sstep_test_1:
  (\"x", V"x") @ V"z" --> V"z".
Proof.
  apply Ssubst.
  apply SubstVar_same.
Qed.

Lemma Lam_nostep:
  forall x e1 e2,
  ~ (\x, e1 --> e2).
Proof.
  intros. intro. inversion H.
Qed.

Lemma Subst_det:
  forall e1 e2 x e3 e3',
  Subst e1 e2 x e3 ->
  Subst e1 e2 x e3' ->
  e3 = e3'.
Proof.
  intros. induction H.
  - inversion H0; subst.
    + reflexivity.
    + congruence.
  - inversion H0; subst.
    + congruence.
    + reflexivity.
  - inversion H0; subst.
Abort.

Lemma Subst_det:
  forall e1 e2 x e3,
  Subst e1 e2 x e3 ->
  forall e3',
  Subst e1 e2 x e3' ->
  e3 = e3'.
Proof.
  induction 1; intros.
  { inversion H; subst; auto.
    congruence.
  }
  { inversion H0; subst; auto.
    congruence.
  }
  { inversion H1; subst; auto.
    f_equal; auto.
  }
  { inversion H; subst; auto.
    congruence.
  }
  { inversion H1; subst; auto.
    { congruence. }
    { f_equal; auto. }
  }
Qed.

Lemma SStep_det:
  forall e e1,
  e --> e1 ->
  forall e2,
  e --> e2 ->
  e1 = e2.
Proof.
  intro. intro. intro. induction H.
  { intros. inversion H0.
    { subst. f_equal. auto. }
    { subst. apply Lam_nostep in H. contradiction. }
  }
  { intros. inversion H0.
    { subst. apply Lam_nostep in H4. contradiction. }
    { subst. eapply Subst_det in H5.
      { eassumption. }
      { assumption. }
    }
  }
Qed.