# Zulip Chat Archive

## Stream: general

### Topic: generalize in term mode

#### Kenny Lau (Apr 21 2018 at 15:50):

@[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x

I have made a `generalize`

in term mode

#### Kenny Lau (Apr 21 2018 at 15:50):

let's say this is the goal:

refl_trans red x z → (∃ (w : α), refl_trans (refl_trans red) y w ∧ refl_trans (refl_trans red) z w)

#### Kenny Lau (Apr 21 2018 at 15:51):

doing `generalize z _`

will give you this on the underscore:

#### Kenny Lau (Apr 21 2018 at 15:51):

⊢ ∀ (x_1 : α), refl_trans red x x_1 → (∃ (w : α), refl_trans (refl_trans red) y w ∧ refl_trans (refl_trans red) x_1 w)

#### Kenny Lau (Apr 21 2018 at 15:51):

is this a good idea?

#### Kenny Lau (Apr 21 2018 at 15:55):

example:

@[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x variables {α : Type*} (red : α → α → Prop) {x y z : α} inductive refl_trans : α → α → Prop | refl {x} : refl_trans x x | step_trans {x y z} : red x y → refl_trans y z → refl_trans x z @[trans] theorem refl_trans.trans (H : refl_trans red x y) : refl_trans red y z → refl_trans red x z := generalize z $ refl_trans.rec_on H (λ x z H, H) $ λ x y z hxy hyz ih w hzw, refl_trans.step_trans hxy $ ih w hzw

#### Kenny Lau (Apr 21 2018 at 15:55):

@Simon Hudon @Patrick Massot what do you guys think?

#### Patrick Massot (Apr 21 2018 at 15:56):

I'm afraid I still have to learn what the tactic mode `generalize`

is good for

#### Patrick Massot (Apr 21 2018 at 15:56):

I'm very curious because it came up a lot recently

#### Patrick Massot (Apr 21 2018 at 15:56):

But I can't learn everything at the same time

#### Kenny Lau (Apr 21 2018 at 15:56):

well you know how `induction`

works with `generalizing`

right

#### Patrick Massot (Apr 21 2018 at 15:57):

No I don't

#### Kenny Lau (Apr 21 2018 at 15:57):

hmm

#### Patrick Massot (Apr 21 2018 at 15:57):

I only do induction on natural numbers

#### Kenny Lau (Apr 21 2018 at 15:57):

so when you're proving that natural number addition is commutative

#### Kenny Lau (Apr 21 2018 at 15:57):

you want to prove that x+y=y+x

#### Kenny Lau (Apr 21 2018 at 15:57):

you induct on the proposition `\forall y, x+y=y+x`

instead

#### Kenny Lau (Apr 21 2018 at 15:58):

(and you prove the base case and inductive step both by induction)

#### Kenny Lau (Apr 21 2018 at 15:58):

(I call this "double induction')

#### Kenny Lau (Apr 21 2018 at 15:58):

the very action of moving the goalpost from `x+y=y+x`

to `\forall y, x+y=y+x`

is called generalizing

#### Kenny Lau (Apr 21 2018 at 15:59):

https://math.stackexchange.com/a/2438135/328173

#### Kenny Lau (Apr 21 2018 at 15:59):

here is it in Fitch style (only part 1 is relevant)

#### Simon Hudon (Apr 21 2018 at 16:04):

@Kenny Lau I'll have to get back to you a bit later. My nephew just arrived

#### Kenny Lau (Apr 21 2018 at 16:04):

ok

#### Patrick Massot (Apr 21 2018 at 16:12):

I can understand why you used your Kenny identity to post such an answer

#### Patrick Massot (Apr 21 2018 at 16:12):

Thanks for the explanation

#### Kenny Lau (Apr 21 2018 at 16:13):

@[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x inductive xnat : Type | zero : xnat | succ : xnat → xnat namespace xnat def add : xnat → xnat → xnat | x zero := x | x (succ y) := succ $ add x y theorem add_comm {x y : xnat} : add x y = add y x := generalize y $ xnat.rec_on x (λ y, xnat.rec_on y rfl $ λ y ih, show succ _ = succ _, from congr_arg succ ih) (λ y ih1 z, xnat.rec_on z (show succ _ = succ _, from congr_arg succ $ ih1 zero) (λ z ih2, congr_arg succ $ ih2.trans $ eq.trans (show succ _ = succ _, from congr_arg succ (ih1 z).symm) (ih1 $ succ z))) end xnat

#### Kenny Lau (Apr 21 2018 at 16:13):

@Patrick Massot somehow it took me a long time to prove this

#### Kenny Lau (Apr 21 2018 at 16:13):

but here you go

#### Kenny Lau (Apr 21 2018 at 16:13):

why did I use my Kenny identity to post such an answer?

#### Kenny Lau (Apr 21 2018 at 16:13):

and you can see that `generalize`

is necessary because I used `ih1`

twice

#### Kenny Lau (Apr 21 2018 at 16:14):

I should make `show`

a term-tactic

#### Kenny Lau (Apr 21 2018 at 16:14):

well that won't really be necessary, forget that

#### Kenny Lau (Apr 21 2018 at 16:14):

but I like my `generalize`

#### Kenny Lau (Apr 21 2018 at 16:14):

a tactic in term mode

#### Kenny Lau (Apr 21 2018 at 16:14):

(a tactic, here, is one which converts your goal to something useful)

#### Kenny Lau (Apr 21 2018 at 16:15):

@Mario Carneiro do you think it is a good idea? I have too many `aux`

theorems in my `free_group.lean`

that can be eliminated by my new invention :P

#### Kenny Lau (Apr 21 2018 at 16:15):

assuming that it is an invention

#### Kenny Lau (Apr 21 2018 at 16:16):

bonus points! `generalize`

also works as `revert`

#### Kenny Lau (Apr 21 2018 at 16:17):

@[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x example (x y : nat) (H : x = y) : false := generalize H _ /- don't know how to synthesize placeholder context: x y : ℕ, H : x = y ⊢ x = y → false -/

#### Kenny Lau (Apr 21 2018 at 17:01):

I think I made a mistake. What I have built is really `revert`

#### Kenny Lau (Apr 21 2018 at 17:01):

Here's the real `generalize`

:

#### Kenny Lau (Apr 21 2018 at 17:01):

@[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π z, x = z → β z) → β x := λ H, H x rfl example (m n : nat) : m + n = 0 := generalize (m + n) _ /- don't know how to synthesize placeholder context: m n : ℕ ⊢ ∀ (z : ℕ), m + n = z → z = 0 -/

#### Chris Hughes (Apr 21 2018 at 17:03):

I always wondered how to revert in term mode, however not sure I've ever had to do it.

#### Kenny Lau (Apr 21 2018 at 17:03):

thanks for your appreciation

#### Kenny Lau (Apr 21 2018 at 17:03):

so, for the sake of completeness:

@[elab_as_eliminator] def revert {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x @[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π z, x = z → β z) → β x := λ H, H x rfl

#### Andrew Ashworth (Apr 21 2018 at 17:05):

in the old days when we didn't have a tactic mode you'd revert using clever `heq`

tricks

#### Chris Hughes (Apr 21 2018 at 17:05):

Usually I just do this.

theorem add_comm {x : xnat} : ∀ {y}, add x y = add y x := xnat.rec_on x (λ y, xnat.rec_on y rfl $ λ y ih, show succ _ = succ _, from congr_arg succ ih) (λ y ih1 z, xnat.rec_on z (show succ _ = succ _, from congr_arg succ $ @ih1 zero) (λ z ih2, congr_arg succ $ ih2.trans $ eq.trans (show succ _ = succ _, from congr_arg succ (@ih1 z).symm) (@ih1 $ succ z)))

#### Kenny Lau (Apr 21 2018 at 17:05):

right, that's what I did in my free group file

#### Kenny Lau (Apr 21 2018 at 17:05):

until I realized that I can build tactics in term mode

#### Andrew Ashworth (Apr 21 2018 at 17:06):

does your generalize use `heq`

under the hood?

#### Chris Hughes (Apr 21 2018 at 17:06):

Are there any examples where you can't just do that?

#### Kenny Lau (Apr 21 2018 at 17:06):

@Chris Hughes so my file has a lot of auxiliary theorems

#### Kenny Lau (Apr 21 2018 at 17:06):

theorem red.trans.aux (H12 : red L₁ L₂) : ∀ {L₃}, red L₂ L₃ → red L₁ L₃ := red.rec_on H12 (λ _ _, id) $ λ _ _ _ H1 H2 ih L₃ H23, red.step_trans H1 $ ih H23 @[trans] theorem red.trans (H12 : red L₁ L₂) (H23 : red L₂ L₃) : red L₁ L₃ := red.trans.aux H12 H23

#### Kenny Lau (Apr 21 2018 at 17:06):

now I can do it in one go:

#### Kenny Lau (Apr 21 2018 at 17:06):

@[trans] theorem red.trans (H12 : red L₁ L₂) (H23 : red L₂ L₃) : red L₁ L₃ := revert H23 $ revert L₃ $ red.rec_on H12 (λ _ _, id) $ λ _ _ _ H1 H2 ih L₃ H23, red.step_trans H1 $ ih _ H23

#### Kenny Lau (Apr 21 2018 at 17:07):

@Andrew Ashworth are we talking about the same `heq`

, i.e. the `heq`

as in Lean? I don't know Coq at all. I showed you my code above though.

#### Kenny Lau (Apr 21 2018 at 17:07):

@Chris Hughes not that I'm aware of

#### Kenny Lau (Apr 21 2018 at 17:07):

I just built that an hour ago, I don't know everything about it

#### Andrew Ashworth (Apr 21 2018 at 17:07):

yeah, because in Coq it'd be `JMeq`

, heh

#### Kenny Lau (Apr 21 2018 at 17:07):

@[elab_as_eliminator] def revert {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x @[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π z, x = z → β z) → β x := λ H, H x rfl

#### Kenny Lau (Apr 21 2018 at 17:08):

I don't see any `heq`

here

#### Andrew Ashworth (Apr 21 2018 at 17:08):

when you print an example that uses generalize

#### Andrew Ashworth (Apr 21 2018 at 17:08):

do you get a `heq`

term

#### Andrew Ashworth (Apr 21 2018 at 17:08):

it may or may not, i'm just curious

#### Chris Hughes (Apr 21 2018 at 17:08):

You can just do some extra lambdas. i.e

`theorem red.trans.aux : ∀ {L₃}, red L₁ L₂ → red L₂ L₃ → red L₁ L₃`

What's wrong with that?

#### Kenny Lau (Apr 21 2018 at 17:09):

I need to rec on the first red

#### Chris Hughes (Apr 21 2018 at 17:09):

I see. Makes a lot of sense then.

#### Kenny Lau (Apr 21 2018 at 17:09):

@[elab_as_eliminator] def revert {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x @[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π z, x = z → β z) → β x := λ H, H x rfl theorem test (m n : nat) : m + n = 0 := generalize (m + n) $ λ z hz, sorry set_option pp.all true #print test /- theorem test : ∀ (m n : nat), @eq.{1} nat (@has_add.add.{0} nat nat.has_add m n) (@has_zero.zero.{0} nat nat.has_zero) := λ (m n : nat), @generalize.{1 0} nat (λ (_x : nat), @eq.{1} nat _x (@has_zero.zero.{0} nat nat.has_zero)) (@has_add.add.{0} nat nat.has_add m n) (λ (z : nat) (hz : @eq.{1} nat (@has_add.add.{0} nat nat.has_add m n) z), sorry) -/

#### Kenny Lau (Apr 21 2018 at 17:09):

@Andrew Ashworth is this what you're talking about?

#### Chris Hughes (Apr 21 2018 at 17:10):

@Andrew Ashworth Are you talking about Kenny's generalize or tactics mode generalize?

#### Kenny Lau (Apr 21 2018 at 17:10):

in that case:

@[elab_as_eliminator] def revert {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x @[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π z, x = z → β z) → β x := λ H, H x rfl theorem test (m n : nat) : m + n = 0 := generalize (m + n) $ λ z hz, sorry set_option pp.all true #print test /- theorem test : ∀ (m n : nat), @eq.{1} nat (@has_add.add.{0} nat nat.has_add m n) (@has_zero.zero.{0} nat nat.has_zero) := λ (m n : nat), @generalize.{1 0} nat (λ (_x : nat), @eq.{1} nat _x (@has_zero.zero.{0} nat nat.has_zero)) (@has_add.add.{0} nat nat.has_add m n) (λ (z : nat) (hz : @eq.{1} nat (@has_add.add.{0} nat nat.has_add m n) z), sorry) -/ theorem test' (m n : nat) : m + n = 0 := begin generalize h : m + n = z, admit end #print test' /- theorem test' : ∀ (m n : nat), @eq.{1} nat (@has_add.add.{0} nat nat.has_add m n) (@has_zero.zero.{0} nat nat.has_zero) := λ (m n : nat), (λ (z : nat) (h : @eq.{1} nat (@has_add.add.{0} nat nat.has_add m n) z), sorry) (@has_add.add.{0} nat nat.has_add m n) (@rfl.{1} nat (@has_add.add.{0} nat nat.has_add m n)) -/

#### Andrew Ashworth (Apr 21 2018 at 17:14):

hm, interesting, i'd have to dig further when I have time

#### Kenny Lau (Apr 21 2018 at 17:15):

thanks for your appreciation

#### Andrew Ashworth (Apr 21 2018 at 17:15):

`heq`

is important when doing dependent case analysis, which is why i was expecting heq to show up in the term there somewhere

#### Andrew Ashworth (Apr 21 2018 at 17:15):

it's probably buried in there somewhere... maybe... underneath one of the definitions

#### Andrew Ashworth (Apr 21 2018 at 17:15):

it's quite a low-level idea

#### Andrew Ashworth (Apr 21 2018 at 17:15):

or i could be really wrong about how lean works, and that also wouldn't surprise me

#### Kenny Lau (Apr 21 2018 at 17:16):

so, eh, which one?

#### Kenny Lau (Apr 21 2018 at 17:16):

`eq`

is already an inductive type

#### Andrew Ashworth (Apr 21 2018 at 17:16):

i can't say because i'm a lean scrub

#### Kenny Lau (Apr 21 2018 at 17:16):

it doesn't depend on `heq`

#### Kenny Lau (Apr 21 2018 at 17:16):

I don't think it uses `heq`

anywhere

#### Chris Hughes (Apr 21 2018 at 17:19):

Here's an alternative method

theorem add_comm {x y : xnat} : add x y = add y x := xnat.rec_on x (λ y, xnat.rec_on y rfl $ λ y ih, show succ _ = succ _, from congr_arg succ ih) (λ y ih1 z, xnat.rec_on z (show succ _ = succ _, from congr_arg succ $ @ih1 zero) (λ z ih2, congr_arg succ $ ih2.trans $ eq.trans (show succ _ = succ _, from congr_arg succ (@ih1 z).symm) (@ih1 $ succ z))) y

#### Andrew Ashworth (Apr 21 2018 at 17:19):

sure, and why that might be is interesting to me, most other tactics in coq that do this sort of thing use `heq`

#### Andrew Ashworth (Apr 21 2018 at 17:19):

https://coq.inria.fr/refman/proof-engine/detailed-tactic-examples.html

#### Kenny Lau (Apr 21 2018 at 17:20):

@Chris Hughes interesting. usually it fails if I put `y`

at the end

#### Kenny Lau (Apr 21 2018 at 17:20):

I still like my method more :P

#### Chris Hughes (Apr 21 2018 at 17:20):

I was expecting it not to work.

#### Kenny Lau (Apr 21 2018 at 17:20):

did you do anything more than my eyes could see

#### Kenny Lau (Apr 21 2018 at 17:20):

I can't really tell if you changed anything in the middle

#### Chris Hughes (Apr 21 2018 at 17:20):

No.

#### Kenny Lau (Apr 21 2018 at 17:21):

very curious indeed

#### Kenny Lau (Apr 21 2018 at 17:46):

more examples: https://github.com/kckennylau/Lean/commit/c9d0c76f7d807f48f4cea0c6043bcc9caf48e09a#diff-fdee7d198ee1f7316cba5649313e084a

#### Patrick Massot (Apr 21 2018 at 17:55):

Congratulations!

#### Patrick Massot (Apr 21 2018 at 17:55):

Two docstrings is a very good start!

#### Kenny Lau (Apr 21 2018 at 17:55):

:P

#### Kenny Lau (Apr 21 2018 at 17:55):

I was making docstrings

#### Kenny Lau (Apr 21 2018 at 17:55):

and then I got carried away by `revert`

and `generalize`

#### Kenny Lau (Apr 22 2018 at 07:54):

@Mario Carneiro do you like this?

#### Kenny Lau (Apr 22 2018 at 07:55):

recap:

@[elab_as_eliminator] def revert {α : Sort*} {β : α → Sort*} (x : α) : (Π x, β x) → β x := λ H, H x @[elab_as_eliminator] def generalize {α : Sort*} {β : α → Sort*} (x : α) : (Π z, x = z → β z) → β x := λ H, H x rfl

#### Mario Carneiro (Apr 22 2018 at 07:56):

I'm not sure I buy the particular applications you've used it for, but this seems okay for `logic.basic`

#### Mario Carneiro (Apr 22 2018 at 07:56):

probably should be `reducible`

#### Kenny Lau (Apr 22 2018 at 07:56):

woohoo, tactics in term mode

#### Mario Carneiro (Apr 22 2018 at 07:57):

I mean, you can use `match`

to the same effect

#### Mario Carneiro (Apr 22 2018 at 07:57):

but I usually just set up my intros in the right order so this isn't needed

#### Kenny Lau (Apr 22 2018 at 07:58):

right, but setting up them make for a bunch of auxiliary theorems

#### Mario Carneiro (Apr 22 2018 at 07:58):

not in my experience

#### Kenny Lau (Apr 22 2018 at 07:58):

#### Kenny Lau (Apr 22 2018 at 07:58):

here

#### Mario Carneiro (Apr 22 2018 at 07:59):

why don't you use the equation compiler?

#### Kenny Lau (Apr 22 2018 at 07:59):

that also needs to be auxiliary

#### Mario Carneiro (Apr 22 2018 at 07:59):

for `red.trans`

#### Kenny Lau (Apr 22 2018 at 07:59):

because `rec_on`

is shorter

#### Mario Carneiro (Apr 22 2018 at 08:00):

eww

#### Kenny Lau (Apr 22 2018 at 08:00):

I thought someone likes short proofs

#### Mario Carneiro (Apr 22 2018 at 08:00):

I like straightforward proofs

#### Mario Carneiro (Apr 22 2018 at 08:01):

the equation compiler makes it really clear how an induction proceeds, and what is the IH

#### Mario Carneiro (Apr 22 2018 at 08:01):

plus, I very much doubt you recouped the loss of having to state an auxiliary

#### Mario Carneiro (Apr 22 2018 at 08:03):

We haven't talked about it much since they appear to be going extinct, but it's possible to write brittle term proofs too

#### Mario Carneiro (Apr 22 2018 at 08:03):

this was a big problem in lean 2

#### Mario Carneiro (Apr 22 2018 at 08:04):

when you do a proof with lots of omitted type information relying on lean to pick up the pieces, if something changes in the unification algorithm or something it can be very difficult to understand the broken proof

Last updated: May 08 2021 at 19:11 UTC