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

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

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

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


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

No.

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

very curious indeed

Congratulations!

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

Two docstrings is a very good start!

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

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

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

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