Anonymize TODOs and floris_mixture

Author: Jesse Michael Han

src/abstract_forcing.lean

@@ -57,7 +57,7 @@ instance : forcing_notion punit := order_top.mk (by finish)
 
 instance forcing_notion_complete_boolean_algebra {α : Type u} [complete_boolean_algebra α] : forcing_notion α := order_top.mk (by finish)
 
---TODO(jesse) rewrite in terms of pSet.rec and Name.rec
+--TODO() rewrite in terms of pSet.rec and Name.rec
 def pSet_equiv_trivial_name : pSet.{u} ≃ (punit-name : Type (u+1)) :=
 { to_fun := λ u,
   begin

src/bfol.lean

@@ -804,7 +804,7 @@ by { ext, simp [bd_not] }
   (s : bounded_term L n) : (f ⊓ g)[s/0] = (f[s/0] ⊓ g[s/0]) :=
 by { ext, simp[bd_and, bd_not] }
 
--- --TODO(floris)
+-- --TODO()
 -- lemma realize_subst_bt {L : Language} {S : bStructure L β} : ∀{n n' l}
 --   (t : bounded_preterm L (n+n'+1) l)
 --   (s : bounded_term L n') (v : dvector S n) (v' : dvector S n') (v'' : dvector S l),

src/bvm.lean

@@ -57,7 +57,7 @@ by {rw[inf_comm], apply bv_cases_left, simpa only [inf_comm]}
 lemma bv_specialize {ι : Type*} {s : ι → 𝔹} (i : ι) {b : 𝔹} {h : s i ≤ b} :
 (⨅(i:ι), s i) ≤ b := infi_le_of_le i h
 
---TODO(jesse) write the version of this for an arbitrary list of instantiations
+--TODO() write the version of this for an arbitrary list of instantiations
 lemma bv_specialize_twice {ι : Type*} {s : ι → 𝔹} (i j : ι) {b : 𝔹} {h : s i ⊓ s j ≤ b} :
 (⨅(i:ι), s i) ≤ b :=
 begin
@@ -589,7 +589,7 @@ poset_yoneda_inv Γ subset_trans $ le_inf ‹_› ‹_›
 --   apply subset_trans
 -- end
 
--- TODO(jesse): mark this as simp
+-- TODO(): mark this as simp
 lemma mem_of_mem_subset {x y z : bSet 𝔹} {Γ} (H₂ : Γ ≤ y ⊆ᴮ z) (H₁ : Γ ≤ x ∈ᴮ y) : Γ ≤ x ∈ᴮ z :=
 by {rw[subset_unfold'] at H₂, from H₂ x ‹_›}
 
@@ -636,7 +636,7 @@ begin
   from (poset_yoneda_inv _ (h_congr _ _) this)
 end
 
--- TODO(jesse) maybe replace this with typeclasses instead?
+-- TODO() maybe replace this with typeclasses instead?
 @[reducible]def B_ext (ϕ : bSet 𝔹 → 𝔹) : Prop :=
   ∀ x y, x =ᴮ y ⊓ ϕ x ≤ ϕ y
 
@@ -734,7 +734,7 @@ lemma bv_cc.mk_iff {Γ} {x y : bSet 𝔹} : Γ ≤ x =ᴮ y ↔ (@quotient.mk _
 
 lemma bv_cc.mk {Γ} {x y : bSet 𝔹} (H : Γ ≤ x =ᴮ y) : (@quotient.mk _ (b_setoid Γ) x) = (@quotient.mk _ (b_setoid Γ) y) := bv_cc.mk_iff.mp ‹_›
 
--- TODO(jesse): automate the generation of these lemmas with typeclasses
+-- TODO(): automate the generation of these lemmas with typeclasses
 def b_setoid_mem (Γ : 𝔹) : quotient (b_setoid Γ) → quotient (b_setoid Γ) → Prop :=
 @quotient.lift₂ (bSet 𝔹) (bSet 𝔹) Prop (b_setoid Γ) (b_setoid Γ) (λ x y, Γ ≤ x ∈ᴮ y)
   begin
@@ -948,7 +948,7 @@ begin
   apply bv_or_elim; [apply bv_use (ulift.up ff), apply bv_use (ulift.up tt)]; refl
 end
 
-def floris_mixture {ι : Type u} (a : ι → 𝔹) (u : ι → bSet 𝔹) : bSet 𝔹 :=
+def anon_mixture {ι : Type u} (a : ι → 𝔹) (u : ι → bSet 𝔹) : bSet 𝔹 :=
   ⟨Σ(i : ι), (u i).type, λx, (u x.fst).func x.snd, λx, a x.fst ⊓ (u x.fst).bval x.snd⟩
 
 /-- Mixing lemma, c.f. Bell's book or Lemma 1 of Hamkins-Seabold -/
@@ -980,7 +980,7 @@ begin
   split; [specialize this (ulift.up ff), specialize this (ulift.up tt)]; exact this
 end
 
--- TODO(jesse) try proving mixing_lemma with floris_mixture and see if anything goes wrong
+-- TODO() try proving mixing_lemma with _mixture and see if anything goes wrong
 
 /-- In particular, the mixing lemma applies when the weights (a_i) form an antichain and the indexing is injective -/
 lemma h_star_of_antichain_injective {ι : Type u} {a : ι → 𝔹} {τ : ι → bSet 𝔹} {h_anti : antichain (a '' set.univ)} {h_inj : function.injective a} :
@@ -1549,7 +1549,7 @@ by {apply top_unique, rw[<-H_top], apply mem.mk'}
 by simp
 
 /--
-TODO(jesse): this name should really belong to check_mem instead
+TODO(): this name should really belong to check_mem instead
 -/
 @[simp]lemma mem_check_of_mem {x : pSet} {i : x.type} {Γ : 𝔹} : Γ ≤ ((x.func i) ̌) ∈ᴮ (x̌) :=
 begin
@@ -1676,7 +1676,7 @@ begin
       rw[this] at H, conv{to_rhs, rw[<-H]}, simp }
 end
 
--- TODO(jesse): refactor this so that the conclusion is simply Γ ≤ ¬ (x̌ ∈ᴮ y̌)
+-- TODO(): refactor this so that the conclusion is simply Γ ≤ ¬ (x̌ ∈ᴮ y̌)
 lemma check_not_mem {x y : pSet} : x ∉ y → ∀ {Γ : 𝔹}, Γ ≤ x̌ ∈ᴮ y̌ → Γ ≤ ⊥ :=
 by {intro H, replace H := not_check_mem_iff.mp H, intros Γ HΓ, rwa ←H}
 
@@ -1731,7 +1731,7 @@ end
 @[simp]lemma check_exists_mem {y : pSet} (H_exists_mem : ∃ z, z ∈ y ) {Γ : 𝔹} : Γ ≤ exists_mem y̌ :=
 by { rcases H_exists_mem with ⟨z,Hz⟩, apply bv_use ž, simp* }
 
--- note(jesse): this lemma is not true; one also requires that x is a check-name
+-- note(): this lemma is not true; one also requires that x is a check-name
 -- lemma definite_mem_definite_iff_of_subset_check {x y : bSet 𝔹} (H_definite₁ : is_definite x) (H_definite₂ : is_definite y) (H_sub : ∃ z : pSet, ⊤ ≤ y ⊆ᴮ ž)  : ⊤ ≤ x ∈ᴮ y ↔ ∃ j : y.type, ⊤ ≤ x =ᴮ y.func j :=
 -- begin
 --   refine ⟨_,_⟩; intro H,
@@ -1842,7 +1842,7 @@ end
 
 lemma collect_spec₂ {Γ : 𝔹} (H_AE : Γ ≤ ⨅ i : u.type, u.bval i ⟹ ⨆ w, ϕ (u.func i) w) :
   Γ ≤ ⨅ w, w ∈ᴮ collect ϕ h_congr_right h_congr_left u ⟹ ⨆ z, z ∈ᴮ u ⊓ ϕ z w :=
-begin -- TODO(jesse):  prove mem_collect_iff
+begin -- TODO():  prove mem_collect_iff
   bv_intro w, bv_imp_intro Hw_mem, rw mem_unfold at Hw_mem, bv_cases_at Hw_mem i Hi,
   apply bv_use (u.func i), bv_split, apply bv_rw' Hi_right,
     { refine B_ext_inf _ _,
@@ -2016,7 +2016,7 @@ prefix `𝒫`:80 := bv_powerset
 -- def bv_powerset' (u : bSet 𝔹) : bSet 𝔹 :=
 -- ⟨u.type → 𝔹, λ f, set_of_indicator' f, λ f, ⊤⟩
 
---TODO (jesse) try proving bv_powerset and bv_powerset' are equivalent
+--TODO () try proving bv_powerset and bv_powerset' are equivalent
 
 -- example {u : bSet 𝔹} : bv_powerset u =ᴮ bv_powerset' u = ⊤ :=
 -- begin
@@ -2295,7 +2295,7 @@ begin
   change _ ≤ bSet.insert1 0 0 =ᴮ bSet.insert1 0 ∅,
   convert bv_refl, unfold has_zero.zero, unfold of_nat, unfold pSet.of_nat, rw check_empty_eq_empty
 end
---TODO(jesse): add simp lemmas ensuing (0 : bSet 𝔹) is the simp normal form of (∅̌), (of_nat 0), etc
+--TODO(): add simp lemmas ensuing (0 : bSet 𝔹) is the simp normal form of (∅̌), (of_nat 0), etc
 
 lemma forall_empty {Γ : 𝔹} {ϕ : bSet 𝔹 → 𝔹} : Γ ≤ ⨅ x, x ∈ᴮ ∅ ⟹ ϕ x :=
 begin

src/bvm_extras.lean

@@ -1720,7 +1720,7 @@ begin
       bv_cases_at H_right' s, apply bv_use s, bv_split, refine le_inf _ ‹_›,
       refine le_inf (le_inf _ _) ‹_›,
         {apply bv_rw' (bv_symm ‹_ ≤ g =ᴮ func (𝒫 prod x y) s›), simp, from ‹_›},
-      -- TODO(jesse) why does apply fail to generate a motive for bv_rw'?
+      -- TODO() why does apply fail to generate a motive for bv_rw'?
       bv_intro w₁, bv_imp_intro Hw₁, replace H_left_right := H_left_right w₁ ‹_›,
       bv_cases_at H_left_right w₂, apply bv_use w₂, bv_split, refine le_inf ‹_› _,
       apply bv_rw' (bv_symm ‹_ ≤ g =ᴮ func (𝒫 prod x y) s›), simp, from ‹_› }
@@ -1763,8 +1763,8 @@ begin
   bv_split_at H, rw[mem_unfold] at H_left H_right,
   bv_cases_at H_left pr₁ Hpr₁, bv_cases_at H_right pr₂ Hpr₂,
   cases pr₁ with i j, cases pr₂ with i' j', simp at *, repeat{auto_cases},
-  rw[pair_eq_pair_iff] at Hpr₁_right Hpr₂_right, auto_cases, -- floris, don't look at the tactic state
-  have := @H_ext i i' Γ_4 (by bv_cc), bv_cc -- TODO(jesse): 𝔹-valued eblast?
+  rw[pair_eq_pair_iff] at Hpr₁_right Hpr₂_right, auto_cases, -- , don't look at the tactic state
+  have := @H_ext i i' Γ_4 (by bv_cc), bv_cc -- TODO(): 𝔹-valued eblast?
 end
 
 lemma function.mk'_is_total {Γ} : Γ ≤ is_total x y (function.mk' F χ H_ext H_mem) :=
@@ -2009,12 +2009,12 @@ end
 --    bv_split_at a_right_left_1, bv_split_at a_right_right_1,
 --    simp only with cleanup at a_right_left_1_1_1 a_right_right_1_1_1,
 --    bv_mp a_right_right_1_1_1 (eq_of_eq_pair_left),
---    bv_mp a_right_right_1_1_1 (eq_of_eq_pair_right), -- TODO(jesse) generate sane variable names
+--    bv_mp a_right_right_1_1_1 (eq_of_eq_pair_right), -- TODO() generate sane variable names
 --    bv_mp a_right_left_1_1_1 (eq_of_eq_pair_left),
 --    bv_mp a_right_left_1_1_1 (eq_of_eq_pair_right),
 --    have : Γ_2 ≤ func u i =ᴮ func u j, apply bv_trans, rw[bv_eq_symm],
 --    assumption, rw[bv_eq_symm], apply bv_trans, rw[bv_eq_symm],
---    assumption, assumption, -- TODO(jesse) write a cc-like tactic to automate this
+--    assumption, assumption, -- TODO() write a cc-like tactic to automate this
 --    suffices : Γ_2 ≤ F i =ᴮ F j,
 --     by {apply bv_trans, assumption, rw[bv_eq_symm], apply bv_trans,
 --        assumption, from this},
@@ -2690,7 +2690,7 @@ begin
   bv_cases_at H_mem k, cases k with k, simp at H_mem_1, refine bv_use _,
   exact (ulift.up $ k + 1), simp, apply bv_rw' H_mem_1,
     { exact @B_ext_term 𝔹 _ (λ z, z =ᴮ ((k+1)̃ ̌)) succ (by simp) (by simp) },
-      -- TODO(jesse): automate calculation of the motive
+      -- TODO(): automate calculation of the motive
     { simp[pSet.of_nat, succ] },
 end
 

src/henkin.lean

@@ -128,7 +128,7 @@ def diagram.mk.map {F : ℕ → Language} {h_succ : ∀{i : ℕ}, F i →ᴸ F (
 | x (y+1) h := by {by_cases x = y + 1, rw[h], exact ⟨λn, id, λn, id⟩, refine h_succ ∘  _,
                   apply diagram.mk.map, apply nat.le_of_le_and_ne_succ, repeat{assumption}}
 
---TODO(jesse) finish converting this to language versions and refactor henkin_language_chain
+--TODO() finish converting this to language versions and refactor henkin_language_chain
 -- @[simp]lemma diagram.mk.map_self_id {F : ℕ → Type*} {h_succ : ∀(i : ℕ), F i → F (i+1)} (x : ℕ) :
 --                   @diagram.mk.map F @h_succ x x (by constructor) = id :=
 -- by {induction x, tidy, simp[diagram.mk.map,*], refl}
@@ -504,7 +504,7 @@ end
 -- to complete the structural recursion
 
 /- The universal map from colimit preterm L_n → preterm L_infty is a bijection -/
--- TODO(jesse) refactor with new colimit lemmas
+-- TODO() refactor with new colimit lemmas
 lemma term_comparison_bijective {L : Language} (l) : function.bijective (@term_comparison L l) :=
 begin
   refine ⟨_,_⟩,
@@ -880,7 +880,7 @@ end
   -- have : ∃ k : ℕ, @ι L T k ⊢' bd_falsum,
   -- {sorry}, -- again, this depends on picking a representative of a germ-eq class
   --          -- on the induced colimit of formulas
-  --          -- remark(Floris): we need a lemma that if a directed union of theories proves f, then an element of it proves f.
+  --          -- remark(): we need a lemma that if a directed union of theories proves f, then an element of it proves f.
   -- cases this with k P', unfold ι at P',
   -- apply is_consistent_henkin_theory_chain hT k,
   -- apply nonempty.map (Lhom.reflect_prf (henkin_language_canonical_map_inj k)),

src/pSet_ordinal.lean

@@ -1049,7 +1049,7 @@ lemma powerset_sound {x : pSet.{u}} : ⟦pSet.powerset x⟧ = Set.powerset ⟦x
 def set_of_indicator {x : pSet.{u}} (χ : x.type → Prop) : pSet.{u} :=
 ⟨{i // χ i}, λ p, x.func (p.1)⟩
 
-def functions (x y : pSet.{u}) : pSet.{u} := -- TODO(jesse): show this satisfies specification
+def functions (x y : pSet.{u}) : pSet.{u} := -- TODO(): show this satisfies specification
 @set_of_indicator (powerset $ prod x y)
   (λ i_S, is_func x y ((powerset $ prod x y).func i_S))
 

src/parse_formula.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 The Flypitch Project. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author(s): Jesse Michael Han, Floris van Doorn
+Author(s):
 
 Parsing formulas from Lean expressions.
 -/
@@ -71,7 +71,7 @@ meta def to_term_empty : Π {n : ℕ}, expr → option (preterm L_empty n)
 | 0     (expr.var k)    := some (var k)
 | _     _               := none
 
--- TODO(jesse) insert a case analysis on whether e' : Prop to determine whether or not to use imp
+-- TODO() insert a case analysis on whether e' : Prop to determine whether or not to use imp
 meta def to_formula_empty : Π {n : ℕ}, expr → option (preformula L_empty n)
 | 0 (expr.pi _ _ e' e)     := ((to_formula_empty e) >>= (λ f, return (all f)))
 | 0 `(%%a = %%b)          := do e₁ <- to_term_empty a, e₂ <- to_term_empty b,

src/print_formula.lean

@@ -53,7 +53,7 @@ meta def print_formula : ∀ {n : ℕ}, bounded_formula L_ZFC n → string := λ
 
 meta def print_formula_list {n} (axms : list (bounded_formula L_ZFC n)) : tactic unit :=
 do tactic.trace (to_string axms)
--- TODO(jesse) format this so that newlines are inserted after commas
+-- TODO() format this so that newlines are inserted after commas
 
 section test
 

src/to_mathlib.lean

@@ -1313,7 +1313,7 @@ do  v_a <- target >>= lhs_of_le,
     Γ_name <- get_unused_name "Γ",
     v <- mk_mvar, v' <- mk_mvar,
     Γ_new <- pose Γ_name none v,
-    -- TODO(jesse) try replacing to_expr with an expression via mk_app instead
+    -- TODO() try replacing to_expr with an expression via mk_app instead
     new_goal <- to_expr ``((%%Γ_new : %%tp) ≤ %%v'),
     tactic.change new_goal,
     ctx <- local_context,
@@ -1334,7 +1334,7 @@ do  v_a <- target >>= lhs_of_le,
     Γ_name <- get_unused_name "Γ",
     v <- mk_mvar, v' <- mk_mvar,
     Γ_new <- pose Γ_name none v,
-    -- TODO(jesse) try replacing to_expr with an expression via mk_app instead
+    -- TODO() try replacing to_expr with an expression via mk_app instead
     new_goal <- to_expr ``((%%Γ_new : %%tp) ≤ %%v'),
     tactic.change new_goal,
     ctx <- local_context,
@@ -1355,7 +1355,7 @@ do  v_a <- target >>= lhs_of_le,
     Γ_name <- get_unused_name "Γ",
     v <- mk_mvar, v' <- mk_mvar,
     Γ_new <- pose Γ_name none v,
-    -- TODO(jesse) try replacing to_expr with an expression via mk_app instead
+    -- TODO() try replacing to_expr with an expression via mk_app instead
     new_goal <- to_expr ``((%%Γ_new : %%tp) ≤ %%v'),
     tactic.change new_goal,
     ctx <- local_context,
@@ -1477,7 +1477,7 @@ begin
     { by simp* }
 end
 
--- TODO(jesse) debug these
+-- TODO() debug these
 -- meta def auto_or_elim_step : tactic unit :=
 -- do  ctx <- local_context >>= (λ l, l.mfilter hyp_is_ineq_sup),
 --     if ctx.length > 0 then