cast woes

Stream: maths

[Johan Commelin]

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

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

[Kenny Lau]

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]

pp.gt_one?

[Kenny Lau]

why is [p.prime] an instance though

[Johan Commelin]

We really need a cast tactic.

[Kenny Lau]

and also why does data.nat.prime use ge and gt @Mario Carneiro

[Johan Commelin]

@Kenny Lau Thanks

[Mario Carneiro]

I guess it's a bit more natural to read prime.gt_one? not a strong argument

[Mario Carneiro]

you can make them all le and lt if you want

[Johan Commelin]

I would love to be able to prove this via

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

[Kevin Buzzard]

Did you read my docs on cast?

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I wrote them, and I certainly also forgot them.

[Kevin Buzzard]

That's why I wrote them :-)

[Kevin Buzzard]

My docs don't seem to help.

[Kevin Buzzard]

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

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]

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 simps job to prove this sort of thing? It's an implication, not an iff or an equality.

[Kevin Buzzard]

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]

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]

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]

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]

I want nat.cast_lt to have greater precedence than \u 1 = 1.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

If I change 1 to q it works.

[Mario Carneiro]

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

[Kevin Buzzard]

I see.

[Kevin Buzzard]

I don't really understand why simp doesn't solve it.

[Kevin Buzzard]

It is exactly nat.cast_lt, no?

[Mario Carneiro]

what?

[Kevin Buzzard]

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

[Mario Carneiro]

1 < ↑p ↔ 1 < p is defeq to an application of nat.cast_lt, but the pattern ↑?M1 < ↑?M2 doesn't match syntactically

[Kevin Buzzard]

I made it match syntactically, no?

[Kevin Buzzard]

I got 1 into \u 1 form

[Kevin Buzzard]

simp sent it back

[Mario Carneiro]

Oh I see

[Kevin Buzzard]

So is it a question of precedence?

[Mario Carneiro]

The problem is that nat.cast_lt is not in a simp normal form, so it rarely triggers

[Mario Carneiro]

simp is not confluent as a result

[Mario Carneiro]

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]

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]

names of any obscure lemmas

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

[Mario Carneiro]

These are not difficult names

[Mario Carneiro]

there is much worse than this in the library

[Kevin Buzzard]

:-)

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

This is unfortunate; most of the coe names have to do with coercions from nat to int in core

[Johan Commelin]

I really don't like these goals.

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

[Kevin Buzzard]

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

[Kevin Buzzard]

;-)

[Kevin Buzzard]

Did you read my docs about cast?

[Johan Commelin]

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]

They don't need motivation, they need pity

[Rob Lewis]

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]

Awesome!

[Kevin Buzzard]

@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]

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]

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]

Thanks, Kevin. This is a good start. The \u \u examples are definitely not trivial, I come across those often enough too.

[Rob Lewis]

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]

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]

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]

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]

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]

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]

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]

@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]

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

[Kevin Buzzard]

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]

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]

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]

Exciting news!

[Paul-Nicolas Madelaine]

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]

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]

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]

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]

@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]

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]

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]

@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]

@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]

Your comments in norm_cast seem helpful for people who want to improve the tactics, not for users

[Patrick Massot]

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

[Kevin Buzzard]

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]

@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]

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

[Paul-Nicolas Madelaine]

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]

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

[Johan Commelin]

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]

One of the tactics is already called norm_cast. The others were hard to name. We're open to suggestions!

[Johan Commelin]

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]

Maybe I was just being sleepy (-;

[Rob Lewis]

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

[Johan Commelin]

@Paul-Nicolas Madelaine Does it make sense to also make convert_mod_cast? Or does exact_mod_cast handle this?

[Johan Commelin]

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

[Patrick Massot]

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]

https://github.com/leanprover-community/mathlib/pull/1000/files#diff-dbd7f4184984f905b3e1ed514ca280ccR65

[Patrick Massot]

that's a python museum!

[Patrick Massot]

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

[Patrick Massot]

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

[Scott Morrison]

It's getting there...

[Scott Morrison]

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

[Scott Morrison]

it's rebuilding as we speak

[Scott Morrison]

It's a lot of building. :-)

[Patrick Massot]

Thanks! Your efforts are very much appreciated

[Paul-Nicolas Madelaine]

@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