## 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?

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.

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?

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

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