What happened to `show_term`

Stream: mathlib4

[Nick_adfor]

I want to use show_term to generate a proof from grind. But it gives me found a proof, but the corresponding tactic failed:.... I used to meet this too when using exact?

import Mathlib


/--
There does not exist an infinite σ-algebra that contains only countably many members.

This theorem states that it is impossible to have a σ-algebra that is both infinite
and countable. The proof proceeds by contradiction, showing that any infinite σ-algebra
must contain at least continuum many sets.
-/
theorem not_exists_infinite_countable_sigma_algebra :
    ¬ ∃ (α : Type) (i : MeasurableSpace α),
      Set.Countable {s : Set α | @MeasurableSet α i s} ∧
      Set.Infinite {s : Set α | @MeasurableSet α i s} := by
  -- Assume by contradiction that such a σ-algebra exists
  by_contra h_contra
  obtain ⟨α, i, h_countable, h_infinite⟩ := h_contra

  -- Define an equivalence relation: x ~ y if they belong to the same measurable sets
  set eqv : α → α → Prop := fun x y => ∀ s : Set α, MeasurableSet s → (x ∈ s ↔ y ∈ s)

  -- Each equivalence class is measurable (can be expressed as countable intersections)
  have h_partition : ∀ x : α, MeasurableSet {y : α | eqv x y} := by
    intro x
    -- Express the equivalence class as an intersection over measurable sets containing x
    -- and complements of measurable sets not containing x
    have h_eqv_class : {y : α | eqv x y} = ⋂ s ∈ {s : Set α | MeasurableSet s ∧ x ∈ s}, s ∩ ⋂ s ∈ {s : Set α | MeasurableSet s ∧ x∉s}, sᶜ := by
      ext y; aesop (config := {warnOnNonterminal := false})
      specialize a sᶜ; aesop (config := {warnOnNonterminal := false})
    rw [h_eqv_class]
    -- The intersection is measurable since it's over countably many measurable sets
    refine' MeasurableSet.biInter _ _ <;> aesop (config := {warnOnNonterminal := false})
    exact h_countable.mono fun s hs => hs.1
    -- Countability of the indexing set for complements
    have h_countable_inter : Set.Countable {s : Set α | MeasurableSet s ∧ x∉s} := by
      exact h_countable.mono fun s hs => hs.1
    exact MeasurableSet.inter left (MeasurableSet.biInter h_countable_inter fun s hs => MeasurableSet.compl hs.1)

  -- The σ-algebra is generated by the equivalence classes
  have h_sigma_gen : ∀ s : Set α, MeasurableSet s ↔ ∃ t : Set (Set α), t ⊆ { {y : α | eqv x y} | x : α } ∧ s = ⋃₀ t := by
    aesop (config := {warnOnNonterminal := false})
    · -- Forward direction: every measurable set is a union of equivalence classes
      use { { y : α | eqv x y } | x ∈ s }
      aesop (config := {warnOnNonterminal := false})
    · -- Reverse direction: any union of equivalence classes is measurable
      have h_measurable_w : ∀ s ∈ w, MeasurableSet s := by
        intro s hs
        specialize left hs
        aesop (config := {warnOnNonterminal := false})
      -- Countability of the indexing set
      have h_countable_w : w.Countable := by
        exact h_countable.mono h_measurable_w
      exact MeasurableSet.sUnion h_countable_w h_measurable_w

  -- The set of equivalence classes must be finite
  have h_eq_classes_finite : Set.Finite { {y : α | eqv x y} | x : α } := by
    by_cases h_eq_classes_infinite : Set.Infinite { {y : α | eqv x y} | x : α }
    · -- If equivalence classes were infinite, the power set would be uncountable
      have h_power_set_uncountable : ¬Set.Countable (Set.powerset { {y : α | eqv x y} | x : α }) := by
        intro h_power_set_countable
        -- Show that the power set has cardinality at least continuum
        have h_power_set_card : Cardinal.mk (Set.powerset { {y : α | eqv x y} | x : α }) ≤ Cardinal.aleph0 := by
          exact Cardinal.mk_le_aleph0_iff.mpr h_power_set_countable.to_subtype
        simp [*] at *
        -- Cantor's theorem gives contradiction with countability
        have h_card_ge_aleph0 : Cardinal.mk { {y : α | eqv x y} | x : α } ≥ Cardinal.aleph0 := by
          exact Cardinal.aleph0_le_mk_iff.mpr (h_eq_classes_infinite.to_subtype)
        exact h_power_set_card.not_gt (lt_of_lt_of_le (Cardinal.cantor _) (Cardinal.power_le_power_left two_ne_zero h_card_ge_aleph0))
      -- But the power set injects into our σ-algebra, contradicting countability
      apply_mod_cast False.elim <| h_power_set_uncountable <| Set.Countable.mono _ <| h_countable.image _
      use fun s => { t | ∃ x ∈ s, { y | eqv x y } = t }
      intro t ht
      use ⋃₀ t
      simp_all [Set.ext_iff]
      refine' ⟨⟨t, ht, fun x => Iff.rfl⟩, fun x => ⟨fun hx => _, fun hx => _⟩⟩
      · -- Show x is in the appropriate equivalence class
        obtain ⟨y, ⟨z, hz, hyz⟩, hy⟩ := hx
        convert hz
        obtain ⟨x_1, hx_1⟩ : ∃ x_1 : α, z = {y | eqv x_1 y} := by
          obtain ⟨x_1, hx_1⟩ := ht hz
          exact ⟨x_1, by ext; simp [hx_1]⟩
        ext
        simp [hx_1]
        -- Calculation
        have h_eqv_x1_y : eqv x_1 y := by
          exact hx_1.subset hyz
        constructor
        · intro hx_mem s hs_meas
          constructor
          · intro hx1_in_s
            -- y in s
            have h_y_in_s : y ∈ s := by
              -- Since $x_1$ and $y$ are equivalent, by definition of $eqv$, we have $x_1 \in s \leftrightarrow y \in s$.
              have hy_in_s : x_1 ∈ s ↔ y ∈ s := by
                apply h_eqv_x1_y s hs_meas;
              -- Apply the equivalence from hy_in_s to hx1_in_s to conclude y is in s.
              apply hy_in_s.mp hx1_in_s
            -- Since eqv y x✝ holds, for any measurable set s, y ∈ s ↔ x✝ ∈ s. Given that y ∈ s, it follows that x✝ ∈ s.
            have h_eqv_y_x : ∀ s : Set α, MeasurableSet s → (y ∈ s ↔ ‹α› ∈ s) := by
              -- Since y and x✝ are in the same equivalence class under eqv, by definition of eqv, this equivalence holds for all measurable sets s.
              intros s hs_meas; exact (hy ‹_›).mpr hx_mem s hs_meas;
            exact h_eqv_y_x s hs_meas |>.1 h_y_in_s
          · intro hx_in_s
            -- y in s
            have h_y_in_s : y ∈ s := by
              have hy_in_s : x_1 ∈ s ↔ y ∈ s := by
                apply h_eqv_x1_y s hs_meas;
              show_term grind +ring
            apply (h_eqv_x1_y s hs_meas).mpr h_y_in_s
        · intro h_eqv_x1_x
          -- calculation
          have h_eqv_y_x1 : eqv y x_1 := by
            -- Since eqv is symmetric, if eqv x_1 y holds, then eqv y x_1 must also hold.
            have h_symm : ∀ x y, eqv x y → eqv y x := by
              -- Since eqv is symmetric, if eqv x y holds, then eqv y x must also hold. This follows directly from the definition of eqv.
              intros x y h_eqv_xy
              intro s hs
              rw [h_eqv_xy s hs];
            exact h_symm _ _ h_eqv_x1_y
          -- calculation
          have h_trans : ∀ a b c, eqv a b → eqv b c → eqv a c := by
            intro a b c hab hbc s hs_meas
            constructor
            · intro ha_in
              exact (hbc s hs_meas).1 ((hab s hs_meas).1 ha_in)
            · intro hc_in
              exact (hab s hs_meas).2 ((hbc s hs_meas).2 hc_in)
          show_term grind

      · -- Show the reverse inclusion
        obtain ⟨y, hy⟩ := ht hx
        simp +zetaDelta at *;
        exact ⟨ y, ⟨ x, hx, by simpa using hy y ⟩, fun z => by simpa [ eq_comm ] using hy z ⟩;
    · -- Case when equivalence classes are finite
      exact Classical.not_not.mp h_eq_classes_infinite

  -- The subsets of equivalence classes are also finite
  have h_subsets_finite : Set.Finite {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }} := by
    exact Set.Finite.subset (Set.Finite.powerset h_eq_classes_finite) fun t ht => ht

  -- Therefore the σ-algebra (unions of subsets) is finite
  have h_measurable_finite : Set.Finite (Set.image (fun t : Set (Set α) => ⋃₀ t) {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }}) := by
    exact h_subsets_finite.image _

  -- This contradicts the assumption that the σ-algebra is infinite
  exact h_infinite (h_measurable_finite.subset fun s hs => by
    obtain ⟨t, ht, rfl⟩ := h_sigma_gen s |>.1 hs
    exact Set.mem_image_of_mem _ ht)

