deterministic timeout + goal accomplished

Stream: general

[Simon Andreys]

I got a "goal accomplished" together with a "deterministic timeout". This appends right at the end of a proof, at the "refl" or "simp" line. I found out that this problem was already encountered one week ago :
https://leanprover.zulipchat.com/#narrow/stream/240192-Berkeley-Lean.20Seminar/topic/Project.20ideas/near/217690233
This error message is quite dreadful (you feel so close, but you are so far), and I think it deserves its own topic. In my case, I found a different proof that work, but I still don't understand why my first, more beautiful proof fails. The issue was also solved in the discussion linked above. What I gathered is that :
-the issue is not actually at the "refl" but happens before, some tactic is messing around, corrupting some goal in the background, and when the compiler checks what's the tactic did, it gets lost.
-In the case linked above, replacing a "have" by a "let" in an isomorphism in the proof solved the problem. The isomorphism had to be describe explicitly.
-In my case, I replaced a proof based on a associativity lemmas by a proof with multiple dsimp and some lower level lemmas. I have still no idea where the error comes from, and I am afraid it is just under the carpet, ready to appear again.

[Simon Andreys]

Since I have a functioning proof (for now), this topic aims at documenting the issue rather than solving my problem, but here is the faulty code anyway :

lemma compq_quotient_assoc (p: polynomial R) (q : polynomial R) (I:ideal $ polynomial R) :
(quotient_cast (le_of_eq (comp_ideal_assoc p q I))).comp ( (compq_quotient q (comp_ideal p I) ).comp (compq_quotient p I))=
compq_quotient (p.comp q) I :=
begin
    dsimp [compq_quotient, quotient_cast],
    repeat {rw quotient_map_assoc},
    congr',
    simp,
    rw compq_assoc,  --goal accomplished but deterministic timeout
end

and the correct proof :

lemma compq_quotient_assoc' (p: polynomial R) (q : polynomial R) (I:ideal $ polynomial R) :
(quotient_cast (le_of_eq (comp_ideal_assoc p q I))).comp ( (compq_quotient q (comp_ideal p I) ).comp (compq_quotient p I))=
compq_quotient (p.comp q) I :=
begin
    apply ring_hom.ext, intro aclass,
    cases ideal.quotient.mk_surjective aclass with a ha,
    dsimp [quotient_cast, compq_quotient, comp_ideal, ideal.quotient_map, ideal.map],
    rw ←  ha,
    repeat {rw ideal.quotient.lift_mk},
    simp,
    dsimp [compq],
    rw comp_assoc,  --works fine, but slow
end

Finally, the full context :

import ring_theory.adjoin_root ring_theory.ideal.operations
import linear_algebra.basis linear_algebra.matrix algebra.module.basic algebra.polynomial.group_ring_action
import tactic

noncomputable theory

--We show that 1, (X-l), ... (X-l)^n is a basis for K[X]/(X-l)^(n+1), using the power basis 1, ..., X^n of K[X]/X^(n+1)

namespace adjoin_root_basis

open polynomial --to use X as the polynomial indeterminate

variables {R:Type} [comm_ring R] (I J : ideal $polynomial R) (p q: polynomial R)

--let us define some casting function to take care of the heterogenous equality problem.

lemma trivial_id_inclusion {I J: ideal R} (ilj:I≤ J) : I ≤ ideal.comap (ring_hom.id R) J :=
begin
intros x xin, simp, exact ilj xin,
end

def quotient_cast {I J:ideal R} (ilj: I≤ J) :=ideal.quotient_map J (ring_hom.id R) (trivial_id_inclusion ilj)

--a few simp-type lemmas for quotient_cast
lemma quotient_cast_id {I : ideal R} (ilj: I≤ I): (quotient_cast ilj)=ring_hom.id I.quotient :=
begin
dsimp [quotient_cast, ideal.quotient_map],ext,
cases ideal.quotient.mk_surjective x with a ha,
rw ← ha,
rw ideal.quotient.lift_mk ,
simp,
end

lemma quotient_cast_composition {I J L : ideal R} (ilj : I≤ J) (jll: J≤L) :
(quotient_cast jll)∘ (quotient_cast ilj)= quotient_cast (le_trans ilj jll):=
begin
dsimp [quotient_cast, ideal.quotient_map], ext,
cases ideal.quotient.mk_surjective x with a ha,
rw ← ha,
repeat {rw ideal.quotient.lift_mk},
simp,
end

--this should do for the nondefinitional equality problem
--question : could this "cast" tric be done more generally to any dependent type ?

--another preliminary : the "associativity" of quotient_map.
#check ideal.quotient_map

--first a little lemma to compose inequalities necessary to quotient_map

