## Stream: general

### Topic: another decidable_eq problem

#### Heather Macbeth (Jan 13 2021 at 01:58):

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 (Jan 13 2021 at 02:00):

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 (Jan 13 2021 at 02:01):

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 (Jan 13 2021 at 03:02):

Maybe adding a decidable_eq iota  argument to basis_constructor might help?

#### Frédéric Dupuis (Jan 13 2021 at 03:57):

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 (Jan 13 2021 at 04:10):

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 (Jan 13 2021 at 04:17):

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

#### Heather Macbeth (Jan 13 2021 at 04:18):

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 (Jan 13 2021 at 04:19):

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

#### Heather Macbeth (Jan 13 2021 at 04:22):

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 (Jan 13 2021 at 04:41):

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

#### Frédéric Dupuis (Jan 13 2021 at 04:42):

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 (Jan 13 2021 at 08:07):

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 (Jan 13 2021 at 15:40):

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 (Jan 14 2021 at 00:03):

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 (Jan 14 2021 at 00:21):

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

Last updated: May 06 2021 at 21:09 UTC