[Aaron Liu]

oh grind wraps its proofs in auxiliary lemmas

[metakuntyyy]

Yeah, I had this too, especially with expose_names. Can't you print the subproof that grind generates? It usually has a suffix _1_1 or something like that. If I understood @Kim Morrison you aren't supposed to fill in the terms generated from grind.

[Kevin Buzzard]

I know next to nothing about grind but certainly with aesop it was very helpful to run show_term on it because you might well discover that ext; simp_all or even rfl proved the result. Is the idea that this is highly unlikely to be the case with grind? Examples of tactics where I have never once found it useful to inspect the term they generate are ring and linarith.

[Nick_adfor]

metakuntyyy said:

Yeah, I had this too, especially with expose_names. Can't you print the subproof that grind generates? It usually has a suffix _1_1 or something like that. If I understood Kim Morrison you aren't supposed to fill in the terms generated from grind.

Yes, it gives not_exists_infinite_countable_sigma_algebra._proof_1_9

[Nick_adfor]

I may think that it is a problem that x✝ cannot be used in have

[Nick_adfor]

What is _proof_1_9?

[metakuntyyy]

You can inspect the proof with

#print not_exists_infinite_countable_sigma_algebra._proof_1_9

I think under certain circumstances proofs are no longer inlined but subproofs are created. Those are usually not exposable but they can be printed and checked. Tactics can generate subproofs which are part of the environment. You can also check that you can't declare
theorem not_exists_infinite_countable_sigma_algebra._proof_1_9 : True := sorryafter your proof, but you can do it before the proof.

