Zulip Chat Archive

Stream: maths

Topic: cast woes


view this post on Zulip Johan Commelin (Mar 13 2019 at 11:52):

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

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 11:54):

pp.gt_one?

view this post on Zulip Kenny Lau (Mar 13 2019 at 11:55):

why is [p.prime] an instance though

view this post on Zulip Johan Commelin (Mar 13 2019 at 11:55):

We really need a cast tactic.

view this post on Zulip Kenny Lau (Mar 13 2019 at 11:55):

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

view this post on Zulip Johan Commelin (Mar 13 2019 at 11:56):

@Kenny Lau Thanks

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 11:57):

you can make them all le and lt if you want

view this post on Zulip 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 },
...

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 12:37):

Did you read my docs on cast?

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 12:37):

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

view this post on Zulip Johan Commelin (Mar 13 2019 at 12:38):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 12:38):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 12:38):

I wrote them, and I certainly also forgot them.

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 12:38):

That's why I wrote them :-)

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:01):

My docs don't seem to help.

view this post on Zulip 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.

view this post on Zulip 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?

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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 := ...

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:11):

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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:12):

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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:12):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:12):

If I change 1 to q it works.

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:13):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:13):

I see.

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:14):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:14):

It is exactly nat.cast_lt, no?

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:14):

what?

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:14):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:15):

I made it match syntactically, no?

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:16):

I got 1 into \u 1 form

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:16):

simp sent it back

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:16):

Oh I see

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:16):

So is it a question of precedence?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:17):

simp is not confluent as a result

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:19):

names of any obscure lemmas

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

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:20):

These are not difficult names

view this post on Zulip Mario Carneiro (Mar 13 2019 at 13:20):

there is much worse than this in the library

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:20):

:-)

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:20):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:21):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:39):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:39):

;-)

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 13:39):

Did you read my docs about cast?

view this post on Zulip 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 (-;

view this post on Zulip Patrick Massot (Mar 13 2019 at 14:22):

They don't need motivation, they need pity

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 13 2019 at 15:03):

Awesome!

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 15:56):

@Rob Lewis a general spec would be "if a mathematician who thinks NZQRC\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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 09 2019 at 16:42):

Exciting news!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Apr 29 2019 at 13:23):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 29 2019 at 15:47):

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

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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:

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 06 2019 at 15:50):

Maybe I was just being sleepy (-;

view this post on Zulip Rob Lewis (May 06 2019 at 15:51):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 14 2019 at 19:49):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (May 14 2019 at 19:51):

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

view this post on Zulip Patrick Massot (May 14 2019 at 19:52):

that's a python museum!

view this post on Zulip Patrick Massot (May 14 2019 at 19:52):

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

view this post on Zulip Patrick Massot (May 14 2019 at 19:53):

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

view this post on Zulip Scott Morrison (May 14 2019 at 20:06):

It's getting there...

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 14 2019 at 20:06):

it's rebuilding as we speak

view this post on Zulip Scott Morrison (May 14 2019 at 20:07):

It's a lot of building. :-)

view this post on Zulip Patrick Massot (May 14 2019 at 20:07):

Thanks! Your efforts are very much appreciated

view this post on Zulip 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