Zulip Chat Archive

Stream: new members

Topic: Variable with braces, parentheses and square brackets


view this post on Zulip AHan (Nov 08 2018 at 06:23):

The below code works.
However, if I changed the h to pp in function p_mod_range, pp will become unknown identifier....
No matter I changed the brackets of variable pp to parentheses or square brackets or braces, neither of them can make variable pp be identified by lean....
Why can't lean identifies variable pp, and how can I fix this ?

import data.nat.prime
import data.int.basic
import data.int.modeq

open nat

lemma mod_range {b : ℕ} : (b > 0) → ∀ (x : ℤ), 0 ≤ x % b ∧ x % b < b :=
begin
  intros h₁ x,
  apply and.intro,
  begin
    apply int.mod_nonneg, simp,
    assume h₃,
    rw h₃ at *,
    cases h₁
  end,
  begin
    apply int.mod_lt_of_pos,
    apply int.coe_nat_lt.elim_right,
    assumption
  end,
end

namespace pf

variables { p: ℕ }  {pp : prime p}

lemma p_mod_range (h: prime p): ∀ (x : ℤ),  0 ≤ x % p ∧ x % p < p :=
  begin
    intro, apply mod_range, apply (prime.pos h),
  end

view this post on Zulip Mario Carneiro (Nov 08 2018 at 07:18):

variables are not added by default to the context of the current theorem unless they appear in the type

view this post on Zulip Mario Carneiro (Nov 08 2018 at 07:18):

you should use include pp to explicitly add it to the context

view this post on Zulip AHan (Nov 08 2018 at 07:19):

Oh Yeah!! include works!

view this post on Zulip AHan (Nov 08 2018 at 07:20):

But why isn't it be added by default to the context?

view this post on Zulip Johan Commelin (Nov 08 2018 at 07:28):

This allows you to introduce a bunch of variables at the top, and selectively use them in the theorems you prove.

view this post on Zulip Johan Commelin (Nov 08 2018 at 07:28):

Otherwise a lot of theorems (and definitions) would have unnecessary assumptions.

view this post on Zulip AHan (Nov 08 2018 at 07:33):

Got it!!
Is the include scope ends until the end of the section or the namespace?
Can I stop include in the middle point, like only include the variables for one function?

view this post on Zulip Johan Commelin (Nov 08 2018 at 07:34):

Yes: omit pp. Otherwise it stops at end section/namespace

view this post on Zulip AHan (Nov 08 2018 at 07:35):

Ok! Thanks a lot for the explanations!

view this post on Zulip AHan (Nov 08 2018 at 08:21):

Although including variable works, some functions like has_mul, has_one in the following code, will have to explicitly name out the variables p, p_gt_one.
And which seems to make using the symbols *, 1 failed, like in function pf_is_right_inv below...
Is there any better way to handle this?

def pf {p : ℕ} := {e : ℤ// 0 ≤ e ∧ e < p}

namespace pf

variables { p: ℕ } { p_gt_one : p > 1 } { pp : prime p }
include p_gt_one

def mul (a b : @pf p) : @pf p :=  ⟨(a.val * b.val) % p,  begin apply mod_range, apply (trans p_gt_one zero_lt_one) end⟩
instance : has_mul (@pf p) := ⟨@mul p p_gt_one⟩
protected def one  : @pf p := ⟨1, begin apply and.intro, apply zero_le_one, apply (int.coe_nat_le.elim_right p_gt_one), end⟩
instance : has_one (@pf p) := ⟨@pf.one p p_gt_one⟩

lemma pf_is_right_inv (a : @pf p) : (a.1 > 0) → a * (@pf.inv p p_gt_one a) = 1 := sorry
end pf

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:25):

I don't think you should have pp and p_gt_one. Because you can deduce p_gt_one from pp.

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:25):

Also, you should make the p argument of pf explicit, so that you can remove the @ from pf later.

view this post on Zulip AHan (Nov 08 2018 at 08:27):

yeah I know I can deduce p_gt_one from pp, but I'm thinking of if in some cases like add, mul, sub, maybe I can make it a bit general, since pp isn't actually needed

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:30):

Ok, but then I wouldn't make it a variable. Just include it as an assumption on that line.

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:30):

And consider renaming p to n to show that you also care about non-primes.

