Michael Stoll / confusion with addition

Stream: new members

[Michael Stoll]

Hi, I am Michael Stoll; I am a math professor working in Arithmetic Geometry with a focus on how to compute things like rational points. I've been tangentially interested in formalizing math for a while and decided that I would now try it a bit more seriously (by supervising students formalizing stuff :smile:). To get a feeling for what working with Lean is like, I've been playing around a bit. Doing so, I encountered the following:

import data.rat.basic
import data.real.basic

namespace experiment

def Q_or_R : bool → Type
| tt := ℚ
| ff := ℝ

@[instance]
def ring_Q_or_R (b : bool) : ring (Q_or_R b) :=
begin
  cases b,
    exact real.ring,
  unfold Q_or_R, exact comm_ring.to_ring ℚ,
end

lemma comm (b : bool) (x y : Q_or_R b) : x + y = y + x :=
begin
  have h₁ := (ring_Q_or_R b),
  have h := h₁.add_comm,
  exact h x y,
end

lemma comm' (b : bool) (x y : Q_or_R b) : x + y = y + x :=
begin
  have h := (ring_Q_or_R b).add_comm,
  exact h x y,
end

end experiment

In the attempted proof of lemma comm, I get an error message at the last step, which says

invalid type ascription, term has type
  @eq (experiment.Q_or_R b)
    (@has_add.add (experiment.Q_or_R b)
       (@add_semigroup.to_has_add (experiment.Q_or_R b)
          (@add_semigroup.mk (experiment.Q_or_R b) (@ring.add (experiment.Q_or_R b) h₁) _))
       x
       y)
    (@has_add.add (experiment.Q_or_R b)
       (@add_semigroup.to_has_add (experiment.Q_or_R b)
          (@add_semigroup.mk (experiment.Q_or_R b) (@ring.add (experiment.Q_or_R b) h₁) _))
       y
       x)
but is expected to have type
  @eq (experiment.Q_or_R b)
    (@has_add.add (experiment.Q_or_R b)
       (@distrib.to_has_add (experiment.Q_or_R b) (@ring.to_distrib (experiment.Q_or_R b) (experiment.ring_Q_or_R b)))
       x
       y)
    (@has_add.add (experiment.Q_or_R b)
       (@distrib.to_has_add (experiment.Q_or_R b) (@ring.to_distrib (experiment.Q_or_R b) (experiment.ring_Q_or_R b)))
       y
       x)
state:
b : bool,
x y : Q_or_R b,
h₁ : ring (Q_or_R b),
h : ∀ (a b_1 : Q_or_R b), a + b_1 = b_1 + a
⊢ x + y = y + x

whereas the proof of comm' goes through.

Can someone explain what is going on here? And, perhaps more importantly, what is the correct way of getting Lean to realize that Q_or_R b is a ring (or a field...) and should be treated as such?

[Riccardo Brasca]

What you are trying to do it is probably a little complicated. If you really want to play with something that is ℝ or ℚ you can try to copy what it is done for docs#is_R_or_C.

Have you a specific reason to do that? Otherwise I would suggest to just go with ℚ, or any field/ring.

[Michael Stoll]

What I am really trying to do is having something like completion_of_ℚ v, where v is something encoding a place of ℚ (which can be infinite, then the completion is ℝ, or finite, then it is the field ℚ_p of p-adic numbers for some prime number p).
Thanks for the pointer. To the beginner's eye, the definition of is_R_or_C does also look fairly complicated...
But I also would like to understand what is going on behind the scenes in my example. Why does comm' work, while comm does not? One would think that both proofs are equivalent.

[Heather Macbeth]

Note that is_R_or_C really axiomatizes a set of properties possessed by $\mathbb{R}$ and $\mathbb{C}$, rather than making an inductive type which puts the two together.

[Johan Commelin]

@Michael Stoll Note that completion of a valuation already exists. Are you looking for a way to uniformly treat these completions? Presumably you would need to prove theorems about complete (normed?) fields, or something like that.

[Michael Stoll]

As a very basic first step, I would like to be able to do computations in these fields in a uniform way (i.e., using rw with field axioms or the ring tactic). Since mathlib has (reals and) p-adic fields, the necessary properties for each individual field should be available, so I would hope that one can just use that in some way.

[Riccardo Brasca]

As a general trick, if exact foo doesn't work, you can try convert foo, that transforms what went wrong in goals. If you get like 28 goals, then it means something is probably false.

[Johan Commelin]

@Michael Stoll

lemma comm (b : bool) (x y : Q_or_R b) : x + y = y + x :=
begin
  let h₁ := (ring_Q_or_R b), -- `let` instead of `have`
  have h := h₁.add_comm,
  exact h x y,
end

[Johan Commelin]

You need let, because ring includes the data about addition/mutliplication/etc...

[Johan Commelin]

have is only for propositions, it forgets all the data.

[Michael Stoll]

OK, thanks!

[Michael Stoll]

