Implicitly bringing structure field props into context

Stream: new members

[Sam]

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]

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

[Kyle Miller]

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]

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]

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

[Kyle Miller]

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]

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]

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]

(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]

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]

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

[Sam]

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]

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]

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]

Or even l3.len.le

[Sam]

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

[Sam]

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]

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

[Kyle Miller]

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]

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]

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]

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]

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]

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]

@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]

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]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

There's also case_bash somewhere.

[Reid Barton]

Ah, I didn't know about that one.

[Scott Morrison]

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

[Sam]

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]

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

[Kevin Buzzard]

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]

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

[Sam]

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

[Kyle Miller]

@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]

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

[Reid Barton]

Er wait maybe it can't be for a structure

[Scott Morrison]

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

[Sam]

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]

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

[Sam]

Right, yeah good.

[Kevin Buzzard]

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

[Sam]

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]

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 :=
  do
  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 :=
begin
  -- have := a.h c,
  add_structure_hyps,
  linarith
end

[Alex J. Best]

Is this what you are thinking?

[Alex J. Best]

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

[Sam]

That's pretty cool @Alex J. Best!

[Sam]

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]

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]

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]

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

[Scott Morrison]

use leanprover

[Sam]

Good tips, thanks.

[Alex J. Best]

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
setup_tactic_parser
namespace tactic
namespace interactive
meta def add_structure_hyps (t : parse texpr) : tactic unit :=
  do
    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 :=
begin
  -- have := a.h c,
  add_structure_hyps d,
  linarith
end

[Sam]

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

[Sam]

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]

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]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Sam]

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.