Zulip Chat Archive

Stream: general

Topic: tactic for applying at appropriate assumptions


Sean Leather (May 03 2018 at 08:35):

I've got a theorem:

theorem lc_value :  {e : exp V}, e.value  e.lc

Is there a tactical way to apply this theorem to all assumptions matching _.value to produce more assumptions _.lc?

Sean Leather (May 03 2018 at 12:29):

How's this for my first attempt at writing a tactic? It can be improved, of course.

meta def apply_matching (p : parse texpr) : tactic expr :=
  do e  to_expr p,
     et  infer_type e,
     guard et.is_arrow <|> fail format!"'apply_matching' expected a function, got '{et}'",
     any_hyp $ λ h, do
       ht  infer_type h,
       unify ht et.binding_domain,
       n  mk_fresh_name,
       note n none (expr.mk_app e [h])

Sean Leather (May 03 2018 at 12:30):

That is, I know some ways in which it can be improved, but comments to that effect are most welcome.

Sean Leather (May 03 2018 at 12:34):

I believe I've jumped into the rabbit hole now.

Simon Hudon (May 03 2018 at 17:35):

If I understand correctly, given a rule r : p -> q (where you call my r p) you're looking for an assumption h : p which would allow you to add an assumption h' : q.

First question: do you expect the user to see the name of that new assumption? If so, I doubt mk_fresh_name will give you appealing names. Maybe you should give at least the option of specifying the name.

Simon Hudon (May 03 2018 at 17:37):

Second question: is there a reason that your rule wouldn't be desirable if you had a pi type where the bound variable occurs in the term?

Simon Hudon (May 03 2018 at 17:38):

Third question: could it not be useful to repeat the process a certain number of times (if the user provides a list of names for the new assumptions, repeat until you run out of names; otherwise, repeat as many times as you can).

Sean Leather (May 04 2018 at 06:39):

@Simon Hudon Thanks for looking at it!

If I understand correctly, given a rule r : p -> q (where you call my r p) you're looking for an assumption h : p which would allow you to add an assumption h' : q.

That's almost correct. My current thinking is to look for all assumptions h_i : p and create all possible new assumptions h_i' : q where h_i' = r h_i.

First question: do you expect the user to see the name of that new assumption? If so, I doubt mk_fresh_name will give you appealing names. Maybe you should give at least the option of specifying the name.

In general, I would expect the new assumptions to be used in something like tauto or possibly just assumption. But I would certainly like to have useful fresh names and not the stuff spit out by mk_fresh_name. (I'm now using get_unused_name, but that doesn't seem much better.) Since multiple fresh names may be created, I think the option of specifying one name is not enough. I thought about doing something like adding a suffix to the name of h. How do I get the name of the hypothesis from the expr? What do you think?

Second question: is there a reason that your rule wouldn't be desirable if you had a pi type where the bound variable occurs in the term?

Perhaps not. Are you suggesting I use is_pi instead of is_arrow?

Third question: could it not be useful to repeat the process a certain number of times (if the user provides a list of names for the new assumptions, repeat until you run out of names; otherwise, repeat as many times as you can).

Repeating is indeed my intention. Is it not doing that? I haven't yet tested. But, looking again at any_hyp_aux, it looks like it does stop at the first success. Is there an existing function for iterating over all of the local context or list expr, or should I write one?

Sean Leather (May 04 2018 at 06:55):

Is there an existing function for iterating over all of the local context or list expr, or should I write one?

Answering my own question: list.mfoldl/list.mfoldr

Sean Leather (May 04 2018 at 08:13):

The latest version with expr.is_pi and list.mfoldl:

meta def apply_matching (p : parse texpr) : tactic unit :=
  do e  to_expr p,
     et  infer_type e,
     guard et.is_pi <|> fail format!"'apply_matching' expected a function, got '{et}'",
     local_context >>= mfoldl
       (λ a h, do
         ht  infer_type h,
         tactic.try (do
           unify ht et.binding_domain,
           n  get_unused_name,
           note n none (expr.mk_app e [h])))
       ()

Sean Leather (May 04 2018 at 08:14):

It's funny and annoying that I keep forgetting the commas in Lean do-notation.

Sean Leather (May 04 2018 at 09:32):

Now with a ' appended to the name of the source hypothesis:

meta def name.update_suffix : name  (string  string)  name
| name.anonymous        _ := name.anonymous
| (name.mk_string s p)  f := name.mk_string (f s) p
| (name.mk_numeral n p) _ := name.mk_numeral n p

meta def apply_matching (p : parse texpr) : tactic unit :=
  do e  to_expr p,
     et  infer_type e,
     guard et.is_pi <|> fail format!"'apply_matching' expected a function, got '{et}'",
     local_context >>= mfoldl
       (λ a h, do
         ht  infer_type h,
         tactic.try $ do
           unify ht et.binding_domain,
           note (h.local_pp_name.update_suffix (flip append "'")) none (expr.mk_app e [h]))
       ()

Sean Leather (May 04 2018 at 09:42):

