# Zulip Chat Archive

## Stream: maths

### Topic: cast woes

#### Johan Commelin (Mar 13 2019 at 11:52):

It's quite humiliating, but how do I kill:

example (p : ℕ) [p.prime] : (p : ℝ) > 1 := sorry

#### Kenny Lau (Mar 13 2019 at 11:54):

import data.nat.prime data.real.basic universes u example (p : ℕ) [p.prime] : (p : ℝ) > 1 := show _ < _, by rw [← nat.cast_one, nat.cast_lt]; apply nat.prime.gt_one; assumption

#### Mario Carneiro (Mar 13 2019 at 11:54):

`pp.gt_one`

?

#### Kenny Lau (Mar 13 2019 at 11:55):

why is `[p.prime]`

an instance though

#### Johan Commelin (Mar 13 2019 at 11:55):

We really need a `cast`

tactic.

#### Kenny Lau (Mar 13 2019 at 11:55):

and also why does `data.nat.prime`

use ge and gt @Mario Carneiro

#### Johan Commelin (Mar 13 2019 at 11:56):

@Kenny Lau Thanks

#### Mario Carneiro (Mar 13 2019 at 11:57):

I guess it's a bit more natural to read `prime.gt_one`

? not a strong argument

#### Mario Carneiro (Mar 13 2019 at 11:57):

you can make them all le and lt if you want

#### Johan Commelin (Mar 13 2019 at 12:00):

I would love to be able to prove this via

suffices : (1 : nat) < (p : nat), { cast_magic using this }, ...

#### Kevin Buzzard (Mar 13 2019 at 12:37):

Did you read my docs on cast?

#### Kevin Buzzard (Mar 13 2019 at 12:37):

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/casts.md

#### Johan Commelin (Mar 13 2019 at 12:38):

Yes, I read those... but I guess I also forgot them

#### Kevin Buzzard (Mar 13 2019 at 12:38):

I feel like at least there's an algorithm in there, even if not a tactic

#### Kevin Buzzard (Mar 13 2019 at 12:38):

I wrote them, and I certainly also forgot them.

#### Kevin Buzzard (Mar 13 2019 at 12:38):

That's why I wrote them :-)

#### Kevin Buzzard (Mar 13 2019 at 13:01):

My docs don't seem to help.

#### Kevin Buzzard (Mar 13 2019 at 13:01):

"1=1" can be proved by simp, but for `a<b iff a<b`

it helps a lot if you know the statement of the lemma.

#### Kevin Buzzard (Mar 13 2019 at 13:01):

`simp`

uses this:

@[simp] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n := int.coe_nat_eq_coe_nat_iff m n

Actually I don't understand this. What does `simp`

to do goals of the form `X -> Y`

? It tries to simplify `X`

and `Y`

and then sees if it has got lucky and the goal has become `Z -> Z`

?

#### Kevin Buzzard (Mar 13 2019 at 13:01):

This works now:

example (q r : ℕ) : (q : ℤ) = r → q = r := by simp

It didn't used to, apparently. But I am a bit weirded out by this -- I thought that it wasn't `simp`

s job to prove this sort of thing? It's an implication, not an iff or an equality.

#### Kevin Buzzard (Mar 13 2019 at 13:01):

import data.real.basic example (p : ℕ) (h : (1 : nat) < (p : nat)) : (1 : ℝ) < p := begin suffices : ((1 : ℕ) : ℝ) < p, simpa using this, rwa nat.cast_lt, end

It wasn't hard for me to construct a proof, but I had to know the general route.

#### Kevin Buzzard (Mar 13 2019 at 13:01):

`simp`

uses this:

@[simp] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n := int.coe_nat_eq_coe_nat_iff m n

Actually I don't understand this. What does `simp`

to do goals of the form `X -> Y`

? It tries to simplify `X`

and `Y`

and then sees if it has got lucky and the goal has become `Z -> Z`

?

Oh -- ha ha --

