generalize in term mode

Stream: general

[Kenny Lau]

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

I have made a generalize in term mode

[Kenny Lau]

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]

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

[Kenny Lau]

⊢ ∀ (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]

is this a good idea?

[Kenny Lau]

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]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

But I can't learn everything at the same time

[Kenny Lau]

well you know how induction works with generalizing right

[Patrick Massot]

No I don't

[Kenny Lau]

hmm

[Patrick Massot]

I only do induction on natural numbers

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

(I call this "double induction')

[Kenny Lau]

the very action of moving the goalpost from x+y=y+x to \forall y, x+y=y+x is called generalizing

[Kenny Lau]

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

[Kenny Lau]

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

[Simon Hudon]

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

[Kenny Lau]

ok

[Patrick Massot]

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

[Patrick Massot]

Thanks for the explanation

[Kenny Lau]

@[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]

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

[Kenny Lau]

but here you go

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

I should make show a term-tactic

[Kenny Lau]

well that won't really be necessary, forget that

[Kenny Lau]

but I like my generalize

[Kenny Lau]

a tactic in term mode

[Kenny Lau]

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

[Kenny Lau]

@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]

assuming that it is an invention

[Kenny Lau]

bonus points! generalize also works as revert

[Kenny Lau]

@[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]

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

[Kenny Lau]

Here's the real generalize:

[Kenny Lau]

@[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]

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

[Kenny Lau]

thanks for your appreciation

[Kenny Lau]

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]

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

[Chris Hughes]

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]

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

[Kenny Lau]

until I realized that I can build tactics in term mode

[Andrew Ashworth]

does your generalize use heq under the hood?

[Chris Hughes]

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

[Kenny Lau]

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

[Kenny Lau]

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]

now I can do it in one go:

[Kenny Lau]

@[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]

@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]

@Chris Hughes not that I'm aware of

[Kenny Lau]

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

[Andrew Ashworth]

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

[Kenny Lau]

@[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]

I don't see any heq here

[Andrew Ashworth]

when you print an example that uses generalize

[Andrew Ashworth]

do you get a heq term

[Andrew Ashworth]

it may or may not, i'm just curious

[Chris Hughes]

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]

I need to rec on the first red

[Chris Hughes]

I see. Makes a lot of sense then.

[Kenny Lau]

@[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]

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

[Chris Hughes]

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

[Kenny Lau]

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]

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

[Kenny Lau]

thanks for your appreciation

[Andrew Ashworth]

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]

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

[Andrew Ashworth]

it's quite a low-level idea

[Andrew Ashworth]

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

[Kenny Lau]

so, eh, which one?

[Kenny Lau]

eq is already an inductive type

[Andrew Ashworth]

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

[Kenny Lau]

it doesn't depend on heq

[Kenny Lau]

I don't think it uses heq anywhere

[Chris Hughes]

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]

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]

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

[Kenny Lau]

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

[Kenny Lau]

I still like my method more :P

[Chris Hughes]

I was expecting it not to work.

[Kenny Lau]

did you do anything more than my eyes could see

[Kenny Lau]

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

[Chris Hughes]

No.

[Kenny Lau]

very curious indeed

[Kenny Lau]

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

[Patrick Massot]

Congratulations!

[Patrick Massot]

Two docstrings is a very good start!

[Kenny Lau]

:P

[Kenny Lau]

I was making docstrings

[Kenny Lau]

and then I got carried away by revert and generalize

[Kenny Lau]

@Mario Carneiro do you like this?

[Kenny Lau]

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]

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

[Mario Carneiro]

probably should be reducible

[Kenny Lau]

woohoo, tactics in term mode

[Mario Carneiro]

I mean, you can use match to the same effect

[Mario Carneiro]

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

[Kenny Lau]

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

[Mario Carneiro]

not in my experience

[Kenny Lau]

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

[Kenny Lau]

here

[Mario Carneiro]

why don't you use the equation compiler?

[Kenny Lau]

that also needs to be auxiliary

[Mario Carneiro]

for red.trans

[Kenny Lau]

because rec_on is shorter

[Mario Carneiro]

eww

[Kenny Lau]

I thought someone likes short proofs

[Mario Carneiro]

I like straightforward proofs

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

this was a big problem in lean 2

[Mario Carneiro]

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