[Nick_adfor]

#print cannot work. _proof_1_9 seems to be an implict one so it cannot be printed.

[metakuntyyy]

Works for me.

image.png

[Nick_adfor]

I may think that it is because that I print it in the wrong line.

[Nick_adfor]

I try to print in the line of have h_y_in_s : y ∈ s := by

[Ruben Van de Velde]

I understand that there will be better ways to inspect what grind does in the future, fwiw

[Nick_adfor]

Now I try to use grind?, and try to rw its generating theorem at something. But the "at something" is still hard to find.

import Mathlib
/--
There does not exist an infinite σ-algebra that contains only countably many members.

This theorem states that it is impossible to have a σ-algebra that is both infinite
and countable. The proof proceeds by contradiction, showing that any infinite σ-algebra
must contain at least continuum many sets.
-/
theorem not_exists_infinite_countable_sigma_algebra :
    ¬ ∃ (α : Type) (i : MeasurableSpace α),
      Set.Countable {s : Set α | @MeasurableSet α i s} ∧
      Set.Infinite {s : Set α | @MeasurableSet α i s} := by
  -- Assume by contradiction that such a σ-algebra exists
  by_contra h_contra
  obtain ⟨α, i, h_countable, h_infinite⟩ := h_contra

  -- Define an equivalence relation: x ~ y if they belong to the same measurable sets
  set eqv : α → α → Prop := fun x y => ∀ s : Set α, MeasurableSet s → (x ∈ s ↔ y ∈ s)

  -- Each equivalence class is measurable (can be expressed as countable intersections)
  have h_partition : ∀ x : α, MeasurableSet {y : α | eqv x y} := by
    intro x
    -- Express the equivalence class as an intersection over measurable sets containing x
    -- and complements of measurable sets not containing x
    have h_eqv_class : {y : α | eqv x y} = ⋂ s ∈ {s : Set α | MeasurableSet s ∧ x ∈ s}, s ∩ ⋂ s ∈ {s : Set α | MeasurableSet s ∧ x∉s}, sᶜ := by
      ext y; aesop (config := {warnOnNonterminal := false})
      specialize a sᶜ; aesop (config := {warnOnNonterminal := false})
    rw [h_eqv_class]
    -- The intersection is measurable since it's over countably many measurable sets
    refine' MeasurableSet.biInter _ _ <;> aesop (config := {warnOnNonterminal := false})
    exact h_countable.mono fun s hs => hs.1
    -- Countability of the indexing set for complements
    have h_countable_inter : Set.Countable {s : Set α | MeasurableSet s ∧ x∉s} := by
      exact h_countable.mono fun s hs => hs.1
    exact MeasurableSet.inter left (MeasurableSet.biInter h_countable_inter fun s hs => MeasurableSet.compl hs.1)

  -- The σ-algebra is generated by the equivalence classes
  have h_sigma_gen : ∀ s : Set α, MeasurableSet s ↔ ∃ t : Set (Set α), t ⊆ { {y : α | eqv x y} | x : α } ∧ s = ⋃₀ t := by
    aesop (config := {warnOnNonterminal := false})
    · -- Forward direction: every measurable set is a union of equivalence classes
      use { { y : α | eqv x y } | x ∈ s }
      aesop (config := {warnOnNonterminal := false})
    · -- Reverse direction: any union of equivalence classes is measurable
      have h_measurable_w : ∀ s ∈ w, MeasurableSet s := by
        intro s hs
        specialize left hs
        aesop (config := {warnOnNonterminal := false})
      -- Countability of the indexing set
      have h_countable_w : w.Countable := by
        exact h_countable.mono h_measurable_w
      exact MeasurableSet.sUnion h_countable_w h_measurable_w

  -- The set of equivalence classes must be finite
  have h_eq_classes_finite : Set.Finite { {y : α | eqv x y} | x : α } := by
    by_cases h_eq_classes_infinite : Set.Infinite { {y : α | eqv x y} | x : α }
    · -- If equivalence classes were infinite, the power set would be uncountable
      have h_power_set_uncountable : ¬Set.Countable (Set.powerset { {y : α | eqv x y} | x : α }) := by
        intro h_power_set_countable
        -- Show that the power set has cardinality at least continuum
        have h_power_set_card : Cardinal.mk (Set.powerset { {y : α | eqv x y} | x : α }) ≤ Cardinal.aleph0 := by
          exact Cardinal.mk_le_aleph0_iff.mpr h_power_set_countable.to_subtype
        simp [*] at *
        -- Cantor's theorem gives contradiction with countability
        have h_card_ge_aleph0 : Cardinal.mk { {y : α | eqv x y} | x : α } ≥ Cardinal.aleph0 := by
          exact Cardinal.aleph0_le_mk_iff.mpr (h_eq_classes_infinite.to_subtype)
        exact h_power_set_card.not_gt (lt_of_lt_of_le (Cardinal.cantor _) (Cardinal.power_le_power_left two_ne_zero h_card_ge_aleph0))
      -- But the power set injects into our σ-algebra, contradicting countability
      apply_mod_cast False.elim <| h_power_set_uncountable <| Set.Countable.mono _ <| h_countable.image _
      use fun s => { t | ∃ x ∈ s, { y | eqv x y } = t }
      intro t ht
      use ⋃₀ t
      simp_all [Set.ext_iff]
      refine' ⟨⟨t, ht, fun x => Iff.rfl⟩, fun x => ⟨fun hx => _, fun hx => _⟩⟩
      · -- Show x is in the appropriate equivalence class
        obtain ⟨y, ⟨z, hz, hyz⟩, hy⟩ := hx
        convert hz
        obtain ⟨x_1, hx_1⟩ : ∃ x_1 : α, z = {y | eqv x_1 y} := by
          obtain ⟨x_1, hx_1⟩ := ht hz
          exact ⟨x_1, by ext; simp [hx_1]⟩
        ext
        simp [hx_1]
        -- Calculation
        have h_eqv_x1_y : eqv x_1 y := by
          exact hx_1.subset hyz

        constructor
        · intro hx_mem s hs_meas
          constructor
          · intro hx1_in_s
            -- y in s
            have h_y_in_s : y ∈ s := by
              -- Since $x_1$ and $y$ are equivalent, by definition of $eqv$, we have $x_1 \in s \leftrightarrow y \in s$.
              have hy_in_s : x_1 ∈ s ↔ y ∈ s := by
                apply h_eqv_x1_y s hs_meas;
              -- Apply the equivalence from hy_in_s to hx1_in_s to conclude y is in s.
              apply hy_in_s.mp hx1_in_s
            -- Since eqv y x✝ holds, for any measurable set s, y ∈ s ↔ x✝ ∈ s. Given that y ∈ s, it follows that x✝ ∈ s.
            have h_eqv_y_x : ∀ s : Set α, MeasurableSet s → (y ∈ s ↔ ‹α› ∈ s) := by
              -- Since y and x✝ are in the same equivalence class under eqv, by definition of eqv, this equivalence holds for all measurable sets s.
              intros s hs_meas; exact (hy ‹_›).mpr hx_mem s hs_meas;
            exact h_eqv_y_x s hs_meas |>.1 h_y_in_s
          · intro hx_in_s
            -- y in s
            have h_y_in_s : y ∈ s := by
              have h_x1_in_s : x_1 ∈ s := by
                rw [Set.subset_def] at ht
                apply ?_
                have h_y_eq_xstar : ∀ (u : Set α), MeasurableSet u → (y ∈ u ↔ x_1 ∈ u) := by exact?
                have h_x1_iff_y : ∀ (u : Set α), MeasurableSet u → (x_1 ∈ u ↔ y ∈ u) := by exact?
                grind?
              have h_x1_iff_y : x_1 ∈ s ↔ y ∈ s := h_eqv_x1_y s hs_meas
              exact h_x1_iff_y.1 h_x1_in_s
            apply (h_eqv_x1_y s hs_meas).mpr h_y_in_s
        · intro h_eqv_x1_x
          -- calculation
          have h_eqv_y_x1 : eqv y x_1 := by
            -- Since eqv is symmetric, if eqv x_1 y holds, then eqv y x_1 must also hold.
            have h_symm : ∀ x y, eqv x y → eqv y x := by
              -- Since eqv is symmetric, if eqv x y holds, then eqv y x must also hold. This follows directly from the definition of eqv.
              intros x y h_eqv_xy
              intro s hs
              rw [h_eqv_xy s hs];
            exact h_symm _ _ h_eqv_x1_y
          -- calculation
          have h_trans : ∀ a b c, eqv a b → eqv b c → eqv a c := by
            intro a b c hab hbc s hs_meas
            constructor
            · intro ha_in
              exact (hbc s hs_meas).1 ((hab s hs_meas).1 ha_in)
            · intro hc_in
              exact (hab s hs_meas).2 ((hbc s hs_meas).2 hc_in)
          show_term grind

      · -- Show the reverse inclusion
        obtain ⟨y, hy⟩ := ht hx
        simp +zetaDelta at *;
        exact ⟨ y, ⟨ x, hx, by simpa using hy y ⟩, fun z => by simpa [ eq_comm ] using hy z ⟩;
    · -- Case when equivalence classes are finite
      exact Classical.not_not.mp h_eq_classes_infinite

  -- The subsets of equivalence classes are also finite
  have h_subsets_finite : Set.Finite {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }} := by
    exact Set.Finite.subset (Set.Finite.powerset h_eq_classes_finite) fun t ht => ht

  -- Therefore the σ-algebra (unions of subsets) is finite
  have h_measurable_finite : Set.Finite (Set.image (fun t : Set (Set α) => ⋃₀ t) {t : Set (Set α) | t ⊆ { {y : α | eqv x y} | x : α }}) := by
    exact h_subsets_finite.image _

  -- This contradicts the assumption that the σ-algebra is infinite
  exact h_infinite (h_measurable_finite.subset fun s hs => by
    obtain ⟨t, ht, rfl⟩ := h_sigma_gen s |>.1 hs
    exact Set.mem_image_of_mem _ ht)

  #print not_exists_infinite_countable_sigma_algebra._proof_1_9