@[simp] theorem imp_self : (a → a) ↔ true := iff_true_intro id

#### Kevin Buzzard (Mar 13 2019 at 13:01):

import data.real.basic example (p : ℕ) (h : (1 : nat) < (p : nat)) : (1 : ℝ) < p := begin suffices : ((1 : ℕ) : ℝ) < p, simpa using this, revert h, suffices : ((1 : ℕ) : ℝ) < p ↔ 1 < p, exact this.2, -- ⊢ ↑1 < ↑p ↔ 1 < p simp, -- gaargh you stupid algorithm -- ⊢ 1 < ↑p ↔ 1 < p sorry end -- @[simp] theorem nat.cast_lt [linear_ordered_semiring α] {m n : ℕ} : -- (m : α) < n ↔ m < n := ...

#### Kevin Buzzard (Mar 13 2019 at 13:10):

It's a bit of a challenge to make `simp`

use `nat.cast_lt`

apparently. Can this be fixed somehow? I was seeing if I could construct a proof which did not involve needing to know the name of `nat.cast_lt`

but just relied on the fact that it was a simp lemma.

#### Kevin Buzzard (Mar 13 2019 at 13:11):

I want `nat.cast_lt`

to have greater precedence than \u 1 = 1.

#### Mario Carneiro (Mar 13 2019 at 13:12):

it's not a question of precedence, it's that 1 is not \u 1

#### Mario Carneiro (Mar 13 2019 at 13:12):

`simp`

cannot solve cast problems, it's just not an appropriate tool

#### Kevin Buzzard (Mar 13 2019 at 13:12):

If I change 1 to `q`

it works.

#### Mario Carneiro (Mar 13 2019 at 13:13):

it will sometimes get lucky but that's all it is

#### Kevin Buzzard (Mar 13 2019 at 13:13):

I see.

#### Kevin Buzzard (Mar 13 2019 at 13:14):

I don't really understand why `simp`

doesn't solve it.

#### Kevin Buzzard (Mar 13 2019 at 13:14):

It is exactly `nat.cast_lt`

, no?

#### Mario Carneiro (Mar 13 2019 at 13:14):

what?

#### Kevin Buzzard (Mar 13 2019 at 13:14):

-- ⊢ ↑1 < ↑p ↔ 1 < p simp, -- gaargh you stupid algorithm -- ⊢ 1 < ↑p ↔ 1 < p

#### Mario Carneiro (Mar 13 2019 at 13:15):

`1 < ↑p ↔ 1 < p`

is defeq to an application of `nat.cast_lt`

, but the pattern `↑?M1 < ↑?M2`

doesn't match syntactically

#### Kevin Buzzard (Mar 13 2019 at 13:15):

I made it match syntactically, no?

#### Kevin Buzzard (Mar 13 2019 at 13:16):

I got 1 into \u 1 form

#### Kevin Buzzard (Mar 13 2019 at 13:16):

simp sent it back

#### Mario Carneiro (Mar 13 2019 at 13:16):

Oh I see

#### Kevin Buzzard (Mar 13 2019 at 13:16):

So is it a question of precedence?

#### Mario Carneiro (Mar 13 2019 at 13:16):

The problem is that `nat.cast_lt`

is not in a simp normal form, so it rarely triggers

#### Mario Carneiro (Mar 13 2019 at 13:17):

`simp`

is not confluent as a result

#### Mario Carneiro (Mar 13 2019 at 13:18):

The honest approach would just be to have `nat.cast_lt`

not be a simp rule at all, but it works opportunistically sometimes

#### Kevin Buzzard (Mar 13 2019 at 13:19):

example (p q : ℕ) (h : (q : nat) < (p : nat)) : (q : ℝ) < p := begin suffices : ((q : ℕ) : ℝ) < p, simpa using this, revert h, suffices : ((q : ℕ) : ℝ) < p ↔ q < p, exact this.2, simp, end

That works, which is kind of cool, because it meant that I didn't need to know the names of any obscure lemmas.

