Setup for hypothesis construction

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

ConNF.lean

@@ -10,7 +10,7 @@ import ConNF.Basic.WellOrder
 import ConNF.Construction.Code
 import ConNF.Construction.ConstructHypothesis
 import ConNF.Construction.ConstructMotive
-import ConNF.Construction.MainMotive
+import ConNF.Construction.InductionStatement
 import ConNF.Construction.NewModelData
 import ConNF.Construction.RunInduction
 import ConNF.Counting.BaseCoding

ConNF/Construction/ConstructHypothesis.lean

@@ -20,22 +20,93 @@ namespace ConNF
 variable [Params.{u}] {α : Λ} (M : (β : Λ) → (β : TypeIndex) < α → Motive β)
   (H : (β : Λ) → (h : (β : TypeIndex) < α) → Hypothesis (M β h) λ γ h' ↦ M γ (h'.trans h))
 
+def constructAllPermSderiv {β : Λ} (h : (β : TypeIndex) < α)
+    (ρ : (constructMotive α M H).data.AllPerm) : (M β h).data.AllPerm :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  letI : LtLevel β := ⟨h⟩
+  ρ.sderiv β
+
+def constructAllPermBotSderiv (ρ : (constructMotive α M H).data.AllPerm) : botModelData.AllPerm :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  ρ.sderiv ⊥
+
+def constructSingleton {β : Λ} (h : (β : TypeIndex) < α)
+    (x : (M β h).data.TSet) : (constructMotive α M H).data.TSet :=
+  letI : Level := ⟨α⟩
+  letI := ltData M
+  letI : LtLevel β := ⟨h⟩
+  Option.some (newSingleton x)
+
+theorem constructMotive_allPermSderiv_forget {β : Λ} (h : (β : TypeIndex) < α)
+    (ρ : (constructMotive α M H).data.AllPerm) :
+    (M β h).data.allPermForget (constructAllPermSderiv M H h ρ) =
+    (constructMotive α M H).data.allPermForget ρ ↘ h := sorry
+
+theorem constructMotive_allPermBotSderiv_forget (ρ : (constructMotive α M H).data.AllPerm) :
+    botModelData.allPermForget (constructAllPermBotSderiv M H ρ) =
+    (constructMotive α M H).data.allPermForget ρ ↘ bot_lt_coe _ := sorry
+
+theorem constructMotive_pos_atom_lt_pos :
+    letI := (constructMotive α M H).data; letI := (constructMotive α M H).pos
+    ∀ (t : Tangle α) (A : α ↝ ⊥) (a : Atom), a ∈ (t.support ⇘. A)ᴬ → pos a < pos t := sorry
+
+theorem constructMotive_pos_nearLitter_lt_pos :
+    letI := (constructMotive α M H).data; letI := (constructMotive α M H).pos
+    ∀ (t : Tangle α) (A : α ↝ ⊥) (M : NearLitter), M ∈ (t.support ⇘. A)ᴺ → pos M < pos t := sorry
+
+theorem constructMotive_smul_fuzz {β γ : Λ} (hβ : (β : TypeIndex) < α)
+    (hγ : (γ : TypeIndex) < α) (hβγ : (β : TypeIndex) ≠ γ) :
+    letI := (M β hβ).data; letI := (M β hβ).pos
+    ∀ (ρ : (constructMotive α M H).data.AllPerm) (t : Tangle β),
+      (constructMotive α M H).data.allPermForget ρ ↘ hγ ↘. • fuzz hβγ t =
+      fuzz hβγ (constructAllPermSderiv M H hβ ρ • t) := sorry
+
+theorem constructMotive_smul_fuzz_bot {γ : Λ} (hγ : (γ : TypeIndex) < α) :
+    letI := botModelData; letI := botPosition
+    ∀ (ρ : (constructMotive α M H).data.AllPerm) (t : Tangle ⊥),
+    (constructMotive α M H).data.allPermForget ρ ↘ hγ ↘. • fuzz (bot_ne_coe (a := γ)) t =
+      fuzz (bot_ne_coe (a := γ)) (constructAllPermBotSderiv M H ρ • t) := sorry
+
+theorem constructMotive_allPerm_of_smul_fuzz :
+    ∀ (ρs : {β : Λ} → (hβ : (β : TypeIndex) < α) → (M β hβ).data.AllPerm)
+    (π : letI := botModelData; AllPerm ⊥),
+    (∀ {β γ : Λ} (hβ : (β : TypeIndex) < α) (hγ : (γ : TypeIndex) < α),
+      letI := (M β hβ).data; letI := (M β hβ).pos
+      ∀ (hδε : (β : TypeIndex) ≠ γ) (t : Tangle β),
+      (ρs hγ)ᵁ ↘. • fuzz hδε t = fuzz hδε (ρs hβ • t)) →
+    (∀ {γ : Λ} (hγ : (γ : TypeIndex) < α) (t : letI := botModelData; Tangle ⊥),
+      letI := botModelData; letI := botPosition
+      (ρs hγ)ᵁ ↘. • fuzz (bot_ne_coe (a := γ)) t = fuzz (bot_ne_coe (a := γ)) (π • t)) →
+    ∃ ρ : (constructMotive α M H).data.AllPerm,
+      (∀ (β : Λ) (hβ : (β : TypeIndex) < α), constructAllPermSderiv M H hβ ρ = ρs hβ) ∧
+      constructAllPermBotSderiv M H ρ = π := sorry
+
+theorem constructMotive_tSet_ext (β : Λ) (hβ : (β : TypeIndex) < α)
+    (x y : (constructMotive α M H).data.TSet) :
+    (∀ z : (M β hβ).data.TSet, z ∈[hβ] x ↔ z ∈[hβ] y) → x = y := sorry
+
+theorem constructMotive_typedMem_singleton_iff {β : Λ} (hβ : (β : TypeIndex) < α)
+    (x y : (M β hβ).data.TSet) :
+    y ∈[hβ] constructSingleton M H hβ x ↔ y = x := sorry
+
 def constructHypothesis (α : Λ) (M : (β : Λ) → (β : TypeIndex) < α → Motive β)
     (H : (β : Λ) → (h : (β : TypeIndex) < α) → Hypothesis (M β h) λ γ h' ↦ M γ (h'.trans h)) :
     Hypothesis (constructMotive α M H) M :=
   {
-    allPermSderiv := sorry
-    allPermBotSderiv := sorry
-    singleton := sorry
-    allPermSderiv_forget := sorry
-    allPermBotSderiv_forget := sorry
-    pos_atom_lt_pos := sorry
-    pos_nearLitter_lt_pos := sorry
-    smul_fuzz := sorry
-    smul_fuzz_bot := sorry
-    allPerm_of_smul_fuzz := sorry
-    tSet_ext := sorry
-    typedMem_singleton_iff := sorry
+    allPermSderiv := constructAllPermSderiv M H
+    allPermBotSderiv := constructAllPermBotSderiv M H
+    singleton := constructSingleton M H
+    allPermSderiv_forget := constructMotive_allPermSderiv_forget M H
+    allPermBotSderiv_forget := constructMotive_allPermBotSderiv_forget M H
+    pos_atom_lt_pos := constructMotive_pos_atom_lt_pos M H
+    pos_nearLitter_lt_pos := constructMotive_pos_nearLitter_lt_pos M H
+    smul_fuzz := constructMotive_smul_fuzz M H
+    smul_fuzz_bot := constructMotive_smul_fuzz_bot M H
+    allPerm_of_smul_fuzz := constructMotive_allPerm_of_smul_fuzz M H
+    tSet_ext := constructMotive_tSet_ext M H
+    typedMem_singleton_iff := constructMotive_typedMem_singleton_iff M H
   }
 
 end ConNF

