Getting pretty printer to display wildcards

Stream: new members

[Connor Gordon]

I'm currently trying to prove a lemma about a recursively-defined function, and I have reduced the goal to

⊢ ⟨_.some, _⟩ = ⟨_.some, _⟩

Both sides of these really should be equal by definition, but clearly something has gone wrong because refl is not working. Is there a way to make Lean display the contents of the wildcards (in some readable fashion; I tried set_option pp.all and it replaced them with about 100 lines of stuff so ideally I don't have to do that) so I can see what's going on?

If you would like more information I can make a minimal working example as to the specifics.

[Kevin Buzzard]

Is this Lean 3? You could see if congr' makes any progress.

[Eric Wieser]

Those _s are proof of something, and the 100 lines of stuff is the proof that you used for them

[Eric Wieser]

A #mwe showing that goals that print in a way that looks like rfl can be false:

-- set_option pp.proofs true
example : classical.some ⟨2, rfl⟩ = classical.some ⟨1, rfl⟩ :=
begin
  sorry -- this is false
end

[Eric Wieser]

set_option pp.implicit true is probably helpful for your example

[Connor Gordon]

This is Lean 3, and congr' is not making any progress.
set_option pp.implicit true displays a bit more information, but still wildcards out the most important part.
As for proofs of this form potentially being false, I definitely can see how that may happen, although it doesn't seem like it should be the case here. I attached a minimal working example; do you have any idea why this might not be working?

import set_theory.ordinal.topology
import set_theory.cardinal.cofinality

universe u

variables (S : set ordinal.{u}) (κ : ordinal.{u}) (α : ordinal.{u})

def set.is_subset_of : Prop := S ⊆ set.Iio κ
def set.is_closed : Prop := ∀ A ⊆ S, A.nonempty → Sup A < κ → Sup A ∈ S
def set.is_unbounded : Prop := ∀ β < κ, ∃ γ ∈ S, β < γ
def set.is_club : Prop := S.is_subset_of κ ∧ S.is_closed κ ∧ S.is_unbounded κ

-- Useful intermediate sequence
def D_seq := λ (f : ordinal.{u} → set ordinal.{u}) β, ⋂ (α < β), f α

-- Existence lemma for unbounded sequence
lemma tail_D_seq_nonempty {κ β γ : ordinal.{u}}
(f : ordinal.{u} → set ordinal.{u}) (hclub : ∀ α, α < κ → set.is_club (f α) κ)
(βltκ : β < κ) (γltκ : γ < κ) (κreg : κ.cof = κ.card)
(κunctbl : κ.card > cardinal.aleph_0) :
  ∃ δ : ordinal.{u}, δ ∈ (D_seq f γ) ∧ δ > β ∧ δ < κ :=
begin
  sorry, -- probably not relevant; omitted for brevity
end

-- Construct the sequence used for proof of unboundedness
noncomputable def unbdd_seq {κ β : ordinal.{u}}
(f : ordinal.{u} → set ordinal.{u}) (hclub : ∀ α, α < κ → set.is_club (f α) κ)
(βltκ : β < κ) (κreg : κ.cof = κ.card) (κunctbl : κ.card > cardinal.aleph_0) :
ℕ → {x : ordinal.{u} // x < κ}
| 0 := ⟨β, βltκ⟩
| (n+1) := let existence := tail_D_seq_nonempty f hclub (unbdd_seq n).prop
(unbdd_seq n).prop κreg κunctbl in
⟨existence.some , existence.some_spec.right.right⟩

-- Convenience lemma to actually use the definition of the sequence
lemma unbdd_seq_aux {κ β : ordinal.{u}} (n : ℕ)
(f : ordinal.{u} → set ordinal.{u}) (hclub : ∀ α, α < κ → set.is_club (f α) κ)
(βltκ : β < κ) (κreg : κ.cof = κ.card) (κunctbl : κ.card > cardinal.aleph_0) :
unbdd_seq f hclub βltκ κreg κunctbl (n+1) =
let existence := tail_D_seq_nonempty f hclub
(unbdd_seq f hclub βltκ κreg κunctbl n).prop
(unbdd_seq f hclub βltκ κreg κunctbl n).prop κreg κunctbl in
⟨existence.some , existence.some_spec.right.right⟩ :=
begin
  dsimp [unbdd_seq],
  sorry,
end

[Kevin Buzzard]

begin
  dsimp [unbdd_seq],
  ext,
  unfold_coes,
end

is a proof, for what it's worth.

[Kyle Miller]

set_option pp.proofs true is how you can get it to pretty print the proofs

[Connor Gordon]

@Kevin Buzzard , your proof works in mwe, but bizarrely if I put it into my full project, it stops working with the error message

unfold tactic failed, lift does not have equational lemmas nor is a projection
state:
κ β : ordinal,
n : ℕ,
f : ordinal → set ordinal,
hclub : ∀ (α : ordinal), α < κ → (f α).is_club κ,
βltκ : β < κ,
κreg : κ.cof = κ.card,
κunctbl : κ.card > cardinal.aleph_0
⊢ ↑⟨_.some, _⟩ = ↑⟨_.some, _⟩

Any idea what might cause this? It feels like the additional information for how other things are implemented shouldn't affect things on this level, but evidently it does somehow.

[Kyle Miller]

Something that's really strange is that for whatever reason you can't rewrite with docs#subtype.coe_mk

[Kevin Buzzard]

yeah my proof is pretty weird; it's vanishingly rare for unfold_coes to finish a proof. @Kyle Miller note that ext, dsimp will remove one \u but not the other one ?!

[Kyle Miller]

Just found another proof that works:

begin
  simp only [unbdd_seq, gt_iff_lt],
  congr',
end

[Kyle Miller]

That docs#gt_iff_lt is odd -- I tried switching every > in the MWE to <, but then the simp fails. Maybe I missed something or flipped them wrong...

[Kyle Miller]

@Kevin Buzzard Yeah, I even tried refine eq.trans (subtype.coe_mk _ _) _, to get rid of that \u, but something about unification is getting confused here

[Connor Gordon]

@Kyle Miller , your proof does work in my main project, so thank you so much for the help. As for all of the other weirdness going on, I have absolutely no idea.