ladder-calculus/coq/bbencode.v

85 lines
2.7 KiB
Coq
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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.