generalize

Stream: general

[Kenny Lau]

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

[Simon Hudon]

Can you give an example?

[Kenny Lau]

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

[Kenny Lau]

@Simon Hudon

[Simon Hudon]

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]

I think one can extend generalize?

[Kenny Lau]

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

[Simon Hudon]

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]

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

[Simon Hudon]

generalized_generalize

[Johan Commelin]

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]

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

[Simon Hudon]

some tactics have generalizing clauses like induction xs generalizing h

[Simon Hudon]

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

[Sean Leather]

Bienvenue, eh!

[Kenny Lau]

I have a truly marvelous idea

[Kenny Lau]

I have a truly marvelous idea

[Kenny Lau]

we can call it generalise

[Simon Hudon]

You are truly evil, @Kenny Lau

[Patrick Massot]

You are truly evil, @Kenny Lau

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

[Simon Hudon]

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

[Simon Hudon]

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]

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

[Simon Hudon]

Yes it does

[Kenny Lau]

I like it, thanks

[Kenny Lau]

let's test if it works with induction

[Kenny Lau]

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

[Simon Hudon]

Can you show me what you have in mind?

[Kenny Lau]

yes, wait a minute

[Kenny Lau]

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]

@Simon Hudon there you go

[Simon Hudon]

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

[Kenny Lau]

why?

[Kenny Lau]

but thanks

[Simon Hudon]

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

[Kenny Lau]

I see

[Simon Hudon]

And you're welcome :)