[Nick_adfor]

I'm really disappointed for the designer of exact?. One can easily check what exact?shows rabbish.

[Ruben Van de Velde]

That's not really a kind way of interacting with people

[Nick_adfor]

I really should find the designer and ask for more details. Whoever hung the bell on the tiger's neck must be able to untie it : )

Ruben Van de Velde said:

That's not really a kind way of interacting with people

[Aaron Liu]

I want to ask, what are you unsatisfied with specifically? Which part could be better? How can we make it better?

[Nick_adfor]

Well, it is that grind and grind only show everything in an implict way. I may want an explicit one, just like rw and simp and have, which makes everything clear

[metakuntyyy]

I think he wants to use terms that grind or exact? generate to replace the tactic invocations and is not satisfied that there are no term mode invocations of that. The tactics succeed because I assume grind generates subproofs. So when he uses show_term or exact? the proof works but it exposes those hidden subproofs, and they can't be used because of hygiene issues, in particular if he's in a different local context.

I had similar issues pop up, but I don't try aggressively replace grind. However exact? once referred to a proof that grind created and it was not really usable.

[Nick_adfor]

I may guess grind only shows some theorem, maybe these theorems can be used in rw some have. But it is just my guess. I really don't know how it works.

[Nick_adfor]

grind only [= Set.setOf_true, usr Set.mem_setOf_eq, = Set.setOf_false] might be three theorems about {x | True} → univ, {x | P x} ↔ P x, {x | False} → ∅. But I cannot find in what set these theorems are used.

