generalize only one occurrence

Stream: new members

[Hannah Fechtner]

Say I have something like
grid 1 1 c d
I'd like to generalize the first 1 to be a and the second 1 to be b, so I get

ha : 1 = a
hb : 1 = b

and
grid a b c d, which is something I can do induction on

Is there any syntax that allows this? I've tried using a conv block, but it won't let me put a generalize line in there. I've tried using set!, but then it puts a "let ..." in my context and won't let me do induction

[Hannah Fechtner]

(if it's helpful, grid is defined inductively as so:

/-- a reversing grid, inductively defined as the set of basic cells, and a vertical and horizontal
closure under appending-/
inductive grid : FreeMonoid ℕ → FreeMonoid ℕ → FreeMonoid ℕ → FreeMonoid ℕ → Prop
  | empty : (grid 1 1 1 1 : Prop)
  | top_bottom (i : ℕ) : grid 1 (of i) 1 (FreeMonoid.of i)
  | sides (i : ℕ) : grid (of i) 1 (of i) 1
  | top_left (i : ℕ) : grid (of i) (of i) 1 1
  | adjacent (i k : ℕ) (h : Nat.dist i k = 1) : grid (of i) (of k) (of i * of k) (of k * of i)
  | separated (i j : ℕ) (h : i +2 ≤ j ∨ j+2 <= i) : grid (of i) (of j) (of i) (of j)
  | vertical (h1: grid u v u' v') (h2 : grid a v' c d) : grid (u * a) v (u' * c) d
  | horizontal (h1: grid u v u' v') (h2 : grid u' b c d) : grid u (v * b) c (v' * d)

[Yaël Dillies]

Usually, when this happens, we write a separate lemma. Does this help?

[Hannah Fechtner]

I have a working method like so: I define

def all_one (a b c d : FreeMonoid' ℕ) := a = 1 → b = 1 → CONCLUSION

and for my theorem foo, I show

grid a b c d \to all_one a b c d

which works fine!

it's just when you use it, it's a bit clunky

Looks like

foo (grid_holds) rfl rfl

(where grid_holds is a proof of grid a b c d)

Those two rfls were annoying me, and I figured it might be cleaner using generalize?

[Hannah Fechtner]

oh, I could even do it more simply, like

theorem foo : grid a b c d → a = 1 → b = 1 → CONCLUSION

[Hannah Fechtner]

if that's the easiest way, I'm happy with my solution! I just wanted to check that I'm not missing any functionality of generalize

[Hannah Fechtner]

(and I'm a bit curious how generalize works, and why this cannot be done - it seems re-write can rewrite a specific occurrence, so I'm curious what works differently under-the-hood)

[Kyle Miller]

I think generalize could theoretically take an occs parameter per generalize clause (the syntax allows generalize h1 : v1 = x1, h2 : v2 = x2, ...). It uses the same motive-construction algorithm (kabstract) as rw.

[Hannah Fechtner]

ooh that would be slick. do you have any idea about the syntax for that? I can't do

  generalize ha : (1 : FreeMonoid' ℕ) = a with {occs := [1]}

since generalize doesn't seem to work with the with keyword

[Kyle Miller]

Someone would have to implement it

[Kyle Miller]

Another thing you can do is set up the local lemma yourself and then use rw to do what generalize does.

[Kyle Miller]

There's also doing something weird like this:

inductive grid : ℕ → ℕ → ℕ → ℕ → Prop

example (c d : ℕ) : grid 1 1 c d ∧ True := by
  set a := 1 with ha
  set b := 1 with hb
  conv => enter [1]; change grid a b c d
  clear_value a b
  /-
  c d b : ℕ
  hb : b = 1
  a : ℕ
  ha : a = b
  ⊢ grid a b c d ∧ True
  -/

[Hannah Fechtner]

thank you Kyle :)

[Hannah Fechtner]

and Yael too for the lemma idea, it finally clicked what you meant, and I've got a more-elegant version working

[Notification Bot]

Hannah Fechtner has marked this topic as resolved.

[Hannah Fechtner]

Yaël Dillies said:

Usually, when this happens, we write a separate lemma. Does this help?

@Yaël Dillies
do you mean something like this?

private theorem all_ones  (h : grid a b c d) (ha : a = 1) (hb : b = 1) :  c = 1 ∧ d = 1 := sorry

theorem all_ones_better (h1 : grid 1 1 c d) : c = 1 ∧ d = 1 := all_ones h1 rfl rfl

[Notification Bot]

Hannah Fechtner has marked this topic as unresolved.

[Yaël Dillies]

I guess so, but I'm a bit confused how you are going to do induction on a = 1 :thinking: