Externalisation

Signed-off-by: zeramorphic <[email protected]>

ConNF.lean

@@ -10,6 +10,7 @@ import ConNF.Basic.WellOrder
 import ConNF.Construction.Code
 import ConNF.Construction.ConstructHypothesis
 import ConNF.Construction.ConstructMotive
+import ConNF.Construction.Externalise
 import ConNF.Construction.InductionStatement
 import ConNF.Construction.NewModelData
 import ConNF.Construction.RunInduction

ConNF/Construction/ConstructMotive.lean

@@ -45,16 +45,16 @@ def leData :
   letI : Level := ⟨α⟩
   letI data : (β : TypeIndex) → [LeLevel β] → ModelData β :=
     λ β hβ ↦ β.recBotCoe (λ _ ↦ botModelData)
-      (λ β hβ ↦ if h : β = α then
+      (λ β hβ ↦ if h : (β : TypeIndex) = α then
           cast (by rw [h]) (newModelData' M)
         else
-          (M β (LeLevel.elim.lt_of_ne (coe_injective.ne h))).data) hβ
+          (M β (LeLevel.elim.lt_of_ne h)).data) hβ
   letI positions : (β : TypeIndex) → [LtLevel β] → Position (Tangle β) :=
     λ β hβ ↦ β.recBotCoe (λ _ ↦ botPosition)
       (λ β hβ ↦
         cast (by
           congr; unfold data; rw [recBotCoe_coe, dif_neg];
-          exact (LtLevel.elim (β := β)).ne ∘ congrArg WithBot.some)
+          exact (LtLevel.elim (β := β)).ne)
         (M β LtLevel.elim).pos) hβ
   LeData.mk (data := data) (positions := positions)
 
@@ -64,7 +64,7 @@ theorem leData_data_bot :
 
 theorem leData_data_lt {β : Λ} (hβ : (β : TypeIndex) < α) :
     (letI : Level := ⟨α⟩; letI : LeLevel β := ⟨hβ.le⟩; (leData M).data β) = (M β hβ).data := by
-  simp only [leData, recBotCoe_coe, dif_neg (hβ.ne ∘ congrArg WithBot.some)]
+  simp only [leData, recBotCoe_coe, dif_neg hβ.ne]
 
 theorem leData_data_eq :
     (letI : Level := ⟨α⟩; letI : LeLevel α := ⟨le_rfl⟩; (leData M).data α) = newModelData' M := by

ConNF/Construction/Externalise.lean

