refl fails to prove `a=a`

Stream: general

[Keefer Rowan]

I got this error message after using the refl tactic,

invalid apply tactic, failed to unify
  ∥2 • x + -(y n + y m)∥ = ∥2 • x + -(y n + y m)∥
with
  ?m_2 = ?m_2

The context is too large to reproduce reasonably here and obviously I shouldn't be able to construct a simple example of this behavior here. Any idea why this could happen?

[Chris Hughes]

What type is x?

[Keefer Rowan]

x : \alpha \alpha : Type*.

[Keefer Rowan]

\alpha is a module over $\mathbb{C}$ also.

[Johan Commelin]

Can you copy paste the goal state?

[Keefer Rowan]

Perhaps one of the two's is of type $\mathbb{C}$ and one is of $\mathbb{N}$ or something like that, how would I check that?

[Keefer Rowan]

∥2 • x + -(y n + y m)∥ = ∥2 • x + -(y n + y m)∥

[Johan Commelin]

No, I mean everything (also the assumptions)

[Chris Hughes]

Can you print what the goal is after set_option pp.all true

[Keefer Rowan]

α : Type u_1,
_inst_1 : add_comm_group α,
_inst_2 : module ℂ α,
_inst_3 : hilbert_space α,
A : submodule ℂ α,
h : is_closed A.carrier,
x : α,
S : set ℝ := range (λ (y : ↥A), ∥x - ↑y∥),
δ : ℝ := Inf S,
x_def : x ∈ ⊤,
S_def : S = range (λ (y : ↥A), ∥x - ↑y∥),
δ_def : δ = Inf S,
p₁ : bdd_below S,
p₂ : S.nonempty,
a : ℕ → ℝ,
a_def₁ : tendsto a at_top (nhds (Inf S)),
a_def₂ : range a ⊆ S,
p₃ : ∀ (n : ℕ), a n ∈ range (λ (y : ↥A), ∥x - ↑y∥),
y : ℕ → α := λ (n : ℕ), (some _).val,
this :
  ∀ (n m : ℕ), 2 * (∥y n - x∥ ^ 2 + ∥y m - x∥ ^ 2) = ∥y n - y m∥ ^ 2 + ∥y n + y m - 2 • x∥ ^ 2,
n m : ℕ,
this : ∥y n - y m∥ ^ 2 + ∥y n + y m - 2 • x∥ ^ 2 = 2 * (∥y n - x∥ ^ 2 + ∥y m - x∥ ^ 2),
this : ∥y n - y m∥ ^ 2 = 2 * (∥y n - x∥ ^ 2 + ∥y m - x∥ ^ 2) - ∥y n + y m - 2 • x∥ ^ 2,
this : ∥-1∥ = 1
⊢ ∥2 • x + -(y n + y m)∥ = ∥2 • x + -(y n + y m)∥

[Johan Commelin]

set_option pp.all true will show you the gory details.

[Johan Commelin]

Use

```
code
more code
```

for code blocks

[Johan Commelin]

Does simp help?

[Chris Hughes]

What's the definition of hilbert_space?

[Johan Commelin]

It might change some invisible things

[Keefer Rowan]

