<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
From mathcomp Require Import all_ssreflect.

(* Lambda calculator *)

Module Lambda.

Inductive expr : Set :=
  | Var of nat
  | Abs of expr
  | App of expr & expr.

Fixpoint shift k (e : expr) :=
  match e with
  | Var n     => if k <= n then Var n.+1 else Var n
  | Abs e1    => Abs (shift k.+1 e1)
  | App e1 e2 => App (shift k e1) (shift k e2)
  end.

Fixpoint open_rec k u (e : expr) :=
  match e with
  | Var n     => if k == n then u else if leq k n then Var n.-1 else e
  | Abs e1    => Abs (open_rec k.+1 (shift 0 u) e1)
  | App e1 e2 => App (open_rec k u e1) (open_rec k u e2)
  end.

Fixpoint reduce (e : expr) : option expr :=
  match e with
  | App (Abs e1) e2 => Some (open_rec 0 e2 e1)
  | App e1 e2 =>
    match reduce e1, reduce e2 with
    | Some e1', _    => Some (App e1' e2)
    | None, Some e2' => Some (App e1 e2')
    | None, None     => None
    end
  | Abs e1 =>
    if reduce e1 is Some e1' then Some (Abs e1') else None
  | _ => None
  end.

Fixpoint eval (n : nat) e :=
  if n is k.+1 then
    if reduce e is Some e' then eval k e' else e
  else e.

Coercion Var : nat >-> expr.

Definition church (n : nat) :=
  Abs (Abs (iter n (App 1) 0)).

Eval compute in church 3.

Definition chadd := Abs (Abs (Abs (Abs (App (App 3 1) (App (App 2 1) 0))))).

Eval compute in eval 6 (App (App chadd (church 3)) (church 2)).

Fixpoint closed_expr n e :=
  match e with
  | Var k => k < n
  | App e1 e2 => closed_expr n e1 && closed_expr n e2
  | Abs e1 => closed_expr n.+1 e1
  end.

Lemma shift_closed n e : closed_expr n e -> shift n e = e.
Proof.
  move: n; induction e => //= k Hc.
  + by rewrite leqNgt Hc.
  + by rewrite IHe.
  + move/andP: Hc => [Hc1 Hc2].
    by rewrite IHe1 // IHe2.
Qed.

Lemma closed_iter_app n k e1 e2 :
  closed_expr k e1 -> closed_expr k e2 ->
  closed_expr k (iter n (App e1) e2).
Proof.
  move=> He1.
  elim: n e2 => //= n IHn e2  He2.
  by rewrite He1 IHn.
Qed.

Lemma closed_church n : closed_expr 0 (church n).
Proof.
  rewrite /church /=.
  by apply closed_iter_app.
Qed.  

Lemma closed_expr_S n e : closed_expr n e -> closed_expr n.+1 e.
Proof.
  move: n.
  induction e => //= k.
  + by apply ltnW.
  + by apply IHe.
  + move/andP => [He1 He2].
    by rewrite IHe1 // IHe2.
Qed.

Hint Resolve closed_iter_app closed_church closed_expr_S.

Lemma open_iter_app k n u e1 e2 :
  open_rec k u (iter n (App e1) e2) =
  iter n (App (open_rec k u e1)) (open_rec k u e2).
Proof.
  elim: n e2 => //= n IHn e2.
  by rewrite IHn.
Qed.

Lemma eval_add m n e : eval (m+n) e = eval m (eval n e).
Proof.
  elim: n e => //= [|n IHn] e.
  + by rewrite addn0.
  + rewrite addnS /=.
    case_eq (reduce e) => [e1|] He //.
    destruct m => //=.
    by rewrite He.
Qed.

Lemma iter_add {A} m n (f : A -> A) x :
  iter (m+n) f x = iter m f (iter n f x).
Proof.
  elim: m x => [|m IHm] x //=.
  by rewrite -addnE  IHm.
Qed.

Lemma reduce_iter_app n (k : nat) x :
  reduce (iter n (App k) x) =
    if reduce x is Some x' then Some (iter n (App k) x') else None.
Proof.
  elim: n => [|n IHn] //=.
    by case: (reduce x).
  rewrite IHn /=.
  by case: (reduce x).
Qed.

Theorem chadd_ok m n :
  exists h, exists h',
    eval h (App (App chadd (church m)) (church n)) = eval h' (church (m+n)).
Proof.
  elim: m n => [|m IHm] n.
    rewrite add0n.
    exists 6; exists 0 => /=.
    rewrite !shift_closed; auto.
    by rewrite !open_iter_app /=.
  move: {IHm}(IHm n.+1) => [h [h' IHm]].
  exists (6+h); exists (6+h').
  rewrite (addSnnS m) -(addn1 m).
  move: (f_equal (eval 6) IHm).
  rewrite -!eval_add => <-.
  simpl.
  rewrite !shift_closed /=; auto.
  rewrite !open_iter_app /=.
  rewrite !reduce_iter_app /=.
  rewrite !reduce_iter_app /=.
  by rewrite iter_add.
Qed.

Inductive reduces : expr -> expr -> Prop :=
  | Rbeta : forall e1 e2, reduces (App (Abs e1) e2) (open_rec 0 e2 e1)
  | Rapp1 : forall e1 e2 e1', 
            reduces e1 e1' -> reduces (App e1 e2) (App e1' e2)
  | Rapp2 : forall e1 e2 e2',
            reduces e2 e2' -> reduces (App e1 e2) (App e1 e2')
  | Rabs  : forall e1 e1',
             reduces e1 e1' -> reduces (Abs e1) (Abs e1').

