Variable inclusion defs vs. theorems

Stream: new members

[Klaus Gy]

Why are variables used only in the proof automatically included in defs but not in theorems?

variable (n : Nat)

-- this gives an error, unknown identifier 'n'
theorem foo (m : Nat) : m = m :=
  have : n = n := by rfl
  rfl

-- this works fine
def foo' (m : Nat) : m = m :=
  have : n = n := by rfl
  rfl

[Kyle Miller]

The rule is that theorem includes variables based on what's mentioned in the theorem statement itself, but def includes variables based on the entire definition.

[Klaus Gy]

thanks! i was a bit surprised that its handled differently but i assume thats by design then :)

[Kyle Miller]

You can use the include n command to force the variable to be included in theorems

[Kyle Miller]

There are two practical reasons for this:

1. Many tactics operate on the whole local context, and it can create artificial dependencies.
2. This allows the proofs to be elaborated asynchronously.

[Kyle Miller]

Even basic tactics like induction/cases can cause variables to become included unnecessarily.

[Kyle Miller]

Example:

variable (n : Nat) (m : Fin n)

def ex : 0 ≤ n := by
  induction n with
  | zero => simp
  | succ _ _ => simp

#check ex
/-
ex (n : Nat) (m : Fin n) : 0 ≤ n
-/

[Klaus Gy]

ah interesting, so the tactic can see m and could potentially use it, so its not auto discarded

[Kyle Miller]

and be sure to look at the local context to see why m is used here

Try changing it to (m : Fin 2). You should observe that it's not included.

[Klaus Gy]

ugh this is cursed, i dont fully understand, seems like the second placeholder assumes something with m, but only if m is available

[Kyle Miller]

In the first example, take a look how m changes, right before each simp.

Then, change it to (m : Fin 2), and look at the local contexts again.

What's the difference?

[Klaus Gy]

seems like induction works by simple induction P(n) => P(n + 1) if no fin n is available but if fin n is available it takes the more general form of (all x in fin n : P(n)) => P(n + 1)

[Kyle Miller]

In particular, since Fin n depends on the induction variable n, the tactic does revert m first, and then intro m in each case. It's the auto-generalizing feature. (The thing where you can use the generalizing clause to add in more variables to generalize.)

[Kyle Miller]

It needs to auto-generalize because n is reverted too, to apply the induction principle.

[Kyle Miller]

(Said another way, induction n basically starts off with revert n, and that's what causes the artificial dependency on m)

[Klaus Gy]

aah ok, thanks! what i wrote is bs, the more general induction principle is not what i wrote. yea makes much more sense now!