[metakuntyyy]

Yeah, grind is really smart and really well designed. It's my favourite tactic, by far. it's designed to solve goals in a way that other tactics can't really do and using terms from grind is not really designed.

[metakuntyyy]

I think grind is only showing grind set theorems. Proofs generated by grind internals are not shown.

[metakuntyyy]

I just checked and replaced all grind with grind? in my project. Most of those were grind only. So grind itself uses a decision procedure to generate those proofs.

[Nick_adfor]

So how grind does on= Set.setOf_true, usr Set.mem_setOf_eq, = Set.setOf_false?

[metakuntyyy]

I don't precisely know which theorem you've used it on. But in general grind will add those facts to the tableau for usage in term generation. Think of it as a simp that doesn't rewrite until it's found a proof. It can also use grind internal lemmas for decision procedures not exposed to the user. I think it's also able to use hypothesis in your context but don't quote me on that. In general I think grind is going to get more powerful as time goes on and as more features are added. If you know how to prove the have statement that you want without grind and make it explicit you can do so. But it goes against the spirit of proof automation.

[Nick_adfor]

Spirit of Proof Automation : )

[Robin Arnez]

There is some stuff in the works to make grind emit "grind tactic" sequences. You should be able to see that with grind => finish? on latest mathlib although it's a bit hard to understand each step.

