Zulip Chat Archive

Stream: general

Topic: generalize in term mode


view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:51):

doing generalize z _ will give you this on the underscore:

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:51):

is this a good idea?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:55):

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

view this post on Zulip Patrick Massot (Apr 21 2018 at 15:56):

I'm afraid I still have to learn what the tactic mode generalize is good for

view this post on Zulip Patrick Massot (Apr 21 2018 at 15:56):

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

view this post on Zulip Patrick Massot (Apr 21 2018 at 15:56):

But I can't learn everything at the same time

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:56):

well you know how induction works with generalizing right

view this post on Zulip Patrick Massot (Apr 21 2018 at 15:57):

No I don't

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:57):

hmm

view this post on Zulip Patrick Massot (Apr 21 2018 at 15:57):

I only do induction on natural numbers

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:57):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:57):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:57):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:58):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:58):

(I call this "double induction')

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:59):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 15:59):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:04):

ok

view this post on Zulip Patrick Massot (Apr 21 2018 at 16:12):

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

view this post on Zulip Patrick Massot (Apr 21 2018 at 16:12):

Thanks for the explanation

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:13):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:13):

but here you go

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:13):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:13):

and you can see that generalize is necessary because I used ih1 twice

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:14):

I should make show a term-tactic

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:14):

well that won't really be necessary, forget that

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:14):

but I like my generalize

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:14):

a tactic in term mode

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:14):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:15):

assuming that it is an invention

view this post on Zulip Kenny Lau (Apr 21 2018 at 16:16):

bonus points! generalize also works as revert

view this post on Zulip 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
-/

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:01):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:01):

Here's the real generalize:

view this post on Zulip 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
-/

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:03):

thanks for your appreciation

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)))

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:05):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:05):

until I realized that I can build tactics in term mode

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:06):

does your generalize use heq under the hood?

view this post on Zulip Chris Hughes (Apr 21 2018 at 17:06):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:06):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:06):

now I can do it in one go:

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:07):

@Chris Hughes not that I'm aware of

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:07):

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

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:07):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:08):

I don't see any heq here

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:08):

when you print an example that uses generalize

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:08):

do you get a heq term

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:08):

it may or may not, i'm just curious

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:09):

I need to rec on the first red

view this post on Zulip Chris Hughes (Apr 21 2018 at 17:09):

I see. Makes a lot of sense then.

view this post on Zulip 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)
-/

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:09):

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

view this post on Zulip Chris Hughes (Apr 21 2018 at 17:10):

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

view this post on Zulip 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))
-/

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:14):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:15):

thanks for your appreciation

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:15):

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

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:15):

it's quite a low-level idea

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:16):

so, eh, which one?

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:16):

eq is already an inductive type

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:16):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:16):

it doesn't depend on heq

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:16):

I don't think it uses heq anywhere

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Andrew Ashworth (Apr 21 2018 at 17:19):

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

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:20):

@Chris Hughes interesting. usually it fails if I put y at the end

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:20):

I still like my method more :P

view this post on Zulip Chris Hughes (Apr 21 2018 at 17:20):

I was expecting it not to work.

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:20):

did you do anything more than my eyes could see

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:20):

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

view this post on Zulip Chris Hughes (Apr 21 2018 at 17:20):

No.

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:21):

very curious indeed

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:46):

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

view this post on Zulip Patrick Massot (Apr 21 2018 at 17:55):

Congratulations!

view this post on Zulip Patrick Massot (Apr 21 2018 at 17:55):

Two docstrings is a very good start!

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:55):

:P

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:55):

I was making docstrings

view this post on Zulip Kenny Lau (Apr 21 2018 at 17:55):

and then I got carried away by revert and generalize

view this post on Zulip Kenny Lau (Apr 22 2018 at 07:54):

@Mario Carneiro do you like this?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 22 2018 at 07:56):

probably should be reducible

view this post on Zulip Kenny Lau (Apr 22 2018 at 07:56):

woohoo, tactics in term mode

view this post on Zulip Mario Carneiro (Apr 22 2018 at 07:57):

I mean, you can use match to the same effect

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 22 2018 at 07:58):

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

view this post on Zulip Mario Carneiro (Apr 22 2018 at 07:58):

not in my experience

view this post on Zulip Kenny Lau (Apr 22 2018 at 07:58):

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

view this post on Zulip Kenny Lau (Apr 22 2018 at 07:58):

here

view this post on Zulip Mario Carneiro (Apr 22 2018 at 07:59):

why don't you use the equation compiler?

view this post on Zulip Kenny Lau (Apr 22 2018 at 07:59):

that also needs to be auxiliary

view this post on Zulip Mario Carneiro (Apr 22 2018 at 07:59):

for red.trans

view this post on Zulip Kenny Lau (Apr 22 2018 at 07:59):

because rec_on is shorter

view this post on Zulip Mario Carneiro (Apr 22 2018 at 08:00):

eww

view this post on Zulip Kenny Lau (Apr 22 2018 at 08:00):

I thought someone likes short proofs

view this post on Zulip Mario Carneiro (Apr 22 2018 at 08:00):

I like straightforward proofs

view this post on Zulip Mario Carneiro (Apr 22 2018 at 08:01):

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

view this post on Zulip Mario Carneiro (Apr 22 2018 at 08:01):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 22 2018 at 08:03):

this was a big problem in lean 2

view this post on Zulip 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