From ad107759bf3f4a814c3d4fe370c5989128ef068b Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Thu, 22 Aug 2024 08:30:46 +0200
Subject: [PATCH] coq: expr alpha conversion

---
 coq/smallstep.v | 41 +++++++++++++++++++++++++++++++++++++----
 coq/typing.v    |  1 -
 2 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/coq/smallstep.v b/coq/smallstep.v
index 45fee88..067678c 100644
--- a/coq/smallstep.v
+++ b/coq/smallstep.v
@@ -9,9 +9,43 @@ 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 expr_alpha : expr_term -> expr_term -> Prop :=
+  | EAlpha_Rename : forall x x' τ e,
+    (expr_abs x τ e) -->α (expr_abs x' τ (expr_subst x (expr_var x') e))
+
+  | EAlpha_TyRename : forall α α' e,
+    (expr_ty_abs α e) -->α (expr_ty_abs α' (expr_specialize α (type_var α') e))
+
+  | EAlpha_SubAbs : forall x τ e e',
+    (e -->α e') ->
+    (expr_abs x τ e) -->α (expr_abs x τ e')
+
+  | EAlpha_SubTyAbs : forall α e e',
+    (e -->α e') ->
+    (expr_ty_abs α e) -->α (expr_ty_abs α e')
+
+  | EAlpha_SubApp1 : forall e1 e1' e2,
+    (e1 -->α e1') ->
+    (expr_app e1 e2) -->α (expr_app e1' e2)
+
+  | EAlpha_SubApp2 : forall e1 e2 e2',
+    (e2 -->α e2') ->
+    (expr_app e1 e2) -->α (expr_app e1 e2')
+
+where "s '-->α' t" := (expr_alpha s t).
+
+
+Example a1 : polymorphic_identity1 -->α polymorphic_identity2.
+Proof.
+  unfold polymorphic_identity1.
+  unfold polymorphic_identity2.
+  apply EAlpha_SubTyAbs.
+  apply EAlpha_Rename.
+Qed.
+
 
 Inductive beta_step : expr_term -> expr_term -> Prop :=
   | E_App1 : forall e1 e1' e2,
@@ -69,8 +103,7 @@ Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
                     multi R y z ->
                     multi R x z.
 
+Notation " s -->α* t " := (multi expr_alpha s t) (at level 40).
 Notation " s -->β* t " := (multi beta_step s t) (at level 40).
-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.
diff --git a/coq/typing.v b/coq/typing.v
index 50af8b4..d11de58 100644
--- a/coq/typing.v
+++ b/coq/typing.v
@@ -137,7 +137,6 @@ Example typing2 :
   forall Γ,
   (context_contains Γ "x" [ %"T"% ]) ->
   Γ |- [[ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% ]] \is [ ∀"U", %"U"% -> %"U"% ].
-   (* Γ |- [ ΛT ↦ λx:T ↦ x ] : ∀T.(T->T) *)
 Proof.
   intros.
   apply T_Sub with (τ:=[∀"T",(%"T"% -> %"T"%)]).