From 361d03c117607c77edcc1a5c327b002a5758108b Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Wed, 21 Aug 2024 20:03:46 +0200
Subject: [PATCH] coq: reimplement type substitution and alpha conversion in
types
---
coq/equiv.v | 76 +++++++++++++++++++++++++++++++++----------
coq/subst.v | 93 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
2 files changed, 151 insertions(+), 18 deletions(-)
diff --git a/coq/equiv.v b/coq/equiv.v
index 39c8e96..0a6ce39 100644
--- a/coq/equiv.v
+++ b/coq/equiv.v
@@ -29,6 +29,7 @@
* rewrite-step of each other, `===` is symmetric and thus `===`
* satisfies all properties required of an equivalence relation.
*)
+
Require Import terms.
Require Import subst.
From Coq Require Import Strings.String.
@@ -41,17 +42,55 @@ Module Equiv.
(** Alpha conversion in types *)
-Reserved Notation "S '-->α' T" (at level 40).
+Reserved Notation "S '--->α' T" (at level 40).
Inductive type_conv_alpha : type_term -> type_term -> Prop :=
- | TEq_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).
+ | TAlpha_Rename : forall x y t t',
+
+ (type_subst1 x (type_var y) t t') ->
+ (type_univ x t) --->α (type_univ y t')
+
+ | TAlpha_SubUniv : forall x τ τ',
+ (τ --->α τ') ->
+ (type_univ x τ) --->α (type_univ x τ')
+
+ | TAlpha_SubSpec1 : forall τ1 τ1' τ2,
+ (τ1 --->α τ1') ->
+ (type_spec τ1 τ2) --->α (type_spec τ1' τ2)
+
+ | TAlpha_SubSpec2 : forall τ1 τ2 τ2',
+ (τ2 --->α τ2') ->
+ (type_spec τ1 τ2) --->α (type_spec τ1 τ2')
+
+ | TAlpha_SubFun1 : forall τ1 τ1' τ2,
+ (τ1 --->α τ1') ->
+ (type_fun τ1 τ2) --->α (type_fun τ1' τ2)
+
+ | TAlpha_SubFun2 : forall τ1 τ2 τ2',
+ (τ2 --->α τ2') ->
+ (type_fun τ1 τ2) --->α (type_fun τ1 τ2')
+
+ | TAlpha_SubMorph1 : forall τ1 τ1' τ2,
+ (τ1 --->α τ1') ->
+ (type_morph τ1 τ2) --->α (type_morph τ1' τ2)
+
+ | TAlpha_SubMorph2 : forall τ1 τ2 τ2',
+ (τ2 --->α τ2') ->
+ (type_morph τ1 τ2) --->α (type_morph τ1 τ2')
+
+ | TAlpha_SubLadder1 : forall τ1 τ1' τ2,
+ (τ1 --->α τ1') ->
+ (type_ladder τ1 τ2) --->α (type_ladder τ1' τ2)
+
+ | TAlpha_SubLadder2 : forall τ1 τ2 τ2',
+ (τ2 --->α τ2') ->
+ (type_ladder τ1 τ2) --->α (type_ladder τ1 τ2')
+
+where "S '--->α' T" := (type_conv_alpha S T).
(** Alpha conversion is symmetric *)
-
Lemma type_alpha_symm :
forall σ τ,
- (σ -->α τ) -> (τ -->α σ).
+ (σ --->α τ) -> (τ --->α σ).
Proof.
(* TODO *)
Admitted.
@@ -179,8 +218,8 @@ Inductive type_eq : type_term -> type_term -> Prop :=
y === z ->
x === z
- | TEq_Rename : forall x y,
- x -->α y ->
+ | TEq_Alpha : forall x y,
+ x --->α y ->
x === y
| TEq_Distribute : forall x y,
@@ -196,7 +235,7 @@ where "S '===' T" := (type_eq S T).
(** Symmetry of === *)
-Lemma type_eq_is_symmetric :
+Lemma TEq_Symm :
forall x y,
(x === y) -> (y === x).
Proof.
@@ -210,7 +249,7 @@ Proof.
apply IHtype_eq1.
apply type_alpha_symm in H.
- apply TEq_Rename.
+ apply TEq_Alpha.
apply H.
apply TEq_Condense.
@@ -267,19 +306,22 @@ Lemma lnf_shape :
Proof.
intros τ H.
induction τ.
-
- left.
- apply FlatUnit.
-
+
left.
apply FlatId.
left.
apply FlatVar.
-
+(*
left.
- apply FlatNum.
-
+ apply IHτ1 in H.
+ apply FlatFun.
+ apply H.
+ destruct H.
+ destruct H.
+
+ apply IHτ1.
+*)
admit.
admit.
admit.
diff --git a/coq/subst.v b/coq/subst.v
index c338fd6..e36e000 100644
--- a/coq/subst.v
+++ b/coq/subst.v
@@ -1,9 +1,62 @@
-From Coq Require Import Strings.String.
+ From Coq Require Import Strings.String.
Require Import terms.
Include Terms.
Module Subst.
+
+(* Type Variable "x" is a free variable in type *)
+Inductive type_var_free (x:string) : type_term -> Prop :=
+ | TFree_Var :
+ (type_var_free x (type_var x))
+
+ | TFree_Ladder : forall τ1 τ2,
+ (type_var_free x τ1) ->
+ (type_var_free x τ2) ->
+ (type_var_free x (type_ladder τ1 τ2))
+
+ | TFree_Fun : forall τ1 τ2,
+ (type_var_free x τ1) ->
+ (type_var_free x τ2) ->
+ (type_var_free x (type_fun τ1 τ2))
+
+ | TFree_Morph : forall τ1 τ2,
+ (type_var_free x τ1) ->
+ (type_var_free x τ2) ->
+ (type_var_free x (type_morph τ1 τ2))
+
+ | TFree_Spec : forall τ1 τ2,
+ (type_var_free x τ1) ->
+ (type_var_free x τ2) ->
+ (type_var_free x (type_spec τ1 τ2))
+
+ | TFree_Univ : forall y τ,
+ ~(y = x) ->
+ (type_var_free x τ) ->
+ (type_var_free x (type_univ y τ))
+.
+
+
+Open Scope ladder_type_scope.
+Example ex_type_free_var1 :
+ (type_var_free "T" (type_univ "U" (type_var "T")))
+.
+Proof.
+ apply TFree_Univ.
+ easy.
+ apply TFree_Var.
+Qed.
+
+Open Scope ladder_type_scope.
+Example ex_type_free_var2 :
+ ~(type_var_free "T" (type_univ "T" (type_var "T")))
+.
+Proof.
+ intro H.
+ inversion H.
+ contradiction.
+Qed.
+
(* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
match t0 with
@@ -15,6 +68,44 @@ Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
| t => t
end.
+Inductive type_subst1 (x:string) (σ:type_term) : type_term -> type_term -> Prop :=
+ | TSubst_VarReplace :
+ (type_subst1 x σ (type_var x) σ)
+
+ | TSubst_VarKeep : forall y,
+ ~(x = y) ->
+ (type_subst1 x σ (type_var y) (type_var y))
+
+ | TSubst_UnivReplace : forall y τ τ',
+ ~(x = y) ->
+ ~(type_var_free y σ) ->
+ (type_subst1 x σ τ τ') ->
+ (type_subst1 x σ (type_univ y τ) (type_univ y τ'))
+
+ | TSubst_Id : forall n,
+ (type_subst1 x σ (type_id n) (type_id n))
+
+ | TSubst_Spec : forall τ1 τ2 τ1' τ2',
+ (type_subst1 x σ τ1 τ1') ->
+ (type_subst1 x σ τ2 τ2') ->
+ (type_subst1 x σ (type_spec τ1 τ2) (type_spec τ1' τ2'))
+
+ | TSubst_Fun : forall τ1 τ1' τ2 τ2',
+ (type_subst1 x σ τ1 τ1') ->
+ (type_subst1 x σ τ2 τ2') ->
+ (type_subst1 x σ (type_fun τ1 τ2) (type_fun τ1' τ2'))
+
+ | TSubst_Morph : forall τ1 τ1' τ2 τ2',
+ (type_subst1 x σ τ1 τ1') ->
+ (type_subst1 x σ τ2 τ2') ->
+ (type_subst1 x σ (type_morph τ1 τ2) (type_morph τ1' τ2'))
+
+ | TSubst_Ladder : forall τ1 τ1' τ2 τ2',
+ (type_subst1 x σ τ1 τ1') ->
+ (type_subst1 x σ τ2 τ2') ->
+ (type_subst1 x σ (type_ladder τ1 τ2) (type_ladder τ1' τ2'))
+.
+
(* scoped variable substitution, replaces free occurences of v with n in expression e *)
Fixpoint expr_subst (v:string) (n:expr_term) (e0:expr_term) :=
match e0 with