@eq.{1} real
    (@has_norm.norm.{u_1} α
       (@normed_group.to_has_norm.{u_1} α
          (@innerc_product_space_is_normed_group.{u_1} α _inst_1 _inst_2
             (@hilbert_space.to_innerc_product_space.{u_1} α _inst_1 _inst_2 _inst_3)))
       (@has_add.add.{u_1} α
          (@add_semigroup.to_has_add.{u_1} α
             (@add_monoid.to_add_semigroup.{u_1} α
                (@add_group.to_add_monoid.{u_1} α (@add_comm_group.to_add_group.{u_1} α _inst_1))))
          (@has_scalar.smul.{0 u_1} nat α
             (@mul_action.to_has_scalar.{0 u_1} nat α (@semiring.to_monoid.{0} nat nat.semiring)
                (@distrib_mul_action.to_mul_action.{0 u_1} nat α (@semiring.to_monoid.{0} nat nat.semiring)
                   (@add_comm_monoid.to_add_monoid.{u_1} α (@add_comm_group.to_add_comm_monoid.{u_1} α _inst_1))
                   (@semimodule.to_distrib_mul_action.{0 u_1} nat α nat.semiring
                      (@add_comm_group.to_add_comm_monoid.{u_1} α _inst_1)
                      (@add_comm_monoid.nat_semimodule.{u_1} α
                         (@add_comm_group.to_add_comm_monoid.{u_1} α _inst_1)))))
             (@bit0.{0} nat nat.has_add (@has_one.one.{0} nat nat.has_one))
             x)
          (@has_neg.neg.{u_1} α (@add_group.to_has_neg.{u_1} α (@add_comm_group.to_add_group.{u_1} α _inst_1))
             (@has_add.add.{u_1} α
                (@add_semigroup.to_has_add.{u_1} α
                   (@add_monoid.to_add_semigroup.{u_1} α
                      (@add_group.to_add_monoid.{u_1} α (@add_comm_group.to_add_group.{u_1} α _inst_1))))
                (y n)
                (y m)))))
    (@has_norm.norm.{u_1} α
       (@normed_group.to_has_norm.{u_1} α
          (@innerc_product_space_is_normed_group.{u_1} α _inst_1 _inst_2
             (@hilbert_space.to_innerc_product_space.{u_1} α _inst_1 _inst_2 _inst_3)))
       (@has_add.add.{u_1} α
          (@add_semigroup.to_has_add.{u_1} α
             (@add_monoid.to_add_semigroup.{u_1} α
                (@add_group.to_add_monoid.{u_1} α (@add_comm_group.to_add_group.{u_1} α _inst_1))))
          (@has_scalar.smul.{0 u_1} complex α
             (@mul_action.to_has_scalar.{0 u_1} complex α
                (@ring.to_monoid.{0} complex
                   (@normed_ring.to_ring.{0} complex (@normed_field.to_normed_ring.{0} complex complex.normed_field)))
                (@distrib_mul_action.to_mul_action.{0 u_1} complex α
                   (@ring.to_monoid.{0} complex
                      (@normed_ring.to_ring.{0} complex
                         (@normed_field.to_normed_ring.{0} complex complex.normed_field)))
                   (@add_group.to_add_monoid.{u_1} α (@add_comm_group.to_add_group.{u_1} α _inst_1))
                   (@semimodule.to_distrib_mul_action.{0 u_1} complex α
                      (@nonzero_semiring.to_semiring.{0} complex
                         (@nonzero_comm_semiring.to_nonzero_semiring.{0} complex
                            (@nonzero_comm_ring.to_nonzero_comm_semiring.{0} complex
                               (@local_ring.to_nonzero_comm_ring.{0} complex
                                  (@field.local_ring.{0} complex complex.field)))))
                      (@add_comm_group.to_add_comm_monoid.{u_1} α _inst_1)
                      (@module.to_semimodule.{0 u_1} complex α
                         (@normed_ring.to_ring.{0} complex
                            (@normed_field.to_normed_ring.{0} complex complex.normed_field))
                         _inst_1
                         _inst_2))))
             (@bit0.{0} complex complex.has_add (@has_one.one.{0} complex complex.has_one))
             x)
          (@has_neg.neg.{u_1} α (@add_group.to_has_neg.{u_1} α (@add_comm_group.to_add_group.{u_1} α _inst_1))
             (@has_add.add.{u_1} α
                (@add_semigroup.to_has_add.{u_1} α
                   (@add_monoid.to_add_semigroup.{u_1} α
                      (@add_group.to_add_monoid.{u_1} α (@add_comm_group.to_add_group.{u_1} α _inst_1))))
                (y n)
                (y m)))))

[Chris Hughes]

I think you might have two different module ℂ α instances.

[Johan Commelin]

Also, it seems like you constructed y using choice, so I guess you need to use some_spec at some point

[Keefer Rowan]

class hilbert_space (α : Type*) [add_comm_group α] [module ℂ α] extends innerc_product_space α, complete_space α.

[Keefer Rowan]

class innerc_product_space (α : Type*) [add_comm_group α] [module ℂ α] extends sesq_form ℂ α (ring_anti_equiv.mk (function.involutive.to_equiv conj conj_involutive)) :=
(herm : ∀ x y, sesq x y = conj (sesq y x))
(nonneg    : ∀ x, 0 ≤ (sesq x x).re)
(definite  : ∀ x, sesq x x = 0 → x = 0)

[Reid Barton]

Try congr

[Johan Commelin]

You have two different mul_actions in that printout

[Chris Hughes]

The 2 on the left is a nat, but the 2 on the right is complex I think.

[Johan Commelin]

Yup

[Johan Commelin]

So I hope simp will help

[Chris Hughes]

Do we have those simp lemmas?

[Johan Commelin]

I hope so

[Keefer Rowan]

After simp with pp : ⊢ ∥2 • x + (-y m + -y n)∥ = ∥2 • x + (-y m + -y n)∥

[Johan Commelin]

@Keefer Rowan So the problem is that the \bu is used in two different ways

[Keefer Rowan]

Do we have that (2 : \N) \bu x = x + x? And then (2:\C) \bu x is given by the module structure?

[Chris Hughes]

What should simp normal form be for this. Move everything to nat I guess is the only choice.

[Chris Hughes]

I bet simp [bit0] will work.

[Johan Commelin]

Keefer Rowan said:

Do we have that (2 : \N) \bu x = x + x? And then (2:\C) \bu x is given by the module structure?

rw [show 2 = 1 + 1, from rfl, add_smul]

[Keefer Rowan]

      simp [bit0],
      rw [add_smul, add_smul, one_smul, one_smul],

showed it.

Thanks all!

Any way to get the pp to show types of numerals?

[Reid Barton]

That's a nice idea. Probably if they aren't nat?

[Johan Commelin]

Could something like elide be used for that? (Not elide itself, but similar concept maybe?)