From 3c86dde677790d85ae33fccc69121726e80ff557 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sat, 21 Sep 2024 01:43:25 +0200
Subject: [PATCH] improve notation for opening/substitution & add proof for
 expr_subst_fresh

---
 coq/subst_lemmas_debruijn.v | 62 ++++++++++++++++++++++++++++++++-----
 coq/terms_debruijn.v        | 50 ++++++++++++++++--------------
 2 files changed, 80 insertions(+), 32 deletions(-)

diff --git a/coq/subst_lemmas_debruijn.v b/coq/subst_lemmas_debruijn.v
index 62c4ead..a3a5b53 100644
--- a/coq/subst_lemmas_debruijn.v
+++ b/coq/subst_lemmas_debruijn.v
@@ -8,7 +8,7 @@ Require Import FSetNotin.
  *)
 Lemma type_subst_fresh : forall (x : atom) (τ:type_DeBruijn) (σ:type_DeBruijn),
   x `notin` (type_fv τ) ->
-  ([ x ~> σ ] τ) = τ
+  ([ x ~tt~> σ ] τ) = τ
 .
 Proof.
   intros.
@@ -48,14 +48,60 @@ Proof.
     reflexivity.
     simpl type_fv in H; fsetdec.
     simpl type_fv in H; fsetdec.
+
+Qed.
+
+(*
+ * Substitution has no effect if the variable is not free
+ *)
+Lemma expr_subst_fresh : forall (x : atom) (t:expr_DeBruijn) (e:expr_DeBruijn),
+  x `notin` (expr_fv e) ->
+  ([ x ~ee~> t ] e) = e
+.
+Proof.
+  intros.
+  induction e.
+
+  - unfold expr_fv in H.
+    apply AtomSetNotin.elim_notin_singleton in H.
+    simpl.
+    case_eq (x == a).
+    congruence.
+    reflexivity.
+
+  - reflexivity.
+
+  - simpl. rewrite IHe.
+    all: auto.
+
+  - simpl; rewrite IHe.
+    auto. auto.
+  - simpl; rewrite IHe.
+    auto. auto.
+  - simpl; rewrite IHe.
+    auto. auto.
+
+  - simpl. rewrite IHe1, IHe2.
+    reflexivity.
+    simpl expr_fv in H; fsetdec.
+    simpl expr_fv in H; fsetdec.
+
+  - simpl. rewrite IHe1, IHe2.
+    reflexivity.
+    simpl expr_fv in H; fsetdec.
+    simpl expr_fv in H; fsetdec.
+
+  - simpl; rewrite IHe.
+    auto. auto.
+  - simpl; rewrite IHe.
+    auto. auto.
 Qed.
 
 
-
-Lemma type_open_lc_core : forall τ i σ1 j σ2,
+Lemma type_open_lc_core : forall (τ:type_DeBruijn) i (σ1:type_DeBruijn) j (σ2:type_DeBruijn),
   i <> j ->
-  {i ~> σ1} τ = {j ~> σ2} ({i ~> σ1} τ) ->
-  ({j ~> σ2} τ) = τ
+  {i ~tt~> σ1} τ = {j ~tt~> σ2} ({i ~tt~> σ1} τ) ->
+  ({j ~tt~> σ2} τ) = τ
 .
 Proof with eauto*.
   induction τ;
@@ -88,7 +134,7 @@ Qed.
  *)
 Lemma type_open_lc : forall k σ τ,
   type_lc τ ->
-  ({ k ~> σ } τ) = τ
+  ({ k ~tt~> σ } τ) = τ
 .
 Proof.
   intros.
@@ -116,9 +162,9 @@ Qed.
 Lemma type_subst_open : forall τ σ1 σ2 x k,
   type_lc σ2 ->
 
-  [x ~> σ2] ({k ~> σ1} τ)
+  [x ~tt~> σ2] ({k ~tt~> σ1} τ)
   =
-  {k ~> [x ~> σ2] σ1} ([x ~> σ2] τ).
+  {k ~tt~> [x ~tt~> σ2] σ1} ([x ~tt~> σ2] τ).
 Proof.
   induction τ;
   intros; simpl; f_equal; auto.
diff --git a/coq/terms_debruijn.v b/coq/terms_debruijn.v
index 626eadf..54a6cdb 100644
--- a/coq/terms_debruijn.v
+++ b/coq/terms_debruijn.v
@@ -152,8 +152,8 @@ Fixpoint type_open_rec (k:nat) (σ:type_DeBruijn) (τ:type_DeBruijn) {struct τ}
     | ty_ladder τ1 τ2 => ty_ladder (type_open_rec k σ τ1) (type_open_rec k σ τ2)
   end.
 
-Notation "'[' z '~>' u ']' e" := (subst_type z u e) (at level 68).
-Notation "'{' k '~>' σ '}' τ" := (type_open_rec k σ τ) (at level 67).
+Notation "'[' z '~tt~>' u ']' e" := (subst_type z u e) (at level 68).
+Notation "'{' k '~tt~>' σ '}' τ" := (type_open_rec k σ τ) (at level 67).
 Definition type_open σ τ := type_open_rec 0 σ τ.
 
 (* is the type locally closed ? *)
@@ -188,33 +188,33 @@ Fixpoint expr_fv (e : expr_DeBruijn) {struct e} : atoms :=
   end.
 
 (* substitute free variable x with expression s in t *)