def comap_ineg_assoc {R1: Type} {R2: Type} {R3:Type} [comm_ring R1] [comm_ring R2] [comm_ring R3] {I: ideal R1} {J: ideal R2} (K:ideal R3)
(f: ring_hom R1 R2) (g: ring_hom R2 R3) (ilfj: I≤ ideal.comap f J) (jlgk : J≤ ideal.comap g K) :
I≤ ideal.comap (g.comp f) K :=λ x xin,jlgk (ilfj xin)

lemma quotient_map_assoc {R1: Type} {R2: Type} {R3:Type} [comm_ring R1] [comm_ring R2] [comm_ring R3] {I: ideal R1} {J: ideal R2} (K:ideal R3)
(f: ring_hom R1 R2) (g: ring_hom R2 R3) (ilfj: I≤ ideal.comap f J) (jlgk : J≤ ideal.comap g K) :
(ideal.quotient_map K g jlgk).comp (ideal.quotient_map J f ilfj )=ideal.quotient_map K (g.comp f) (comap_ineg_assoc K f g ilfj jlgk):=
begin
apply ring_hom.ext, intro xclass,
cases ideal.quotient.mk_surjective xclass with x hx, rw ← hx,
dsimp [ideal.quotient_map],
repeat {rw ideal.quotient.lift_mk},simp,
end

--Now we construct some ring homomorphisms between quotients.

def compq (q:polynomial R) : ring_hom (polynomial R) (polynomial R):=
{
to_fun:= λ p, p.comp q,
map_add':=λ p r, begin apply add_comp, end ,
map_mul':= λ p r, begin simp, end,
map_one':= begin simp, end,
map_zero':=begin simp, end,
}

lemma compq_assoc (p:polynomial R) (q: polynomial R) : (compq p).comp (compq q) =compq (q.comp p):=
begin
apply ring_hom.ext, intro x,
dsimp [compq],
apply comp_assoc, --Key step
end

def comp_ideal (p: polynomial R) (I: ideal $polynomial R) :=ideal.map (compq p) I

--a simp lemma describing the composition
lemma comp_ideal_assoc (p q:polynomial R) (I: ideal $ polynomial R) : comp_ideal q (comp_ideal p I) =comp_ideal (p.comp q) I:=
begin
dsimp [comp_ideal],
rw ideal.map_map, --Key step
congr',
rw compq_assoc q p,
end

--a simp lemma used to define the quotient map
lemma compq_comp_ideal (p:polynomial R) (I:ideal $ polynomial R) : ∀ (r:polynomial R),
r∈ I → r.comp p ∈ comp_ideal p I :=
begin
intros r rin,
apply ideal.subset_span, --key step 1
dsimp [compq],
use r,
split,
{exact rin,},{simp,},
end

def compq_quotient (p:polynomial R) (I: ideal $polynomial R) : I.quotient →+* (comp_ideal p I).quotient :=
ideal.quotient_map (comp_ideal p I) (compq p) (compq_comp_ideal p I)

#check compq_quotient p I
#check (compq_quotient q (comp_ideal p I) ).comp (compq_quotient p I)
#check (quotient_cast (le_of_eq (comp_ideal_assoc p q I))).comp ( (compq_quotient q (comp_ideal p I) ).comp (compq_quotient p I))

--the lemma that "trivally" composes the compq_quotient maps. We need the quotient_cast map to
--make the equality between quotients by ideals wich are equal but not equal by def.

lemma compq_quotient_assoc (p: polynomial R) (q : polynomial R) (I:ideal $ polynomial R) :
(quotient_cast (le_of_eq (comp_ideal_assoc p q I))).comp ( (compq_quotient q (comp_ideal p I) ).comp (compq_quotient p I))=
compq_quotient (p.comp q) I :=
begin
dsimp [compq_quotient, quotient_cast],
repeat {rw quotient_map_assoc},
congr',
simp,
rw compq_assoc, --goal accomplished but deterministic timeout
end

lemma compq_quotient_assoc' (p: polynomial R) (q : polynomial R) (I:ideal $ polynomial R) :
(quotient_cast (le_of_eq (comp_ideal_assoc p q I))).comp ( (compq_quotient q (comp_ideal p I) ).comp (compq_quotient p I))=
compq_quotient (p.comp q) I :=
begin
apply ring_hom.ext, intro aclass,
cases ideal.quotient.mk_surjective aclass with a ha,
dsimp [quotient_cast, compq_quotient, comp_ideal, ideal.quotient_map, ideal.map],
rw ← ha,
repeat {rw ideal.quotient.lift_mk},
simp,
dsimp [compq],
rw comp_assoc, --works fine, but slow
end

