From 221c017640c36a220b129ac0c115e83a4fc9af0b Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sun, 18 Aug 2024 10:47:35 +0200
Subject: [PATCH] coq: alpha conversion in types

---
 coq/equiv.v | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

diff --git a/coq/equiv.v b/coq/equiv.v
index 703d68c..ff77ed6 100644
--- a/coq/equiv.v
+++ b/coq/equiv.v
@@ -30,13 +30,33 @@
  * satisfies all properties required of an equivalence relation.
  *)
 Require Import terms.
+Require Import subst.
 From Coq Require Import Strings.String.
 
 Include Terms.
+Include Subst.
 
 Module Equiv.
 
 
+(** Alpha conversion in types *)
+
+Reserved Notation "S '-->α' T" (at level 40).
+Inductive type_conv_alpha : type_term -> type_term -> Prop :=
+  | Eq_Alpha : forall x y t,
+  (type_univ x t) -->α (type_univ y (type_subst x (type_var y) t))
+where "S '-->α' T" := (type_conv_alpha S T).
+
+(** Alpha conversion is symmetric *)
+
+Lemma type_alpha_symm :
+  forall σ τ,
+  (σ -->α τ) -> (τ -->α σ).
+Proof.
+ (* TODO *)
+Admitted.
+
+
 (** Define all rewrite steps $\label{coq:type-dist}$ *)
 
 Reserved Notation "S '-->distribute-ladder' T" (at level 40).
@@ -123,6 +143,10 @@ Inductive type_eq : type_term -> type_term -> Prop :=
     y === z ->
     x === z
 
+  | L_Rename : forall x y,
+    x -->α y ->
+    x === y
+
   | L_Distribute : forall x y,
     x -->distribute-ladder y ->
     x === y
@@ -147,12 +171,12 @@ Proof.
     apply L_Refl.
   }
 
-  2:{
+  3:{
     apply L_Condense.
     apply distribute_inverse.
     apply H.
   }
-  2:{
+  3:{
     apply L_Distribute.
     apply condense_inverse.
     apply H.
@@ -161,6 +185,10 @@ Proof.
   apply L_Trans with (y:=y).
   apply IHtype_eq2.
   apply IHtype_eq1.
+
+  apply type_alpha_symm in H.
+  apply L_Rename.
+  apply H.
 Qed.
 
 (** "flat" types do not contain ladders $\label{coq:type-flat}$ *)