Basic TTT stuff

Signed-off-by: Sky Wilshaw <[email protected]>

ConNF.lean

@@ -22,6 +22,8 @@ import ConNF.Counting.Conclusions
 import ConNF.Counting.CountSupportOrbit
 import ConNF.Counting.Recode
 import ConNF.Counting.Twist
+import ConNF.External.Basic
+import ConNF.External.WellOrder
 import ConNF.FOA.BaseAction
 import ConNF.FOA.BaseApprox
 import ConNF.FOA.Coherent

ConNF/External/Basic.lean

@@ -0,0 +1,155 @@
+import ConNF.Model.Result
+
+/-!
+# New file
+
+In this file...
+
+## Main declarations
+
+* `ConNF.foo`: Something new.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal ConNF.TSet
+
+namespace ConNF
+
+variable [Params.{u}] {α β γ δ ε ζ : Λ} (hβ : (β : TypeIndex) < α) (hγ : (γ : TypeIndex) < β)
+  (hδ : (δ : TypeIndex) < γ) (hε : (ε : TypeIndex) < δ) (hζ : (ζ : TypeIndex) < ε)
+
+def union (x y : TSet α) : TSet α :=
+  (xᶜ' ⊓' yᶜ')ᶜ'
+
+notation:68 x:68 " ⊔[" h "] " y:68 => _root_.ConNF.union h x y
+notation:68 x:68 " ⊔' " y:68 => x ⊔[by assumption] y
+
+@[simp]
+theorem mem_union_iff (x y : TSet α) :
+    ∀ z : TSet β, z ∈' x ⊔' y ↔ z ∈' x ∨ z ∈' y := by
+  rw [union]
+  intro z
+  rw [mem_compl_iff, mem_inter_iff, mem_compl_iff, mem_compl_iff, or_iff_not_and_not]
+
+def higherIndex (α : Λ) : Λ :=
+  (exists_gt α).choose
+
+theorem lt_higherIndex {α : Λ} :
+    (α : TypeIndex) < higherIndex α :=
+  WithBot.coe_lt_coe.mpr (exists_gt α).choose_spec
+
+theorem tSet_nonempty (h : ∃ β : Λ, (β : TypeIndex) < α) : Nonempty (TSet α) := by
+  obtain ⟨α', hα⟩ := h
+  constructor
+  apply typeLower lt_higherIndex lt_higherIndex lt_higherIndex hα
+  apply cardinalOne lt_higherIndex lt_higherIndex
+
+def univ : TSet α :=
+  (tSet_nonempty ⟨β, hβ⟩).some ⊔' (tSet_nonempty ⟨β, hβ⟩).someᶜ'
+
+@[simp]
+theorem mem_univ_iff :
+    ∀ x : TSet β, x ∈' univ hβ := by
+  intro x
+  rw [univ, mem_union_iff, mem_compl_iff]
+  exact em _
+
+/-- The set of all ordered pairs. -/
+def orderedPairs : TSet α :=
+  vCross hβ hγ hδ (univ hδ)
+
+@[simp]
+theorem mem_orderedPairs_iff (x : TSet β) :
+    x ∈' orderedPairs hβ hγ hδ ↔ ∃ a b, x = ⟨a, b⟩' := by
+  simp only [orderedPairs, vCross_spec, mem_univ_iff, and_true]
+
+def converse (x : TSet α) : TSet α :=
+  converse' hβ hγ hδ x ⊓' orderedPairs hβ hγ hδ
+
+@[simp]
+theorem op_mem_converse_iff (x : TSet α) :
+    ∀ a b, ⟨a, b⟩' ∈' converse hβ hγ hδ x ↔ ⟨b, a⟩' ∈' x := by
+  intro a b
+  simp only [converse, mem_inter_iff, converse'_spec, mem_orderedPairs_iff, op_inj, exists_and_left,
+    exists_eq', and_true]
+
+def cross (x y : TSet γ) : TSet α :=
+  converse hβ hγ hδ (vCross hβ hγ hδ x) ⊓' vCross hβ hγ hδ y
+
+@[simp]
+theorem mem_cross_iff (x y : TSet γ) :
+    ∀ a, a ∈' cross hβ hγ hδ x y ↔ ∃ b c, a = ⟨b, c⟩' ∧ b ∈' x ∧ c ∈' y := by
+  intro a
+  rw [cross, mem_inter_iff, vCross_spec]
+  constructor
+  · rintro ⟨h₁, b, c, rfl, h₂⟩
+    simp only [op_mem_converse_iff, vCross_spec, op_inj] at h₁
+    obtain ⟨b', c', ⟨rfl, rfl⟩, h₁⟩ := h₁
+    exact ⟨b, c, rfl, h₁, h₂⟩
+  · rintro ⟨b, c, rfl, h₁, h₂⟩
+    simp only [op_mem_converse_iff, vCross_spec, op_inj]
+    exact ⟨⟨c, b, ⟨rfl, rfl⟩, h₁⟩, ⟨b, c, ⟨rfl, rfl⟩, h₂⟩⟩
+
+def singletonImage (x : TSet β) : TSet α :=
+  singletonImage' hβ hγ hδ hε x ⊓' (cross hβ hγ hδ (cardinalOne hδ hε) (cardinalOne hδ hε))
+
+@[simp]
+theorem singletonImage_spec (x : TSet β) :
+    ∀ z w,
+    ⟨ {z}', {w}' ⟩' ∈' singletonImage hβ hγ hδ hε x ↔ ⟨z, w⟩' ∈' x := by
+  intro z w
+  rw [singletonImage, mem_inter_iff, singletonImage'_spec, and_iff_left_iff_imp]
+  intro hzw
+  rw [mem_cross_iff]
+  refine ⟨{z}', {w}', rfl, ?_⟩
+  simp only [mem_cardinalOne_iff, singleton_inj, exists_eq', and_self]
+
+theorem exists_of_mem_singletonImage {x : TSet β} {z w : TSet δ}
+    (h : ⟨z, w⟩' ∈' singletonImage hβ hγ hδ hε x) :
+    ∃ a b, z = {a}' ∧ w = {b}' := by
+  simp only [singletonImage, mem_inter_iff, mem_cross_iff, op_inj, mem_cardinalOne_iff] at h
+  obtain ⟨-, _, _, ⟨rfl, rfl⟩, ⟨a, rfl⟩, ⟨b, rfl⟩⟩ := h
+  exact ⟨a, b, rfl, rfl⟩
+
+/-- Turn a model element encoding a relation into an actual relation. -/
+def ExternalRel (r : TSet α) : Rel (TSet δ) (TSet δ) :=
+  λ x y ↦ ⟨x, y⟩' ∈' r
+
+@[simp]
+theorem externalRel_converse (r : TSet α) :
+    ExternalRel hβ hγ hδ (converse hβ hγ hδ r) = (ExternalRel hβ hγ hδ r).inv := by
+  ext
+  simp only [ExternalRel, op_mem_converse_iff, Rel.inv_apply]
+
+/-- The codomain of a relation. -/
+def codom (r : TSet α) : TSet γ :=
+  (typeLower lt_higherIndex hβ hγ hδ (singletonImage lt_higherIndex hβ hγ hδ r)ᶜ[lt_higherIndex])ᶜ'
+
+@[simp]
+theorem mem_codom_iff (r : TSet α) (x : TSet δ) :
+    x ∈' codom hβ hγ hδ r ↔ x ∈ (ExternalRel hβ hγ hδ r).codom := by
+  simp only [codom, mem_compl_iff, mem_typeLower_iff, not_forall, not_not]
+  constructor
+  · rintro ⟨y, hy⟩
+    obtain ⟨a, b, rfl, hb⟩ := exists_of_mem_singletonImage lt_higherIndex hβ hγ hδ hy
+    rw [singleton_inj] at hb
+    subst hb
+    rw [singletonImage_spec] at hy
+    exact ⟨a, hy⟩
+  · rintro ⟨a, ha⟩
+    use {a}'
+    rw [singletonImage_spec]
+    exact ha
+
+/-- The domain of a relation. -/
+def dom (r : TSet α) : TSet γ :=
+  codom hβ hγ hδ (converse hβ hγ hδ r)
+
+@[simp]
+theorem mem_dom_iff (r : TSet α) (x : TSet δ) :
+    x ∈' dom hβ hγ hδ r ↔ x ∈ (ExternalRel hβ hγ hδ r).dom := by
+  rw [dom, mem_codom_iff, externalRel_converse, Rel.inv_codom]
+
+end ConNF

ConNF/External/WellOrder.lean

@@ -0,0 +1,31 @@
+import ConNF.External.Basic
+
+/-!
+# New file
+
+In this file...
+
+## Main declarations
+
+* `ConNF.foo`: Something new.
+-/
+
+noncomputable section
+universe u
+
+open Cardinal Ordinal ConNF.TSet
+
+namespace ConNF
+
+variable [Params.{u}] {α β γ δ ε ζ : Λ} (hβ : (β : TypeIndex) < α) (hγ : (γ : TypeIndex) < β)
+  (hδ : (δ : TypeIndex) < γ) (hε : (ε : TypeIndex) < δ) (hζ : (ζ : TypeIndex) < ε)
+
+/-- A set in our model that is a well-order. Internal well-orders are exactly external well-orders,
+so we externalise the definition for convenience. -/
+def InternalWellOrder (r : TSet α) : Prop :=
+  IsWellOrder (TSet δ) (ExternalRel hβ hγ hδ r)
+
+def InternallyWellOrdered (x : TSet γ) : Prop :=
+  ∃ r, InternalWellOrder hβ hγ hδ r ∧ x = dom hβ hγ hδ r
+
+end ConNF

ConNF/Levels/StrSet.lean

@@ -132,7 +132,8 @@ end StrSet
 class TypedMem (X Y : Type _) (β α : outParam TypeIndex) where
   typedMem : β < α → X → Y → Prop
 
-notation:50 x:50 " ∈[" h:50 "] " y:50 => TypedMem.typedMem h x y
+notation:50 x:50 " ∈[" h "] " y:50 => TypedMem.typedMem h x y
+notation:50 x:50 " ∈' " y:50 => TypedMem.typedMem (by assumption) x y
 
 instance {β α : TypeIndex} : TypedMem (StrSet β) (StrSet α) β α where
   typedMem h x y :=

ConNF/Model/Hailperin.lean

@@ -356,8 +356,8 @@ theorem exists_converse (x : TSet α) :
         exact hab
 
 theorem exists_cardinalOne :
-    ∃ x : TSet α, ∀ a : TSet β, a ∈[hβ] x ↔ ∃ b, ∀ c : TSet γ, c ∈[hγ] a ↔ c = b := by
-  have := exists_of_symmetric {a | ∃ b, ∀ c : TSet γ, c ∈[hγ] a ↔ c = b} hβ ?_
+    ∃ x : TSet α, ∀ a : TSet β, a ∈[hβ] x ↔ ∃ b, a = singleton hγ b := by
+  have := exists_of_symmetric {a | ∃ b, a = singleton hγ b} hβ ?_
   · obtain ⟨y, hy⟩ := this
     use y
     intro a
@@ -369,13 +369,11 @@ theorem exists_cardinalOne :
     constructor
     · rintro ⟨z, ⟨a, ha⟩, rfl⟩
       refine ⟨ρ ↘ hβ ↘ hγ • a, ?_⟩
-      intro b
-      simp only [mem_smul_iff', allPerm_inv_sderiv', ha, inv_smul_eq_iff]
+      simp only [ha, smul_singleton]
     · rintro ⟨a, ha⟩
       rw [Set.mem_smul_set_iff_inv_smul_mem]
       refine ⟨ρ⁻¹ ↘ hβ ↘ hγ • a, ?_⟩
-      intro b
-      simp only [mem_smul_iff', inv_inv, allPerm_inv_sderiv', ha, smul_eq_iff_eq_inv_smul]
+      simp only [ha, smul_singleton, allPerm_inv_sderiv']
 
 theorem exists_subset :
     ∃ x : TSet α, ∀ a b, op hγ hδ a b ∈[hβ] x ↔ ∀ c : TSet ε, c ∈[hε] a → c ∈[hε] b := by

ConNF/Model/Result.lean

@@ -21,62 +21,117 @@ variable [Params.{u}] {α β γ δ ε ζ : Λ} (hβ : (β : TypeIndex) < α) (h
   (hδ : (δ : TypeIndex) < γ) (hε : (ε : TypeIndex) < δ) (hζ : (ζ : TypeIndex) < ε)
 
 theorem ext (x y : TSet α) :
-    (∀ z : TSet β, z ∈[hβ] x ↔ z ∈[hβ] y) → x = y :=
+    (∀ z : TSet β, z ∈' x ↔ z ∈' y) → x = y :=
   tSet_ext' hβ x y
 
-theorem exists_inter (x y : TSet α) :
-    ∃ w : TSet α, ∀ z : TSet β, z ∈[hβ] w ↔ z ∈[hβ] x ∧ z ∈[hβ] y :=
-  TSet.exists_inter hβ x y
+def inter (x y : TSet α) : TSet α :=
+  (TSet.exists_inter hβ x y).choose
 
-theorem exists_compl (x : TSet α) :
-    ∃ y : TSet α, ∀ z : TSet β, z ∈[hβ] y ↔ ¬z ∈[hβ] x :=
-  TSet.exists_compl hβ x
+notation:69 x:69 " ⊓[" h "] " y:69 => _root_.ConNF.inter h x y
+notation:69 x:69 " ⊓' " y:69 => x ⊓[by assumption] y
 
+@[simp]
+theorem mem_inter_iff (x y : TSet α) :
+    ∀ z : TSet β, z ∈' x ⊓' y ↔ z ∈' x ∧ z ∈' y :=
+  (TSet.exists_inter hβ x y).choose_spec
+
+def compl (x : TSet α) : TSet α :=
+  (TSet.exists_compl hβ x).choose
+
+notation:1024 x:1024 " ᶜ[" h "]" => _root_.ConNF.compl h x
+notation:1024 x:1024 " ᶜ'" => xᶜ[by assumption]
+
+@[simp]
+theorem mem_compl_iff (x : TSet α) :
+    ∀ z : TSet β, z ∈' xᶜ' ↔ ¬z ∈' x :=
+  (TSet.exists_compl hβ x).choose_spec
+
+notation:1024 "{" x "}[" h "]" => _root_.ConNF.singleton h x
+notation:1024 "{" x "}'" => {x}[by assumption]
+
+@[simp]
 theorem mem_singleton_iff (x y : TSet β) :
-    y ∈[hβ] singleton hβ x ↔ y = x :=
+    y ∈' {x}' ↔ y = x :=
   typedMem_singleton_iff' hβ x y
 
+notation:1024 "{" x ", " y "}[" h "]" => _root_.ConNF.TSet.up h x y
+notation:1024 "{" x ", " y "}'" => {x, y}[by assumption]
+
+@[simp]
 theorem mem_up_iff (x y z : TSet β) :
-    z ∈[hβ] up hβ x y ↔ z = x ∨ z = y :=
+    z ∈' {x, y}' ↔ z = x ∨ z = y :=
   TSet.mem_up_iff hβ x y z
 
+notation:1024 "⟨" x ", " y "⟩[" h ", " h' "]" => _root_.ConNF.TSet.op h h' x y
+notation:1024 "⟨" x ", " y "⟩'" => ⟨x, y⟩[by assumption, by assumption]
+
 theorem op_def (x y : TSet γ) :
-    op hβ hγ x y = up hβ (singleton hγ x) (up hγ x y) :=
+    (⟨x, y⟩' : TSet α) = { {x}', {x, y}' }' :=
   rfl
 
-theorem exists_singletonImage (x : TSet β) :
-    ∃ y : TSet α, ∀ z w,
-    op hγ hδ (singleton hε z) (singleton hε w) ∈[hβ] y ↔ op hδ hε z w ∈[hγ] x :=
-  TSet.exists_singletonImage hβ hγ hδ hε x
+def singletonImage' (x : TSet β) : TSet α :=
+  (TSet.exists_singletonImage hβ hγ hδ hε x).choose
+
+@[simp]
+theorem singletonImage'_spec (x : TSet β) :
+    ∀ z w,
+    ⟨ {z}', {w}' ⟩' ∈' singletonImage' hβ hγ hδ hε x ↔ ⟨z, w⟩' ∈' x :=
+  (TSet.exists_singletonImage hβ hγ hδ hε x).choose_spec
+
+def insertion2' (x : TSet γ) : TSet α :=
+  (TSet.exists_insertion2 hβ hγ hδ hε hζ x).choose
+
+@[simp]
+theorem insertion2'_spec (x : TSet γ) :
+    ∀ a b c, ⟨ { {a}' }', ⟨b, c⟩' ⟩' ∈' insertion2' hβ hγ hδ hε hζ x ↔
+    ⟨a, c⟩' ∈' x :=
+  (TSet.exists_insertion2 hβ hγ hδ hε hζ x).choose_spec
+
+def insertion3' (x : TSet γ) : TSet α :=
+  (TSet.exists_insertion3 hβ hγ hδ hε hζ x).choose
+
+theorem insertion3'_spec (x : TSet γ) :
+    ∀ a b c, ⟨ { {a}' }', ⟨b, c⟩' ⟩' ∈' insertion3' hβ hγ hδ hε hζ x ↔
+    ⟨a, b⟩' ∈' x :=
+  (TSet.exists_insertion3 hβ hγ hδ hε hζ x).choose_spec
+
+def vCross (x : TSet γ) : TSet α :=
+  (TSet.exists_cross hβ hγ hδ x).choose
+
+@[simp]
+theorem vCross_spec (x : TSet γ) :
+    ∀ a, a ∈' vCross hβ hγ hδ x ↔ ∃ b c, a = ⟨b, c⟩' ∧ c ∈' x :=
+  (TSet.exists_cross hβ hγ hδ x).choose_spec
+
+def typeLower (x : TSet α) : TSet δ :=
+  (TSet.exists_typeLower hβ hγ hδ hε x).choose
 
-theorem exists_insertion2 (x : TSet γ) :
-    ∃ y : TSet α, ∀ a b c, op hγ hδ (singleton hε (singleton hζ a)) (op hε hζ b c) ∈[hβ] y ↔
-    op hε hζ a c ∈[hδ] x :=
-  TSet.exists_insertion2 hβ hγ hδ hε hζ x
+@[simp]
+theorem mem_typeLower_iff (x : TSet α) :
+    ∀ a, a ∈' typeLower hβ hγ hδ hε x ↔ ∀ b, ⟨ b, {a}' ⟩' ∈' x :=
+  (TSet.exists_typeLower hβ hγ hδ hε x).choose_spec
 
-theorem exists_insertion3 (x : TSet γ) :
-    ∃ y : TSet α, ∀ a b c, op hγ hδ (singleton hε (singleton hζ a)) (op hε hζ b c) ∈[hβ] y ↔
-    op hε hζ a b ∈[hδ] x :=
-  TSet.exists_insertion3 hβ hγ hδ hε hζ x
+def converse' (x : TSet α) : TSet α :=
+  (TSet.exists_converse hβ hγ hδ x).choose
 
-theorem exists_cross (x : TSet γ) :
-    ∃ y : TSet α, ∀ a, a ∈[hβ] y ↔ ∃ b c, a = op hγ hδ b c ∧ c ∈[hδ] x :=
-  TSet.exists_cross hβ hγ hδ x
+@[simp]
+theorem converse'_spec (x : TSet α) :
+    ∀ a b, ⟨a, b⟩' ∈' converse' hβ hγ hδ x ↔ ⟨b, a⟩' ∈' x :=
+  (TSet.exists_converse hβ hγ hδ x).choose_spec
 
-theorem exists_typeLower (x : TSet α) :
-    ∃ y : TSet δ, ∀ a, a ∈[hε] y ↔ ∀ b, op hγ hδ b (singleton hε a) ∈[hβ] x :=
-  TSet.exists_typeLower hβ hγ hδ hε x
+def cardinalOne : TSet α :=
+  (TSet.exists_cardinalOne hβ hγ).choose
 
-theorem exists_converse (x : TSet α) :
-    ∃ y : TSet α, ∀ a b, op hγ hδ a b ∈[hβ] y ↔ op hγ hδ b a ∈[hβ] x :=
-  TSet.exists_converse hβ hγ hδ x
+@[simp]
+theorem mem_cardinalOne_iff :
+    ∀ a : TSet β, a ∈' cardinalOne hβ hγ ↔ ∃ b, a = {b}' :=
+  (TSet.exists_cardinalOne hβ hγ).choose_spec
 
-theorem exists_cardinalOne :
-    ∃ x : TSet α, ∀ a : TSet β, a ∈[hβ] x ↔ ∃ b, ∀ c : TSet γ, c ∈[hγ] a ↔ c = b :=
-  TSet.exists_cardinalOne hβ hγ
+def subset' : TSet α :=
+  (TSet.exists_subset hβ hγ hδ hε).choose
 
-theorem exists_subset :
-    ∃ x : TSet α, ∀ a b, op hγ hδ a b ∈[hβ] x ↔ ∀ c : TSet ε, c ∈[hε] a → c ∈[hε] b :=
-  TSet.exists_subset hβ hγ hδ hε
+theorem subset'_spec :
+    ∀ a b, ⟨a, b⟩' ∈' subset' hβ hγ hδ hε ↔ ∀ c : TSet ε, c ∈' a → c ∈' b :=
+  (TSet.exists_subset hβ hγ hδ hε).choose_spec
 
 end ConNF