Hint Constructors reduces.

Inductive RT_closure {A} (R : A -> A -> Prop) : A -> A -> Prop :=
  | RTbase : forall a, RT_closure R a a
  | RTnext : forall a b c, R a b -> RT_closure R b c -> RT_closure R a c.

Lemma reduces_iter n e1 e2 e2' :
  reduces e2 e2' -> reduces (iter n (App e1) e2) (iter n (App e1) e2').
Proof. elim: n => //=; auto. Qed.

Lemma open_rec_closed n u e : closed_expr n e -> open_rec n u e = e.
Proof.
  move: n u.
  induction e => //= k u Hc.
  + case: ifP => Hk1.
      by rewrite (eqP Hk1) ltnn in Hc.
    by rewrite leqNgt Hc.
  + by rewrite IHe.
  + move/andP: Hc => [Hc1 Hc2].
    by rewrite IHe1 // IHe2.
Qed.

Theorem chadd_ok' m n :
  RT_closure reduces (App (App chadd (church m)) (church n)) (church (m+n)).
Proof.
  eapply RTnext; repeat constructor.
  simpl.
  rewrite !shift_closed; auto.
  eapply RTnext; repeat constructor.
  simpl.
  rewrite !open_rec_closed; auto.
  rewrite !shift_closed; auto.
  eapply RTnext; repeat constructor.
  simpl.
  rewrite open_iter_app /=.
  eapply RTnext; repeat constructor.
  rewrite open_iter_app /=.
  eapply RTnext.
    constructor.
    constructor.
    apply reduces_iter.
    repeat constructor.
  rewrite /= open_iter_app /=.
  eapply RTnext.
    repeat constructor.
    apply reduces_iter.
    repeat constructor.
  rewrite open_iter_app /=.
  rewrite -iter_add.
  by constructor.
Qed.

Lemma reduce_ok e e' : reduce e = Some e' -> reduces e e'.
Proof.
  move: e'.
  induction e => //= e'.
    by case_eq (reduce e) => // e1 He [] <-; auto.
  destruct e1.
  + by case_eq (reduce e2) => // e2' He2 [] <-; auto.
  + by move => [] <-; auto.
  + case_eq (reduce (App e1_1 e1_2)) => [e1'|] He1.
      by move => [] <-; auto.
    by case_eq (reduce e2) => // e2' He2 [] <-; auto.
Qed.

Lemma closed_expr_shift h k e :
  closed_expr h e -> closed_expr h.+1 (shift k e).
Proof.
  move: h k.
  induction e => //= h k Hc.
  + case: ifP => Hk /=.
     by rewrite -(addn1 n) -(addn1 h) ltn_add2r.
    apply ltnW.
    by rewrite -(addn1 n) -(addn1 h) ltn_add2r.
  + by apply IHe.
  + move/andP: Hc => [Hc1 Hc2].    
    by rewrite IHe1 // IHe2.
Qed.

Lemma closed_expr_open n e1 e2 k e' :
  closed_expr n.+1 e1 -> k <= n -> closed_expr n e2 ->
  open_rec k e2 e1 = e' -> closed_expr n e'.
Proof.
  move: n k e' e2.
  induction e1 => // h k e' e2 He1 Hk He2 <- //=.
  + case: ifP => Hk1 //.
    rewrite /= in He1.
    case: ifP => Hk2 //=.
      destruct n.
        by rewrite leqn0 Hk1 in Hk2.
      rewrite succnK.
      by rewrite -(ltn_add2r 1) !addn1.
    rewrite leqNgt in Hk2.
    by apply (leq_trans (negbFE Hk2)).
  + apply (IHe1 _ (k.+1) _ (shift 0 e2)) => //.
    by apply closed_expr_shift.
  + move: He1 => /= /andP [He11 He12].
    rewrite (IHe1_1 _ k _ e2) //.
    by rewrite (IHe1_2 _ k _ e2).
Qed.

Lemma closed_inv n e e' :
  closed_expr n e -> reduce e = Some e' -> closed_expr n e'.
Proof.
  move=> Hc Hr.
  apply reduce_ok in Hr.
  move: n Hc.
  induction Hr => //= n Hc.
  + move/andP: Hc => [Hc1 Hc2].
    by apply (closed_expr_open n e1 e2 0).
  + move/andP: Hc => [Hc1 Hc2].
    by rewrite IHHr.
  + move/andP: Hc => [Hc1 Hc2].
    by rewrite Hc1 IHHr.
  + by apply IHHr.
Qed.

End Lambda.