char_p question

Stream: new members

[George McNinch]

Hi-- newbie here. Having finished the natural numbers game and skimming some tutorials, I started fiddling around and got stuck on the following point; maybe someone can get me unstuck?!

I wanted to understand how char_p works. So I did the following:

(I don't think I'll include the imports in this question for now at least).

variables (F : Type) [field F][char_p F 2]
variables a b c d: F

so I'm working in characteristic 2. I see that I can prove things like the following

example  : ↑2*a = 0 :=
   begin
     rw char_p.cast_eq_zero F 2,
     rw zero_mul,
   end

(Probably there is an easier way to do this, but I'll worry about that later!) What I don't see how to do is to get the "additive" form of this statement. I'd like to prove e.g.

example : a + a = 0

It seems that I should be able to "reverse engineer" this by looking e.g. at the proof of add_pow_char_of_commute, but I couldn't quite follow all that I was looking at. And I think I'm probably worried about "the easy bit" ...

Here is (one of the ways...) that I've started the proof of my example above:

example : a + a = 0:=
begin
  rw ← one_mul a,
  rw ← add_mul 1 1 a,
  rw one_add_one_eq_two,  -- at this point the goal reads  ⊢ 2 * a = 0
  -- -- one attempt (?)
  -- simp, -->  2=0 ∨ a =0
  -- left,  -->  2=0
  --  -- what are the types of the terms in that final equation??

  -- alternatively,  just trying to rewrite the 2 as 0 doesn't seem to work:
  -- rw char_p.cast_eq_zero F 2 -->  "did not find instance of pattern"
end

I guess that the issue is 2 vs ↑2, i.e. coercion. But I'm not quite sure how to handle it.
Explanations/thoughts/suggestions appreciated!

[Kevin Buzzard]

Please please please include the imports! Check out the #mwe link. Make it easier for us to help!

[Kevin Buzzard]

By the way, assuming you're using VS Code you can just click on the = in 2=0 in the infoview to see what the types of the terms are.

[Yaël Dillies]

I am guessing that you need docs#nat.cast_two.

[George McNinch]

@Yaël Dillies thanks! Indeed, this works:

example : a + a = 0:=
begin
  rw ← one_mul a,
  rw ← add_mul 1 1 a,
  simp,
  left,
  rw one_add_one_eq_two,
  rw ← nat.cast_two,
  rw char_p.cast_eq_zero F 2
end

Can I ask: prior to rewriting via nat.cast_two, is the term 2 * a obtained via nsmul :ℕ → F → F?? (Well, I'm not sure I've asked this question in a sensible way so am happy to be corrected).

[Yaël Dillies]

No, the 2 in 2 * a is 2 : F, not 2 : ℕ.

[George McNinch]

Huh -- thanks! So then what is the difference between ↑2 : F and 2 : F?

[George McNinch]

@Kevin Buzzard thanks; I'll aim for a MWE in future questions.
Also: I've been using emacs, just because I've used emacs for everything, for as long as I can remember. But maybe the VSCode support for lean is substantially better??

[George McNinch]

Surely there is some way to see those types in emacs...

[Yaël Dillies]

↑(2 : ℕ) : F means 0 + 1 + 1 while 2 : F means 1 + 1. Those are propositionally equal (you can produce a proof that they are equal) but not definitionally equal (replacing each thing by its definition does not turn the LHS into the RHS).

[Kevin Buzzard]

Yes, VS Code support for Lean is substantially better (for example you can see the type of every term in the goal view at the click of a button). [remark: I still use emacs for essentially everything, from writing papers to writing talks, because I know it back to front and I've been using it for 30 years, but I use VS Code for Lean]

[Mario Carneiro]

Also docs#two_mul is probably better to use here than one_add_one_eq_two

[George McNinch]

Right, I get why those two expressions aren't definitionally equal.

Is it true then that for n : ℕ, the application ↑n for some reason yields 0 + n : F (in my setting, at least)?

Or rather than guessing, maybe I should just ask where is the 0+ bit coming from?

Well, probably I should go read about coercion more carefully...; anyhow, thanks for answers!

[Yaël Dillies]

No, ↑n is 0 + 1 + ... + 1, while n is bit0 (bit1 ...) where bit0 a = a + a and bit1 a = a + a + 1.

[George McNinch]

@Mario Carneiro Thanks; indeed, I was pretty skeptical about one_add_one_eq_two. (I decided to triage that concern until I understood the other bit).

[Mario Carneiro]

here's a pretty simple proof using just what simp already knows about multiplication in a field

import algebra.char_p.basic

example {F} [field F] [char_p F 2] (a : F) : 2 * a = 0 :=
begin
  have := char_p.cast_eq_zero F 2,
  simp at this,
  simp [this],
end

[Kevin Buzzard]

import algebra.char_p.basic

example {F} [field F] [char_p F 2] (a : F) : 2 * a = 0 :=
begin
  have := char_p.cast_eq_zero F 2,
  simp * at *,
end

(only posting this because it's rare that I can golf Mario)

[George McNinch]

Great; thanks all.