Zulip Chat Archive

Stream: new members

Topic: Reassign variable value


view this post on Zulip rory (Nov 06 2019 at 10:06):

I'm proving a theorem which uses subgoal as have p : k ∣ int.gcd a b ↔ k ∣ int.gcd b (a - n*b) , but I didn't impose any constraint on k, k is just a variable of type , is there a way to reassign k value, or to reassign k value, I have to prove have p : ∀ k : ℤ, k ∣ int.gcd a b ↔ k ∣ int.gcd b (a - n*b)

view this post on Zulip Johan Commelin (Nov 06 2019 at 10:11):

Can you give a bit more context?

view this post on Zulip Johan Commelin (Nov 06 2019 at 10:11):

I'm not sure I understand what the problem is

view this post on Zulip rory (Nov 06 2019 at 10:13):

I'm not sure I understand what the problem is

So this is the theorem I'm proving,

theorem prop4 (a b : ℤ) (h : a ≠ 0 ∧ b ≠ 0) (k : ℤ):
∀ n : ℤ, int.gcd a b = int.gcd b (a - n*b) :=
....stuff...
  have p₅ : k ∣ int.gcd a b ↔ k ∣ int.gcd b (a - n*b),
  ...stuff...
  have p₆ : int.gcd a b ∣ int.gcd b (a - n*b),

view this post on Zulip rory (Nov 06 2019 at 10:14):

I want to prove p6 using p5

view this post on Zulip Johan Commelin (Nov 06 2019 at 10:15):

Aha... yes, you can't change k. So you have to restate p₅ as \forall k : ℤ, ...

view this post on Zulip Johan Commelin (Nov 06 2019 at 10:16):

And so you should remove k from the hypotheses of prop4

view this post on Zulip rory (Nov 06 2019 at 10:18):

So there's no way for subgoals to share a \forall k generally

view this post on Zulip Johan Commelin (Nov 06 2019 at 10:20):

No... what you are asking for is an implicit universal quantifier. But how would Lean know if you want this or not

view this post on Zulip Johan Commelin (Nov 06 2019 at 10:21):

For all it knows, you might want to use the specific that you assumed something about somewhere else

view this post on Zulip rory (Nov 06 2019 at 10:21):

Okay, that makes sense

view this post on Zulip Simon Hudon (Nov 06 2019 at 14:40):

This might be an indication that you should write a separate lemma and use a variable declaration.


Last updated: May 08 2021 at 10:12 UTC