[Nick_adfor]

Okay, now it is

            -- y in s
            have h_y_in_s : y ∈ s := by
              grind =>
                instantiate only [#ca88]
                instantiate only [#6671]

[Nick_adfor]

What's the difference? it show me some inner things than before.

            -- y in s
            have h_y_in_s : y ∈ s := by
              grind

[Nick_adfor]

Nick_adfor said:

I'm really disappointed for the designer of exact?. One can easily check what exact?shows rabbish.

A lot of guys like butterfly here, very thanks for the butterfly : )

[Chris Henson]

Please see #butterfly for its meaning here

[Nick_adfor]

Nick_adfor said:

I may think that it is a problem that x✝ cannot be used in have

The root of all evil is ext. ext generates an implicit variable x✝, and implicit variables like x✝ cannot be included in the statement — expressions such as eqv y x✝ are invalid. Therefore, it should be replaced with an explicit variableapply Set.ext; intro w

[Nick_adfor]

grind is such a tactic that seems to be able to perform certain operations on implicit variables internally.
However, grind? generates some operations on sets

Try this:
  [apply] grind only [= Set.subset_def, = Set.setOf_true, usr Set.mem_setOf_eq, = Set.setOf_false]

which I don’t think are necessary when replacing automatic operations with manual ones.
It’s possible that grind? is not as precise as simp?

[Nick_adfor]

I quit my trial because of all these internal issues. Sometimes I get carried away using simp? to generate a simp only, only to run into problems—like in different versions, theorems get new namespaces or their names change. This past weekend, I was obsessively trying to replace grind with more basic tactics, but I got stuck on an implicit x✝. These meaningless entanglements don’t provide any real benefit to the code—maybe they slightly improve runtime by reducing automatic searches? Or perhaps they increase readability by forcing everything to be explicit? I honestly don’t know

[Ruben Van de Velde]

Nick_adfor said:

Nick_adfor said:

I may think that it is a problem that x✝ cannot be used in have

The root of all evil is ext. ext generates an implicit variable x✝, and implicit variables like x✝ cannot be included in the statement — expressions such as eqv y x✝ are invalid. Therefore, it should be replaced with an explicit variable: apply Set.ext; intro w(Line 81)

Note that ext y works to create a named variable

[Nick_adfor]

Ruben Van de Velde said:

Nick_adfor said:

Nick_adfor said:

I may think that it is a problem that x✝ cannot be used in have

The root of all evil is ext. ext generates an implicit variable x✝, and implicit variables like x✝ cannot be included in the statement — expressions such as eqv y x✝ are invalid. Therefore, it should be replaced with an explicit variable: apply Set.ext; intro w(Line 81)

Note that ext y works to create a named variable

Ok, its another way to replace apply Set.ext; intro w

[Nick_adfor]

Zulip show a strange thing. Sometimes all the backticks fail to show in the correct place.

[Nick_adfor]

simp, rw it shows correctly

[Nick_adfor]

But this part shows wrongly.

[Nick_adfor]

image.png

[Aaron Liu]

Nick_adfor said:

These meaningless entanglements don’t provide any real benefit to the code—maybe they slightly improve runtime by reducing automatic searches? Or perhaps they increase readability by forcing everything to be explicit? I honestly don’t know

They increase maintainability by forcing you to use your own names instead of the fragile autogenerated names which could change whenever

[Kim Morrison]

Nick_adfor said:

I really should find the designer and ask for more details. Whoever hung the bell on the tiger's neck must be able to untie it : )

Ruben Van de Velde said:

That's not really a kind way of interacting with people

@Nick_adfor I wrote exact?. Carefully written, well-motivated, and easy to review PRs to the lean4 repository improving it are much appreciated.

[Nick_adfor]

Kim Morrison said:

Nick_adfor said:

I really should find the designer and ask for more details. Whoever hung the bell on the tiger's neck must be able to untie it : )

Ruben Van de Velde said:

That's not really a kind way of interacting with people

Nick_adfor I wrote exact?. Carefully written, well-motivated, and easy to review PRs to the lean4 repository improving it are much appreciated.

Ok, Kim, it might be my careless checking.

[Nick_adfor]

/--
Implementation of the `exact?` tactic.

* `ref` contains the input syntax and is used for locations in error reporting.
* `required` contains an optional list of terms that should be used in closing the goal.
* `requireClose` indicates if the goal must be closed.
  It is `true` for `exact?` and `false` for `apply?`.
-/

https://github.com/leanprover/lean4/blob/744f98064b056ee27fc8c97f524797c8cc96f436/src/Lean/Elab/Tactic/LibrarySearch.lean#L20-L55

[Nick_adfor]

But I may think this doc cannot explain why ...but the corresponding tactic failed:...exact? happens. I may use my experience to understand it as an 'implict variable' problem or a 'renamed variable' problem.

[Nick_adfor]

Just like _proof_1_9, suffix _1_1 etc. I may think these theorem are 'implict variables' as I cannot extract them in the proof, only computer itself can check it.

[Kim Morrison]

No. grind produces an auxiliary declaration containing the proof term it generates. So show_term fails (this is by-design, and not a bug), because if you replace the grind call with the name of that auxiliary definition, the grind hasn't been run so that auxiliary definition doesn't exist.

You can still see exactly what term grind produced: after the entire declaration containing show_term grind, write #print not_exists_infinite_countable_sigma_algebra._proof_1_10 and you will see in the info view the giant term that grind has produced.

grind is not intended to produce proofs that can be readily replaced with term mode proofs. Instead you can use grind => finish? to produce a "grind script" (in v4.26.0 these will be printed merely by writing grind?), which you can paste in to replace the grind call, and allows you to modify the actions grind takes (but still not extract a small proof term).

If you are interested in tactics that produce concise proof terms, I encourage looking at canonical.

[Nick_adfor]

Kim Morrison said:

No. grind produces an auxiliary declaration containing the proof term it generates. So show_term fails (this is by-design, and not a bug), because if you replace the grind call with the name of that auxiliary definition, the grind hasn't been run so that auxiliary definition doesn't exist.

You can still see exactly what term grind produced: after the entire declaration containing show_term grind, write #print not_exists_infinite_countable_sigma_algebra._proof_1_10 and you will see in the info view the giant term that grind has produced

grind is not intended to produce proofs that can be readily replaced with term mode proofs. Instead you can use grind => finish? to produce a "grind script" (in v4.26.0 these will be printed merely by writing grind?), which you can paste in to replace the grind call, and allows you to modify the actions grind takes (but still not extract a small proof term)

If you are interested in tactics that produce concise proof terms, I encourage looking at canonical

Okay, https://github.com/chasenorman/CanonicalLean & https://arxiv.org/abs/2504.06239