-Fixpoint ex_subst (x:atom) (s:expr_DeBruijn) (t:expr_DeBruijn) {struct t} : expr_DeBruijn :=
+Fixpoint expr_subst (x:atom) (s:expr_DeBruijn) (t:expr_DeBruijn) {struct t} : expr_DeBruijn :=
   match t with
   | ex_fvar n => if x == n then s else t
   | ex_bvar y => ex_bvar y
-  | ex_ty_abs t' => ex_ty_abs (ex_subst x s t')
-  | ex_ty_app t' σ => ex_ty_app (ex_subst x s t') σ
-  | ex_morph σ t' => ex_morph σ (ex_subst x s t')
-  | ex_abs σ t' => ex_abs σ (ex_subst x s t')
-  | ex_app t1 t2 => ex_app (ex_subst x s t1) (ex_subst x s t2)
-  | ex_let t1 t2 => ex_let (ex_subst x s t1) (ex_subst x s t2)
-  | ex_ascend τ t' => ex_ascend τ (ex_subst x s t')
-  | ex_descend τ t' => ex_descend τ (ex_subst x s t')
+  | ex_ty_abs t' => ex_ty_abs (expr_subst x s t')
+  | ex_ty_app t' σ => ex_ty_app (expr_subst x s t') σ
+  | ex_morph σ t' => ex_morph σ (expr_subst x s t')
+  | ex_abs σ t' => ex_abs σ (expr_subst x s t')
+  | ex_app t1 t2 => ex_app (expr_subst x s t1) (expr_subst x s t2)
+  | ex_let t1 t2 => ex_let (expr_subst x s t1) (expr_subst x s t2)
+  | ex_ascend τ t' => ex_ascend τ (expr_subst x s t')
+  | ex_descend τ t' => ex_descend τ (expr_subst x s t')
   end.
 
 (* substitute free type-variable α with type τ in e *)
-Fixpoint ex_subst_type (α:atom) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
+Fixpoint expr_subst_type (α:atom) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
   match e with
   | ex_fvar n => ex_fvar n
   | ex_bvar y => ex_bvar y
-  | ex_ty_abs e' => ex_ty_abs (ex_subst_type α τ e')
-  | ex_ty_app e' σ => ex_ty_app (ex_subst_type α τ e') (subst_type α τ σ)
-  | ex_morph σ e' => ex_morph (subst_type α τ σ) (ex_subst_type α τ e')
-  | ex_abs σ e' => ex_abs (subst_type α τ σ) (ex_subst_type α τ e')
-  | ex_app e1 e2 => ex_app (ex_subst_type α τ e1) (ex_subst_type α τ e2)
-  | ex_let e1 e2 => ex_let (ex_subst_type α τ e1) (ex_subst_type α τ e2)
-  | ex_ascend σ e' => ex_ascend (subst_type α τ σ) (ex_subst_type α τ e')
-  | ex_descend σ e' => ex_descend (subst_type α τ σ) (ex_subst_type α τ e')
+  | ex_ty_abs e' => ex_ty_abs (expr_subst_type α τ e')
+  | ex_ty_app e' σ => ex_ty_app (expr_subst_type α τ e') (subst_type α τ σ)
+  | ex_morph σ e' => ex_morph (subst_type α τ σ) (expr_subst_type α τ e')
+  | ex_abs σ e' => ex_abs (subst_type α τ σ) (expr_subst_type α τ e')
+  | ex_app e1 e2 => ex_app (expr_subst_type α τ e1) (expr_subst_type α τ e2)
+  | ex_let e1 e2 => ex_let (expr_subst_type α τ e1) (expr_subst_type α τ e2)
+  | ex_ascend σ e' => ex_ascend (subst_type α τ σ) (expr_subst_type α τ e')
+  | ex_descend σ e' => ex_descend (subst_type α τ σ) (expr_subst_type α τ e')
   end.
 
 (* replace a free variable with a new (dangling) bound variable *)
@@ -247,10 +247,6 @@ Fixpoint expr_open_rec (k:nat) (t:expr_DeBruijn) (e:expr_DeBruijn) {struct e} :
     | ex_descend σ e' => ex_descend σ (expr_open_rec k t e')
   end.
 
-Definition expr_open t e := expr_open_rec 0 t e.
-
-
-
 (* replace (dangling) index with another expression *)
 Fixpoint expr_open_type_rec (k:nat) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct e} : expr_DeBruijn :=
   match e with
@@ -266,6 +262,12 @@ Fixpoint expr_open_type_rec (k:nat) (τ:type_DeBruijn) (e:expr_DeBruijn) {struct
     | ex_descend σ e' => ex_descend σ (expr_open_type_rec k τ e')
   end.
 
+Notation "'[' z '~ee~>' u ']' e" := (expr_subst z u e) (at level 68).
+Notation "'[' z '~et~>' u ']' e" := (expr_subst_type z u e) (at level 68).
+Notation "'{' k '~ee~>' t '}' e" := (expr_open_rec k t e) (at level 67).
+Notation "'{' k '~et~>' τ '}' e" := (expr_open_type_rec k τ e) (at level 67).
+
+Definition expr_open t e := expr_open_rec 0 t e.
 Definition expr_open_type τ e := expr_open_type_rec 0 τ e.