Zulip Chat Archive

Stream: new members

Topic: Lean displaying _ in local context

Keefer Rowan (May 20 2020 at 22:08):

I can't come up with a simpler example of this phenomenon, so I can only give you a slightly convoluted one. A complicated function I defined has one of its equations printed by Lean (by the #print command) as

set.subset_of_sts_all_less_than_finite_func.equations._eqn_2 :  {n : } (m : ) (A : set (all_less_than n).set_to_subtype)
(h : A.subset_of_sts_all_less_than_finite_size_of = m.succ) (x_val : (all_less_than n).set_to_subtype)
(x_property : x_val  A),
  subset_of_sts_all_less_than_finite_func h x_val, x_property =
    dite (x_val = classical.some _) (λ (hyp : x_val = classical.some _), m, _⟩)
      (λ (hyp : ¬x_val = classical.some _), (subset_of_sts_all_less_than_finite_func _ x_val, _⟩).val, _⟩)

Note the _. These terms are fairly complicated and it doesn't seem like they can be inferred from the local context, so I'm confused as to why Lean represents them with _. Is this a a printing option?

My problem is that these _'s propagate when trying to prove stuff about my definition, making it hard to complete proofs as an important part of the definition is just given as _.

Keefer Rowan (May 20 2020 at 22:13):

As an example of the problem I'm having, I have this in my local context,

h : m, _⟩ = (subset_of_sts_all_less_than_finite_func _ y_val, _⟩).val, _⟩

but rw subtype.mk.inj_eq at h, fails as rewrite tactic failed, did not find instance of the pattern in the target expression ⟨?m_3, ?m_4⟩ = ⟨?m_5, ?m_6⟩, which doesn't make any sense, but I'm assuming it has something to do with the _'s.

Anas Himmi (May 20 2020 at 22:14):

try putting

set_option pp.implicit  true

it may show you what's wrong

Alex J. Best (May 20 2020 at 22:14):

It's because they are proofs (so terms whose type is a Prop) so any two proofs of the same prop are equal, hence sometimes not that relevant to see them all the time, this can be controlled with set_option pp.proofs true

Alex J. Best (May 20 2020 at 22:14):

set_option pp.proofs true
noncomputable theory
lemma t : classical.some (1, dec_trivial:  p, 0 < p) = 2 := sorry
#print t

Keefer Rowan (May 20 2020 at 22:20):

Any idea why rw subtype.mk.inj_eq at h isn't working?

Alex J. Best (May 20 2020 at 22:24):

Not without a #mwe ;)

Last updated: Dec 20 2023 at 11:08 UTC