#### Mario Carneiro (Mar 13 2019 at 13:19):

names of any obscure lemmas

You mean "names of anything at all", right?

#### Mario Carneiro (Mar 13 2019 at 13:20):

These are not difficult names

#### Mario Carneiro (Mar 13 2019 at 13:20):

there is much worse than this in the library

#### Kevin Buzzard (Mar 13 2019 at 13:20):

:-)

#### Kevin Buzzard (Mar 13 2019 at 13:20):

To a beginning maths undergraduate, they're all obscure lemmas :-)

#### Kevin Buzzard (Mar 13 2019 at 13:21):

To me, they're a little obscure because some have `cast`

and some have `coe`

#### Mario Carneiro (Mar 13 2019 at 13:21):

This is unfortunate; most of the `coe`

names have to do with coercions from nat to int in core

#### Johan Commelin (Mar 13 2019 at 13:34):

I really don't like these goals.

example (p : ℕ) [p.prime] (n : ℤ) : (((p : ℚ) ^ -n) : ℝ) = (p : ℝ) ^ -n := sorry

#### Kevin Buzzard (Mar 13 2019 at 13:39):

I don't think you need that p is prime there

#### Kevin Buzzard (Mar 13 2019 at 13:39):

;-)

#### Kevin Buzzard (Mar 13 2019 at 13:39):

Did you read my docs about cast?

#### Johan Commelin (Mar 13 2019 at 13:44):

Kevin, I'd rather not prove these things by hand. Even if I can after reading a bunch of docs etc... I'm providing motivation for tactic-writers (-;

#### Patrick Massot (Mar 13 2019 at 14:22):

They don't need motivation, they need pity

#### Rob Lewis (Mar 13 2019 at 14:25):

I haven't fully read this thread (and I can't right now, I need to run in two minutes). But: we have a new intern in Amsterdam, as of last week, who's probably going to think about a cast tactic as his first project. We have some ideas about how to proceed. But if you have thoughts, desiderata, etc, put a list together for us.

#### Johan Commelin (Mar 13 2019 at 15:03):

Awesome!

#### Kevin Buzzard (Mar 13 2019 at 15:56):

@Rob Lewis a general spec would be "if a mathematician who thinks $\mathbb{N}\subset\mathbb{Z}\subset\mathbb{Q}\subset\mathbb{R}\mathbb{C}$ can't figure out why something even needs to be proved here, the tactic should prove it. I would be very interested in working with you or others on making a more formal spec, because I do not really understand what goes into the process and yet I feel like I have some understanding of what we mathematicians are missing. Should I just formalise some unit tests?

#### Kevin Buzzard (Mar 13 2019 at 16:49):

import data.complex.basic -- ℕ, ℤ, ℚ, ℝ, ℂ variables (an bn cn dn : ℕ) (az bz cz dz : ℤ) (aq bq cq dq : ℚ) variables (ar br cr dr : ℝ) (ac bc cc dc : ℂ) example : (an : ℤ) = bn → an = bn := sorry example : an = bn → (an : ℤ) = bn := sorry example : az = bz ↔ (az : ℚ) = bz := sorry example : (aq : ℝ) = br ↔ (aq : ℂ) = br := sorry example : (an : ℚ) = bz ↔ (an : ℂ) = bz := sorry example : (((an : ℤ) : ℚ) : ℝ) = bq ↔ ((an : ℚ) : ℂ) = (bq : ℝ) := sorry example : (an : ℤ) < bn ↔ an < bn := sorry example : (an : ℚ) < bz ↔ (an : ℝ) < bz := sorry example : ((an : ℤ) : ℝ) < bq ↔ (an : ℚ) < bq := sorry -- zero and one cause special problems example : 0 < (bq : ℝ) ↔ 0 < bq := sorry example : aq < (1 : ℕ) ↔ (aq : ℝ) < (1 : ℤ) := sorry example : (an : ℤ) + bn = (an + bn : ℕ) := sorry example : (an : ℂ) + bq = ((an + bq) : ℚ) := sorry example : (((an : ℤ) : ℚ) : ℝ) + bn = (an + (bn : ℤ)) := sorry example : (((((an : ℚ) : ℝ) * bq) + (cq : ℝ) ^ dn) : ℂ) = (an : ℂ) * (bq : ℝ) + cq ^ dn := sorry example : ((an : ℤ) : ℝ) < bq ∧ (cr : ℂ) ^ 2 = dz ↔ (an : ℚ) < bq ∧ ((cr ^ 2) : ℂ) = dz := sorry

