tactic for applying at appropriate assumptions

Stream: general

[Sean Leather]

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]

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]

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

[Sean Leather]

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

[Simon Hudon]

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]

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]

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]

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

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]

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]

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

[Sean Leather]

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]

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]

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

[Simon Hudon]

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]

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

[Simon Hudon]

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

Care to elaborate?

[Sean Leather]

 (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]

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]

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]

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]

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]

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]

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]

 (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]

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]

 (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]

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]

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]

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]

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]

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

... and goals?

[Simon Hudon]

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]

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]

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

[Sean Leather]

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]

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]

how about have_spec (for specialization)?

[Simon Hudon]

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]

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]

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

[Sean Leather]

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]

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]

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

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]

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

[Simon Hudon]

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]

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]

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]

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.