Unwinding definitions involving if else

Stream: new members

[Jakob Scholbach]

I have defined a notion of a separable degree of a polynomial like so (F is a field):

def separable_degree (f : polynomial F) (p : ℕ) [HF : char_p F p] (n : ℕ) : Prop :=
  if p = 0 then
    polynomial.degree f = n
  else
    ∃ g : polynomial F,
    polynomial.degree g = n ∧
    g.separable ∧
    ∃ m : ℕ, (polynomial.expand F (p ^ m)) g = f

Now, in the middle of some proof, given assumptions h : separable_degree F f p n,, p = 0 and char_p F 0, I would like to unwind it to get polynomial.degree f = n. How do I do this? Attempting a rw command does not seem to work. Thanks!

Maybe related question: I noticed that the definition of char_p is a class (not a def). Is there a (practical) difference between these two approaches?

[Jakob Scholbach]

P.S. if there are somehow more efficient ways of encoding the same definition, I'd be happy to learn about this as well.

[Eric Wieser]

For the specific case of p = 0 you might do better to split into zero and succ using pattern matching

[Huỳnh Trần Khanh]

For ite (if-then-else) expressions you can always use split_ifs. Though I think pattern matching is a better way to define this.

[Huỳnh Trần Khanh]

To each their own, and ite is a perfectly valid way of doing things.

[Adam Topaz]

For this definition, maybe it would be better to define the exponential characteristic of a field, and when making the definition above, use that so you no longer have an if_then_else.

[Adam Topaz]

I feel like having this exponential characteristic and some small API around it would be useful anyway

[Johan Commelin]

@Jakob Scholbach After making such a definition (no matter whether you use the equation compiler, or if .. then .. else .. I would write two lemmas:

lemma separable_degree_of_char_zero (f : polynomial F) (n : ℕ) [char_p F 0] :
  separable_degree f 0 n \iff polynomial.degree f = n :=
begin
  rw [if_pos rfl],
  refl
end

lemma separable_degree_of_char_pos (f : polynomial F) (p  : ℕ) (hp : 0 < p) [char_p F p] (n : ℕ) :
  separable_degree f p n \iff \exists g, etc etc :=
begin
  rw [if_neg], -- 2 goals
  { refl },
  { /- prove that p \ne 0 if 0 < p, which should be nat.pos_iff_ne_zero, or so -/ }
end

[Johan Commelin]

On the other hand... I think that Adam's idea is also a good one.

[Johan Commelin]

Another thing to consider is whether you want a definition of separable_degree that spits out n, instead of taking f and n as inputs, and spitting out true/false

[Eric Wieser]

Presumably using docs#nat.find for the else branch?

[Jakob Scholbach]

Johan Commelin said:

Another thing to consider is whether you want a definition of separable_degree that spits out n, instead of taking f and n as inputs, and spitting out true/false

Yes, in my mind it would be more natural / more easy to use later on, if there is a function roughly like def separable_degree (f : polynomial F) : \N. I oriented myself with the setup of the characteristic of a field in algebra.char_p.basic which "only" spits out a proposition. I personally find it somewhat cumbersome to use that approach, but I was not sure why it had been implemented there in this indirect way and if something prevents me from coming up with a definition that somehow in the middle uses the existence-and-unicity of a number with a certain property. Do you have some advice on that?

[Eric Wieser]

char_p is the way it is because it used a typeclass, and is a property of a type, not a particular value within that type. We could have gone for [fact (char_p R = 0)] instead, but that's less desirable for a number of reasons

[Jakob Scholbach]

Hm, still being very new to all this I'm not sure I really understand what you are alluding to. Do you mind elaborating a bit? -- what are the downsides of directly having a function that assigns some n : \N to a field? Which of these downsides apply / don't apply to the situation with the separable degree?

[Johan Commelin]

Another benefit is that you can reuse literally the same p for many rings. Otherwise you might have to rewrite quite often to show that ring_char (zmod p) = ring_char (polynomial (zmod p)) = ring_char (algebraic_closure (zmod p)) = ...

[Johan Commelin]

And sometimes those rewrites will be in places where Lean doesn't like to rewrite.

[Johan Commelin]

So it's quite useful down the road to just have the same p everywhere, it saves contentless effort

[Johan Commelin]

On the other hand, the degree of a polynomial is of a different nature, you don't typically consider many constructions that preserve the degree

[Jakob Scholbach]

Oh, I embarassingly didn't know that there is the function ring_char, so my complaint was somehow not quite to the point! That said, is there some tutorial etc. with some minimal working examples describing the ramifications of the way such things are set up? As a rule of thumb, what I am taking from your answers, @Eric Wieser and @Johan Commelin , is that using the output of a function is less advisable when the result of the function will be be used "a lot" because I would need to reverse-compile the definition of the function whenever I really want to use the output, and in this case it is more efficient to make it a property of a type?

[Johan Commelin]

It's somehow similar to constructions like fraction_field. You need a construction, because otherwise you don't know it exists. But you also want to be able to be able to treat Q as the fraction field of Z. But it isn't equal to fraction_field Z, only isomorphic.

[Johan Commelin]

So you prove everything using two rings and a predicate that one is the fraction field of the other.

[Johan Commelin]

Which often makes the proofs easier (but you need an mathematically-artificial variables line at the top of your file) and it also makes it easier to apply this.

[Johan Commelin]

ring_char exists, but I don't think it is used a lot in mathlib

[Jakob Scholbach]

@the analogy between fraction fields and characteristic: it the datum of an isomorphism Q \cong Frac(Z) akin to the datum of providing a proof of an equation such as ring_char (zmod p) = ring_char (polynomial (zmod p))?

[Jakob Scholbach]

(metaphorically speaking, of course)

[Johan Commelin]

yes, but it will be even harder to use, because it is not an equality but an isom

[Jakob Scholbach]

OK, thanks. That was a useful lesson!