There are some example goals. Some, but not all, can be solved with `simp`

. One or two might be even solvable with `rfl`

. I got a bit silly with the last one in the sense that I introduced \and -- this just shows my inexperience with this sort of thing. I don't know what is reasonable. What is reasonable? If you give me a subset of these things, I can tell you how I would prove them following the tricks I've picked up. Problems such as this were constantly showing up last summer when I was working with a team of undergraduates solving undergraduate level mathematics problems -- you might think some of the examples are artificial but when students have a question about natural numbers and they start subtracting and dividing, they do drift into Z and Q, and I would sometimes see \u \u as a consequence.

#### Kevin Buzzard (Mar 13 2019 at 16:52):

I don't even know if \iff is asking more than one might naturally expect a tactic to deliver. Rob I would be very happy to work with you on developing a spec, but of course I can tell you nothing about tactic design. Even a tactic which only proves one-way implications and equalities would be useful, but I have seen with my own eyes that mathematicians sometimes want one-way implications and sometimes two-way ones.

#### Rob Lewis (Mar 14 2019 at 08:49):

Thanks, Kevin. This is a good start. The `\u \u`

examples are definitely not trivial, I come across those often enough too.

#### Rob Lewis (Mar 14 2019 at 08:50):

We'll come back and talk about a formal spec once Paul-Nicolas has made some more progress, but these examples help a lot for the moment.

#### Patrick Massot (Mar 26 2019 at 10:36):

One more data point about casts and stupid arithmetic goal. This afternoon I want students to prove that if `f : ℝ → ℝ`

sequentially tends to `y₀`

at `x₀`

then it tends to `y₀`

en `x₀`

. I almost gave on this idea, although this is the perfect illustration for the current chapter (negation of quantified statements). I ended writing in the assignment Lean file:

axiom limite_inv_succ : ∀ ε > 0, ∃ N : ℕ, ∀ n ≥ N, 1/(n+1 : ℝ) ≤ ε axiom inv_succ_pos : ∀ n : ℕ, 1/(n+1 : ℝ) > 0

because I couldn't see a way to prove them without devoting a whole lecture to casts and coes.

#### Neil Strickland (Mar 26 2019 at 10:42):

I've been doing some basic undergraduate exercises. I think that this one is a good test case for the cast infrastructure:

/- We are asked to pass judgement on the following "definition" : k : ℝ → ℤ sends x ∈ ℝ to the closest integer. We define precisely what it means for n to be the closest integer to x : we should have | x - m | > | x - n | for any integer m ≠ n. We then show that if m ∈ ℤ, there is no closest integer to m + 1/2. From this we deduce that there is no function k with the expected properties. This is much harder work than you might think. A lot of the problem is caused by the cast maps ℤ → ℚ → ℝ -/ def is_closest_integer (n : ℤ) (x : ℝ) := ∀ m : ℤ, m ≠ n → abs ( x - m ) > abs ( x - n ) /- Even basic identities like 1/2 - 1 = -1/2 cannot easily be proved directly in ℝ, because there are no general algorithms for exact calculation in ℝ. We need to work in ℚ and then apply the cast map. -/ def half_Q : ℚ := 1 / 2 def neg_half_Q : ℚ := - half_Q noncomputable def half_R : ℝ := half_Q noncomputable def neg_half_R : ℝ := neg_half_Q /- Here is a small identity that could in principle be proved by a long string of applications of the commutative ring axioms. The "ring" tactic automates the process of finding this string. For reasons that I do not fully understand, the ring tactic seems to work more reliably if we do it in a separate lemma so that the terms are just free variables. We can then substitute values for this variables as an extra step. In particular, we will substitute h = 1/2, and then give a separate argument that the final term 2 * h - 1 is zero. -/ lemma misc_identity (m n h : ℝ) : (m + h) - (2 * m + 1 - n) = - ((m + h) - n) + (2 * h - 1) := by ring /- We now prove that there is no closest integer to m + 1/2. The obvious approach would be to focus attention on the candidates n = m and n = m + 1, but it turns out that that creates more work than necessary. It is more efficient to prove that for all n, the integer k = 2 m + 1 - n is different from n and lies at the same distance from m + 1/2, so n does not have the required property. -/ lemma no_closest_integer (n m : ℤ) : ¬ (is_closest_integer n ((m : ℝ) + half_R)) := begin intro h0, let x_Q : ℚ := (m : ℚ) + half_Q, let x_R : ℝ := (m : ℝ) + half_R, let k := 2 * m + 1 - n, by_cases e0 : k = n, {-- In this block we consider the possibility that k = n, and -- show that it is impossible. exfalso, dsimp[k] at e0, let e1 := calc (1 : ℤ) = (2 * m + 1 + -n) + n - 2 * m : by ring ... = n + n - 2 * m : by rw[e0] ... = 2 * (n - m) : by ring, have e2 := calc (1 : ℤ) = int.mod 1 2 : rfl ... = int.mod (2 * (n - m)) 2 : congr_arg (λ x, int.mod x 2) e1 ... = 0 : int.mul_mod_right 2 (n - m), exact (dec_trivial : (1 : ℤ) ≠ 0) e2, },{ let h1 := ne_of_gt (h0 k e0), let u_R := x_R - n, let v_R := x_R - k, have h2 : v_R = - u_R + (2 * half_R - 1) := begin dsimp[u_R,v_R,x_R,k], rw[int.cast_add,int.cast_add,int.cast_mul,int.cast_bit0], rw[int.cast_one,int.cast_neg], exact misc_identity (↑ m) (↑ n) half_R, end, have h3 : 2 * half_Q - 1 = 0 := dec_trivial, have h4 : 2 * half_R - 1 = (((2 * half_Q - 1) : ℚ) : ℝ) := begin dsimp[half_R], rw[rat.cast_add,rat.cast_mul,rat.cast_bit0,rat.cast_neg,rat.cast_one], end, have h5 : 2 * half_R - 1 = 0 := by rw[h4,h3,rat.cast_zero], rw[h5,add_zero] at h2, have h6 : abs v_R = abs u_R := by rw[h2,abs_neg], exact h1 h6, } end lemma k_does_not_exist : ¬ ∃ (k : ℝ → ℤ), (∀ x : ℝ, is_closest_integer (k x) x) := begin rintro ⟨k,k_spec⟩, let x : ℝ := (0 : ℤ) + half_R, exact no_closest_integer (k x) 0 (k_spec x) end

#### Sebastien Gouezel (Mar 26 2019 at 10:46):

Instead of `1/(n+1)`

, you can use `((1:R)/2)^n`

(and the fact that this sequence tends to `0`

, which should already be there). No need to cast with this one.

#### Kevin Buzzard (Mar 26 2019 at 12:03):

Even basic identities like 1/2 - 1 = -1/2 cannot easily be

proved directly in ℝ, because there are no general algorithms

for exact calculation in ℝ. We need to work in ℚ and then

apply the cast map.

import tactic.norm_num data.real.basic example : ( 1 : ℝ) / 2 - 1 = -1 / 2 := by norm_num

?

#### Kevin Buzzard (Mar 26 2019 at 12:07):

For reasons that I do not fully understand, the ring tactic

