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

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

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: Dec 20 2023 at 11:08 UTC