@@ -0,0 +1,119 @@
+import ConNF.Construction.RunInduction
+
+/-!
+# Externalisation
+
+In this file, we convert many of our *internal* results (i.e. inside the induction) to *external*
+ones (i.e. defined using the global `TSet`/`AllPerm` definitions).
+
+## Main declarations
+
+* `ConNF.foo`: Something new.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal WithBot
+
+namespace ConNF
+
+variable [Params.{u}]
+
+instance globalModelData : {α : TypeIndex} → ModelData α
+  | (α : Λ) => (motive α).data
+  | ⊥ => botModelData
+
+instance globalPosition : {α : TypeIndex} → Position (Tangle α)
+  | (α : Λ) => (motive α).pos
+  | ⊥ => botPosition
+
+instance globalTypedNearLitters {α : Λ} : TypedNearLitters α :=
+  (motive α).typed
+
+instance globalLtData [Level] : LtData where
+
+instance globalLeData [Level] : LeData where
+
+omit [ConNF.Params.{u}] in
+theorem heq_funext {α : Sort _} {β γ : α → Sort _} {f : (x : α) → β x} {g : (x : α) → γ x}
+    (h : ∀ x, HEq (f x) (g x)) : HEq f g := by
+  cases funext λ x ↦ type_eq_of_heq (h x)
+  simp only [heq_eq_eq] at h ⊢
+  exact funext h
+
+theorem globalLeData_eq [Level] :
+    globalLeData = leData (λ β _ ↦ motive β) := by
+  apply LeData.ext
+  · ext β hβ
+    induction β using recBotCoe
+    case bot => rfl
+    case coe β =>
+      by_cases h : (β : TypeIndex) = α
+      · cases coe_injective h
+        rw [leData_data_eq]
+        unfold globalLeData globalModelData
+        dsimp only
+        rw [motive_eq]
+        rfl
+      · rw [leData_data_lt _ (hβ.elim.lt_of_ne h)]
+        rfl
+  · apply heq_funext
+    intro β
+    apply heq_funext
+    intro hβ
+    induction β using recBotCoe
+    case bot => rfl
+    case coe β =>
+      rw [leData]
+      simp only [coe_inj, id_eq, eq_mpr_eq_cast, recBotCoe_bot, recBotCoe_coe, LtLevel.elim.ne]
+      exact HEq.symm (cast_heq _ _)
+
+instance globalPreCoherentData [Level] : PreCoherentData where
+  allPermSderiv h := cast (by rw [globalLeData_eq])
+    ((preCoherentData (λ β _ ↦ motive β) (λ β _ ↦ hypothesis β)).allPermSderiv h)
+  singleton h := cast (by rw [globalLeData_eq])
+    ((preCoherentData (λ β _ ↦ motive β) (λ β _ ↦ hypothesis β)).singleton h)
+
+omit [Params] in
+@[simp]
+theorem heq_cast_eq_iff {α β γ : Type _} {x : α} {y : β} {h : α = γ} :
+    HEq (cast h x) y ↔ HEq x y := by
+  cases h
+  rw [cast_eq]
+
+theorem globalPreCoherentData_eq [Level] :
+    globalPreCoherentData = preCoherentData (λ β _ ↦ motive β) (λ β _ ↦ hypothesis β) := by
+  have := globalLeData_eq
+  rw [LeData.ext_iff] at this
+  apply PreCoherentData.ext
+  · exact this.1
+  · exact this.2
+  · unfold globalPreCoherentData
+    apply heq_funext; intro β
+    apply heq_funext; intro γ
+    apply heq_funext; intro hβ
+    apply heq_funext; intro hγ
+    apply heq_funext; intro hβγ
+    simp only [heq_cast_eq_iff]
+    rfl
+  · unfold globalPreCoherentData
+    apply heq_funext; intro β
+    apply heq_funext; intro γ
+    apply heq_funext; intro hβ
+    apply heq_funext; intro hγ
+    apply heq_funext; intro hβγ
+    simp only [heq_cast_eq_iff]
+    rfl
+
+def globalCoherentData [Level] : CoherentData where
+  allPermSderiv_forget := globalPreCoherentData_eq ▸ (coherentData _ _).allPermSderiv_forget
+  pos_atom_lt_pos := globalPreCoherentData_eq ▸ (coherentData _ _).pos_atom_lt_pos
+  pos_nearLitter_lt_pos := globalPreCoherentData_eq ▸ (coherentData _ _).pos_nearLitter_lt_pos
+  smul_fuzz := globalPreCoherentData_eq ▸ (coherentData _ _).smul_fuzz
+  allPerm_of_basePerm := globalPreCoherentData_eq ▸ (coherentData _ _).allPerm_of_basePerm
+  allPerm_of_smulFuzz := globalPreCoherentData_eq ▸ (coherentData _ _).allPerm_of_smulFuzz
+  tSet_ext := globalPreCoherentData_eq ▸ (coherentData _ _).tSet_ext
+  typedMem_singleton_iff := globalPreCoherentData_eq ▸ (coherentData _ _).typedMem_singleton_iff
+
+end ConNF

ConNF/Setup/CoherentData.lean

@@ -27,6 +27,7 @@ TODO: We're going to try allowing model data at level `⊥` to vary. That is, we
 variable [Params.{u}] [Level]
 
 /-- A convenience typeclass to hold data below the current level. -/
+@[ext]
 class LeData where
   [data : (β : TypeIndex) → [LeLevel β] → ModelData β]
   [positions : (β : TypeIndex) → [LtLevel β] → Position (Tangle β)]
@@ -37,6 +38,7 @@ instance [LeData] : (β : TypeIndex) → [LeLevel β] → ModelData β :=
 instance [LeData] : (β : TypeIndex) → [LtLevel β] → Position (Tangle β) :=
   LeData.positions
 
+@[ext]
 class PreCoherentData extends LeData where
   allPermSderiv {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) : AllPerm β → AllPerm γ
   singleton {β γ : Λ} [LeLevel β] [LeLevel γ] (h : (γ : TypeIndex) < β) : TSet γ → TSet β
@@ -74,6 +76,7 @@ typedMem_tSetForget {β : Λ} {γ : TypeIndex} [LeLevel β] [LeLevel γ]
   y ∈[hγ] xᵁ → ∃ z : TSet γ, y = zᵁ
 ```
 -/
+@[ext]
 class CoherentData extends PreCoherentData where
   allPermSderiv_forget {β γ : TypeIndex} [LeLevel β] [LeLevel γ] (h : γ < β) (ρ : AllPerm β) :
     (ρ ↘ h)ᵁ = ρᵁ ↘ h