seems to work more reliably if we do it in a separate lemma

so that the terms are just free variables. We can then

substitute values for this variables as an extra step. In

particular, we will substitute h = 1/2, and then give a

separate argument that the final term 2 * h - 1 is zero.

`ring`

can sometimes be a bit ropey when division is involved. One could probably beef it up by putting in a "clear denominators" step.

#### Kevin Buzzard (Mar 26 2019 at 13:27):

Oh, it's the casts as well. @Rob Lewis here's something to add to the list of cast test cases:

example (m n : ℤ) : (m : ℝ) + 1/2 - ((2 * m + 1 - n) : ℤ) = -(m + 1/2 - n) := ???

It can be solved by `simp;ring`

#### Kevin Buzzard (Mar 26 2019 at 13:34):

@Neil Strickland here's my take on the result.

import tactic.norm_num data.real.basic def is_closest_integer (n : ℤ) (x : ℝ) := ∀ m : ℤ, m ≠ n → abs ( x - m ) > abs ( x - n ) lemma no_closest_integer (n m : ℤ) : ¬ (is_closest_integer n ((m : ℝ) + 1/2)) := begin intro h0, let x_R : ℝ := (m : ℝ) + 1/2, let k := 2 * m + 1 - n, by_cases e0 : k = n, {-- In this block we consider the possibility that k = n, and -- show that it is impossible. exfalso, change 2 * m + 1 - n = n at e0, -- I prefer this to dsimp -- every operation I make here is "natural" hence will be in mathlib somewhere -- and I find it using ctrl-space and name guesswork rw [sub_eq_iff_eq_add, ←two_mul, eq_comm, ←sub_eq_iff_eq_add', ←mul_sub] at e0, -- e0 : 2 * (n - m) = 1 have e2 : (2 * (n - m)) % 2 = 0 := int.mul_mod_right _ _, rw [e0, @int.mod_eq_of_lt (1 : ℤ) (2 : ℤ) (dec_trivial) (dec_trivial)] at e2, -- e2 : 1 = 0 cases e2, -- just showing off here },{ let h1 := ne_of_gt (h0 k e0), apply h1, convert abs_neg _, -- get rid of k show (m : ℝ) + 1/2 - ((2 * m + 1 - n) : ℤ) = -(m + 1/2 - n), -- simp does the casts, although it's a sin to apply it when not closing a goal -- instead of simp one should say: -- suffices : -(1 : ℝ) + (2⁻¹ + (↑n + (↑m + -(2 * ↑m)))) = -2⁻¹ + (↑n + -↑m), -- simpa, simp, -- now ring finishes the job ring } end lemma k_does_not_exist : ¬ ∃ (k : ℝ → ℤ), (∀ x : ℝ, is_closest_integer (k x) x) := begin rintro ⟨k,k_spec⟩, let x : ℝ := (0 : ℤ) + 1/2, exact no_closest_integer (k x) 0 (k_spec x) end

#### Neil Strickland (Mar 26 2019 at 17:16):

@Kevin Buzzard Thanks, that's better than my version. I will see what I can learn from it.

#### Kevin Buzzard (Mar 26 2019 at 17:18):

I know you might have pedagogical obstructions to writing your code, so I didn't know how much of my version you'd like. No doubt you can get some super-mangled version of the proof that 2(m-n)=1 is false which is unreadable.

#### Paul-Nicolas Madelaine (Apr 09 2019 at 16:38):

Here is the first version of the cast tactic I've been working one and that @Rob Lewis mentioned a few weeks ago

https://github.com/lean-forward/coe_tactic

Basically it's a simplify tactic with the appropriate set of lemmas, plus a little heuristic to infer casts in some cases.

#### Paul-Nicolas Madelaine (Apr 09 2019 at 16:42):

for instance, the expression ` (an : ℚ) + (bz : ℚ) `

will first be rewritten as ` ((an : ℤ) : ℚ) + (bz : ℚ) `

by the heuristic, and then as ` ((an : ℤ) + bz) : ℚ) `

by the appropriate simp lemma

#### Johan Commelin (Apr 09 2019 at 16:42):

Exciting news!

#### Paul-Nicolas Madelaine (Apr 12 2019 at 15:25):

If anyone feels inspired, I'm also trying to change the names of the different tactics.

Mainly I want to replace coe with cast, as it seems more appropriate.

But there's also the problem of the simpa equivalent of norm_coe, which right now is named norm_coe_a

So I'm taking any ideas to name these tactics as clearly

as possible

#### Paul-Nicolas Madelaine (Apr 29 2019 at 13:01):

Hello everyone,

I've worked a lot on trying to improve the code and make it as clear and usable as possible.

There are now 5 tactics:

- norm_cast

- rw_mod_cast, that applies a list of rw rules and normalizes between them

- apply_mod_cast, that normalizes the goal and a given expression, and then applies the expression

- exact_mod_cast, that is similar to apply_mod_cast but for exact

- assumption_mod_cast, that normalizes the goal and all the expressions from the context, then uses assumption

I've also copied padics files from mathlib and tried to improve the proofs using these tactics.

I'm waiting for any feedback about what should be changed or added to the tactics,

and whether they could be added to mathlib

#### Patrick Massot (Apr 29 2019 at 13:06):

Thank you very much for this work! I'm not fighting those kinds of problems those days, but I'll try to find some time to come back to projects I used to work on but gave up because of those issues. Do you know whether your work could be adapted to other coercions and casts? In the perfectoid project we also have many coercion fights, but with more complicated types that nat or int.

#### Kevin Buzzard (Apr 29 2019 at 13:12):

Here was an example we ran into -- if K was a field and K-hat was its completion (with respect to some topology blah blah blah), also a field in cases of interest, then we had an injective map from K to K-hat (a coercion, in fact), so we had a proof that if x was non-zero then coe(x) was also non-zero. Now say x is non-zero. The constructor` units.mk0`

can be used to make a unit out of x, which a mathematician would also call x. The fact that the unit x got coerced into the unit (coe x) was not `rfl`

because we needed to apply `units.ext`

. Mathematicians find these sorts of goals very frustrating because we don't want to waste our time proving x=x, and when rfl doesn't work it's frustrating. @Patrick Massot @Johan Commelin do you know what -- I think we needed some unit predicate instead of explicitly carrying around the useless inverse which we never used (because it's uniquely determined by x).

