refl can't solve `subtype.mk x h1 = subtype.mk x h2`

Stream: general

[Eric Wieser]

I'm seeing something very weird on these lines:

https://github.com/leanprover-community/mathlib/blob/b8875386202f5675d7a5c52a41d5fc79831e257a/src/combinatorics/stars_and_bars.lean#L194-L199

Specifically, if I replace ext : 1, refl with refl, the proofs breaks.

The only difference between the two goal states is inside the second argument of subtype.mk containing the proof - so why does lean not accept refl as a proof?

[Eric Wieser]

mwe:

import tactic

inductive stars_and_bars : Π s b : ℕ, Type
| nil : stars_and_bars 0 0
| star {s b} (x : stars_and_bars s b) : stars_and_bars (nat.succ s) b
| bar {s b} (x : stars_and_bars s b) : stars_and_bars s (nat.succ b)

namespace stars_and_bars
open list

lemma to_list.star_proof {s b : ℕ} {l : list bool}
  (hl : l.count ff = s ∧ l.count tt = b) :
  (ff :: l).count ff = s.succ ∧ (ff :: l).count tt = b :=
⟨(count_cons_self _ _).trans (congr_arg nat.succ hl.1),
  (count_cons_of_ne tt_eq_ff_eq_false _).trans hl.2⟩

def to_list : Π {s b : ℕ},
  stars_and_bars s b → {l : list bool // l.count ff = s ∧ l.count tt = b}
| 0 0 nil := ⟨[], count_nil _, count_nil _⟩
| _ .(b) (@star s b x) := ⟨ff :: to_list x, stars_and_bars.to_list.star_proof (to_list x).prop⟩
| .(s) _ (@bar s b x) := ⟨tt :: to_list x, sorry⟩

@[simp] lemma to_list_star {s b : ℕ} (x : stars_and_bars s b) :
  to_list (star x) = ⟨ff :: to_list x, to_list.star_proof (to_list x).prop⟩ :=
begin
  rw to_list,
  -- `ff :: ↑(x.to_list), _⟩ = ⟨ff :: ↑(x.to_list), _⟩`, but `refl` fails
  success_if_fail { refl },
  ext : 1,
  -- ↑⟨ff :: ↑(x.to_list), _⟩ = ↑⟨ff :: ↑(x.to_list), _⟩
  simp_rw subtype.coe_mk,
  -- ↑⟨ff :: ↑(x.to_list), _⟩ = ff :: ↑(x.to_list)
  success_if_fail {simp_rw subtype.coe_mk},  -- also fails
  refl -- ok
end

end stars_and_bars

[Kevin Buzzard]

The type of the first missing proof is count ff (ff :: ↑(to_list._main x)) = s.succ ∧ count tt (ff :: ↑(to_list._main x)) = b and the type of the second missing proof is the not-quite-the-same count ff (ff :: ↑(x.to_list)) = s.succ ∧ count tt (ff :: ↑(x.to_list)) = b.

[Eric Wieser]

Indeed - but presumably those types must be defeq else the equality wouldn't be type-correct

[Kevin Buzzard]

begin
  rw to_list,
  have h1 := to_list._main._proof_2 s b x,
  have h2 := to_list.star_proof x.to_list.prop,
  have foo : h1 = h2, -- type mismatch at application

[Eric Wieser]

And yet, the types seem compatible enough that we can state the equality of the subtypes?

[Leonardo de Moura]

@Eric Wieser This looks like a bug in Lean 3. A similar example works as expected in Lean 4.
https://github.com/leanprover/lean4/blob/master/tests/lean/run/starsAndBars.lean

[Eric Wieser]

Whether it reproduced in lean4 was going to be my next question, thanks!