view this post on Zulip AHan (Nov 08 2018 at 08:32):

What do you mean include it as an assumption on that line?

view this post on Zulip AHan (Nov 08 2018 at 08:32):

OH yes, renaming is a good suggestion!

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:33):

def mul {h : p > 1} (a b : @pf p) : @pf p := blah

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:33):

But it will be annoying to use, because you have to carry that proof around all the time.

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:34):

And I think you don't need it.

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:34):

You can define it for p = 1 just fine.

view this post on Zulip AHan (Nov 08 2018 at 08:34):

Yes.... seems like really annoying...
Maybe I should give up the idea of taking care of non-primes

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:34):

I guess p = 0 is problematic.

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:35):

Sure, after all, others have already done that. So if you are just experimenting, I wouldn't try to be as general as possible.

view this post on Zulip AHan (Nov 08 2018 at 08:38):

Yeah I'm just experimenting, but "others have already done that", do you mean in the mathlib or is it in some other trustable third party library?

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:38):

No in mathlib.

view this post on Zulip AHan (Nov 08 2018 at 08:40):

Which file does it reside in?
Cause this experiment isn't actually my main goal, I did this mainly because my main goal need this, and I didn't find this in mathlib...

view this post on Zulip Mario Carneiro (Nov 08 2018 at 08:41):

What are you doing exactly? I'm not sure if it's in mathlib but I don't know what it is. It looks sort of like zmod

view this post on Zulip AHan (Nov 08 2018 at 08:45):

I want to examine some algorithms correctness, and the algorithms need prime field
So I'm thinking of defining a type of prime field and use as an instance of class field

view this post on Zulip Mario Carneiro (Nov 08 2018 at 08:46):

If by prime field you mean Z/pZ where p is a prime, that's zmod

view this post on Zulip Mario Carneiro (Nov 08 2018 at 08:47):

Or do you mean the smallest subfield of a given field? I don't think we have that but you can fake it with rat.cast

view this post on Zulip AHan (Nov 08 2018 at 08:48):

@Johan Commelin I've done what you suggested, but the problem that I can't use the symbol * and 1 still exists...

def pf (p : ℕ) := {e : ℤ// 0 ≤ e ∧ e < p}

namespace pf

variables ( p: ℕ ) ( pp : prime p )
include pp

def mul (a b : pf p) : pf p := ⟨(a.val * b.val) % p,     begin apply mod_range, apply prime.pos pp end⟩
instance : has_mul (pf p) := ⟨@mul p pp⟩
protected def one  : pf p := ⟨1, begin apply and.intro, apply zero_le_one, apply (int.coe_nat_lt.elim_right (prime.gt_one pp)), end⟩
instance : has_one (pf p) := ⟨@pf.one p pp⟩

lemma pf_is_right_inv (a : pf p) : (a.1 > 0) → a * (@pf.inv p pp a) = 1 :=

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:50):

Ok, what happens if you do not include pp?

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:50):

Just don't make any assumptions on p.

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:50):

But, like Mario said, you are basically redefining zmod n.

view this post on Zulip AHan (Nov 08 2018 at 08:53):

@Mario Carneiro Yeah Z/pZ exactly the thing I want
Do you mean the zmod in modeq ? Isn't is some sort of equivalence class instead of some types like int or nat ?

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:54):

https://github.com/leanprover/mathlib/blob/dbb3ff0b5b2e42aa71d8167d7efdb3aa12d6e483/data/zmod/basic.lean#L10

view this post on Zulip Johan Commelin (Nov 08 2018 at 08:54):

It is really almost the same as what you did. The set of naturals between 0 and n.

view this post on Zulip AHan (Nov 08 2018 at 08:57):

If I don't include pp, since I have to prove the result of mul < p, I will have to include something like p_gt_zeroin the assumption

view this post on Zulip AHan (Nov 08 2018 at 09:02):

Oh!! Thank you very much! (Didn't notice this... as I can't find zmod via C-c C-d....)

view this post on Zulip Johan Commelin (Nov 08 2018 at 09:34):

@AHan Sure, that's right. You will notice that zmod uses pnat: positive natural numbers.

view this post on Zulip AHan (Nov 08 2018 at 12:55):

Yes, didn't even notice that there were pnat, this really helped a lot! Thank you!


Last updated: May 15 2021 at 00:39 UTC