Move renaming lemmas on normal forms to NormalForms.

They don't belong in the Weakening module because they rely on simple untyped renamings.
CoqHott · Sep 28, 2023 · ac2e141 · ac2e141
1 parent 1f16171
commit ac2e141
Show file tree

Hide file tree

Showing 2 changed files with 56 additions and 56 deletions.
diff --git 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
@@ -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 {Γ Δ} (ρ : Δ ≤ Γ).