Hmm. I thought perhaps I could remove ht ← infer_type h and unify ht et.binding_domain because note would type check the expression expr.mk_app e [h]), but I ended up generating a new hypothesis for every existing hypothesis. note is defined with assertv_core, but it didn't do what I would expect from a cursory reading.

Simon Hudon (May 04 2018 at 12:06):

Sorry I missed the first question. At least, you didn't miss it

Simon Hudon (May 04 2018 at 12:08):

I would change:

 et ← infer_type e,
 guard et.is_pi <|> fail format!"'apply_matching' expected a function, got '{et}'",

to

 (expr.pi _ _ ed _) <- infer_type | fail format!"'apply_matching' expected a function, got '{et}'",

Simon Hudon (May 04 2018 at 12:09):

and .local_pp_name.update_suffix (flip append "'") to .local_pp_name.update_suffix (++ "'")

Simon Hudon (May 04 2018 at 12:12):

note is defined with assertv_core, but it didn't do what I would expect from a cursory reading.

Care to elaborate?

Sean Leather (May 04 2018 at 12:12):

 (expr.pi _ _ ed _) <- infer_type | fail format!"'apply_matching' expected a function, got '{et}'",

What is | here? Is this equivalent to the following bracketing (assuming said bracketing is valid)?

((expr.pi _ _ ed _) <- infer_type) | (fail format!"'apply_matching' expected a function, got '{et}'"),

Sean Leather (May 04 2018 at 12:13):

and .local_pp_name.update_suffix (flip append "'") to .local_pp_name.update_suffix (++ "'")

Ah, sections are supported. I wasn't sure and didn't try.

Simon Hudon (May 04 2018 at 12:14):

No, I don't think that's syntactically valid. It's because (expr.pi _ _ ed _) <- infer_type is an incomplete pattern matching statement. | comes in to say "here's what you do if it doesn't match ..."

Sean Leather (May 04 2018 at 12:16):

note is defined with assertv_core, but it didn't do what I would expect from a cursory reading.

Care to elaborate?

About? :simple_smile:

Sean Leather (May 04 2018 at 12:17):

No, I don't think that's syntactically valid. It's because (expr.pi _ _ ed _) <- infer_type is an incomplete pattern matching statement. | comes in to say "here's what you do if it doesn't match ..."

I see. Is this | strictly for pattern-matching in do-notation? Is it notation defined somewhere, or is it built in?

Simon Hudon (May 04 2018 at 12:18):

And there's a subtle difference with <|>. While do x <- a <|> b, c means a <|> b >>= λ x, c, do x <- a | b, c means:

a >>= λ x₀,
match x₀ with
 | x := c
 | _ := b
end

Simon Hudon (May 04 2018 at 12:19):

i.e. when you run b, you exit immediately. If b is not a fail statement but a statement like return none, the whole function returns non.

Sean Leather (May 04 2018 at 12:22):

 (expr.pi _ _ ed _) <- infer_type | fail format!"'apply_matching' expected a function, got '{et}'",

Except that, with this, I no longer have et. :wink:

Simon Hudon (May 04 2018 at 12:24):

note is defined with assertv_core, but it didn't do what I would expect from a cursory reading.

Care to elaborate?

About?

Hoping to break records of quotes within quotes, here's my answer. Please, let's make this an Inception of quotes.

What did you expect from assertv_core and how did the reality differ?

Simon Hudon (May 04 2018 at 12:27):

 (expr.pi _ _ ed _) <- infer_type | fail format!"'apply_matching' expected a function, got '{et}'",

Except that, with this, I no longer have et. :wink:

I missed the occurrence in the error message. What a bummer! I thought we could get rid of it. Let's go with:

 et <- infer_type,
 (expr.pi _ _ ed _) <- pure et | fail format!"'apply_matching' expected a function, got '{et}'",

Sean Leather (May 04 2018 at 12:27):

What did you expect from assertv_core and how did the reality differ?

As I said, I expected it to type-check the expression.

Sean Leather (May 04 2018 at 12:29):

Let's go with:

 et <- infer_type,
 (expr.pi _ _ ed _) <- pure et | fail format!"'apply_matching' expected a function, got '{et}'",

Hmm, I'm not convinced that's better. :wink:

Simon Hudon (May 04 2018 at 12:31):

Oh I see. I would think that too. But as the developers keep pointing out, they are very aggressive in their optimization. They try to never type check by default. The whole proof will be type checked at the end so that's not unsafe but it does mean that you have to unify or type_check when you think you need it.

Sean Leather (May 04 2018 at 12:32):

Oh I see. I would think that too. But as the developers keep pointing out, they are very aggressive in their optimization. They try to never type check by default. The whole proof will be type checked at the end so that's not unsafe but it does mean that you have to unify or type_check when you think you need it.

Oh, interesting. So, you can introduce badly typed hypotheses?

Sean Leather (May 04 2018 at 12:33):

Oh, interesting. So, you can introduce badly typed hypotheses?

... and goals?

Simon Hudon (May 04 2018 at 12:33):