[Simon Andreys]

The faulty proof uses a lemma quotient_map_assoc on the composition of ideal.quotient_map, maybe a similar lemma already exists but the closest I could find was ideal.comp_quotient_map_eq_of_comp_eq
The lemma quotient_map_assoc does not return any error, but I fear that it's where the mess happens. It's a shame because it looks useful.

[Kevin Buzzard]

The problem with the timing-out proof is congr' (if you put sorry immediately after the congr' you get the timeout).

[Simon Andreys]

Indeed, but there may still be a mess earlier. When I get rid of the congr' and I try to do a rw, I get a "motive is not type correct". With simp_rw, the goal accomplished+timeout is back :

begin
    dsimp [compq_quotient, quotient_cast],
    repeat {rw quotient_map_assoc},
    simp,
     simp_rw compq_assoc q p,  -- rw gives a "motive is not type correct" error, so I use simp_rw
    refl, --ga +timeout
end

[Mario Carneiro]

you need four backticks for the spoiler tag if you want to put code in it

[Simon Andreys]

@Mario Carneiro thanks, it's done.

[Simon Andreys]

There is no coloration though.

[Mario Carneiro]

you need ```lean probably

[Mario Carneiro]

it's set as the default language in this zulip instance but I guess it doesn't work under spoiler tags

[Simon Andreys]

Indeed color is back !

[Simon Andreys]

I think I understand the problem a bit more, having tested different things. I think it lies in the argument (hIJ : I ≤ ideal.comap f J) of ideal.quotient_map . In VSCode, this argument is hidden in the current goal during the proof (but I get to see it if I hover on it). I think the rw tactics fails because if it replaces an expression in the first argument of quotient_map but does not modify it in the second argument, the obtained expression makes no sense. I suppose simp_rw and congr' both have a faulty treatment of this second argument. This is why taking a representative with ideal.quotient.mk_surjective and proving things outside of the quotient works in the second proof.

[Mario Carneiro]

So far I've managed to reduce the bad congr' proof to this:

example {R : Type} [comm_ring R] (p q : polynomial R) (I : ideal (polynomial R))
  (h1 : I ≤ ideal.comap
    ((ring_hom.id (polynomial R)).comp ((compq q).comp (compq p)))
    (comp_ideal (p.comp q) I))
  (h2 : I ≤ ideal.comap (compq (p.comp q)) (comp_ideal (p.comp q) I)) :
  (comp_ideal (p.comp q) I).quotient_map
    ((ring_hom.id (polynomial R)).comp ((compq q).comp (compq p))) h1 =
  (comp_ideal (p.comp q) I).quotient_map (compq (p.comp q)) h2 :=
begin
  have H_congr_lemma := λ {I : ideal (polynomial R)} (J : ideal (polynomial R))
    (f f_1 : polynomial R →+* polynomial R) (e_3 : f = f_1)
    (hIJ : I ≤ ideal.comap f J) (hIJ_1 : I ≤ ideal.comap f_1 J),
  (λ (I J : ideal (polynomial R)) (f f_1 : polynomial R →+* polynomial R) (e_3 : f = f_1)
   (hIJ : I ≤ ideal.comap f J),
     @eq.drec (polynomial R →+* polynomial R) f
       (λ (f_1 : polynomial R →+* polynomial R) (e_3 : f = f_1),
          J.quotient_map f hIJ = J.quotient_map f_1
              (@eq.rec (polynomial R →+* polynomial R) f
                 (λ (f : polynomial R →+* polynomial R), I ≤ ideal.comap f J)
                 hIJ f_1 e_3))
       rfl f_1 e_3)
    I J f f_1 e_3 hIJ,
  have := @H_congr_lemma I (comp_ideal (p.comp q) I)
    ((ring_hom.id (polynomial R)).comp ((compq q).comp (compq p)))
    (compq (p.comp q))
    sorry
    h1
    h2,
  exact this,
end

[Mario Carneiro]

The theorem statement is the state immediately before congr'. AFAICT it typechecks, so rw is not to blame

[Mario Carneiro]

The H_congr_lemma is the proof generated by congr'. It also typechecks, but applying the proof (which is the final have and exact this) fails. I notice that the type of the have is not literally the same as the goal, it produces something other than h2 on the rhs

[Simon Andreys]

Nice ! I should learn how to get these generated proofs. I did not mean to say that rw was to blame, I meant that it cannot be applied because of the second argument, and this is why I was cornered into using congr' in the first place.

[Simon Andreys]

I've written a lemma to replace the sorry, in your code, to be sure it was not interfering. The second have produces

(comp_ideal (p.comp q) I).quotient_map ((ring_hom.id (polynomial R)).comp ((compq q).comp (compq p))) h1 =
(comp_ideal (p.comp q) I).quotient_map (compq (p.comp q)) _

where _ is of type

(λ (f : polynomial R →+* polynomial R), I ≤ ideal.comap f (comp_ideal (p.comp q) I))  (compq (p.comp q))

Implementing the substitution (i.e. replacing f by (compq (p.comp q) ) in the expression) gives the type of h2. This type is equal to the type of h2, but not definitionally (edit : no, they are defeq) ! This problem, again. Does this mean there is some heq issue in congr' ?

[Mario Carneiro]

are you sure it is not defeq? I tried the same thing and rfl proves they are equal

[Simon Andreys]

Okay, they are defeq. Why is this not h2 then ?

[Mario Carneiro]

it is, I'm pretty sure

[Mario Carneiro]

but I also have evidence that lean is unfolding lots of things and I'm not sure why yet

[Mario Carneiro]

for example, the error goes away if you make ring_hom.id an axiom

[Mario Carneiro]

More minimized:

import data.polynomial.eval

example {R : Type} [comm_ring R] (p q : polynomial R)
  (P : (polynomial R → polynomial R) → Prop)
  (h1 : P p.comp) (h2 : P q.comp) (e : p.comp = q.comp) :
  (eq.rec h1 e : P q.comp) = h2 :=
by {change h2 = h2, exact rfl}

[Mario Carneiro]

the weird thing is that the change works but the exact doesn't, meaning that the elaborator and kernel disagree about the defeq

[Simon Andreys]

So it is indeed a problem of defeq on the type of h2 ? Very strange indeed.

[Reid Barton]

is anything irreducible today?

[Mario Carneiro]

polynomial.comp appears to be today's culprit

[Mario Carneiro]

it still doesn't make any sense to me that this would be unfolded though

[Reid Barton]

This looks similar to the other weirdness then

[Mario Carneiro]

amusingly, lean is totally fine with the proof proof_irrel _ _

[Reid Barton]

in that, putting everything else aside, :this: both sides of the equality are propositions

[Mario Carneiro]

actually eval₂ looks like a better candidate for irreducibility

[Mario Carneiro]

also finsupp.sum

[Reid Barton]

https://github.com/leanprover-community/mathlib/blob/b7649bcd2d4db889ae2651637e2c8969c89f4c1f/src/data/polynomial/eval.lean#L479-L485

[Reid Barton]

or do you mean better than tensor_algebra or whatever it was

[Mario Carneiro]

oh curious

[Reid Barton]

(For @Simon Andreys and others, I'm referring to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/218215493)

[Mario Carneiro]

Uh oh:

import data.polynomial.eval

example {R : Type} [comm_ring R] (p q r : polynomial R)
  (c : R →+* polynomial R)
  (P : (polynomial R) → Prop)
  (h1 : P (p.eval₂ c q)) (h2 : P (p.eval₂ c r))
  (e : (p.eval₂ c q) = (p.eval₂ c r)) :
  h2 = eq.rec h1 e := rfl -- timeout

irreducibility may not be good enough

[Mario Carneiro]

Aha, it's not eval2 that's the problem, it's fine if you use eval2 over another semiring. It's the polynomial R semiring instance

[Mario Carneiro]

or at least, it's the combination of the two

[Mario Carneiro]

import data.polynomial.basic

@[irreducible] def polynomial.eval₂' {R S} [semiring R] [semiring S]
  (f : R → S) (x : S) (p : polynomial R) : S :=
p.sum (λ _ a, f a * x)

example {R S : Type} [semiring R] [semiring S]
  (f : R → polynomial S) (x : polynomial S) (p q : polynomial R)
  (P : polynomial S → Prop)
  (h1 : P (p.eval₂' f x)) (h2 : P (q.eval₂' f x))
  (e : (p.eval₂' f x) = (q.eval₂' f x)) :
  h2 = eq.rec h1 e := rfl

Replacing the definition of eval₂' with sorry makes it work, so clearly lean is reducing the irreducible

[Simon Andreys]

The issue is quite out of my scope, but what I gather is that the elaborator does reduce some expression while the compilator doesn't (or the other way around ?), and this problem was already raised before and is linked with the irreducible tag. It's reassuring in some way, since I kinda understand what may cause it (some Prop in the parameters of a function is wrongly typed by some tactic), and how to work around (unfold and dsimp, and use low level lemmas, as unpleasant it may be). Better even, the root problem may be solved at some point and the "high" level proof be efficient again.

[Simon Andreys]

I was overly optimistic when saying that I knew how to work around the problem : it resurfaced at the next lemma. I will use a less composite approach to construct the isomorphism I want.