From Undecidability.L Require Export Tactics.

(** * Scott encoding of numbers *)

Fixpoint enc (n : nat) :=
  match n with
  | 0   => lambda(lambda (1))
  | S n => lambda(lambda ( 0 (enc n)))
  end.

Lemma enc_proc m :
  proc (enc m).
Proof.
(* Goal: proc (enc m) *)
  induction m; value.
Qed.

Hint Resolve enc_proc : cbv.

Lemma enc_injective m n : enc m = enc n -> m = n.
Proof. 
(* Goal: forall _ : @eq term (enc m) (enc n), @eq nat m n *)
  revert n; induction m; intros n; destruct n; inversion 1; eauto.
Qed.

Lemma enc_inj m n : enc m ≡ enc n -> m = n.
Proof.
(* Goal: forall _ : equiv (tenc s) (tenc t), @eq term s t *)
  intros. destruct (enc_proc m) as [? []], (enc_proc n) as [? []]. rewrite H1, H3 in H.
(* Goal: False *)
  eapply unique_normal_forms in H; value. subst. eapply enc_injective; congruence.
Qed.

Definition Zero : term := .\"z","s"; "z".
Definition Succ : term := .\"n","z","s"; "s" "n".

Hint Unfold Zero Succ : cbv.

Lemma Succ_correct n : Succ (enc n) ≻* enc (S n).
Proof.
(* Goal: star (app Succ (enc n)) (enc (S n)) *)
  solvered.
Qed.

Definition Add  := Eval cbn in rho (.\ "a", "n", "m"; "n" "m" (.\"n"; !Succ ("a" "n" "m"))).

Hint Unfold Add : cbv.

Lemma Add_correct n m :
  Add (enc n) (enc m) ≡ enc (n + m).
Proof.
(* Goal: equiv (app N (enc n)) (tenc (enc n)) *)
  induction n; solveeq.
Qed.

(** * Scott encoding of terms *)

Fixpoint tenc t :=
  lambda ( (* var *) lambda ( (* app *) lambda ( (* lambda *)
     match t with
       | var n => (var 2) (enc n)
       | app s t => (var 1) (tenc s) (tenc t)
       | lambda s => (var 0) (tenc s)
     end
  ))).

Lemma tenc_proc s : proc (tenc s).
Proof.
(* Goal: proc (tenc s) *)
  induction s; value.
Qed.

Hint Resolve tenc_proc : cbv.

Lemma tenc_injective s t : tenc s = tenc t -> s = t.
Proof.
(* Goal: forall _ : @eq term (tenc s) (tenc t), @eq term s t *)
  revert t; induction s; intros t; destruct t; inversion 1.
  - eauto using enc_injective.
  - erewrite IHs1, IHs2; eauto.
  - erewrite IHs; eauto.
Qed.

Lemma tenc_inj s t : tenc s ≡ tenc t -> s = t.
Proof.
(* Goal: forall _ : equiv (tenc s) (tenc t), @eq term s t *)
  intros. destruct (tenc_proc t) as [? []], (tenc_proc s) as [? []]. rewrite H1, H3 in H.
(* Goal: False *)
  eapply unique_normal_forms in H; value. eapply tenc_injective. congruence.
Qed.

Definition Var : term := .\"n";     .\"v","a","l"; "v" "n".
Definition App : term := .\"s","t"; .\"v","a","l"; "a" "s" "t".
Definition Lam : term := .\"s";     .\"v","a","l"; "l" "s".

Lemma Var_correct n : Var (enc n) ≡ tenc (n).
Proof.
(* Goal: equiv (app Lam (tenc s)) (tenc (lambda s)) *)
  solveeq.
Qed.

Lemma App_correct s t : App (tenc s) (tenc t) ≡ tenc (s t).
Proof.
(* Goal: equiv (app Lam (tenc s)) (tenc (lambda s)) *)
  solveeq.
Qed.

Lemma Lam_correct s : Lam (tenc s) ≡ tenc (lambda s).
Proof.
(* Goal: equiv (app Lam (tenc s)) (tenc (lambda s)) *)
  solveeq.
Qed.

Definition N := rho ( .\"N", "n"; "n"
   !(tenc Zero)
   (.\"n"; !Lam (!Lam (!App !(tenc 0) ("N" "n"))))).

Lemma N_correct n : N (enc n) ≡ tenc(enc n).
Proof.
(* Goal: equiv (app N (enc n)) (tenc (enc n)) *)
  induction n; solveeq.
Qed.

Definition Q := Eval cbn in rho ( .\"Q", "s"; "s"
   (.\"n";     !Lam (!Lam (!Lam (!App !(tenc 2) (!N "n")))))
   (.\"s","t"; !Lam (!Lam (!Lam (!App (!App !(tenc 1) ("Q" "s")) ("Q" "t")))))
   (.\"s";     !Lam (!Lam (!Lam (!App !(tenc 0) ("Q" "s"))))) ).

Lemma Q_correct s : Q (tenc s) ≡ tenc(tenc s).
Proof.
(* Goal: equiv (app Lam (tenc s)) (tenc (lambda s)) *)
  induction s; (try assert (R:=N_correct n)); solveeq.
Qed.

(** ** Scott encoding of booleans *)

Definition benc (b:bool) : term := if b then T else F.
Hint Unfold T F : cbv.

Lemma benc_proc b : proc (benc b).
Proof.
(* Goal: proc (benc b) *)
  destruct b; value. 
Qed.
Hint Resolve benc_proc : cbv.

Lemma T_equiv_F : ~ T ≡ F.
Proof.
(* Goal: False *)
  cbv. intros H. eapply unique_normal_forms in H; value. inv H. 
Qed.
