rfl proofs broken

Stream: lean4

[Wrenna Robson]

I just updated my Mathlib version + accompanying Lean version and now certain rfl proofs are broken.

For an example

def swaps (a : Array α) (bs : List (Fin a.size × Fin a.size)) : Array α :=
  match bs with
  | [] => a
  | (b :: bs) => (a.swap b.1 b.2).swaps
    (bs.map (fun b => (b.1.cast (a.size_swap _ _).symm, b.2.cast (a.size_swap _ _).symm)))
    termination_by bs.length

@[simp]
theorem swaps_nil (a : Array α) : a.swaps [] = a := by rw [swaps]

The theorem here was rfl before - now it is not. Also, and much worse, proofs that use it appear to not work - specifically places where rw [swaps_nil] doesn't work for "motive is not type correct" reasons are no longer addressed by using simp_rw instead.

Do I need to change how I approach things?

[Ruben Van de Velde]

Is this the thing where definitions using well-founded recursion are irreducible by default now?

[Ruben Van de Velde]

I think rfl not working anymore is expected, but the other question maybe not?

[Wrenna Robson]

Yes, it appears to be (in that if I add a @[reducible] it works).

[Wrenna Robson]

I don't entirely understand the consequences of that or if there's a better way of doing it.

[Ruben Van de Velde]

Me neither :)

[Joachim Breitner]

That is one option. Another one is to use unseal swaps in for the theorem you need. Or just keep the proof with the rw – using rfl for well-founded definitions is always a bit of a code smell, as it unfolds the function to the (internal) construction using WellFounded.fix

[Wrenna Robson]

Mmm - my issue is, as I say, that then I'm finding other, more complex proofs don't work.

[Wrenna Robson]

Specifically, this one:

