Zulip Chat Archive

Stream: general

Topic: refine_struct


view this post on Zulip Simon Hudon (May 31 2018 at 18:25):

@Patrick Massot I finally got around to writing a refine_struct tactic to generalize and simplify the automation of the indexed_product proofs.

You can see it in action here https://github.com/cipher1024/lean-differential-topology/blob/master/src/indexed_product.lean.

You can use it as:

refine_struct { some_field := foo, .. },
repeat
{ intro x,
  have_field,
  apply (field x) }

In short, refine_struct acts a bit like refine but tags every goal it produces with the name of the field that requires it. Then you can use tactics such as have_field / let_field to add an assumption or a local definition that stands for the accessor of the current field. You can also use apply_field if you just want to use it as a rule.

Does it look useful in this state? My next step would be to PR it into mathlib.

view this post on Zulip Patrick Massot (May 31 2018 at 19:41):

Do you examples of using have_field, let_field and aply_field? I can see in the indexed product that you don't need to provide any data, which is already really nice, but I don't understand how the other tactics can be used

view this post on Zulip Simon Hudon (May 31 2018 at 19:49):

I you were to write the proof of semigroup by hand, it would go like this:

instance semigroup [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
begin
  refine_struct { .. },
  { intros x y i, apply_field, apply (x i), apply (y i) },
  { have_field,
    intros, funext, simp!, apply field }
end

view this post on Zulip Simon Hudon (May 31 2018 at 19:50):

The first proof constructs the semigroup operator and the second proves associativity. While the first proof only works for binary functions, the second one is pretty much what the tactic does.

view this post on Zulip Simon Hudon (May 31 2018 at 19:51):

In the second proof, apply_field would work if funext didn't discard the goal's tags

view this post on Zulip Patrick Massot (May 31 2018 at 19:55):

it seems have_field already discards it

view this post on Zulip Patrick Massot (May 31 2018 at 19:56):

why simp! rather than dsimp?

view this post on Zulip Simon Hudon (May 31 2018 at 19:56):

Yeah, you're right. I'll fix that

view this post on Zulip Simon Hudon (May 31 2018 at 19:56):

No reasons, I hadn't thought of using dsimp that way

view this post on Zulip Patrick Massot (May 31 2018 at 19:58):

just trying to say more precisely what Lean shoud do (I also tend to use exact when it works, instead of apply like you did)

view this post on Zulip Patrick Massot (May 31 2018 at 19:58):

anyway, it looks very nice

view this post on Zulip Patrick Massot (May 31 2018 at 20:00):

can you also do Kevin's instance : comm_monoid ℕ+ using it?

view this post on Zulip Simon Hudon (May 31 2018 at 20:00):

I see. I would only use one command in that case but I wanted to demonstrate apply_field.

view this post on Zulip Simon Hudon (May 31 2018 at 20:00):

Can you send me a link?

view this post on Zulip Simon Hudon (May 31 2018 at 20:00):

Is it the transport problem?

view this post on Zulip Patrick Massot (May 31 2018 at 20:03):

no, building this instance on pnat, given we already have it on nat

view this post on Zulip Simon Hudon (May 31 2018 at 20:03):

It should be doable

view this post on Zulip Patrick Massot (May 31 2018 at 20:03):

https://github.com/leanprover/mathlib/blob/ad92a9ba47f417916aab365d13db653fa8991a84/data/pnat.lean#L52

view this post on Zulip Simon Hudon (May 31 2018 at 20:04):

Thanks, I'll have a look after dinner :)

view this post on Zulip Patrick Massot (May 31 2018 at 20:04):

Kevin complained about Lean not being smart enough to do it by itself

view this post on Zulip Patrick Massot (May 31 2018 at 20:04):

Is it already dinner time in Quebec?

view this post on Zulip Simon Hudon (May 31 2018 at 20:09):

Here's my first attempt:

instance : comm_monoid ℕ+ :=
begin
  refine_struct
    { mul       := λ m n : ℕ+, (⟨m.1 * n.1, mul_pos m.2 n.2⟩ : ℕ+),
      one       := succ_pnat 0, .. },
  repeat
  { have_field,
    intros, refine subtype.eq _, apply field }
end

view this post on Zulip Simon Hudon (May 31 2018 at 20:09):

It's a mistake to expect Lean to be smart. Lean is effective.

view this post on Zulip Simon Hudon (May 31 2018 at 20:09):

It is a bit early for dinner but my sister just had a baby so I'm giving her a hand

view this post on Zulip Simon Hudon (May 31 2018 at 20:10):

Ok, I gotta run now

view this post on Zulip Patrick Massot (May 31 2018 at 20:10):

thanks!

view this post on Zulip Patrick Massot (May 31 2018 at 20:21):

Ok, so obvisouly I can add

meta def derive_field' : tactic unit :=
do b  target >>= is_prop,
  if b then do
     field  get_current_field,
     intros,
     `[refine subtype.eq _],
     applyc field
  else do skip

And the instance becomes

instance : comm_monoid ℕ+ :=
begin
  refine_struct
    { mul       := λ m n : ℕ+, (m.1 * n.1, mul_pos m.2 n.2 : ℕ+),
      one       := succ_pnat 0, .. } ; derive_field'
end

view this post on Zulip Patrick Massot (May 31 2018 at 20:21):

Question: can we start derive_field by some testing whether the target type is a pi type of a sub-type?

view this post on Zulip Patrick Massot (May 31 2018 at 20:22):

@Kevin Buzzard did you see that?

view this post on Zulip Patrick Massot (May 31 2018 at 20:23):

It's a mistake to expect Lean to be smart. Expect Simon to be smart.

view this post on Zulip Simon Hudon (Jun 01 2018 at 00:27):

Haha! That was not quite my point ...

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:31):

I think there is a good lesson in there though... "Computers don't prove theorems, people prove theorems"

view this post on Zulip Simon Hudon (Jun 01 2018 at 00:32):

Is this the slogan for the new National Reasoning Association?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:33):

the Bot Lobby

view this post on Zulip Simon Hudon (Jun 01 2018 at 00:38):

Are you trying to emphasize the "people prove theorems" or the "computers are innocent"?

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:40):

In all seriousness, I would say it's important not to lose sight of the fact that computers do nothing more than what you tell them to

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:40):

so if you want magical tactics, you need magical people to support them

view this post on Zulip Simon Hudon (Jun 01 2018 at 00:41):

Yeah, my point exactly

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 00:45):

or just sufficiently advanced technology

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:45):

No

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:45):

that's the point

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:46):

the sufficiently advanced tech has to come from us

view this post on Zulip Simon Hudon (Jun 01 2018 at 00:47):

The difference is that, from magic, you expect all your wildest dreams to be fulfilled while with effective technology, you expect a specific task to be handled. The technology is more useful because it's easier to know when it will work and when it won't

view this post on Zulip Mario Carneiro (Jun 01 2018 at 00:47):

it's one thing to expect miracles of "the CS community" in general, but that seems much less reasonable when you restrict scope to the <=10 people who are actually involved in writing tactics that you will see

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:19):

That's why I have to learn. But I have so many other things I want to do :-/

view this post on Zulip Kevin Buzzard (Jun 01 2018 at 01:19):

It's wonderful being busy isn't it

view this post on Zulip Simon Hudon (Jun 01 2018 at 01:21):

It sounds like a sarcastic comment but I have found that since my schedule has been filling up, I've been able to get things done quicker

view this post on Zulip Patrick Massot (Jun 01 2018 at 06:55):

Question: can we start derive_field by some testing whether the target type is a pi type of a sub-type?

What about this question?

view this post on Zulip Simon Hudon (Jun 01 2018 at 11:39):

Yes that can be done. Are those the only two situations where you'd like to use derive_field?

view this post on Zulip Simon Hudon (Jun 01 2018 at 14:39):

I'm not sure what the best way to generalize derive_field is. I'm thinking of breaking it into derive_method and derive_proof_of_law. You could use them as refine_struct { .. } ; try { derive_field <|> derive_proof_of_law. Then, we can add a tactic argument to derive_proof_of_law and use it as derive_proof_of_law { intro } or derive_proof_of_law { refine subtype.eq _ }. I don't know if that's simpler than having separate tactics for pi instances and for subtypes.

view this post on Zulip Patrick Massot (Jun 01 2018 at 16:33):

maybe two separate tactics make more sense actually (one for pi and one for subtypes)

view this post on Zulip Simon Hudon (Jun 01 2018 at 16:36):

The benefit over the previous automation is, even if you do need specialized code, the simplified code is much simpler than in the current version of pi_instance

view this post on Zulip Mario Carneiro (Jun 01 2018 at 16:43):

I like this approach for exactly this reason. I wasn't a fan of pi_instance originally because it was a lot of code for a specialized problem; this puts most of the code in an obviously general setting and now pi_instance is both simpler and requires less input


Last updated: May 08 2021 at 09:11 UTC