refine_struct

Stream: general

[Simon Hudon]

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

[Patrick Massot]

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

[Simon Hudon]

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

[Simon Hudon]

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.

[Simon Hudon]

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

[Patrick Massot]

it seems have_field already discards it

[Patrick Massot]

why simp! rather than dsimp?

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

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)

[Patrick Massot]

anyway, it looks very nice

[Patrick Massot]

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

[Simon Hudon]

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

[Simon Hudon]

Can you send me a link?

[Simon Hudon]

Is it the transport problem?

[Patrick Massot]

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

[Simon Hudon]

It should be doable

[Patrick Massot]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

Is it already dinner time in Quebec?

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

Ok, I gotta run now

[Patrick Massot]

thanks!

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

@Kevin Buzzard did you see that?

[Patrick Massot]

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

[Simon Hudon]

Haha! That was not quite my point ...

[Mario Carneiro]

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

[Simon Hudon]

Is this the slogan for the new National Reasoning Association?

[Mario Carneiro]

the Bot Lobby

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

Yeah, my point exactly

[Kevin Buzzard]

or just sufficiently advanced technology

[Mario Carneiro]

No

[Mario Carneiro]

that's the point

[Mario Carneiro]

the sufficiently advanced tech has to come from us

[Simon Hudon]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's wonderful being busy isn't it

[Simon Hudon]

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

[Patrick Massot]

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?

[Simon Hudon]

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

[Simon Hudon]

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.

[Patrick Massot]

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

[Simon Hudon]

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

[Mario Carneiro]

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