theorem swaps_append (a : Array α) (bs₁ bs₂ : List (Fin a.size × Fin a.size)) :
    a.swaps (bs₁ ++ bs₂) = (a.swaps bs₁).swaps
    (bs₂.map (fun b => (b.1.cast (a.size_swaps _).symm, b.2.cast (a.size_swaps _).symm))) :=
  match bs₁ with
  | [] => by simp_rw [List.nil_append, swaps_nil, Fin.cast_eq_self, Prod.mk.eta, map_id']
  | (b₁ :: bs₁) => by
    rw [cons_append, swaps_cons, map_append]
    refine' ((a.swap b₁.1 b₁.2).swaps_append _ _).trans _
    rw [map_map]
    rfl
  termination_by bs₁.length

[Wrenna Robson]

I would like to avoid the code smell (and maybe I need to change my definition) but I don't know how I should necessarily do that.

[Joachim Breitner]

The definition is fine, but likely the proofs have to be updated. Note that it’s already a warning flag that you have a rw […] followed by rfl, because if after rw the goal is trivial (with reducible transparency), it would have solved it.

I guess you need to add swaps to one or both rw calls.

[Joachim Breitner]

Somehow this didn’t make it into the 4.8.0 release announcement, it seems…

[Joachim Breitner]

Ah, that's because it’s in 4.9.0-rc1 :-)

[Wrenna Robson]

Well, my proof works if I add that reducibility to my definition but it sounds like I shouldn't and I should find another proof - but I'm having difficulty doing that.

[Ruben Van de Velde]

I think your smoothest way forward is likely to mark your definition as reducible (or semireducible?) for now

[Wrenna Robson]

Uh. OK, even odder behaviour. Let me pull up more of the code.

[Wrenna Robson]

@[reducible]
def swaps (a : Array α) (bs : List (Fin a.size × Fin a.size)) : Array α :=
  match bs with
  | [] => a
  | (b :: bs) => (a.swap b.1 b.2).swaps
    (bs.map (fun b => (b.1.cast (a.size_swap _ _).symm, b.2.cast (a.size_swap _ _).symm)))
    termination_by bs.length

@[simp]
theorem swaps_nil (a : Array α) : a.swaps [] = a := by rw [swaps]

@[simp]
theorem swaps_cons (a : Array α) (b : Fin a.size × Fin a.size)
    (bs : List (Fin a.size × Fin a.size)) : a.swaps (b :: bs) = (a.swap b.1 b.2).swaps
    (bs.map (fun b => (b.1.cast (a.size_swap _ _).symm, b.2.cast (a.size_swap _ _).symm))) :=
  by rw [swaps]

theorem swaps_singleton (a : Array α) (b : Fin a.size × Fin a.size) :
  a.swaps [b] = a.swap b.1 b.2 := by simp_rw [swaps_cons, map_nil, swaps_nil]

@[simp]
theorem size_swaps (a : Array α) (bs : List (Fin a.size × Fin a.size)) :
    (a.swaps bs).size = a.size :=
  match bs with
  | [] => by rw[swaps_nil]
  | (b :: bs) => by rw [swaps_cons, size_swaps, size_swap]
  termination_by bs.length

theorem swaps_append (a : Array α) (bs₁ bs₂ : List (Fin a.size × Fin a.size)) :
    a.swaps (bs₁ ++ bs₂) = (a.swaps bs₁).swaps
    (bs₂.map (fun b => (b.1.cast (a.size_swaps _).symm, b.2.cast (a.size_swaps _).symm))) :=
  match bs₁ with
  | [] => by simp_rw [List.nil_append, swaps_nil, Fin.cast_eq_self, Prod.mk.eta, map_id']
  | (b₁ :: bs₁) => by
    rw [cons_append, swaps_cons, map_append]
    refine' ((a.swap b₁.1 b₁.2).swaps_append _ _).trans _
    simp_rw [map_map, comp_def, Fin.cast_trans, swaps_cons]
  termination_by bs₁.length

Note the swaps_nil and final swaps_cons in the latter. If I change the proof of swaps_cons and swaps_nil to rfl instead of by rw [swaps], it allows me to use them in the simp_rw call. But a different proof changes the behaviour.

[Wrenna Robson]

Now I think this is something to do with the fact that this proof also needs well-founded recursion or whatnot (the issue is the fact that the list depends on the array!)

[Wrenna Robson]

But it feels... counter to fundamental things I thought I understand if the proof used for a theorem changes its behaviour when used in tactics.

[Wrenna Robson]

For comparison, here's the outputs of #print swaps_cons with the proof rfl and by rw [swaps]

theorem Array.swaps_cons.{u_1} : ∀ {α : Type u_1} (a : Array α) (b : Fin a.size × Fin a.size)
  (bs : List (Fin a.size × Fin a.size)),
  a.swaps (b :: bs) = (a.swap b.1 b.2).swaps (List.map (fun b_1 => (Fin.cast ⋯ b_1.1, Fin.cast ⋯ b_1.2)) bs) :=
fun {α} a b bs => rfl

theorem Array.swaps_cons.{u_1} : ∀ {α : Type u_1} (a : Array α) (b : Fin a.size × Fin a.size)
  (bs : List (Fin a.size × Fin a.size)),
  a.swaps (b :: bs) = (a.swap b.1 b.2).swaps (List.map (fun b_1 => (Fin.cast ⋯ b_1.1, Fin.cast ⋯ b_1.2)) bs) :=
fun {α} a b bs =>
  Eq.mpr
    (id
      (congrArg
        (fun _a =>
          _a =
            (a.swap b.1 b.2).swaps
              (List.map
                (fun b_1 =>
                  (Fin.cast (Eq.symm (size_swap a b.1 b.2)) b_1.1, Fin.cast (Eq.symm (size_swap a b.1 b.2)) b_1.2))
                bs))
        (swaps.eq_2 a b bs)))
    (Eq.refl
      ((a.swap b.1 b.2).swaps
        (List.map (fun b_1 => (Fin.cast (swaps.proof_1 a b) b_1.1, Fin.cast (swaps.proof_1 a b) b_1.2)) bs)))

[Markus Himmel]

Wrenna Robson said:

Note the swaps_nil and final swaps_cons in the latter. If I change the proof of swaps_cons and swaps_nil to rfl instead of by rw [swaps], it allows me to use them in the simp_rw call. But a different proof changes the behaviour.

My guess is that the reason for this is that your goals are quite dependently typed (since the type of b involves a.size) and so they hard to rewrite for simp. If simp fails to rewrite using a lemma which is proved by rfl, then it falls back to dsimp (which just inserts an application of id for the resulting type). This happens in your proof of swaps_append, but if you change the proof of swaps_nil to something that is not rfl, then simp cannot fall back to dsimp.

[Wrenna Robson]

Yeah, that makes sense - I can't see a way round it...

[Kim Morrison]

Wrenna Robson said:

Yes, it appears to be (in that if I add a @[reducible] it works).

You only need semireducible!

[Wrenna Robson]

I can never remember the difference or why they matter <_<

[Wrenna Robson]

Is there a way, by the way, if you are defining a function on a list, to define it "backwards" - that is to say, instead of using the actual constructors [] and ::, use [] and concat instead?

[Kim Morrison]

Semireducible is the default. The recent change is to make well founded definitions irreducible, and here you (may) want to change it back to how it was, i.e. the default, i.e. semireducible.

[Wrenna Robson]

Right.

[Wrenna Robson]

Wrenna Robson said:

Is there a way, by the way, if you are defining a function on a list, to define it "backwards" - that is to say, instead of using the actual constructors [] and ::, use [] and concat instead?

Yes, and it is usable thanks to #11257 - thanks, @Eric Wieser !

[François G. Dorais]

By the way, in some corner case where types were not quite known so no unsealing was evident, I found that this often works by with_unfolding_all rfl. There doesn't seem to be a term variant, as far as I know.