## Stream: new members

### Topic: Unwinding definitions involving if else

#### Jakob Scholbach (Feb 28 2021 at 14:28):

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 (Feb 28 2021 at 14:28):

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 (Feb 28 2021 at 15:18):

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 (Feb 28 2021 at 15:45):

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 (Feb 28 2021 at 15:46):

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

#### Adam Topaz (Feb 28 2021 at 15:58):

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 (Feb 28 2021 at 15:58):

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

#### Johan Commelin (Mar 01 2021 at 06:57):

@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 (Mar 01 2021 at 06:58):

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

#### Johan Commelin (Mar 01 2021 at 06:58):

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 (Mar 01 2021 at 07:01):

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

#### Jakob Scholbach (Mar 01 2021 at 08:06):

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 (Mar 01 2021 at 08:11):

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 (Mar 01 2021 at 08:18):

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 (Mar 01 2021 at 08:21):

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 (Mar 01 2021 at 08:21):

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

#### Johan Commelin (Mar 01 2021 at 08:22):

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

#### Johan Commelin (Mar 01 2021 at 08:22):

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 (Mar 01 2021 at 08:35):

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 (Mar 01 2021 at 08:38):

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 (Mar 01 2021 at 08:38):

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

#### Johan Commelin (Mar 01 2021 at 08:39):

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 (Mar 01 2021 at 08:39):

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

#### Jakob Scholbach (Mar 01 2021 at 08:46):

@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 (Mar 01 2021 at 08:46):

(metaphorically speaking, of course)

#### Johan Commelin (Mar 01 2021 at 08:51):

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

#### Jakob Scholbach (Mar 01 2021 at 08:56):

OK, thanks. That was a useful lesson!

Last updated: May 08 2021 at 10:12 UTC