Finish building IH

Signed-off-by: zeramorphic <[email protected]>
leanprover-community · Mar 27, 2024 · 7b6760b · 7b6760b
1 parent d4a4fb0
commit 7b6760b
Show file tree

Hide file tree

Showing 2 changed files with 126 additions and 37 deletions.
diff --git a/ConNF/Model/Construction.lean b/ConNF/Model/Construction.lean
@@ -11,6 +11,7 @@ namespace ConNF.Construction
 
 variable [Params.{u}] [BasePositions]
 
+@[ext]
 structure Tang (α : Λ) (TSet : Type u) (Allowable : Type u)
     [Group Allowable] [MulAction Allowable TSet] [MulAction Allowable (Address α)] where
   set : TSet
@@ -1456,6 +1457,75 @@ theorem mk_tSet_step (α : Λ) (ihs : (β : Λ) → β < α → IH β)
   rw [← foaData_tSet_eq]
   exact mk_tSet α (mk_codingFunction_le α ihs h)
 
+noncomputable def posStep (α : Λ) (ihs : (β : Λ) → β < α → IH β)
+    (h : ∀ (β : Λ) (hβ : β < α), IHProp β (fun γ hγ => ihs γ (hγ.trans_lt hβ))) :
+    letI : Level := ⟨α⟩
+    letI := tangleDataStep α ihs
+    Tang α (TSet α) (Allowable α) → μ :=
+  letI : Level := ⟨α⟩
+  letI : TangleDataLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).tangleData⟩
+  letI : PositionedTanglesLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedTangles⟩
+  letI : TypedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).typedObjects
+  letI : PositionedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedObjects
+  fun t => NewTangle.pos (mk_tSet_step α ihs h) (t.set, t.support)
+
+theorem posStep_injective (α : Λ) (ihs : (β : Λ) → β < α → IH β)
+    (h : ∀ (β : Λ) (hβ : β < α), IHProp β (fun γ hγ => ihs γ (hγ.trans_lt hβ))) :
+    letI : Level := ⟨α⟩
+    letI := tangleDataStep α ihs
+    Function.Injective (posStep α ihs h) := by
+  letI : Level := ⟨α⟩
+  letI : TangleDataLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).tangleData⟩
+  letI : PositionedTanglesLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedTangles⟩
+  letI : TypedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).typedObjects
+  letI : PositionedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedObjects
+  intro t₁ t₂ ht
+  have := NewTangle.pos_injective (mk_tSet_step α ihs h) ht
+  simp only [Prod.mk.injEq] at this
+  exact Tang.ext _ _ this.1 this.2
+
+theorem posStep_typedAtom (α : Λ) (ihs : (β : Λ) → β < α → IH β)
+    (h : ∀ (β : Λ) (hβ : β < α), IHProp β (fun γ hγ => ihs γ (hγ.trans_lt hβ))) :
+    letI : Level := ⟨α⟩
+    letI : TangleDataLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).tangleData⟩
+    letI : PositionedTanglesLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedTangles⟩
+    letI : TypedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).typedObjects
+    letI : PositionedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedObjects
+    letI := tangleDataStep α ihs
+    ∀ (a : Atom) (t : Tang α (TSet α) (Allowable α)),
+    t.set = newTypedAtom a → pos a ≤ posStep α ihs h t := by
+  letI : Level := ⟨α⟩
+  letI : TangleDataLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).tangleData⟩
+  letI : PositionedTanglesLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedTangles⟩
+  letI : TypedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).typedObjects
+  letI : PositionedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedObjects
+  intro a t ha
+  have := NewTangle.pos_not_mem_deny (mk_tSet_step α ihs h) (t.set, t.support)
+  contrapose! this
+  refine ⟨pos a, ?_, this.le⟩
+  exact Or.inl (Or.inr ⟨a, ha, rfl⟩)
+
+theorem posStep_typedNearLitter (α : Λ) (ihs : (β : Λ) → β < α → IH β)
+    (h : ∀ (β : Λ) (hβ : β < α), IHProp β (fun γ hγ => ihs γ (hγ.trans_lt hβ))) :
+    letI : Level := ⟨α⟩
+    letI : TangleDataLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).tangleData⟩
+    letI : PositionedTanglesLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedTangles⟩
+    letI : TypedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).typedObjects
+    letI : PositionedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedObjects
+    letI := tangleDataStep α ihs
+    ∀ (N : NearLitter) (t : Tang α (TSet α) (Allowable α)),
+    t.set = newTypedNearLitter N → pos N ≤ posStep α ihs h t := by
+  letI : Level := ⟨α⟩
+  letI : TangleDataLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).tangleData⟩
+  letI : PositionedTanglesLt := ⟨fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedTangles⟩
+  letI : TypedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).typedObjects
+  letI : PositionedObjectsLt := fun β hβ => (ihs β (coe_lt_coe.mp hβ.elim)).positionedObjects
+  intro N t hN
+  have := NewTangle.pos_not_mem_deny (mk_tSet_step α ihs h) (t.set, t.support)
+  contrapose! this
+  refine ⟨pos N, ?_, this.le⟩
+  exact Or.inr ⟨N, hN, rfl⟩
+
 noncomputable def buildStep (α : Λ) (ihs : (β : Λ) → β < α → IH β)
     (h : ∀ (β : Λ) (hβ : β < α), IHProp β (fun γ hγ => ihs γ (hγ.trans_lt hβ))) : IH α :=
   letI : Level := ⟨α⟩
