Using structure fields as they're defined

Stream: general

[Eric Wieser]

Is it possible to do something like this?

example : my_structure :=
{ f := sorry,
  prop_a := sorry,
  prop_b := begin
     rw some_stuff,
     rw prop_a, -- I want to reuse my proof of a
     sorry
  end }

Obviously right now prop_a doesn't resolve. Currently, my options look to be:

• Use a private definition to provide my definition of f and proof ofprop_a first, and then put it in the struct later
• Do something horrible with let in

[Johan Commelin]

I guess that lean doesn't want to be bothered with figuring out whether proofs refer to each other in a cyclic manner...

[Eric Wieser]

I'd be happy with it requiring source order

[Reid Barton]

I don't think that really makes sense unfortunately.

[Eric Wieser]

Or in most cases, probably even struct field order

[Reid Barton]

Like, what term do you expect it to produce

[Reid Barton]

It has to produce something you could write by hand anyways

[Eric Wieser]

I guess I'd want it to just inline the term it already produced

[Eric Wieser]

Is using private the right thing to do here?

[Johan Commelin]

I think I would go for that option, yes.

[Johan Commelin]

The let in is not really horrible, but I understand why you call it horrible :rolling_eyes: :rofl: :oops: :shrug:

[Reid Barton]

Another possibility is

example : my_structure :=
begin
  refine { f := [...], .. },
  all_goals { have prop_a : [...] := [...] },
  { exact prop_a },
  { rw [some_stuff, prop_a], [...] }
end

[Reid Barton]

let in is bad, but I think have is less bad, so that's another possible option

[Alex J. Best]

I guess the have is weird if the f is something complicated that appears in the type of prop_a

structure my_structure :=
(f : ℕ → ℕ)
(prop_a : f 0 = 0)
(prop_b : f 0 + 0 = 0)
example : my_structure := have prop_a : id 0 = 0 := rfl,
{ f := id,
  prop_a := prop_a,
  prop_b := begin
     rw prop_a, -- I want to reuse my proof of a
  end }

[Reid Barton]

The have is still probably worse than just writing a separate lemma

[Eric Wieser]

Do private lemmas appear in the online docs?

[Kevin Lacker]

if you name it like blah_blah_aux then people will know not to use it

[Eric Wieser]

Right, but my hope was the private keyword would do something sensible

[Reid Barton]

Normally private is not recommended but if it's literally a field of a structure that you provide anyways, I guess it's okay

[Kevin Lacker]

o rly. why isn't private recommended?

[Johan Commelin]

Because 95% of the time, it turns out that someone else has a use for your lemma

[Johan Commelin]

So they will be happy if they can use it outside the file where it's defined.

[Kevin Lacker]

seems strange to me based on the analogy to other programming, but I guess there is basically never a reason to refactor a lean lemma to "change its behavior", because it has no behavior, so there isn't really any need to say like, don't depend on this because its behavior may change

[Gabriel Ebner]

It's not impossible, but you'll need to modify the C++ code for this.

[Reid Barton]

Kevin Lacker said:

seems strange to me based on the analogy to other programming

I agree there could theoretically be a world in which a module has a public API which is stable and an implementation which is not, but mathlib is nowhere near that point and it seems difficult in practice because Lean really likes to unfold definitions.

[Johan Commelin]

I've recently marked some things private that were used in setting up a bundled homomorphism. In that case, I think it's justified, because everything this scaffolding achieves can be done using the API of bundled morphisms as well, once the bundled hom is available.

[Eric Wieser]

Right, the use case you describe is exactly mine - all the lemmas are going to end up bundled in a larger structure, exposing them under two different names is just confusing

[Mario Carneiro]

I would recommend something like this:

structure my_structure :=
(f : ℕ → ℕ)
(prop_a : f 0 = 0)
(prop_b : f 0 + 0 = 0)
example : my_structure :=
let f : ℕ → ℕ := id in
have prop_a : f 0 = 0 := rfl,
{ f := f,
  prop_a := prop_a,
  prop_b := begin
     rw prop_a, -- I want to reuse my proof of a
  end }

[Mario Carneiro]

Kevin Lacker said:

o rly. why isn't private recommended?

Johan Commelin said:

Because 95% of the time, it turns out that someone else has a use for your lemma

Exhibit A, where Kevin Lacker uses a "private" lemma from norm_num

[Mario Carneiro]

Kevin Lacker said:

seems strange to me based on the analogy to other programming, but I guess there is basically never a reason to refactor a lean lemma to "change its behavior", because it has no behavior, so there isn't really any need to say like, don't depend on this because its behavior may change

Actually this is a thing. Definitions do change their behavior, either when the definition changes to something defeq, or something which is equal but not defeq, or something which is really different but only differs in "out of bounds" areas that most theorems don't care about, or type of an intermediate definition changes and the API layer needs to be reworked but theorems above that don't have to change.

[Mario Carneiro]

We usually call it "refactoring"

[Kevin Lacker]

Mario Carneiro said:

Kevin Lacker said:

o rly. why isn't private recommended?

Johan Commelin said:

Because 95% of the time, it turns out that someone else has a use for your lemma

Exhibit A, where Kevin Lacker uses a "private" lemma from norm_num

hey, i didn't want to use a private lemma from norm_num, some reviewer suggested it because it made the code 1 token shorter

[Junyan Xu]

Aren't structures implemented as sigma types? The fields should have a linear order on them so no cyclic reference is possible. In fact, when defining the type of a structure it is allowed to use previously defined fields, and it's odd to me that you can't do so when exhibiting a term of the type.

[Mario Carneiro]

It's not clear to me what you are responding to or what you mean. Do you have an example? Structures are just an extension of sigma types, cyclic reference is impossible, and fields can have types that refer to previous fields

[Junyan Xu]

This was the "cyclic" concern:
Johan Commelin said:

I guess that lean doesn't want to be bothered with figuring out whether proofs refer to each other in a cyclic manner...

[Junyan Xu]

I'm just complaining as I find it inconvenient.

[Junyan Xu]

The specific situation is that I want to use fac' when proving uniq' in is_limit: https://leanprover-community.github.io/mathlib_docs/category_theory/limits/is_limit.html#category_theory.limits.is_limit

[Scott Morrison]

Just write a preliminary lemma with the fact you want to use twice. (Or a let X := Y in ... statement.)

[Junyan Xu]

when proving fac' I can just intro/lambda without specifying the types, but when writing a lemma I have to write the types, and can't just write the term. Just seems unnecessarily verbose to me.

[Scott Morrison]

Have you seen tactic#extract_goal?

[Junyan Xu]

I've seen that but my issue isn't with difficulty writing down the lemma but the space the lemma would occupy. My reaction to inability to refer to the prior field is not to replicate the proof or extract a lemma, but to find an alternative proof. I've tried tactic#abstract before but nothing happened. Maybe time to give it a try again.
(Maybe nothing appears in the local context but I can use it as a global definition/theorem?)

[Mario Carneiro]

There is a straightforward syntactic modification that will make the proof available later. You don't have to write the type

[Junyan Xu]

Mario Carneiro said:

There is a straightforward syntactic modification that will make the proof available later. You don't have to write the type

Not sure if this the way you're talking about, but I managed to make tactic#abstract work! If the theorem you're proving is named foo, you can abstract goal { /- proof of goal -/ } in tactic mode to extract the first goal to a lemma, and then you can refer to the lemma using foo.goal either within the same proof, or later in the same file. The prefix foo. is what I was missing, and isn't mentioned in the documentation.

[Mario Carneiro]

I was talking about using let, but that works too