Variable with braces, parentheses and square brackets

Stream: new members

[AHan]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[AHan]

Oh Yeah!! include works!

[AHan]

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

[Johan Commelin]

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

[Johan Commelin]

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

[AHan]

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?

[Johan Commelin]

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

[AHan]

Ok! Thanks a lot for the explanations!

[AHan]

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

[Johan Commelin]

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

[Johan Commelin]

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

[AHan]

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

[Johan Commelin]

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

[Johan Commelin]

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

[AHan]

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

[AHan]

OH yes, renaming is a good suggestion!

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

And I think you don't need it.

[Johan Commelin]

You can define it for p = 1 just fine.

[AHan]

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

[Johan Commelin]

I guess p = 0 is problematic.

[Johan Commelin]

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

[AHan]

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?

[Johan Commelin]

No in mathlib.

[AHan]

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...

[Mario Carneiro]

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

[AHan]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[AHan]

@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 :=

[Johan Commelin]

Ok, what happens if you do not include pp?

[Johan Commelin]

Just don't make any assumptions on p.

[Johan Commelin]

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

[AHan]

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

[Johan Commelin]

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

[Johan Commelin]

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

[AHan]

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

[AHan]

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

[Johan Commelin]

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

[AHan]

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