Zulip Chat Archive

Stream: new members

Topic: Implicitly bringing structure field props into context

Sam (Nov 16 2021 at 22:07):

I'm playing around with the pattern of defining a structure that associates a value with some propositions about the value.

Trivial example:

structure list3 := (val : list ) (len : val.length = 3)

I'm finding that one disadvantage of this approach is that the tactics don't seem to treat the val field as a local hypothesis.

This works fine - library_search finds the len prop:

example (l3 : list3) : (l3.val.length = 3) := by library_search

However this does not:

example (l3 : list3) : (l3.val.length <= 3) := by library_search

But I can persuade it to work if I explicitly bring len into the context:

example (l3 : list3) : (l3.val.length <= 3) := by { have l3.len := l3.len, library_search, }

Is there anything that I can do to make l3.len implicitly in context whenever l3 is? I want the behaviour of the last example with the have, but without having to type the have.

On a slightly more general note, is this pattern common and considered good? Or are there reasons that I shouldn't be trying to group values and their propositions like this?

Kyle Miller (Nov 16 2021 at 22:10):

One way, though somewhat explicit, is cases l3. This essentially brings all the fields into the context.

Kyle Miller (Nov 16 2021 at 22:14):

If you have just a single proposition, it's more common to use subtype: {val : list nat // val.length = 3}. Sometimes you might write it as a set and use the coercion to subtype.

But using custom structures to "bundle" data with properties is fairly common, too. I think whether it's good comes down to seeing how you tend to use it -- do they make the interface to your definitions and theorems cleaner?

Sam (Nov 16 2021 at 22:15):

Actually cases is explicitly not what I want, because I want to keep l3 intact. cases replaces l3 with its constituent parts, but I want to leave it as it is and augment the context with the len prop.

Sam (Nov 16 2021 at 22:16):

I have more than one prop, but I could AND them together I suppose. What advantages does subtype give here?

Kyle Miller (Nov 16 2021 at 22:18):

The advantage of a subtype is that there's a bunch of pre-written lemmas to help you out (like you get that list3.val is injective). It's a tradeoff, since then you'd have to /\ everything together, and that's not very nice.

Sam (Nov 16 2021 at 22:18):

I think the bundle will be a cleaner interface once I've built up all of the relevant lemmas on the bundle structure, but I'm finding declaring those lemmas to be a bit tricky for reasons like this.

Kyle Miller (Nov 16 2021 at 22:18):

Do you have an example where you need l3 to remain intact? There are some cases I can think of, but I'm wondering what your own constraint is here.

Kyle Miller (Nov 16 2021 at 22:20):

