Zulip Chat Archive

Stream: new members

Topic: Michael Stoll / confusion with addition


Michael Stoll (Feb 17 2022 at 16:13):

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 (Feb 17 2022 at 16:21):

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 (Feb 17 2022 at 16:30):

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 (Feb 17 2022 at 16:31):

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

Johan Commelin (Feb 17 2022 at 16:35):

@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 (Feb 17 2022 at 16:39):

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 (Feb 17 2022 at 16:39):

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 (Feb 17 2022 at 16:39):

@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 (Feb 17 2022 at 16:40):

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

Johan Commelin (Feb 17 2022 at 16:40):

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

Michael Stoll (Feb 17 2022 at 16:41):

OK, thanks!

Michael Stoll (Feb 17 2022 at 16:42):

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

Eric Rodriguez (Feb 17 2022 at 16:48):

norm_num is your friend!

Yaël Dillies (Feb 17 2022 at 16:50):

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 (Feb 17 2022 at 16:51):

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 (Feb 17 2022 at 16:53):

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

Eric Rodriguez (Feb 17 2022 at 16:54):

can you post a #mwe?

Michael Stoll (Feb 17 2022 at 16:55):

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

Frédéric Dupuis (Feb 17 2022 at 16:55):

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 (Feb 17 2022 at 17:00):

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 (Feb 17 2022 at 17:03):

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 (Feb 17 2022 at 17:03):

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

Riccardo Brasca (Feb 17 2022 at 17:04):

docs#zero_ne_one

Riccardo Brasca (Feb 17 2022 at 17:04):

With some symm

Riccardo Brasca (Feb 17 2022 at 17:04):

Even better, we have docs#one_ne_zero

Michael Stoll (Feb 17 2022 at 17:04):

@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 (Feb 17 2022 at 17:06):

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

Riccardo Brasca (Feb 17 2022 at 17:07):

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 (Feb 17 2022 at 21:47):

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 (Feb 18 2022 at 02:59):

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 (Feb 18 2022 at 03:06):

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 (Feb 18 2022 at 03:09):

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 (Feb 18 2022 at 03:14):

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 (Feb 18 2022 at 19:22):

@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 (Feb 19 2022 at 05:34):

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 vxv=1∏_{v} ∥x∥_v = 1, where vv 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 (Feb 19 2022 at 05:37):

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 (Feb 19 2022 at 09:58):

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

Kevin Buzzard (Feb 19 2022 at 12:02):

Just over Qp or general local fields?

Michael Stoll (Feb 19 2022 at 18:38):

Over ℚ_p and ℝ for starters.

Michael Stoll (Feb 20 2022 at 18:59):

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 (Feb 20 2022 at 19:02):

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 (Feb 20 2022 at 19:03):

library_search timed out on this.

Kevin Buzzard (Feb 20 2022 at 19:05):

Did you have the decidability assumption?

Michael Stoll (Feb 20 2022 at 19:05):

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 (Feb 20 2022 at 19:05):

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 (Feb 20 2022 at 19:07):

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

Kyle Miller (Feb 20 2022 at 19:07):

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 (Feb 20 2022 at 19:09):

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 (Feb 20 2022 at 19:40):

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

Kyle Miller (Feb 20 2022 at 19:48):

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


Last updated: Dec 20 2023 at 11:08 UTC