From Coq Require Import Strings.String.

Require Import terms.
Require Import subst.
Require Import smallstep.

Include Terms.
Include Subst.
Include Smallstep.

Open Scope ladder_type_scope.
Open Scope ladder_expr_scope.

(*  let bb_zero = Λα ↦ λs: α->α ↦ λz: α ↦ z
 *                ∀α.(α->α)->α->α
*)
Definition bb_zero : expr_term :=
  (expr_ty_abs "α"
    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
      (expr_abs "z" (type_var "α")
        (expr_var "z")))).

(*  let bb_one = Λα ↦ λs: α->α ↦ λz: α ↦ s z
*)
Definition bb_one : expr_term :=
  (expr_ty_abs "α"
    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
      (expr_abs "z" (type_var "α")
        (expr_app (expr_var "s") (expr_var "z"))))).

(*  let bb_two = Λα ↦ λs: α->α ↦ λz: α ↦ s (s z)
*)
Definition bb_two : expr_term :=
  (expr_ty_abs "α"
    (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
      (expr_abs "z" (type_var "α")
        (expr_app (expr_var "s") (expr_app (expr_var "s") (expr_var "z")))))).


Definition bb_succ : expr_term :=
  (expr_abs "n" (type_ladder (type_id "ℕ")
                    (type_ladder (type_id "BBNat")
                     (type_univ "α"
                      (type_fun (type_fun (type_var "α") (type_var "α"))
                         (type_fun (type_var "α") (type_var "α"))))))

       (expr_ascend (type_ladder (type_id "ℕ") (type_id "BBNat"))
          (expr_ty_abs "α"
            (expr_abs "s" (type_fun (type_var "α") (type_var "α"))
              (expr_abs "z" (type_var "α")
                (expr_app (expr_var "s")
                  (expr_app (expr_app
                      (expr_ty_app (expr_var "n") (type_var "α"))
                      (expr_var "s"))
                    (expr_var "z")))))))).

Definition e1 : expr_term :=
  (expr_let "bb-zero" (type_ladder (type_id "ℕ")
                        (type_ladder (type_id "BBNat")
                          (type_univ "α"
                            (type_fun (type_fun (type_var "α") (type_var "α"))
                              (type_fun (type_var "α") (type_var "α"))))))
                       bb_zero
                       (expr_app (expr_app (expr_var "+") (expr_var "bb-zero")) (expr_var "bb-zero"))
  ).

Definition t1 : expr_term := (expr_app (expr_var "x") (expr_var "x")).

Compute (expr_subst "x"
    (expr_ty_abs "α" (expr_abs "a" (type_var "α") (expr_var "a")))
    bb_one
).

Example  example_let_reduction :
    e1 -->β  (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
Proof.
    apply E_AppLet.
Qed.

Compute     (expr_app bb_succ bb_zero) -->β bb_one.

Example  example_succ :
    (expr_app bb_succ bb_zero) -->β bb_one.
Proof.
Admitted.