(Right now, I'm struggling to prove that ¬1 = 0 where 0 and 1 are rationals...)

[Eric Rodriguez]

norm_num is your friend!

[Yaël Dillies]

I doubt is_R_or_C is a model to follow. It's mostly a bunch of ad hoc axioms put together. I hope we get rid of it eventually.

[Riccardo Brasca]

I agree is_R_or_C is not optimal, but its existence shows it's not easy to work with something that "is ℝ or ℂ".

[Michael Stoll]

norm_num does not appear to work here: norm_num failed to simplify.

[Eric Rodriguez]

can you post a #mwe?

[Michael Stoll]

Sorry, I realized that my 0 and 1 are living somewhere else (in a completion of ℚ ...).

[Frédéric Dupuis]

Yaël Dillies said:

I doubt is_R_or_C is a model to follow. It's mostly a bunch of ad hoc axioms put together. I hope we get rid of it eventually.

It could probably be replaced by something like has_imaginary_unit that provides I and some prop typeclasses, but it looks like a lot of effort for not a whole lot of gains.

[Heather Macbeth]

Or "simultaneously a a finite-dimensional extension field of ℝ and a star_ring, with the star fixing only ℝ", but again
Frédéric Dupuis said:

it looks like a lot of effort for not a whole lot of gains.

[Riccardo Brasca]

BTW @Michael Stoll maybe you can just define Q_or_R as an inductive type with only two constructors, one for ℚ and one for ℝ. (It's morally the same as you have now.)

[Michael Stoll]

Is there a theorem somewhere that 1 ≠ 0 in a field?

[Riccardo Brasca]

docs#zero_ne_one

[Riccardo Brasca]

With some symm

[Riccardo Brasca]

Even better, we have docs#one_ne_zero

[Michael Stoll]

@Riccardo Brasca I'm essentially doing this in my actual code:

def completion_of_ℚ : plcℚ → Type
| infty := ℝ
| (finpl p h) := by exactI padic p

[Michael Stoll]

Thanks again. I guess I should have searched for "one_ne_zero" or similar in the docs...

[Riccardo Brasca]

Yes, understanding the name convention is an important skill... at the beginning it's not very easy to get used to it, but it works very well

[Alex J. Best]

We have some docs on it at https://leanprover-community.github.io/contribute/naming.html, using this and the search in vscode (essentially grep with regex) and finally tactic#library_search are the most efficient ways of finding lemmas (maybe even in that order!)

[Yakov Pechersky]

I haven't seen a lot of success on types defined via coproducts or their equivalent. So I'm interested to hear about your progress and results!

[Reid Barton]

The sensitivity conjecture proof does something in the same vein, https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean#L148 and following

[Yakov Pechersky]

That's cool, thanks Reid! But a little different, since many of the proofs are valid through induction on the index, not just casing on tt ff

[Yakov Pechersky]

Is it the case there is some result where the results of the finite completions lead to a proof of the infinite completions?

[Michael Stoll]

@Yakov Pechersky I'm still very much at the beginning and trying to find my way. I'll post something here when I have results (but more likely, I'll post some more questions before I get there...).

[Johan Commelin]

Yakov Pechersky said:

Is it the case there is some result where the results of the finite completions lead to a proof of the infinite completions?

There are some connections, yes! For example $∏_{v} ∥x∥_v = 1$, where $v$ runs over all the finite and infinite valuations. In other words, if you have a rational number, and you take the product of all it's p-adic norms, then you get ∥(x : ℝ)∥⁻¹.

[Johan Commelin]

This means that you can compute one of the norms, if you know all the others. A more high-brow version of this is true for quadratic forms over ℚ: if you know all the Hilbert symbols are all-but-one of the completions, then you can compute the final one. And this is actually useful! It is an important ingredient in Ancona's proof of Grothendieck's "standard conjecture of Hodge type" for abelian fourfolds. (This was a recent advancement after decades of "no progress at all".)

[Michael Stoll]

Hilbert symbols (and in particular, their product formula) are actually what I am after here.

[Kevin Buzzard]

Just over Qp or general local fields?

[Michael Stoll]

Over ℚ_p and ℝ for starters.

[Michael Stoll]

Here is a question related to ite. Say, I have a term containing ite P a b and I have an assumption h : P in my state. I would like to rewrite ite P a b into a. So I was looking for a lemma in mathlib that says something like

lemma ite_left_of_cond {α : Type} (P : Prop) [decidable P] (x y : α) : P → ite P x y = x := ...

so that I can do rw ite_left_of_cond P x y h. But this does not seem to exist in this form.
It is not hard to prove this from what is in mathlib (from ite_eq_iff, say), but I was wondering why such an obvious-looking statement is not there. The statements that are there (like, e.g., ite_eq_left_iff) have, to my inexperienced eyes, a more conrived and less easy-to-use appearance.
But maybe there is a better way to do what I want, and that's why nobody misses ite_left_of_cond?

[Kyle Miller]

I usually reach for simp [h] first, then maybe try to find the right lemma later. It ends up being docs#if_pos

A way to find it:

import tactic

lemma ite_left_of_cond {α : Type} (P : Prop) [decidable P] (x y : α) (h : P) : ite P x y = x :=
begin
  library_search
end

[Michael Stoll]

library_search timed out on this.

[Kevin Buzzard]

Did you have the decidability assumption?

[Michael Stoll]

Thanks for the pointer to if_pos. Why are some statements dealing with ite named if_... rather than ite_...? It doesn't make it easier to find what you need...

[Kyle Miller]

Did you run the code I posted, or did you try it with yours? With mine, I made sure to put the h : P before the colon.

[Michael Stoll]

OK, sorry, I missed the subtle difference between having he assumption before or after the colon.

[Kyle Miller]

The way library_search works, as I understand it, is that it tries to apply everything in the entire library, which is why there's a difference here.

[Kevin Buzzard]

Michael Stoll said:

Thanks for the pointer to if_pos. Why are some statements dealing with ite named if_... rather than ite_...? It doesn't make it easier to find what you need...

It might be because things like if_true are in core; mathlib is much better at sticking to the naming conventions.

[Michael Stoll]

(In fact, if_pos and if_neg are in core as well.)

[Kyle Miller]

Michael Stoll said:

Why are some statements dealing with ite named if_... rather than ite_...?

There's notation for ite P x y that's commonly used: if P then x else y. You can find lemmas having to do with if h : P then x else y under dif or dite, too, for "dependent if" or "dependent if-then-else".