equational lemmas

Stream: general

[Simon Hudon]

when using add_decl to create a definition, is it possible to declare an accompanying equational lemma?

[Mario Carneiro]

As far as I know, there is no way to define equational lemmas "just like" the ones generated by the equation compiler. Maybe @Sebastian Ullrich can confirm?

[Simon Hudon]

By "just like", I assume specifically that you're saying that simp and unfold won't pick up on them

[Simon Hudon]

Actually, I should say that's what I'm looking for.

[Mario Carneiro]

Yes, there is a C (and maybe lean?) function get_equation_lemmas which returns these things, but I don't think users have access to change it

[Simon Hudon]

Yeah I saw it. I was pretty disappointed that it was built in

[Sebastian Ullrich]

Right, equation lemmas are currently stored in an environment extension, which only exposes read-only access via tactic.get_eqn_lemmas

[Simon Hudon]

Blast! Foiled again :stuck_out_tongue_closed_eyes:

[Simon Hudon]

By the way, why I got you here, beside fields with underscore, is there any information about structures and substructures? I'm looking at group and it does not seem to have any underscore fields even though it has plenty of ancestry

[Sebastian Ullrich]

It should still use old_structure_cmd

[Simon Hudon]

I see. I'm a bit vague on how that works. Does it mean that parent structures are expanded fully and not a trace of the fact that it's a parent is left?

[Sebastian Ullrich]

Right. Well, the only trace is the synthesized parent coercions.

[Mario Carneiro]

luckily, these are completely replicable by users

[Kevin Buzzard]

One of my kids is doing the exercises in Software Foundations in Lean this week, that was definitely a parent coercion

[Simon Hudon]

@Mario Carneiro Unfortunately, this time, it's not about replicating it. I'm building proofs that structures like groups are transportable. I can unfold projections like group.mul but most axioms are in terms of has_mul.mul.

[Simon Hudon]

My best idea right now is hard coding references to has_foo.foo for multiple foos.

[Mario Carneiro]

I don't see the problem. Won't the parent instance be embedded in the has_mul.mul application?

[Simon Hudon]

Let's say that from equiv a b and group a, I'm building group b. With a list of all the fields of group, I'd call dsimp [...]. I'm not sure what to do if I find the group b instance in there.

[Simon Hudon]

Should I look for all projections applied to that group instance?

[Mario Carneiro]

I'm still confused. Where would there be a group b instance?

[Mario Carneiro]

In the type of a field?

[Mario Carneiro]

@[to_additive name.mk_string "mk" (name.mk_string "add_group" name.anonymous)]
constructor group.mk : Π {α : Type u} (mul : α → α → α)
(mul_assoc :
  ∀ (a b c : α),
    @eq α (@has_mul.mul α (@has_mul.mk α mul) (@has_mul.mul α (@has_mul.mk α mul) a b) c)
      (@has_mul.mul α (@has_mul.mk α mul) a (@has_mul.mul α (@has_mul.mk α mul) b c))) (one : α)
(one_mul : ∀ (a : α), @eq α (@has_mul.mul α (@semigroup.to_has_mul α (@semigroup.mk α mul mul_assoc)) 1 a) a)
(mul_one : ∀ (a : α), @eq α (@has_mul.mul α (@semigroup.to_has_mul α (@semigroup.mk α mul mul_assoc)) a 1) a)
(inv : α → α),
  (∀ (a : α),
     @eq α
       (@has_mul.mul α
          (@semigroup.to_has_mul α (@monoid.to_semigroup α (@monoid.mk α mul mul_assoc one one_mul mul_one)))
          (@has_inv.inv α (@has_inv.mk α inv) a)
          a)
       1) →
  group α

[Simon Hudon]

Here's part of the transportable class:

class transportable (f : Type u → Type v) :=
(on_equiv : Π {α β : Type u} (e : equiv α β), equiv (f α) (f β))

[Simon Hudon]

To build equiv (group a) (group b) I first need the to_fun definition (which is the hairy part we're now talking about)

[Simon Hudon]

Ah! Yes, that's where the instance would be:

(@has_mul.mul α
          (@semigroup.to_has_mul α (@monoid.to_semigroup α (@monoid.mk α mul mul_assoc one one_mul mul_one)))
          (@has_inv.inv α (@has_inv.mk α inv) a)

[Simon Hudon]

So it does not appear directly as an argument to a projection

[Mario Carneiro]

You can unfold all those if you want

[Mario Carneiro]

it reduces to mul of course

[Simon Hudon]

I just remembered unfold_projs exists. Is this what you think I should use?

[Mario Carneiro]

shouldn't dsimp work?

[Mario Carneiro]

or is the problem that you don't know what to simplify

[Mario Carneiro]

You can use whnf to give it a good kick

[Simon Hudon]

Mario Carneiro: or is the problem that you don't know what to simplify

Yes exactly. What I'm starting with is the list of all the fields of group

[Simon Hudon]

whnf still would be pretty involved. If I just apply it to the proposition, nothing will happen because it's an equality. Then I'd need to traverse the whole expression

[Mario Carneiro]

Of course you have to traverse the expression. How else would you figure out what to transport?

[Simon Hudon]

cancellation rules on equiv are doing a lot already. I thought I could use more high level primitives. My tactic is outrageously slow already without hand crafting traversals

[Mario Carneiro]

oh, I see, you are using heuristic simplification

[Simon Hudon]

Yes. Do you think it might be why it's all so slow?

[Mario Carneiro]

hard to say without knowing exactly what you are doing, but yes, I expect that a general analysis would be both more reliable and faster (and also a lot of work to write)

[Mario Carneiro]

If you aren't going for the full decision procedure, then it seems okay to just have an ad hoc list and let users add to it as necessary

[Simon Hudon]

That makes sense. I'll have to do optimization at some point anyway

[Mario Carneiro]

Even having an approximate transportable implementation would be very helpful, I think

[Simon Hudon]

I'll try to wrap up a prototype quickly. The feedback will be useful to pick a direction. I think the performances will be very noticeable

[Mario Carneiro]

Did you ever look at Johannes's transport tactic, with its relator based approach?

[Simon Hudon]

Only a while ago and never managed to understand it. I'll have another look

[Simon Hudon]

Btw, here's what I have, if you want to check it out:

https://github.com/cipher1024/transport/blob/master/src/transport.lean#L114

[Johan Commelin]

@Simon Hudon do you have any clue how close this brings us to the parametricity results of Wadler that @Mario Carneiro has been talking about?

[Johan Commelin]

It is not clear to me how our "naive transporatability" notion compares to Wadler's parametricity when it comes to ease of use. I also don't know how they compare when it comes to ease of implementation...

[Simon Hudon]

Actually, I haven't followed that conversation too closely. I'll have to catch up

[Simon Hudon]

Can you point me to the beginning of that conversation?

[Kenny Lau]

How does Lean tell the difference between an automatically generated .equations._eqn_1 and one that I prove manually?

[Simon Hudon]

I have gone down that road before. In Lean 3, there's no way of getting Lean to use your lemmas as definitional equations

[Kenny Lau]

this is so sad

[Simon Hudon]

I'm hopeful it'll get better in Lean 4