coq: preliminary small-step semantics

coq/smallstep.v

@@ -0,0 +1,51 @@
+From Coq Require Import Strings.String.
+Require Import terms.
+Require Import subst.
+
+Include Terms.
+Include Subst.
+
+Module Smallstep.
+
+Reserved Notation " s '-->α' t " (at level 40).
+Reserved Notation " s '-->β' t " (at level 40).
+Reserved Notation " s '-->δ' t " (at level 40).
+
+Inductive beta_step : expr -> expr -> Prop :=
+  | E_AppLeft : forall e1 e1' e2,
+    e1 -->β e1' ->
+    (expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
+
+  | E_AppRight : forall e1 e2 e2',
+    e2 -->β e2' ->
+    (expr_tm_app e1 e2) -->β (expr_tm_app e1 e2')
+
+  | E_AppTmAbs : forall x τ e a,
+    (expr_tm_app (expr_tm_abs x τ e) a) -->β (expr_subst x a e)
+
+  | E_AppTyAbs : forall x e a,
+    (expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
+
+  | E_AppLet : forall x t e a,
+    (expr_let x t a e) -->β (expr_subst x a e)
+
+where "s '-->β' t" := (beta_step s t).
+
+(*
+Inductive multi {X : Type} (R : relation X) : relation X :=
+  | multi_refl : forall (x : X), multi R x x
+  | multi_step : forall (x y z : X),
+                    R x y ->
+                    multi R y z ->
+                    multi R x z.
+
+Notation " s -->β* t " := (multi beta_step s t) (at level 40).
+*)
+
+(*
+Inductive delta_expand : expr -> expr -> Prop :=
+  | E_ImplicitCast
+  (expr_tm_app e1 e2)
+*)
+
+End Smallstep.