From ac2e141cb744df0a3bb144b639640b666a1f2407 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Thu, 28 Sep 2023 10:51:30 +0200
Subject: [PATCH] Move renaming lemmas on normal forms to NormalForms.

They don't belong in the Weakening module because they rely on simple
untyped renamings.
---
 theories/NormalForms.v | 56 ++++++++++++++++++++++++++++++++++++++++++
 theories/Weakening.v   | 56 ------------------------------------------
 2 files changed, 56 insertions(+), 56 deletions(-)

diff --git a/theories/NormalForms.v b/theories/NormalForms.v
index 3efcc470..641a3ada 100644
--- a/theories/NormalForms.v
+++ b/theories/NormalForms.v
@@ -129,3 +129,59 @@ Inductive isCanonical : term -> Type :=
   | can_tRefl {A x}: isCanonical (tRefl A x).
 
 #[global] Hint Constructors isCanonical : gen_typing.
+
+(** ** Normal and neutral forms are stable by renaming *)
+
+Section RenWhnf.
+
+  Variable (ρ : nat -> nat).
+
+  Lemma whne_ren t : whne t -> whne (t⟨ρ⟩).
+  Proof.
+    induction 1 ; cbn.
+    all: now econstructor.
+  Qed.
+
+  Lemma whnf_ren t : whnf t -> whnf (t⟨ρ⟩).
+  Proof.
+    induction 1 ; cbn.
+    all: econstructor.
+    now eapply whne_ren.
+  Qed.
+
+  Lemma isType_ren A : isType A -> isType (A⟨ρ⟩).
+  Proof.
+    induction 1 ; cbn.
+    all: econstructor.
+    now eapply whne_ren.
+  Qed.
+
+  Lemma isPosType_ren A : isPosType A -> isPosType (A⟨ρ⟩).
+  Proof.
+    destruct 1 ; cbn.
+    all: econstructor.
+    now eapply whne_ren.
+  Qed.
+
+  Lemma isFun_ren f : isFun f -> isFun (f⟨ρ⟩).
+  Proof.
+    induction 1 ; cbn.
+    all: econstructor.
+    now eapply whne_ren.
+  Qed.
+
+  Lemma isPair_ren f : isPair f -> isPair (f⟨ρ⟩).
+  Proof.
+    induction 1 ; cbn.
+    all: econstructor.
+    now eapply whne_ren.
+  Qed.
+
+  Lemma isCanonical_ren t : isCanonical t <~> isCanonical (t⟨ρ⟩).
+  Proof.
+    split.
+    all: destruct t ; cbn ; inversion 1.
+    all: now econstructor.
+  Qed.
+
+End RenWhnf.
diff --git a/theories/Weakening.v b/theories/Weakening.v
index 0b63fa1d..fc01da69 100644
--- a/theories/Weakening.v
+++ b/theories/Weakening.v
@@ -220,62 +220,6 @@ Proof.
       now econstructor.
 Qed.
 
-(** ** Normal and neutral forms are stable by weakening *)
-
-Section RenWhnf.
-
-  Variable (ρ : nat -> nat).
-
-  Lemma whne_ren t : whne t -> whne (t⟨ρ⟩).
-  Proof.
-    induction 1 ; cbn.
-    all: now econstructor.
-  Qed.
-
-  Lemma whnf_ren t : whnf t -> whnf (t⟨ρ⟩).
-  Proof.
-    induction 1 ; cbn.
-    all: econstructor.
-    now eapply whne_ren.
-  Qed.
-  
-  Lemma isType_ren A : isType A -> isType (A⟨ρ⟩).
-  Proof.
-    induction 1 ; cbn.
-    all: econstructor.
-    now eapply whne_ren.
-  Qed.
-
-  Lemma isPosType_ren A : isPosType A -> isPosType (A⟨ρ⟩).
-  Proof.
-    destruct 1 ; cbn.
-    all: econstructor.
-    now eapply whne_ren.
-  Qed.
-  
-  Lemma isFun_ren f : isFun f -> isFun (f⟨ρ⟩).
-  Proof.
-    induction 1 ; cbn.
-    all: econstructor.
-    now eapply whne_ren.
-  Qed.
-
-  Lemma isPair_ren f : isPair f -> isPair (f⟨ρ⟩).
-  Proof.
-    induction 1 ; cbn.
-    all: econstructor.
-    now eapply whne_ren.
-  Qed.
-
-  Lemma isCanonical_ren t : isCanonical t <~> isCanonical (t⟨ρ⟩).
-  Proof.
-    split.
-    all: destruct t ; cbn ; inversion 1.
-    all: now econstructor.
-  Qed.
-
-End RenWhnf.
-
 Section RenWlWhnf.
 
   Context {Γ Δ} (ρ : Δ ≤ Γ).