Zulip Chat Archive

Stream: general

Topic: generalisation of mk_eq_symm


view this post on Zulip Scott Morrison (Mar 16 2018 at 10:19):

I am really struggling to write a tactic that "does mk_eq_symm, but even inside binders". I would like to have something that given h : \forall x : X, f x = g x, spits back \forall x : X, g x = f x. Can anyone point me in the right direction?

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:20):

(I need this to work its way through arbitrarily many binders, possibly zero.)

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:27):

So far I have

meta def mk_eq_symm_under_binders_aux : expr  expr  tactic expr
| e (expr.pi n bi d b) := do
                             b'  mk_eq_symm_under_binders_aux (expr.app e b) b,
                             pure (expr.lam n bi d b')
| e t := mk_eq_symm e

meta def mk_eq_symm_under_binders : expr  tactic expr
| e := do t  infer_type e, mk_eq_symm_under_binders_aux e t

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 10:28):

Whilst of course I can't help, the recent thread here about using rw really opened my eyes to how this sort of thing wasn't "happening by default" as it were. I am still a little unclear about why eq.symm can't be used directly but this is probably just my poor understanding of the notion of equality in type theory. If I had write a tactic proof which did this I would just continually apply conv to everything.

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:34):

Yes! I know how to achieve this with conv. I need this tactic in service of my "rewrite searching" tactic, unfortunately, so a human isn't available to help direct the conv. I need to be able to determine if a rewrite is applying to the entire expression, or just a subexpression, but the only way to ask Lean to rewrite an entire expression seems to be via simp_lemmas.rewrite, which doesn't provide a facility for applying the rule in reverse, so I'm going to have to build the reverse rule myself.

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:36):

But what I have above is stupid. The expr.app e b is silly, it's not b that I'm meant to put in there, it's.... something. :-)

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 10:36):

I am a little disappointed that something like repeat {by conv in (_ = _) {rw eq.symm}} doesn't work in tactic mode :-)

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 10:37):

Or, more precisely, that I couldn't get it to work :-)

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:44):

I wrote an extremely similar tactic for alias

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:45):

I think my fundamental difficulty is I don't know how to construct an expr.lam.

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:45):

I will look at alias!

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:45):

meta def mk_iff_mp_app (iffmp : name) : expr → (nat → expr) → tactic expr
| (expr.pi n bi e t) f := expr.lam n bi e <$> mk_iff_mp_app t (λ n, f (n+1) (expr.var n))
| `(%%a ↔ %%b) f := pure $ @expr.const tt iffmp [] a b (f 0)
| _ f := fail "Target theorem must have the form `Π x y z, a ↔ b`"

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:45):

e.g., if I have f : \nat \to \nat, how to I construct the expr for \lambda n, f (n+1)?

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:46):

That tactic directly constructs a proof of \forall x y z, a -> b from \forall x y z, a <-> b

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:47):

I don't think it even needs to be a tactic (I only used a tactic in that case so I could fail with a nice error message)

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:48):

So how does expr.var work?

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:48):

That has me confused.

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:48):

expr.var is a de bruijn variable

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:49):

so \forall x y z, x = y becomes roughly pi "x" (pi "y" (pi "z" (app (app (const "eq") (var 2)) (var 1)))

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:50):

the number counts how many binders back the variable is

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:51):

I see. (Or, at least I can imagine writing voodoo code based on what I see. :-)

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:52):

I have an aversion to writing code that has suboptimal asymptotics, so I may have been too clever in the definition there, what with the accumulation function and all

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:54):

Also, I don't think you will be able to use mk_eq_symm in the function

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 10:54):

I guess one question for Scott then is whether he is likely to be applying his tactic to terms built from strings of length 10^10 :-)

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:54):

What will go wrong with mk_eq_symm?

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:54):

because when you are working on an expr manually like this, you have to deal with open terms, and tactics don't like open terms

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:55):

open meaning containing an unbound var

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:55):

(Or you can let me find out for myself in a minute or two..)

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:55):

I see. But I can just build it directly myself?

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:55):

(as you did in your example)

view this post on Zulip Mario Carneiro (Mar 16 2018 at 10:56):

yes

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 10:57):

Is it just a coincidence that Mario posted code with the line lam n, f (n+1) seconds before Scott asked about how to construct the expr for lam n, f (n+1)?

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:58):

apparently yes :-)

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:58):

They have nothing to do with each other. :-)

view this post on Zulip Scott Morrison (Mar 16 2018 at 10:58):

(and wow, this looks like it may be working!)

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 10:59):

I thought so but I thought I'd ask as I am frantically cut-and-pasting into a text file and just wanted to check that zulip didn't have some "slightly re-order the messages" functionality

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 11:01):

It's about time I learnt something about tactics and one way of learning is to write some docs.

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:02):

Thank you all! Things are looking good here. :-) all_rewrites seems to be working, finding lots of rewrites that rw itself can't see.

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 11:02):

Can you post what you wrote?

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 11:02):

[if you're happy to do so of course!]

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:02):

It's probably slow as molasses ... but that's a different problem.

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:04):

meta def mk_eq_symm_under_binders_aux : expr  (nat  expr)  tactic expr
| (expr.pi n bi d b) f := expr.lam n bi d <$> mk_eq_symm_under_binders_aux b (λ n, f (n+1) (expr.var n))
| `(%%a = %%b) e := mk_eq_symm (e 0)
| _ _ := fail "expression must have the form `Π x y z, a = b`"

meta def mk_eq_symm_under_binders : expr  tactic expr
| e := do t  infer_type e, mk_eq_symm_under_binders_aux t (λ _, e)

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:04):

That's just the mk_eq_symm_under_binders part.

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:05):

Then there's

meta def rewrite_entire (r : (expr × bool)) (e : expr) : tactic (expr × expr) :=
do let sl := simp_lemmas.mk,
   r'  if r.2 then mk_eq_symm_under_binders r.1 else pure r.1,
   sl  sl.add r',
   sl.rewrite e

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:05):

which given r, a rule and a bool flag indicating whether to use the rule in reverse, and an expression e, either rewrite the entire expression e using the rule, returning the replacement and the proof, or fails.

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 11:06):

Now I will tell my students to alias rw to this and they will never have to worry about why it used to sometimes fail :-)

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:07):

And then there's https://gist.github.com/semorrison/9b3a0f42fbd697d562a8b6daa960f14e

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:07):

for the actual implementation of all_rewrites

view this post on Zulip Scott Morrison (Mar 16 2018 at 11:07):

which still needs a little more wrapper before you can use it in interactive mode...

view this post on Zulip Kevin Buzzard (Mar 16 2018 at 11:09):

Thanks for this. I know I could just try to learn tactics by reading the tactic code in core Lean etc but the problem with doing that is that it can often be pretty hard-core. It's like trying to learn Lean by reading core lean and instantly finding opt_params everywhere with no explanation as to what they are.


Last updated: May 15 2021 at 23:13 UTC