#### Paul-Nicolas Madelaine (Apr 29 2019 at 13:13):

@Patrick Massot

The only thing to do to make it work on other types of casts should be (theoretically) to add new lemmas to the set of norm_cast lemmas.

But in practiced I've only used it on nat/int/rat/reals and padics, so I definitely have to try using it on more complex examples.

#### Kevin Buzzard (Apr 29 2019 at 13:15):

I think the main problems my students had were all with these use examples (nat/int/rat/real) -- it will be interesting to see how much better you have made their lives!

#### Patrick Massot (Apr 29 2019 at 13:17):

I think what really need now is documentation of your work. We have the test file, which is much better than nothing, but we also need some documentation *text*, explaining what the tactics are doing, roughly how they are doing it, what we can hope for, what is out of scope, how to add new lemmas, etc. I know it's no fun at all. But a *lot* of software development (especially in free software) turn out to be useless for lack of documentation

#### Paul-Nicolas Madelaine (Apr 29 2019 at 13:19):

@Kevin Buzzard I didn't understand every detail of the example by lack of mathematical background, but the units.ext should be rewritten as an equivalence to be used in the current version of my code. apart from this it should work.

#### Paul-Nicolas Madelaine (Apr 29 2019 at 13:20):

@Patrick Massot I recently added comments to the norm_cast file, but I will try to rewrite a more detailed documentation page if that's necessary

#### Patrick Massot (Apr 29 2019 at 13:23):

Your comments in `norm_cast`