Let's go with:

 et <- infer_type,
 (expr.pi _ _ ed _) <- pure et | fail format!"'apply_matching' expected a function, got '{et}'",

Hmm, I'm not convinced that's better. :wink:

Yeah, that's less of an improvement

Simon Hudon (May 04 2018 at 12:35):

Oh, interesting. So, you can introduce badly typed hypotheses?

... and goals?

The expressions and goals are still type checked from time to time but you can find a way.

Simon Hudon (May 04 2018 at 12:36):

I think to_expr type checks the expression so that already filters out a lot of nonsense

Sean Leather (May 04 2018 at 12:37):

note is defined with assertv_core, but it didn't do what I would expect from a cursory reading.

Care to elaborate?

About?

Hoping to break records of quotes within quotes, here's my answer. Please, let's make this an Inception of quotes.

I think Zulip needs threads within topics within streams... :house_buildings:

Sean Leather (May 04 2018 at 12:42):

Current version:

meta def note_all_applied (p : parse texpr) : tactic unit :=
  do e  to_expr p,
     et  infer_type e,
     guard et.is_pi <|> fail format!"'note_all_applied' expected a function, got '{et}'",
     local_context >>= mfoldl
       (λ a h, do
         ht  infer_type h,
         tactic.try $ do
           unify ht et.binding_domain,
           note (h.local_pp_name.update_suffix (++ "'")) none (e.mk_app [h]))
       ()

I'm not really sure about a good name. apply_matching is certainly not good: too much of a connection to apply.

Simon Hudon (May 04 2018 at 12:51):

how about have_spec (for specialization)?

Simon Hudon (May 04 2018 at 12:51):

I think you you should check if the domain of e is a proposition. If it is, having multiple specializations will only be noisy

Sean Leather (May 04 2018 at 12:57):

how about have_spec (for specialization)?

1. My immediate thought is to expand spec to specification.
2. I would not naturally think of this as specialization. The resulting type depends on the argument.

Johan Commelin (May 04 2018 at 13:00):

and Kevin is defining the spectrum of a ring... although that will probably be called Spec.

Sean Leather (May 04 2018 at 13:23):

I think you you should check if the domain of e is a proposition. If it is, having multiple specializations will only be noisy

I don't follow. If I have this:

have h : Prop := true,
note_all_applied or_true

I see this:

h : Prop,
h' : h  true  true

Simon Hudon (May 04 2018 at 13:59):

a proposition

assume h :  x  y,
assume h' :  x  y,
note_all_applied (not_lt_of_ge x y)

The above should only produce one more assumption, not two.

Sean Leather (May 06 2018 at 09:26):

@Simon Hudon I'm sorry, but I'm still not getting what you're saying.

What do you mean by a proposition? I used h : Prop, but you may be thinking of something else.

I tried to make a working example out of your code, and this is what I have:

example {x y : } (h h' : x  y) : Prop := by note_all_applied not_lt_of_ge

The state:

x y : ,
h h' : x  y,
h' h'' : ¬y < x
 ?m_1

So, two things are clearly problematic here:

  • Output hypotheses (h', h'') with the same type (¬y < x). However, there are input hypotheses with the same type. I'm not sure this is something the tactic should handle because:
    • Handling duplicate outputs adds complexity when the duplicate inputs already exist, and, consequently, this complexity appears unnecessary.
    • If the tactic did something else, what would it be, and would it still be predictable?
  • Duplicate h' hypotheses. The output hypothesis naming could certainly be better. It would be nice to have fresh, readable, predictable names, perhaps similar to what cases and induction do. Do you have any suggestions for this?

That said, I'm not sure what the above has to do with propositions. The same issues can be shown with non-Prop types:

example (x y : ) : Prop := by note_all_applied nat.succ
x y x' y' : 
 Prop

Simon Hudon (May 06 2018 at 17:52):

What I was trying to point out is that the types of h,h',h' and h'' themselves have type Prop. Maybe I should have called them proofs instead of proposition. Sorry for the confusion.

I was saying that using many of them in your tactic would result in repetition because of proof irrelevant.

Simon Hudon (May 06 2018 at 17:52):

As you point out, that might make for a highly redundant tactic code.

Simon Hudon (May 06 2018 at 18:02):

If you decide to adopt that more aggressive simplification, you can replace mfold or for_each with:

meta def for_each_considering_proof_irrelevance {α : Type}
  (irrel : bool) (f : α → tactic unit) (xs : list α) : tactic unit :=
if irrel then
  xs.any_of f
else
  xs.for_each f

Sean Leather (May 07 2018 at 06:26):

Thanks for pointing at for_each and any_of. Funny that they don't seem to be used at all in the Lean core library.

Scott Morrison (Aug 09 2018 at 06:44):

Hi @Sean Leather, what happened to this tactic? I think I want it now, and I'm not sure where to look for it.

Sean Leather (Aug 09 2018 at 07:18):

You mean the one and only tactic I ever wrote? It's here. I think I use it in the same repository, but I'm not convinced it is actually that useful.


Last updated: Dec 20 2023 at 11:08 UTC