# Zulip Chat Archive

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