ConNF/Construction/ConstructMotive.lean

@@ -1,4 +1,4 @@
-import ConNF.Construction.MainMotive
+import ConNF.Construction.InductionStatement
 import ConNF.Construction.NewModelData
 import ConNF.Counting.Conclusions
 
@@ -82,10 +82,6 @@ abbrev TangleLe (β : TypeIndex) (hβ : β ≤ α) : Type _ :=
     letI : Level := ⟨α⟩; letI := leData M; letI : LeLevel β := ⟨hβ⟩
     Tangle β
 
-def castTSetLeBot :
-    TSetLe M ⊥ bot_le ≃ (letI := botModelData; TSet ⊥) :=
-  Equiv.refl _
-
 def castTSetLeLt {β : Λ} (hβ : (β : TypeIndex) < α) :
     TSetLe M β hβ.le ≃ (M β hβ).data.TSet :=
   castTSet rfl (heq_of_eq <| leData_data_lt M hβ)
@@ -94,10 +90,6 @@ def castTSetLeEq {β : Λ} (hβ : (β : TypeIndex) = α) :
     TSetLe M β hβ.le ≃ (newModelData' M).TSet :=
   castTSet hβ (by cases hβ; exact heq_of_eq <| leData_data_eq M)
 
-def castAllPermLeBot :
-    AllPermLe M ⊥ bot_le ≃ (letI := botModelData; AllPerm ⊥) :=
-  Equiv.refl _
-
 def castAllPermLeLt {β : Λ} (hβ : (β : TypeIndex) < α) :
     AllPermLe M β hβ.le ≃ (M β hβ).data.AllPerm :=
   castAllPerm rfl (heq_of_eq <| leData_data_lt M hβ)
@@ -106,10 +98,6 @@ def castAllPermLeEq {β : Λ} (hβ : (β : TypeIndex) = α) :
     AllPermLe M β hβ.le ≃ (newModelData' M).AllPerm :=
   castAllPerm hβ (by cases hβ; exact heq_of_eq <| leData_data_eq M)
 
-def castTangleLeBot :
-    TangleLe M ⊥ bot_le ≃ (letI := botModelData; Tangle ⊥) :=
-  Equiv.refl _
-
 def castTangleLeLt {β : Λ} (hβ : (β : TypeIndex) < α) :
     TangleLe M β hβ.le ≃ (letI := (M β hβ).data; Tangle β) :=
   castTangle rfl (heq_of_eq <| leData_data_lt M hβ)