another decidable_eq problem

Stream: general

[Heather Macbeth]

Something is wrong with my definition of orthonormal here: as evidence, note that if orthonormal is changed to linear_independent throughout, then there are no errors.

import analysis.normed_space.inner_product

open_locale classical
open finite_dimensional

variables (𝕜 : Type*) {E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
variables {ι : Type*}

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

def orthonormal [decidable_eq ι] (v : ι → E) : Prop :=
∀ i j, ⟪v i, v j⟫ = if i = j then (1:𝕜) else (0:𝕜)

lemma basis_constructor [fintype ι] [nonempty ι]
  {v : ι → E} (he : orthonormal 𝕜 v) (card_eq : fintype.card ι = findim 𝕜 E) :
  is_basis 𝕜 v :=
sorry

variables (E)

def my_set [finite_dimensional 𝕜 E] : fin (findim 𝕜 E) → E := sorry

lemma my_set_spec [finite_dimensional 𝕜 E] : orthonormal 𝕜 (my_set 𝕜 E) := sorry

instance : nonempty (fin (findim 𝕜 E)) := sorry

example [finite_dimensional 𝕜 E] : is_basis 𝕜 (my_set 𝕜 E) :=
basis_constructor 𝕜 (my_set_spec 𝕜 E) (by simp) -- error is here!

[Heather Macbeth]

The error message is a beauty!

type mismatch at application
  basis_constructor 𝕜 (my_set_spec 𝕜 E)
term
  my_set_spec 𝕜 E
has type
 @orthonormal 𝕜 E _inst_1 _inst_2
    (fin
       (@findim 𝕜 E
          (@normed_field.to_field 𝕜 ... ***etc etc***
but is expected to have type ***etc etc***
 ```

[Heather Macbeth]

But run through diff-checker, the difference in terms is

classical.prop_decidable (a = b))

vs

@subtype.decidable_eq ℕ
  (λ (x : ℕ),
    x <
      @findim 𝕜 E
        (@normed_field.to_field 𝕜
            (@nondiscrete_normed_field.to_normed_field 𝕜
              (@is_R_or_C.to_nondiscrete_normed_field 𝕜 _inst_1)))
        (@normed_group.to_add_comm_group E (@inner_product_space.to_normed_group 𝕜 E _inst_1 _inst_2))
        (@normed_space.to_semimodule 𝕜 E
            (@nondiscrete_normed_field.to_normed_field 𝕜
              (@is_R_or_C.to_nondiscrete_normed_field 𝕜 _inst_1))
            (@inner_product_space.to_normed_group 𝕜 E _inst_1 _inst_2)
            (@inner_product_space.to_normed_space 𝕜 E _inst_1 _inst_2)))
  (λ (a b : ℕ), nat.decidable_eq a b)
  a
  b)

[Chris Hughes]

Maybe adding a decidable_eq iota argument to basis_constructor might help?

[Frédéric Dupuis]

I think I would have just given up with this decidable_eq stuff and gone with something like

def orthonormal (v : ι → E) : Prop :=
(∀ i, ∥v i∥ = 1) ∧ (∀ i j, i ≠ j → ⟪v i, v j⟫ = 0)

[Heather Macbeth]

Thanks both! I really would like to get it working the "if then else" way. It feels like whack-a-mole: Chris' idea solves my toy example (posted here) but creates new problems in my real use case. I have tried twice to get a useful #mwe, without success, so let me just link the branch:
https://github.com/leanprover-community/mathlib/compare/exists-orthonormal-basis
it would be great if someone has the energy to track down the issue.

[Frédéric Dupuis]

Is there any particular reason to use if-then-else if it creates this mess?

[Heather Macbeth]

Good question! ... it's just a hunch, but I suspect that arguments like the following will be cleaner:

/-- An orthonormal set is linearly independent. -/
lemma linear_independent_of_orthonormal (v : ι → E) (he : orthonormal 𝕜 v) :
  linear_independent 𝕜 v :=
begin
  rw linear_independent_iff,
  intros l hl,
  ext i,
  have h_fun : (λ j a, a * ⟪v i, v j⟫) = λ j a, a * (if i = j then (1:𝕜) else (0:𝕜)),
  { ext j,
    simp [he i j] },
  have key : ⟪v i, finsupp.total ι E 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw hl,
  simpa [finsupp.total_apply, finsupp.inner_sum, h_fun] using key
end

[Heather Macbeth]

anything with summing, anything where one would write it on paper using https://en.wikipedia.org/wiki/Kronecker_delta

[Heather Macbeth]

I haven't tried it, but it feels like one would have to break into cases to prove the above lemma using the other definition?

[Frédéric Dupuis]

I see. Yeah, maybe I just don't have enough patience for this sort of typeclass mess :-)

[Frédéric Dupuis]

Though for a case like this we would probably anyway want a lemma stating l.sum (λ j a, a * ⟪v i, v j⟫) = l i.

[Sebastien Gouezel]

I'd go for Frédéric's solution, which avoids all the mess (but you would still prove the lemmas that ⟪v i, v i⟫ = 1 and ⟪v i, v j⟫ = 0 for i different from j, which is what you really need). If you really want to go for the ite definition, a way to fix things is probably to remove open_locale classical, and add decidable_eq assumptions in all the statements where Lean complains. But IMHO having less typeclasses in definitions is good; because it means Lean will have to work less whenever it encounters the definition.

[Heather Macbeth]

Sebastien Gouezel said:

If you really want to go for the ite definition, a way to fix things is probably to remove open_locale classical, and add decidable_eq assumptions in all the statements where Lean complains.

I got it working with this suggestion. Now that my pride has been satisfied with this small victory over Lean, perhaps I can switch to Frédéric's method :)

[Joseph Myers]

Heather Macbeth said:

Good question! ... it's just a hunch, but I suspect that arguments like the following will be cleaner:

/-- An orthonormal set is linearly independent. -/
lemma linear_independent_of_orthonormal (v : ι → E) (he : orthonormal 𝕜 v) :
  linear_independent 𝕜 v :=

Frédéric's definition looks like it should be convenient for deducing that from linear_independent_of_ne_zero_of_inner_eq_zero.

[Heather Macbeth]

Ah, thanks for the pointer, I didn't know we had this already!