From 7e9411c625253958aded1adf4536da0cba376749 Mon Sep 17 00:00:00 2001 From: zeramorphic Date: Sun, 24 Nov 2024 18:50:06 +0000 Subject: [PATCH] Setup for hypothesis construction Signed-off-by: zeramorphic --- ConNF.lean | 2 +- ConNF/Construction/ConstructHypothesis.lean | 95 ++++++++++++++++--- ConNF/Construction/ConstructMotive.lean | 14 +-- ...ainMotive.lean => InductionStatement.lean} | 0 4 files changed, 85 insertions(+), 26 deletions(-) rename ConNF/Construction/{MainMotive.lean => InductionStatement.lean} (100%) diff --git a/ConNF.lean b/ConNF.lean index 2f3c495a06..fbfac5ea31 100644 --- a/ConNF.lean +++ b/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 diff --git a/ConNF/Construction/ConstructHypothesis.lean b/ConNF/Construction/ConstructHypothesis.lean index d3f9f27d75..6abe0dcc35 100644 --- a/ConNF/Construction/ConstructHypothesis.lean +++ b/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 diff --git a/ConNF/Construction/ConstructMotive.lean b/ConNF/Construction/ConstructMotive.lean index c5a60cdb04..e5f4bcd6aa 100644 --- a/ConNF/Construction/ConstructMotive.lean +++ b/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β) diff --git a/ConNF/Construction/MainMotive.lean b/ConNF/Construction/InductionStatement.lean similarity index 100% rename from ConNF/Construction/MainMotive.lean rename to ConNF/Construction/InductionStatement.lean