Require Import String.
Open Scope string_scope.


Notation var := string.
Definition var_eq : forall x y : var, {x = y} + {x <> y} := string_dec.
Infix "==v" := var_eq (no associativity, at level 50).

Module Ulc.

  Inductive exp : Set :=
  | Var (x : var)
  | Abs (x : var) (body : exp)
  | App (e1 e2 : exp).

  Fixpoint subst (rep : exp) (x : var) (e : exp) : exp :=
    match e with
    | Var y => if y ==v x then rep else Var y
    | Abs y e1 => Abs y (if y ==v x then e1 else subst rep x e1)
    | App e1 e2 => App (subst rep x e1) (subst rep x e2)
    end.


(*|
This time, for a change, we'll define big-step semantics.
|*)

  Inductive eval : exp -> exp -> Prop :=
  | BigAbs : forall x e,
    eval (Abs x e) (Abs x e)
  | BigApp : forall e1 x e1' e2 v2 v,
    eval e1 (Abs x e1')
    -> eval e2 v2
    -> eval (subst v2 x e1') v
    -> eval (App e1 e2) v.
(*|
Note that we omit a [Var] case, since variable terms can't be *closed*,
and therefore they aren't meaningful as top-level programs.
|*)

  Inductive value : exp -> Prop :=
  | Value : forall x e, value (Abs x e).

  Local Hint Constructors eval value : core.

(*|
Every value executes to itself, and `eval` only produces values.
|*)

  Theorem value_eval : forall v,
    value v
    -> eval v v.
  Proof.
  Admitted.

  Local Hint Resolve value_eval : core.

  Theorem eval_value : forall e v,
    eval e v
    -> value v.
  Proof.
  Admitted.
  
  Local Hint Resolve eval_value : core.

  Coercion Var : var >-> exp.
  Notation "\ x , e" := (Abs x e) (at level 50).
  Infix "@" := App (at level 49, left associativity).

(*|
Church numerals
===============

Here are two curious definitions.
|*)
  

  Definition zero := \"f", \"x", "x".
  Definition plus1 := \"n", \"f", \"x", "f" @ ("n" @ "f" @ "x").

(*|
We can build up any natural number [n] as [plus1^n @ zero].  Let's prove
that, in fact, these definitions constitute a workable embedding of the
natural numbers in lambda-calculus.

A term [plus^n @ zero] evaluates to something very close to what this
function returns.
|*)

  Fixpoint canonical' (n : nat) : exp :=
    match n with
    | O => "x"
    | S n' => "f" @ ((\"f", \"x", canonical' n') @ "f" @ "x")
    end.

(*|
This missing piece is this wrapper.
|*)
  Definition canonical n := \"f", \"x", canonical' n.

(*|
Let's formalize our definition of what it means to represent a number.
|*)

  Definition represents (e : exp) (n : nat) :=
    eval e (canonical n).

  Theorem zero_ok : represents zero 0.
  Proof.
  Admitted.

  Theorem plus1_ok :
    forall e n, represents e n ->
           represents (plus1 @ e) (S n).
  Proof.
  Admitted.
(*|
What's basically going on here?  The representation of number [n] is [N]
such that, for any function [f]: N(f) = f^n.
That is, we represent a number as its repeated-composition operator.
So, given a number, we can use it to repeat any operation.  In particular,
to implement addition, we can just repeat [plus1]!
|*)
  Definition add := \"n", \"m", "n" @ plus1 @ "m".

  Example add_1_2 : exists v,
      eval (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v
      /\ eval (plus1 @ (plus1 @ (plus1 @ zero))) v.
  Proof.
  Admitted.
(*|
By the way: since [canonical'] doesn't mention variable "m", substituting
for "m" has no effect.  This fact will come in handy shortly.
|*)

  Lemma subst_m_canonical' : forall n m,
    subst m "m" (canonical' n) = canonical' n.
  Proof.
  Admitted.
(*|
This inductive proof is the workhorse for the next result, so let's skip
ahead there.
|*)
  Lemma add_ok' : forall n m,
eval
  (subst (\ "f", (\ "x", canonical' m)) "x"
     (subst (\ "n", (\ "f", (\ "x", "f" @ (("n" @ "f") @ "x")))) "f"
        (canonical' n))) (canonical (n + m)).
  Proof.
  Admitted.
  Theorem add_ok : forall n ne m me,
      represents ne n
      -> represents me m
      -> represents (add @ ne @ me) (n + m).
  Proof.
  Admitted.
(*|
Let's repeat the same exercise for multiplication.
|*)

  Definition mult := \"n", \"m", "n" @ (add @ "m") @ zero.

  Example mult_1_2 : exists v,
      eval (mult @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v
      /\ eval (plus1 @ (plus1 @ zero)) v.
  Proof.
  Admitted.
  Lemma mult_ok' : forall n m,
eval
  (subst (\ "f", (\ "x", "x")) "x"
     (subst
        (\ "m",
          ((\ "f", (\ "x", canonical' m)) @
             (\ "n", (\ "f",
                       (\ "x", "f" @ (("n" @ "f") @ "x"))))) @ "m")
        "f" (canonical' n))) (canonical (n * m)).
  Proof.
  Admitted.

  Theorem mult_ok : forall n ne m me,
      represents ne n
      -> represents me m
      -> represents (mult @ ne @ me) (n * m).
  Proof.
  Admitted.
End Ulc.