feat(set_theory/lists): finite ZFA

Author: digama0

set_theory/lists.lean

@@ -0,0 +1,334 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+
+A computable model of hereditarily finite sets with atoms
+(ZFA without infinity). This is useful for calculations in naive
+set theory.
+-/
+import tactic.interactive data.list.basic
+
+variables {α : Type*}
+
+@[derive decidable_eq]
+inductive {u} lists' (α : Type u) : bool → Type u
+| atom : α → lists' ff
+| nil {} : lists' tt
+| cons' {b} : lists' b → lists' tt → lists' tt
+
+def lists (α : Type*) := Σ b, lists' α b
+
+namespace lists'
+
+def cons : lists α → lists' α tt → lists' α tt
+| ⟨b, a⟩ l := cons' a l
+
+@[simp] def to_list : ∀ {b}, lists' α b → list (lists α)
+| _ (atom a)    := []
+| _ nil         := []
+| _ (cons' a l) := ⟨_, a⟩ :: l.to_list
+
+@[simp] theorem to_list_cons (a : lists α) (l) :
+  to_list (cons a l) = a :: l.to_list :=
+by cases a; simp [cons]
+
+@[simp] def of_list : list (lists α) → lists' α tt
+| []       := nil
+| (a :: l) := cons a (of_list l)
+
+@[simp] theorem to_of_list (l : list (lists α)) : to_list (of_list l) = l :=
+by induction l; simp *
+
+@[simp] theorem of_to_list : ∀ (l : lists' α tt), of_list (to_list l) = l :=
+suffices ∀ b (h : tt = b) (l : lists' α b),
+  let l' : lists' α tt := by rw h; exact l in
+  of_list (to_list l') = l', from this _ rfl,
+λ b h l, begin
+  induction l, {cases h}, {exact rfl},
+  case lists'.cons' : b a l IH₁ IH₂ {
+    intro, change l' with cons' a l,
+    simpa [cons] using IH₂ rfl }
+end
+
+end lists'
+
+mutual inductive lists.equiv, lists'.subset
+with lists.equiv : lists α → lists α → Prop
+| refl (l) : lists.equiv l l
+| antisymm {l₁ l₂ : lists' α tt} :
+  lists'.subset l₁ l₂ → lists'.subset l₂ l₁ → lists.equiv ⟨_, l₁⟩ ⟨_, l₂⟩
+with lists'.subset : lists' α tt → lists' α tt → Prop
+| nil {l} : lists'.subset lists'.nil l
+| cons {a a' l l'} : lists.equiv a a' → a' ∈ lists'.to_list l' →
+  lists'.subset l l' → lists'.subset (lists'.cons a l) l'
+local infix ~ := equiv
+
+namespace lists'
+
+instance : has_subset (lists' α tt) := ⟨lists'.subset⟩
+
+instance {b} : has_mem (lists α) (lists' α b) :=
+⟨λ a l, ∃ a' ∈ l.to_list, a ~ a'⟩
+
+theorem mem_def {b a} {l : lists' α b} :
+  a ∈ l ↔ ∃ a' ∈ l.to_list, a ~ a' := iff.rfl
+
+@[simp] theorem mem_cons {a y l} : a ∈ @cons α y l ↔ a ~ y ∨ a ∈ l :=
+by simp [mem_def, or_and_distrib_right, exists_or_distrib]
+
+theorem cons_subset {a} {l₁ l₂ : lists' α tt} :
+  lists'.cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂ :=
+begin
+  refine ⟨λ h, _, λ ⟨⟨a', m, e⟩, s⟩, subset.cons e m s⟩,
+  generalize_hyp h' : lists'.cons a l₁ = l₁' at h,
+  cases h with l a' a'' l l' e m s, {cases a, cases h'},
+  cases a, cases a', cases h', exact ⟨⟨_, m, e⟩, s⟩
+end
+
+theorem of_list_subset {l₁ l₂ : list (lists α)} (h : l₁ ⊆ l₂) :
+  lists'.of_list l₁ ⊆ lists'.of_list l₂ :=
+begin
+  induction l₁, {exact subset.nil},
+  refine subset.cons (equiv.refl _) _ (l₁_ih (list.subset_of_cons_subset h)),
+  simp at h, simp [h]
+end
+
+@[refl] theorem subset.refl {l : lists' α tt} : l ⊆ l :=
+by rw ← lists'.of_to_list l; exact
+   of_list_subset (list.subset.refl _)
+
+theorem subset_nil {l : lists' α tt} :
+  l ⊆ lists'.nil → l = lists'.nil :=
+begin
+  rw ← of_to_list l,
+  induction to_list l; intro h, {refl},
+  rcases cons_subset.1 h with ⟨⟨_, ⟨⟩, _⟩, _⟩
+end
+
+theorem mem_of_subset' {a} {l₁ l₂ : lists' α tt}
+  (s : l₁ ⊆ l₂) (h : a ∈ l₁.to_list) : a ∈ l₂ :=
+begin
+  induction s with _ a a' l l' e m s IH, {cases h},
+  simp at h, rcases h with rfl|h,
+  exacts [⟨_, m, e⟩, IH h]
+end
+
+theorem subset_def {l₁ l₂ : lists' α tt} :
+  l₁ ⊆ l₂ ↔ ∀ a ∈ l₁.to_list, a ∈ l₂ :=
+⟨λ H a, mem_of_subset' H, λ H, begin
+  rw ← of_to_list l₁,
+  revert H, induction to_list l₁; intro,
+  { exact subset.nil },
+  { simp at H, exact cons_subset.2 ⟨H.1, ih H.2⟩ }
+end⟩
+
+end lists'
+
+namespace lists
+
+@[pattern] def atom (a : α) : lists α := ⟨_, lists'.atom a⟩
+
+@[pattern] def of' (l : lists' α tt) : lists α := ⟨_, l⟩
+
+@[simp] def to_list : lists α → list (lists α)
+| ⟨b, l⟩ := l.to_list
+
+def is_list (l : lists α) : Prop := l.1
+
+def of_list (l : list (lists α)) : lists α := of' (lists'.of_list l)
+
+theorem is_list_to_list (l : list (lists α)) : is_list (of_list l) :=
+eq.refl _
+
+theorem to_of_list (l : list (lists α)) : to_list (of_list l) = l :=
+by simp [of_list, of']
+
+theorem of_to_list : ∀ {l : lists α}, is_list l → of_list (to_list l) = l
+| ⟨tt, l⟩ _ := by simp [of_list, of']
+
+instance [decidable_eq α] : decidable_eq (lists α) :=
+by unfold lists; apply_instance
+
+instance [has_sizeof α] : has_sizeof (lists α) :=
+by unfold lists; apply_instance
+
+def induction_mut (C : lists α → Sort*) (D : lists' α tt → Sort*)
+  (C0 : ∀ a, C (atom a)) (C1 : ∀ l, D l → C (of' l))
+  (D0 : D lists'.nil) (D1 : ∀ a l, C a → D l → D (lists'.cons a l)) :
+  pprod (∀ l, C l) (∀ l, D l) :=
+begin
+  suffices : ∀ {b} (l : lists' α b),
+    pprod (C ⟨_, l⟩) (match b, l with
+    | tt, l := D l
+    | ff, l := punit
+    end),
+  { exact ⟨λ ⟨b, l⟩, (this _).1, λ l, (this l).2⟩ },
+  intros, induction l with a b a l IH₁ IH₂,
+  { exact ⟨C0 _, ⟨⟩⟩ },
+  { exact ⟨C1 _ D0, D0⟩ },
+  { suffices, {exact ⟨C1 _ this, this⟩},
+    exact D1 ⟨_, _⟩ _ IH₁.1 IH₂.2 }
+end
+
+def mem (a : lists α) : lists α → Prop
+| ⟨ff, l⟩ := false
+| ⟨tt, l⟩ := a ∈ l
+
+instance : has_mem (lists α) (lists α) := ⟨mem⟩
+
+theorem is_list_of_mem {a : lists α} : ∀ {l : lists α}, a ∈ l → is_list l
+| ⟨_, lists'.nil⟩       _ := rfl
+| ⟨_, lists'.cons' _ _⟩ _ := rfl
+
+theorem equiv.antisymm_iff {l₁ l₂ : lists' α tt} :
+  of' l₁ ~ of' l₂ ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁ :=
+begin
+  refine ⟨λ h, _, λ ⟨h₁, h₂⟩, equiv.antisymm h₁ h₂⟩,
+  cases h with _ _ _ h₁ h₂,
+  { simp [lists'.subset.refl] }, { exact ⟨h₁, h₂⟩ }
+end
+
+attribute [refl] equiv.refl
+
+theorem equiv_atom {a} {l : lists α} : atom a ~ l ↔ atom a = l :=
+⟨λ h, by cases h; refl, λ h, h ▸ equiv.refl _⟩
+
+theorem equiv.symm {l₁ l₂ : lists α} (h : l₁ ~ l₂) : l₂ ~ l₁ :=
+by cases h with _ _ _ h₁ h₂; [refl, exact equiv.antisymm h₂ h₁]
+
+theorem equiv.trans : ∀ {l₁ l₂ l₃ : lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃ :=
+begin
+  let trans := λ (l₁ : lists α), ∀ ⦃l₂ l₃⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃,
+  suffices : pprod (∀ l₁, trans l₁)
+    (∀ (l : lists' α tt) (l' ∈ l.to_list), trans l'), {exact this.1},
+  apply induction_mut,
+  { intros a l₂ l₃ h₁ h₂,
+    rwa ← equiv_atom.1 h₁ at h₂ },
+  { intros l₁ IH l₂ l₃ h₁ h₂,
+    cases h₁ with _ _ l₂, {exact h₂},
+    cases h₂ with _ _ l₃, {exact h₁},
+    cases equiv.antisymm_iff.1 h₁ with hl₁ hr₁,
+    cases equiv.antisymm_iff.1 h₂ with hl₂ hr₂,
+    apply equiv.antisymm_iff.2; split; apply lists'.subset_def.2,
+    { intros a₁ m₁,
+      rcases lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩, 
+      rcases lists'.mem_of_subset' hl₂ m₂ with ⟨a₃, m₃, e₂₃⟩,
+      exact ⟨a₃, m₃, IH _ m₁ e₁₂ e₂₃⟩ },
+    { intros a₃ m₃,
+      rcases lists'.mem_of_subset' hr₂ m₃ with ⟨a₂, m₂, e₃₂⟩, 
+      rcases lists'.mem_of_subset' hr₁ m₂ with ⟨a₁, m₁, e₂₁⟩,
+      exact ⟨a₁, m₁, (IH _ m₁ e₂₁.symm e₃₂.symm).symm⟩ } },
+  { rintro _ ⟨⟩ },
+  { intros a l IH₁ IH₂, simpa [IH₁] using IH₂ }
+end
+
+instance : setoid (lists α) :=
+⟨(~), equiv.refl, @equiv.symm _, @equiv.trans _⟩
+
+section decidable
+
+@[simp] def equiv.decidable_meas :
+  (psum (Σ' (l₁ : lists α), lists α) $
+   psum (Σ' (l₁ : lists' α tt), lists' α tt)
+   Σ' (a : lists α), lists' α tt) → ℕ
+| (psum.inl ⟨l₁, l₂⟩) := sizeof l₁ + sizeof l₂
+| (psum.inr $ psum.inl ⟨l₁, l₂⟩) := sizeof l₁ + sizeof l₂
+| (psum.inr $ psum.inr ⟨l₁, l₂⟩) := sizeof l₁ + sizeof l₂
+
+local attribute [-simp] add_comm add_assoc
+open well_founded_tactics
+
+theorem sizeof_pos {b} (l : lists' α b) : 0 < sizeof l :=
+by cases l; {unfold_sizeof, trivial_nat_lt}
+
+theorem lt_sizeof_cons' {b} (a : lists' α b) (l) :
+  sizeof (⟨b, a⟩ : lists α) < sizeof (lists'.cons' a l) :=
+by {unfold_sizeof, exact lt_add_of_pos_right _ (sizeof_pos _)}
+
+@[instance] mutual def equiv.decidable, subset.decidable, mem.decidable [decidable_eq α]
+with equiv.decidable : ∀ l₁ l₂ : lists α, decidable (l₁ ~ l₂)
+| ⟨ff, l₁⟩ ⟨ff, l₂⟩ := decidable_of_iff' (l₁ = l₂) $
+  by cases l₁; refine equiv_atom.trans (by simp [atom])
+| ⟨ff, l₁⟩ ⟨tt, l₂⟩ := is_false $ by rintro ⟨⟩
+| ⟨tt, l₁⟩ ⟨ff, l₂⟩ := is_false $ by rintro ⟨⟩
+| ⟨tt, l₁⟩ ⟨tt, l₂⟩ := begin
+  haveI :=
+    have sizeof l₁ + sizeof l₂ <
+         sizeof (⟨tt, l₁⟩ : lists α) + sizeof (⟨tt, l₂⟩ : lists α),
+    by default_dec_tac,
+    subset.decidable l₁ l₂,
+  haveI :=
+    have sizeof l₂ + sizeof l₁ <
+         sizeof (⟨tt, l₁⟩ : lists α) + sizeof (⟨tt, l₂⟩ : lists α),
+    by default_dec_tac,
+    subset.decidable l₂ l₁,
+  exact decidable_of_iff' _ equiv.antisymm_iff,
+end
+with subset.decidable : ∀ l₁ l₂ : lists' α tt, decidable (l₁ ⊆ l₂)
+| lists'.nil l₂ := is_true subset.nil
+| (@lists'.cons' _ b a l₁) l₂ := begin
+  haveI :=
+    have sizeof (⟨b, a⟩ : lists α) + sizeof l₂ <
+         sizeof (lists'.cons' a l₁) + sizeof l₂,
+    from add_lt_add_right (lt_sizeof_cons' _ _) _,
+    mem.decidable ⟨b, a⟩ l₂,
+  haveI :=
+    have sizeof l₁ + sizeof l₂ <
+         sizeof (lists'.cons' a l₁) + sizeof l₂,
+    by default_dec_tac,
+    subset.decidable l₁ l₂,
+  exact decidable_of_iff' _ (@lists'.cons_subset _ ⟨_, _⟩ _ _)
+end
+with mem.decidable : ∀ (a : lists α) (l : lists' α tt), decidable (a ∈ l)
+| a lists'.nil := is_false $ by rintro ⟨_, ⟨⟩, _⟩
+| a (lists'.cons' b l₂) := begin
+  haveI :=
+    have sizeof a + sizeof (⟨_, b⟩ : lists α) <
+         sizeof a + sizeof (lists'.cons' b l₂),
+    from add_lt_add_left (lt_sizeof_cons' _ _) _,
+    equiv.decidable a ⟨_, b⟩,
+  haveI :=
+    have sizeof a + sizeof l₂ <
+         sizeof a + sizeof (lists'.cons' b l₂),
+    by default_dec_tac,
+    mem.decidable a l₂,
+  refine decidable_of_iff' (a ~ ⟨_, b⟩ ∨ a ∈ l₂) _,
+  rw ← lists'.mem_cons, refl
+end
+using_well_founded {
+  rel_tac := λ _ _, `[exact ⟨_, measure_wf equiv.decidable_meas⟩],
+  dec_tac := `[assumption] }
+
+end decidable
+
+end lists
+
+namespace lists'
+
+theorem mem_equiv_left {l : lists' α tt} :
+  ∀ {a a'}, a ~ a' → (a ∈ l ↔ a' ∈ l) :=
+suffices ∀ {a a'}, a ~ a' → a ∈ l → a' ∈ l,
+  from λ a a' e, ⟨this e, this e.symm⟩,
+λ a₁ a₂ e₁ ⟨a₃, m₃, e₂⟩, ⟨_, m₃, e₁.symm.trans e₂⟩
+
+theorem mem_of_subset {a} {l₁ l₂ : lists' α tt}
+  (s : l₁ ⊆ l₂) : a ∈ l₁ → a ∈ l₂ | ⟨a', m, e⟩ :=
+(mem_equiv_left e).2 (mem_of_subset' s m)
+
+theorem subset.trans {l₁ l₂ l₃ : lists' α tt}
+  (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃ :=
+subset_def.2 $ λ a₁ m₁, mem_of_subset h₂ $ mem_of_subset' h₁ m₁
+
+end lists'
+
+def finsets (α : Type*) := quotient (@lists.setoid α)
+
+namespace finsets
+
+instance : has_emptyc (finsets α) := ⟨⟦lists.of' lists'.nil⟧⟩
+
+instance [decidable_eq α] : decidable_eq (finsets α) :=
+by unfold finsets; apply_instance
+
+end finsets

set_theory/zfc.lean

@@ -1,3 +1,10 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Mario Carneiro
+
+A model of ZFC in Lean.
+-/
 import data.set.basic
 
 universes u v
@@ -37,7 +44,7 @@ theorem equiv.refl (x) : equiv x x :=
 pSet.rec_on x $ λα A IH, ⟨λa, ⟨a, IH a⟩, λa, ⟨a, IH a⟩⟩
 
 theorem equiv.euc {x} : Π {y z}, equiv x y → equiv z y → equiv x z :=
-pSet.rec_on x $ λα A IH y, pSet.rec_on y $ λβ B _ ⟨γ, Γ⟩ ⟨αβ, βα⟩ ⟨γβ, βγ⟩,
+pSet.rec_on x $ λα A IH y, pSet.cases_on y $ λβ B ⟨γ, Γ⟩ ⟨αβ, βα⟩ ⟨γβ, βγ⟩,
 ⟨λa, let ⟨b, ab⟩ := αβ a, ⟨c, bc⟩ := βγ b in ⟨c, IH a ab bc⟩,
   λc, let ⟨b, cb⟩ := γβ c, ⟨a, ba⟩ := βα b in ⟨a, IH a ba cb⟩⟩