Merge pull request #57 from CoqHott/move-nf-ren

Move renaming lemmas on normal forms to NormalForms.
CoqHott · Oct 2, 2023 · 30deee3 · 30deee3
2 parents 1f16171 + dc66f00
commit 30deee3
Show file tree

Hide file tree

Showing 2 changed files with 58 additions and 57 deletions.
diff --git a/theories/NormalForms.v b/theories/NormalForms.v
@@ -129,3 +129,61 @@ 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.
+
+#[global] Hint Resolve whne_ren whnf_ren isType_ren isPosType_ren isFun_ren isCanonical_ren : gen_typing.
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 {Γ Δ} (ρ : Δ ≤ Γ).
@@ -317,7 +261,6 @@ Section RenWlWhnf.
 
 End RenWlWhnf.
 
-#[global] Hint Resolve whne_ren whnf_ren isType_ren isPosType_ren isFun_ren isCanonical_ren : gen_typing.
 #[global] Hint Resolve whne_ren_wl whnf_ren_wl isType_ren_wl isPosType_ren_wl isFun_ren_wl isCanonical_ren_wl : gen_typing.
 
 (** ** Adaptation of AutoSubst's asimpl to well typed weakenings *)