## Stream: general

### Topic: generalize

#### Kenny Lau (Apr 19 2018 at 09:43):

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

#### Simon Hudon (Apr 19 2018 at 22:51):

Can you give an example?

#### 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


@Simon Hudon

#### 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?

#### Kenny Lau (Apr 20 2018 at 11:40):

I think one can extend generalize?

#### 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)

#### 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

#### Kenny Lau (Apr 20 2018 at 12:32):

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

#### Simon Hudon (Apr 20 2018 at 12:34):

generalized_generalize

#### 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.

#### 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?)

#### Simon Hudon (Apr 20 2018 at 12:37):

some tactics have generalizing clauses like induction xs generalizing h

#### Simon Hudon (Apr 20 2018 at 12:50):

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

Bienvenue, eh!

#### Kenny Lau (Apr 20 2018 at 14:04):

I have a truly marvelous idea

#### Kenny Lau (Apr 20 2018 at 14:04):

I have a truly marvelous idea

#### Kenny Lau (Apr 20 2018 at 14:04):

we can call it generalise

#### Simon Hudon (Apr 20 2018 at 14:05):

You are truly evil, @Kenny Lau

#### 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.

#### 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

#### 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!

#### Kenny Lau (Apr 20 2018 at 15:23):

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

Yes it does

#### Kenny Lau (Apr 20 2018 at 15:23):

I like it, thanks

#### Kenny Lau (Apr 20 2018 at 15:23):

let's test if it works with induction

#### Kenny Lau (Apr 20 2018 at 15:23):

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

#### Simon Hudon (Apr 20 2018 at 15:24):

Can you show me what you have in mind?

#### Kenny Lau (Apr 20 2018 at 15:24):

yes, wait a minute

#### 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


#### Kenny Lau (Apr 20 2018 at 15:28):

@Simon Hudon there you go

#### 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

why?

but thanks

#### 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

I see

#### Simon Hudon (Apr 20 2018 at 15:36):

And you're welcome :)

Last updated: May 14 2021 at 00:42 UTC