seem helpful for people who want to improve the tactics, not for users

#### Patrick Massot (Apr 29 2019 at 13:23):

And the user facing tactis (the interactive ones) don't even have docstrings

#### Kevin Buzzard (Apr 29 2019 at 15:36):

Kevin Buzzard I didn't understand every detail of the example by lack of mathematical background, but the units.ext should be rewritten as an equivalence to be used in the current version of my code. apart from this it should work.

I think `units.ext_iff`

is the iff version

#### Paul-Nicolas Madelaine (Apr 29 2019 at 15:44):

@Kevin Buzzard well if you send me a particular proof that is actually a lot of boiler plate code to move casts around, I will try to make it clearer with my tactics

#### Kevin Buzzard (Apr 29 2019 at 15:47):

I cannot do this right now but I will certainly remember your suggestion!

#### Paul-Nicolas Madelaine (May 06 2019 at 14:37):

I made a pull request on the mathlib repository : https://github.com/leanprover-community/mathlib/pull/988,

therefore the coe_tactic repo is no longer up to date.

#### Johan Commelin (May 06 2019 at 15:33):

@Paul-Nicolas Madelaine Thanks a lot for writing these tactics! I look forward to using them :octopus:

#### Johan Commelin (May 06 2019 at 15:35):

One comment... for some reason `mod_cast`

sounds too much like you are doing something with modular arithmetic... would it make sense to call the tactics `norm_cast`

after `norm_num`

?

Ok... maybe that actually sounds like you are taking norms... I don't know. I should probably just get used to it :grinning_face_with_smiling_eyes:

#### Rob Lewis (May 06 2019 at 15:37):

One of the tactics is already called `norm_cast`

. The others were hard to name. We're open to suggestions!

#### Johan Commelin (May 06 2019 at 15:49):

Wait, what does the `mod`

in `mod_cast`

stand for? I thought it stood for "modify". But should I read `rw_mod_cast`

as "`rw`

modulo casts"? If so, then I think it's actually a good name.

#### Johan Commelin (May 06 2019 at 15:50):

Maybe I was just being sleepy (-;

#### Rob Lewis (May 06 2019 at 15:51):

Yes, we have rewrite/apply/exact/assumption modulo casts.

#### Johan Commelin (May 14 2019 at 19:49):

@Paul-Nicolas Madelaine Does it make sense to also make `convert_mod_cast`

? Or does `exact_mod_cast`

handle this?

#### Johan Commelin (May 14 2019 at 19:49):

(I haven't tested yet, waiting for the tactics to land in the nightly cache...)

#### Patrick Massot (May 14 2019 at 19:50):

What is the status of Scott's efforts to bring us more compiled stuff? Does he have that branch ready for you somewhere?

#### Johan Commelin (May 14 2019 at 19:51):

#### Patrick Massot (May 14 2019 at 19:52):

that's a python museum!

#### Patrick Massot (May 14 2019 at 19:52):

This syntax is has been replaced by a now obsolete syntax!

#### Patrick Massot (May 14 2019 at 19:53):

anyway, https://tqft.net/lean/mathlib/ doesn't look very helpful

#### Scott Morrison (May 14 2019 at 20:06):

It's getting there...

#### Scott Morrison (May 14 2019 at 20:06):

I modified the script, attempting to make it more robust against build failures, and accidentally deleted everything

#### Scott Morrison (May 14 2019 at 20:06):

it's rebuilding as we speak

#### Scott Morrison (May 14 2019 at 20:07):

It's a lot of building. :-)

#### Patrick Massot (May 14 2019 at 20:07):

Thanks! Your efforts are very much appreciated

#### Paul-Nicolas Madelaine (May 15 2019 at 08:31):

@Johan Commelin the exact_mod_cast tactic is really just a normalization then a call to the `exact`

tactic, so `convert_mod_cast`

would make sense, and it could also normalize the new goals

Last updated: May 09 2021 at 10:11 UTC