Zulip Chat Archive

Stream: general

Topic: another decidable_eq problem


view this post on Zulip 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!

view this post on Zulip 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***
 ```

view this post on Zulip 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)

view this post on Zulip Chris Hughes (Jan 13 2021 at 03:02):

Maybe adding a decidable_eq iota argument to basis_constructor might help?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip 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