@@ -1469,9 +1539,9 @@ noncomputable def buildStep (α : Λ) (ihs : (β : Λ) → β < α → IH β)
   {
     __ := tangleDataStep α ihs
     __ := typedObjectsStep α ihs
-    pos := sorry
-    pos_typedAtom := sorry
-    pos_typedNearLitter := sorry
+    pos := ⟨posStep α ihs h, posStep_injective α ihs h⟩
+    pos_typedAtom := posStep_typedAtom α ihs h
+    pos_typedNearLitter := posStep_typedNearLitter α ihs h
   }
 
 noncomputable def buildStepFn (α : Λ) (ihs : (β : Λ) → β < α → IH β)

diff --git a/ConNF/NewTangle/Position.lean b/ConNF/NewTangle/Position.lean
@@ -13,30 +13,33 @@ universe u
 namespace ConNF.NewTangle
 
 variable [Params.{u}] [Level] [BasePositions] [TangleDataLt] [PositionedTanglesLt] [TypedObjectsLt]
+  [PositionedObjectsLt]
 
-#exit
-
-def posBound (t : NewTangle) : Set μ :=
-  {ν | ∃ (A : ExtendedIndex α) (a : Atom), ⟨A, inl a⟩ ∈ t.S ∧
+def posBound (t : NewTSet) (S : Support α) : Set μ :=
+  {ν | ∃ (A : ExtendedIndex α) (a : Atom), ⟨A, inl a⟩ ∈ S ∧
     ∃ (β : TypeIndex) (_ : LtLevel β) (s : Tangle β) (γ : Λ) (_ : LtLevel γ) (hβγ : β ≠ γ),
     a.1 = fuzz hβγ s ∧ ν = pos s} ∪
-  {ν | ∃ (A : ExtendedIndex α) (N : NearLitter), ⟨A, inr N⟩ ∈ t.S ∧
+  {ν | ∃ (A : ExtendedIndex α) (N : NearLitter), ⟨A, inr N⟩ ∈ S ∧
     ∃ (β : TypeIndex) (_ : LtLevel β) (s : Tangle β) (γ : Λ) (_ : LtLevel γ) (hβγ : β ≠ γ),
-    Set.Nonempty ((N : Set Atom) ∩ (fuzz hβγ s).toNearLitter) ∧ ν = pos s}
+    Set.Nonempty ((N : Set Atom) ∩ (fuzz hβγ s).toNearLitter) ∧ ν = pos s} ∪
+  {ν | ∃ a : Atom, t = newTypedAtom a ∧ ν = pos a} ∪
+  {ν | ∃ N : NearLitter, t = newTypedNearLitter N ∧ ν = pos N}
 
-def posBound' (t : NewTangle) : Set μ :=
-  (⋃ (c ∈ t.S) (A ∈ {A | c.1 = A}) (a ∈ {a | c.2 = inl a}) (β : TypeIndex) (_ : LtLevel β)
+def posBound' (t : NewTSet) (S : Support α) : Set μ :=
+  (⋃ (c ∈ S) (A ∈ {A | c.1 = A}) (a ∈ {a | c.2 = inl a}) (β : TypeIndex) (_ : LtLevel β)
     (γ : Λ) (_ : LtLevel γ) (hβγ : β ≠ γ)
     (s : Tangle β) (_ : s ∈ {s | a.1 = fuzz hβγ s}),
     {ν | ν = pos s}) ∪
-  (⋃ (c ∈ t.S) (A ∈ {A | c.1 = A}) (N ∈ {N | c.2 = inr N}) (β : TypeIndex) (_ : LtLevel β)
+  (⋃ (c ∈ S) (A ∈ {A | c.1 = A}) (N ∈ {N | c.2 = inr N}) (β : TypeIndex) (_ : LtLevel β)
     (γ : Λ) (_ : LtLevel γ)(hβγ : β ≠ γ)
     (s : Tangle β) (_ : s ∈ {s | Set.Nonempty ((N : Set Atom) ∩ (fuzz hβγ s).toNearLitter)}),
-    {ν | ν = pos s})
+    {ν | ν = pos s}) ∪
+  (⋃ (a ∈ {a | t = newTypedAtom a}), {pos a}) ∪
+  (⋃ (N ∈ {a | t = newTypedNearLitter a}), {pos N})
 
-theorem posBound_eq_posBound' (t : NewTangle) : posBound t = posBound' t := by
+theorem posBound_eq_posBound' (t : NewTSet) (S : Support α) : posBound t S = posBound' t S := by
   rw [posBound, posBound']
-  refine congr_arg₂ _ ?_ ?_
+  refine congr_arg₂ _ (congr_arg₂ _ (congr_arg₂ _ ?_ ?_) ?_) ?_
   · ext ν
     simp only [ne_eq, exists_and_right, mem_setOf_eq, setOf_eq_eq_singleton', mem_singleton_iff,
       setOf_eq_eq_singleton, iUnion_exists, iUnion_iUnion_eq_left, mem_iUnion, exists_prop]
@@ -53,11 +56,15 @@ theorem posBound_eq_posBound' (t : NewTangle) : posBound t = posBound' t := by
       exact ⟨⟨A, inr N⟩, hNS, N, rfl, β, inferInstance, γ, inferInstance, hβγ, s, hNs, hν⟩
     · rintro ⟨⟨A, x⟩, hNS, N, rfl, β, _, γ, _, hβγ, s, hNs, hν⟩
       exact ⟨A, N, hNS, β, inferInstance, s, ⟨γ, inferInstance, hβγ, hNs⟩, hν⟩
+  · ext ν
+    simp only [mem_setOf_eq, mem_iUnion, mem_singleton_iff, exists_prop]
+  · ext ν
+    simp only [mem_setOf_eq, mem_iUnion, mem_singleton_iff, exists_prop]
 
-theorem small_posBound (t : NewTangle) : Small (posBound t) := by
+theorem small_posBound (t : NewTSet) (S : Support α) : Small (posBound t S) := by
   rw [posBound_eq_posBound', posBound']
-  refine Small.union ?_ ?_
-  · refine Small.bUnion t.S.small (fun c _ => ?_)
+  refine Small.union (Small.union (Small.union ?_ ?_) ?_) ?_
+  · refine Small.bUnion S.small (fun c _ => ?_)
     refine Small.bUnion (by simp only [setOf_eq_eq_singleton', small_singleton]) (fun A _ => ?_)
     refine Small.bUnion ?_ (fun a _ => ?_)
     · refine Set.Subsingleton.small ?_
@@ -75,7 +82,7 @@ theorem small_posBound (t : NewTangle) : Small (posBound t) := by
       exact fuzz_injective _ (h₁.symm.trans h₂)
     · simp only [ne_eq, mem_setOf_eq, setOf_eq_eq_singleton, small_singleton, forall_exists_index,
         implies_true, forall_const]
-  · refine Small.bUnion t.S.small (fun c _ => ?_)
+  · refine Small.bUnion S.small (fun c _ => ?_)
     refine Small.bUnion (by simp only [setOf_eq_eq_singleton', small_singleton]) (fun A _ => ?_)
     refine Small.bUnion ?_ (fun N _ => ?_)
     · refine Set.Subsingleton.small ?_
@@ -99,52 +106,64 @@ theorem small_posBound (t : NewTangle) : Small (posBound t) := by
       · exact Or.inl ⟨a, Or.inr ⟨ha, ha'⟩, rfl⟩
     · simp only [ne_eq, mem_setOf_eq, setOf_eq_eq_singleton, small_singleton, forall_exists_index,
         implies_true, forall_const]
-
-def posDeny (t : NewTangle) : Set μ :=
-  {ν | ∃ ν' ∈ posBound t, ν ≤ ν'}
-
-theorem mk_posDeny (t : NewTangle) : #(posDeny t) < #μ := by
-  have := (small_posBound t).trans_le Params.κ_le_μ_ord_cof
+  · refine Small.bUnion ?_ (fun _ _ => small_singleton _)
+    refine Set.Subsingleton.small ?_
+    intro a₁ ha₁ a₂ ha₂
+    exact newTypedAtom_injective (ha₁.symm.trans ha₂)
+  · refine Small.bUnion ?_ (fun _ _ => small_singleton _)
+    refine Set.Subsingleton.small ?_
+    intro N₁ hN₁ N₂ hN₂
+    exact newTypedNearLitter_injective (hN₁.symm.trans hN₂)
+
+def posDeny (t : NewTSet × Support α) : Set μ :=
+  {ν | ∃ ν' ∈ posBound t.1 t.2, ν ≤ ν'}
+
+theorem mk_posDeny (t : NewTSet × Support α) : #(posDeny t) < #μ := by
+  have := (small_posBound t.1 t.2).trans_le Params.κ_le_μ_ord_cof
   rw [← Params.μ_ord] at this
   obtain ⟨ν, hν⟩ := Ordinal.lt_cof_type this
   refine (Cardinal.mk_subtype_le_of_subset ?_).trans_lt (card_Iic_lt ν)
   rintro ν₁ ⟨ν₂, hν₂, hν₁⟩
   exact hν₁.trans (hν ν₂ hν₂).le
 
-theorem exists_wellOrder (h : #NewTangle = #μ) :
-    ∃ (r : NewTangle → NewTangle → Prop) (_ : IsWellOrder NewTangle r),
+theorem exists_wellOrder (h : #NewTSet = #μ) :
+    ∃ (r : NewTSet × Support α → NewTSet × Support α → Prop)
+    (_ : IsWellOrder (NewTSet × Support α) r),
     Ordinal.type r = Cardinal.ord #μ := by
-  rw [Cardinal.eq] at h
-  obtain ⟨e⟩ := h
+  have : #(NewTSet × Support α) = #μ
+  · simp only [Cardinal.mk_prod, Cardinal.lift_id, h, mk_support]
+    exact Cardinal.mul_eq_self Params.μ_isStrongLimit.isLimit.aleph0_le
+  rw [Cardinal.eq] at this
+  obtain ⟨e⟩ := this
   refine ⟨e ⁻¹'o (· < ·), RelIso.IsWellOrder.preimage ((· < ·) : μ → μ → Prop) e, ?_⟩
   rw [Ordinal.type_preimage ((· < ·) : μ → μ → Prop) e, Params.μ_ord]
 
-def wellOrder (h : #NewTangle = #μ) : NewTangle → NewTangle → Prop :=
+def wellOrder (h : #NewTSet = #μ) : NewTSet × Support α → NewTSet × Support α → Prop :=
   (exists_wellOrder h).choose
 
-instance wellOrder_isWellOrder (h : #NewTangle = #μ) :
-    IsWellOrder NewTangle (wellOrder h) :=
+instance wellOrder_isWellOrder (h : #NewTSet = #μ) :
+    IsWellOrder (NewTSet × Support α) (wellOrder h) :=
   (exists_wellOrder h).choose_spec.choose
 
-theorem wellOrder_type (h : #NewTangle = #μ) :
+theorem wellOrder_type (h : #NewTSet = #μ) :
     Ordinal.type (wellOrder h) = Cardinal.ord #μ :=
   (exists_wellOrder h).choose_spec.choose_spec
 
-theorem mk_posDeny' (h : #NewTangle = #μ) (t : NewTangle) :
+theorem mk_posDeny' (h : #NewTSet = #μ) (t : NewTSet × Support α) :
     #{ s // wellOrder h s t } + #(posDeny t) < #μ := by
   refine Cardinal.add_lt_of_lt Params.μ_isStrongLimit.isLimit.aleph0_le ?_ (mk_posDeny t)
   simp only [Ordinal.card_typein]
   have := Ordinal.typein_lt_type (wellOrder h) t
   rw [wellOrder_type, Cardinal.lt_ord] at this
   exact this
 
-noncomputable def pos (h : #NewTangle = #μ) : NewTangle → μ :=
+noncomputable def pos (h : #NewTSet = #μ) : NewTSet × Support α → μ :=
   chooseWf posDeny (mk_posDeny' h)
 
-theorem pos_injective (h : #NewTangle = #μ) : Injective (pos h) :=
+theorem pos_injective (h : #NewTSet = #μ) : Injective (pos h) :=
   chooseWf_injective
 
-theorem pos_not_mem_deny (h : #NewTangle = #μ) (t : NewTangle) :
+theorem pos_not_mem_deny (h : #NewTSet = #μ) (t : NewTSet × Support α) :
     pos h t ∉ posDeny t :=
   chooseWf_not_mem_deny t