From 13165a7951b9322b65a6debc17ffe01c8d245f6d Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Thu, 25 Jul 2024 12:42:32 +0200
Subject: [PATCH] coq: smallstep: define delta expansion

---
 coq/smallstep.v | 59 +++++++++++++++++++++++++++++++++++--------------
 1 file changed, 42 insertions(+), 17 deletions(-)

diff --git a/coq/smallstep.v b/coq/smallstep.v
index ae19f41..c3da0a3 100644
--- a/coq/smallstep.v
+++ b/coq/smallstep.v
@@ -1,51 +1,76 @@
 From Coq Require Import Strings.String.
 Require Import terms.
 Require Import subst.
+Require Import typing.
 
 Include Terms.
 Include Subst.
+Include Typing.
 
 Module Smallstep.
 
-Reserved Notation " s '-->α' t " (at level 40).
 Reserved Notation " s '-->β' t " (at level 40).
 Reserved Notation " s '-->δ' t " (at level 40).
+Reserved Notation " s '-->eval' t " (at level 40).
 
 Inductive beta_step : expr_term -> expr_term -> Prop :=
-  | E_AppLeft : forall e1 e1' e2,
+  | E_App1 : forall e1 e1' e2,
     e1 -->β e1' ->
     (expr_tm_app e1 e2) -->β (expr_tm_app e1' e2)
 
-  | E_AppRight : forall e1 e2 e2',
+  | E_App2 : 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_TypApp : forall e e' τ,
+    e -->β e' ->
+    (expr_ty_app e τ) -->β (expr_ty_app e' τ)
 
-  | E_AppTyAbs : forall x e a,
+  | E_TypAppLam : forall x e a,
     (expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
 
+  | E_AppLam : forall x τ e a,
+    (expr_tm_app (expr_tm_abs x τ e) a) -->β (expr_subst 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),
+
+
+Inductive delta_step : expr_term -> expr_term -> Prop :=
+
+  | E_ImplicitCast : forall (Γ:context) (f:expr_term) (h:string) (a:expr_term) (τ:type_term) (s:type_term) (p:type_term),
+
+    (context_contains Γ h (type_morph p s)) ->
+    Γ |- f \is (type_fun s τ) ->
+    Γ |- a \is p ->
+    (expr_tm_app f a) -->δ (expr_tm_app f (expr_tm_app (expr_var h) a))
+
+where "s '-->δ' t" := (delta_step s t).
+
+
+Inductive eval_step : expr_term -> expr_term -> Prop :=
+  | E_Beta : forall s t,
+    (s -->β t) ->
+    (s -->eval t)
+
+  | E_Delta : forall s t,
+    (s -->δ t) ->
+    (s -->eval t)
+
+where "s '-->eval' t" := (eval_step s t).
+
+Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
+  | 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_term -> expr_term -> Prop :=
-  | E_ImplicitCast
-  (expr_tm_app e1 e2)
-*)
+Notation " s -->δ* t " := (multi delta_step s t) (at level 40).
+Notation " s -->eval* t " := (multi eval_step s t) (at level 40).
 
 End Smallstep.