(Also, I'm finding have l3.len := l3.len to be odd -- it seems like you're creating a new name that shadows l3.len, right? Would have l3_len := l3.len be the same? Without having tested it, it seems like using l3.len like this tricks library_search into printing out that it's using l3.len.)

Sam (Nov 16 2021 at 22:22):

I'm building up a library of functions and lemmas that operate on list3s. (It's not actually list3, that's a simplified example.) So I'll be using values of that type, so I want to keep it around.

Sam (Nov 16 2021 at 22:22):

Yes l3_len works the same. As far as I can tell I'm just shadowing it.

Sam (Nov 16 2021 at 22:23):

example (l3 : list3) : (l3.val.length <= 3) := by { have l3_len := l3.len, library_search, }

library_search is giving me exact (eq.symm l3_len).ge

Sam (Nov 16 2021 at 22:26):

Which of course I can manually simplify to exact (eq.symm l3.len).ge. But it would be cool if it just got that without me doing any work.

Kyle Miller (Nov 16 2021 at 22:27):

Anyway, I think the short answer is "no, there's not something that automatically includes fields of a structure into the context". You could write a tactic to do this if you wanted, but you'd have to call it.

You could also modify library_search to walk through things in your context and add Prop fields to its list of assumptions.

Yaël Dillies (Nov 16 2021 at 22:27):

Or even l3.len.le

Sam (Nov 16 2021 at 22:30):

Modifying library_search to do it is intriguing, but I expect that's an unreasonable amount of work, isn't it?

Sam (Nov 16 2021 at 22:33):

Although actually, this is about more than library_search. That was just the easy example. I've observed similar behaviour with things like simp, where using have to bring field props into context is required. What I'm actually looking for is a way to do this that operates irrespective of tactic.

Sam (Nov 16 2021 at 22:35):

Oh yeah @Yaël Dillies , good point. I guess library_search isn't even giving me the best way here.

Kyle Miller (Nov 16 2021 at 22:39):

You could make a variant of cases that introduces an x with h : x = l3, does cases x, uses h to create rewrites for fields of l3, then rewrites the fields that cases x created with it.

In practice, I find I just add things I think I might need when I'm trying to find things when writing proofs. Like library_search [l3.len] should probably work.

Sam (Nov 16 2021 at 22:42):

Yeah, I think just writing the slightly over explicit code is the way to go, rather than trying anything too complicated like making custom tactics. I think the have shadowing trick actually works quite nicely, it's just a bit verbose.

Sam (Nov 16 2021 at 22:43):

Do you think it would make sense to add a feature like this into the language, though? Perhaps some attribute that can be applied to structures to specify that certain fields are implicitly in the context?

Eric Wieser (Nov 16 2021 at 22:46):

What exactly is the problem you're trying to solve? Is it "I want to be reminded of this in the goal view", and so just a user experience thing? Or is it "library_search can't find my proof unless I add a have"?

Kyle Miller (Nov 16 2021 at 22:46):

It seems that if this is something you need (and not just for library_search and simp convenience) then it suggests that it'd be better to unbundle the structure.

(I checked: library_search [l3.len] does work.)

Kyle Miller (Nov 16 2021 at 22:48):

I guess there's also things that operate using assumption, which I think simp does when trying to fill in hypotheses to simp lemmas.

Sam (Nov 16 2021 at 22:48):

@Eric Wieser It's "tactics generally can't find my proof unless I add a have". It's convenient with things like simp? * too. And presumably other tactics as well, but I've only actually played with simple examples so far.

Kevin Buzzard (Nov 16 2021 at 22:49):

Different tactics look at different things, but no tactic is going to start fishing fields out of a structure apart from tactics like tidy which is a finishing tactic which will take your structure apart mercilessly.

Scott Morrison (Nov 16 2021 at 22:50):

Actually, fishing fields out of structures would be an excellent additional to library_search, and completely doable.

Scott Morrison (Nov 16 2021 at 22:50):

library_search hands off to solve_by_elim after it has successfully applied a library lemma, and it should be possible to tell solve_by_elim that it is allowed to use projections of local hypotheses.

Reid Barton (Nov 16 2021 at 22:51):

I was going to mention docs#tactic.auto_cases (which is used by tidy) but (1) it doesn't know about your custom structure (2) it uses cases (3) it's apparently not an interactive tactic

Eric Wieser (Nov 16 2021 at 22:51):

I'm not sure whether simp * or linarith should pull fields out of structures, but library_search certainly should

Scott Morrison (Nov 16 2021 at 22:51):

There's also case_bash somewhere.

Reid Barton (Nov 16 2021 at 22:51):

Ah, I didn't know about that one.

Scott Morrison (Nov 16 2021 at 22:51):

auto_cases is extremely lame. It was amongst the first tactics I ever wrote, and should be redone.

Sam (Nov 16 2021 at 22:53):

That sounds reasonable @Kevin Buzzard, but I'm actually not imagining this as being a feature of tactics themselves. In my imagination, it's a feature of the structure that whenever it exists in the context, it automatically adds its own props into the context at the top level.

I'm very new to lean though, so I don't know if that makes sense when you get to the technical details. I was hoping that there was just some attribute I could throw on the structure or something like that.

Sam (Nov 16 2021 at 22:54):

Improving library_search to do this sounds cool, but that was really only the simple case I was using as an example.

Kevin Buzzard (Nov 16 2021 at 22:54):

I really don't want add_assoc, add_comm, add_zero, zero_add, add_left_neg... all being thrown into my local context every time I make something an additive abelian group.

Kevin Buzzard (Nov 16 2021 at 22:55):

Aah, but you only want it for certain structures I guess.

Sam (Nov 16 2021 at 22:55):

Certain structures, and even only certain fields of certain structures.

Kyle Miller (Nov 16 2021 at 22:55):

@Scott Morrison I was imagining modifying docs#tactic.solve_by_elim.mk_assumption_set, which is called once at the beginning of library_search, and it could add Prop-fields of non-excluded local hypotheses.

Reid Barton (Nov 16 2021 at 22:58):

There is some danger of infinite regress since the field could be another structure of the same type.

Reid Barton (Nov 16 2021 at 22:58):

Er wait maybe it can't be for a structure

Scott Morrison (Nov 16 2021 at 23:02):

Sounds good. Behind an additional flag, of course. I'd guess that just doing a single pass over the hypotheses is good enough.

Sam (Nov 16 2021 at 23:04):

I assume anything that works for structures would/should also work for subtypes, right? This doesn't work yet.

example (l3: {val : list nat // val.length = 3}) : (l3.val.length = 3) := by library_search,

Eric Wieser (Nov 16 2021 at 23:04):

src#subtype shows you that it's just another structure

Sam (Nov 16 2021 at 23:05):

Right, yeah good.

Kevin Buzzard (Nov 16 2021 at 23:05):

Presumably library_search is finding the function which takes a structure and spits out the field.

Sam (Nov 16 2021 at 23:06):

I'm not sure if I'm misunderstanding you Kevin, but just to be clear, that snipped I just posted doesn't work currently.

Alex J. Best (Nov 16 2021 at 23:09):

Here's a silly prototype:

import tactic

structure a :=
(b : )
(h : 1 < b)
  -- tactic.get_constructors_for
  -- #check tactic.get_decls_from

open tactic expr
meta def add_structure_hyps : tactic unit :=
  l  tactic.expanded_field_list `a,
  l.mfoldl (λ _ b, do
    -- trace b,
    c  mk_const $ name.append b.1 b.2,
    l  get_local `c,
    let d := expr.mk_app c [l],
    ty  infer_type d,
    i  is_prop ty,
    guardb i >> note `this ty d >> skip <|> skip,
    skip) ()
  -- l.mfoldl (λ _ b, do

lemma oof (c : a) : 1 < c.b + 1 :=
  -- have := a.h c,

Alex J. Best (Nov 16 2021 at 23:09):

Is this what you are thinking?

Alex J. Best (Nov 16 2021 at 23:10):

Currently it is silly and names everything this and hardcodes the name c, but you get the idea I hope

Sam (Nov 16 2021 at 23:13):

That's pretty cool @Alex J. Best!

Sam (Nov 16 2021 at 23:14):

That doesn't have the usability I was hoping for because it requires an explicit tactic invocation, and it's not automatically associated with the structure, but if nothing better comes out of this discussion I'll probably use something based on that.

Alex J. Best (Nov 16 2021 at 23:19):

Yeah it could certainly be added as a pre-processing step for linarith to do this, but we like small lego-block style tactics so people can combine them in different ways, it certainly seems useful to me to have this as an independent tactic for other purposes too.

Sam (Nov 16 2021 at 23:29):

Off topic, but I wish Lean was named something that I could google things about without having to carefully refine my search to avoid sifting through tons of articles from Startup Bros all excited about their lean management practices.

Kevin Buzzard (Nov 16 2021 at 23:35):

The trick is to google for lean prover or lean theorem prover

Scott Morrison (Nov 16 2021 at 23:35):

use leanprover

Sam (Nov 16 2021 at 23:36):

Good tips, thanks.

Alex J. Best (Nov 16 2021 at 23:40):

Slightly more advanced version :grinning:

import tactic

structure a :=
(b : )
(h : 1 < b)
(h2 : 5 < b^2 + 3)
  -- tactic.get_constructors_for
  -- #check tactic.get_decls_from

open tactic expr
namespace tactic
namespace interactive
meta def add_structure_hyps (t : parse texpr) : tactic unit :=
    h  i_to_expr t,
    tyo  infer_type h,
    l  tactic.expanded_field_list (expr.const_name tyo),
    l.mfoldl (λ _ b, do
      c  mk_const $ name.append b.1 b.2,
      let d := expr.mk_app c [h],
      ty  infer_type d,
      i  is_prop ty,
      guardb i >> note `this ty d >> skip <|> skip,
      skip) ()
end interactive
end tactic

lemma oof (c d : a) : 1 < d.b + 1 :=
  -- have := a.h c,
  add_structure_hyps d,

Sam (Nov 16 2021 at 23:47):

Very cool @Alex J. Best! Thanks - I'll be stealing that immediately!

Sam (Nov 16 2021 at 23:53):

I realise that this probably isn't going to happen, because people don't seem too interested in this more magic version of the idea, but I'd like to refine my description of what I'd ideally like to see.

I would like any tactic that makes use of local hypothesese to automatically see "nested" local hypothesese that exist as structure fields. simp, library_search, finish, linarith etc and anything else that makes use of the local state would have them available.

Without knowing the details of how tactics are implemented, I'm imagining that this could be done by modifying whatever the equivalent of get_local_hypothesese() is.

If this would introduce too much overhead by bringing too many things into scope, I'm happy for this to be opt-in on a per-field basis with an attribute on the structure declaration. Like @[simp], there are some places where this makes more sense than others.

Sam (Nov 16 2021 at 23:55):

These nested hypotheses wouldn't necessarily need to be actually brought into the local context to be displayed to the user - they would just be visible to tactics that use them.

Sam (Nov 16 2021 at 23:56):

Do people think this idea is bad and/or technically infeasible?

Scott Morrison (Nov 17 2021 at 00:03):

I don't think it's either bad or techinically infeasible. The biggest problem is that is proposes modify many tactics at once (some implemented in core, some in mathlib). We are very keen to keep tactics simple and focused -- think of the philosophy of unix command line tools.

Scott Morrison (Nov 17 2021 at 00:04):

I think a with_projections { ... } might be good. It would just pull out projections as local hypotheses during the scope of the { ... }.

Scott Morrison (Nov 17 2021 at 00:04):

As said above, I do think that this change should/could be made to library_search.

Sam (Nov 17 2021 at 00:17):

That seems reasonable @Scott Morrison, and with_projections seems like an interesting way to go.

My motivation is generally increasing the usability of subtypes and subtype-like structures, which appear to be a generally powerful idea, but currently a bit finicky and verbose to use. Conceptually, I think of this not as a modification to individual tactics, but to what it means for something to be in the local context. I now realise that that's probably not how it would work in implementation.

I still think this would be a nice feature, and it doesn't feel like it compromises the simple tactics philosophy to me, but I'll cede to your opinion as being far more informed than mine.

Last updated: Dec 20 2023 at 11:08 UTC