Zulip Chat Archive

Stream: general

Topic: generalize


view this post on Zulip Kenny Lau (Apr 19 2018 at 09:43):

Could someone build a tactic that allows us to generalize at hypotheses?

view this post on Zulip Simon Hudon (Apr 19 2018 at 22:51):

Can you give an example?

view this post on Zulip Kenny Lau (Apr 20 2018 at 05:52):

example (m n p q : nat) (H : m + n = p) : m + n = q :=
begin
  generalize h : m + n = x at h ,
  guard_hyp h := m + n = x,
  guard_hyp H := x = p,
  guard_target x = q,
  admit
end

view this post on Zulip Kenny Lau (Apr 20 2018 at 05:52):

@Simon Hudon

view this post on Zulip Simon Hudon (Apr 20 2018 at 11:33):

I see. So it reverts your hypotheses for you. That should be doable. I'll look into it. Any idea what it should be called?

view this post on Zulip Kenny Lau (Apr 20 2018 at 11:40):

I think one can extend generalize?

view this post on Zulip Kenny Lau (Apr 20 2018 at 11:41):

i.e. still call it generalize, since it builds upon the current generalize (so there won’t be beackwards compatibility problem)

view this post on Zulip Simon Hudon (Apr 20 2018 at 11:44):

generalize is defined in the core library and they usually don't take pull requests there. We may have to give it a different name and put it in mathlib

view this post on Zulip Kenny Lau (Apr 20 2018 at 12:32):

I’m not sure what I would call it. What do you think?

view this post on Zulip Simon Hudon (Apr 20 2018 at 12:34):

generalized_generalize

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:35):

Can't you have tactic modifying tactics? Then you could just write generalize simp or generalize wlog and of course also generalize generalize.
Life would be so much simpler.

view this post on Zulip Simon Hudon (Apr 20 2018 at 12:35):

Or ageneralize. a for assumption. We can also call it generalizea (not to be confused with the Canadian generalize, eh?)

view this post on Zulip Simon Hudon (Apr 20 2018 at 12:37):

some tactics have generalizing clauses like induction xs generalizing h

view this post on Zulip Simon Hudon (Apr 20 2018 at 12:50):

(kudos for the hockey stick, @Sean Leather :rolling_on_the_floor_laughing: )

view this post on Zulip Sean Leather (Apr 20 2018 at 12:53):

Bienvenue, eh!

view this post on Zulip Kenny Lau (Apr 20 2018 at 14:04):

I have a truly marvelous idea

view this post on Zulip Kenny Lau (Apr 20 2018 at 14:04):

I have a truly marvelous idea

view this post on Zulip Kenny Lau (Apr 20 2018 at 14:04):

we can call it generalise

view this post on Zulip Simon Hudon (Apr 20 2018 at 14:05):

You are truly evil, @Kenny Lau

view this post on Zulip Patrick Massot (Apr 20 2018 at 15:03):

You are truly evil, @Kenny Lau

Don't forget we learned this morning that Kenny is nothing but Kevin's evil part.

view this post on Zulip Simon Hudon (Apr 20 2018 at 15:07):

I wasn't there for that. It all adds up ... his constructivism should really have been a dead give away

view this post on Zulip Simon Hudon (Apr 20 2018 at 15:07):

Btw @Kenny Lau I just made a pull request with your requested feature:

https://github.com/leanprover/mathlib/pull/110

Let me know if you like it!

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:23):

@Simon Hudon does it work with more than one local hypothesis?

view this post on Zulip Simon Hudon (Apr 20 2018 at 15:23):

Yes it does

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:23):

I like it, thanks

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:23):

let's test if it works with induction

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:23):

could you test if you can generalize a list and then do induction?

view this post on Zulip Simon Hudon (Apr 20 2018 at 15:24):

Can you show me what you have in mind?

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:24):

yes, wait a minute

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:28):

example (α : Sort*) (L₁ L₂ L₃ : list α)
  (H : L₁ ++ L₂ = L₃) : L₁ ++ L₂ = L₂ :=
begin
  generalize_a h : L₁ ++ L₂ = L at H,
  induction L with hd tl ih,
  case list.nil
  { guard_hyp H := list.nil = L₃ },
  case list.cons
  { guard_hyp H := hd :: tl = L₃ },
  admit
end

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:28):

@Simon Hudon there you go

view this post on Zulip Simon Hudon (Apr 20 2018 at 15:35):

I had to change it to:

example (α : Sort*) (L₁ L₂ L₃ : list α)
  (H : L₁ ++ L₂ = L₃) : L₁ ++ L₂ = L₂ :=
begin
  generalize_a h : L₁ ++ L₂ = L at H,
  induction L with hd tl ih,
  case list.nil
  { tactic.cleanup,
    change list.nil = L₃ at H,
    admit },
  case list.cons
  { change hd :: tl = L₃ at H,
    admit },
end

but it worked

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:35):

why?

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:35):

but thanks

view this post on Zulip Simon Hudon (Apr 20 2018 at 15:36):

guard_hyp and guard_target are fairly intolerant. If your expressions contain meta variables and that they don't match, it will fail. At least, I believe that's the reason

view this post on Zulip Kenny Lau (Apr 20 2018 at 15:36):

I see

view this post on Zulip Simon Hudon (Apr 20 2018 at 15:36):

And you're welcome :)


Last updated: May 14 2021 at 00:42 UTC