!4#4473 Proving that Gram–Schmidt terminates

Stream: mathlib4

[Jeremy Tan]

The following recursive definition of the Gram–Schmidt process doesn't work in Lean 4; how can I get it to work?

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.LinearAlgebra.Matrix.Block

open scoped BigOperators

open Finset Submodule FiniteDimensional

variable (𝕜 : Type _) {E : Type _} [IsROrC 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]

variable {ι : Type _} [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι (· < ·)]

attribute [local instance] IsWellOrder.toHasWellFounded

local notation "⟪" x ", " y "⟫" => @inner 𝕜 _ _ x y

noncomputable def gramSchmidt (f : ι → E) : ι → E
  | n => f n - ∑ i : Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
  termination_by gramSchmidt f n => n
  decreasing_by exact mem_Iio.1 i.2

[Mario Carneiro]

try have : i < n := ... inside the sigma

[Jeremy Tan]

As it is I get a huge number of identical copies of the error

type mismatch
  Iff.mp mem_Iio i.property
has type
  ↑i < n : Prop
but is expected to have type
  (invImage (fun a ↦ a) instWellFoundedRelation).1 (↑i) a✝ : Prop

With

noncomputable def gramSchmidt (f : ι → E) : ι → E
  | n => f n - ∑ i : Iio n,
    have : i < n := by exact mem_Iio.1 i.2
    orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
  termination_by gramSchmidt f n => n

I'm instead getting this error on gramSchmidt f i:

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
ι: Type u_3
inst✝¹: LinearOrder ι
inst✝: LocallyFiniteOrderBot ι
a✝: ι
n: ι := a✝
i: { x // x ∈ Iio n }
this: ↑i < n
⊢ False

And I believe that my termination_by is correct since n is of the well-founded type ι

[Mario Carneiro]

oh, I just noticed that you are doing well founded recursion on a weird type

[Mario Carneiro]

It needs to be something with a WellFoundedRelation instance, not sure if IsWellOrder implies that

[Jeremy Tan]

Ultimately all of this is from !4#4473. I can see that the induction is on n : ι; given that I have [LinearOrder ι] [LocallyFiniteOrderBot ι] [IsWellOrder ι (· < ·)] how can I get a proper WellFoundedRelation from this, and state termination_by correctly?

[Mario Carneiro]

Note that in the (invImage (fun a ↦ a) instWellFoundedRelation).1 (↑i) a✝ : Prop error message, if you dig down into instWellFoundedRelation you will notice that it uses instSizeOf, i.e. the default well order on any type which comes from the default sizeof which makes everything 0, which is the empty relation

[Mario Carneiro]

oh, and using termination_by' IsWellOrder.toHasWellFounded fails because of

failed to synthesize instance
  IsWellOrder ι fun x x_1 ↦ x < x_1

...which is true, the well order instance is not in the context

[Mario Carneiro]

this is really interesting. The following works:

variable {ι : Type _} [LinearOrder ι] [LocallyFiniteOrderBot ι] [inst : IsWellOrder ι (· < ·)]

attribute [local instance] IsWellOrder.toHasWellFounded

noncomputable def gramSchmidt (f : ι → E) (n : ι) : E :=
  have := inst
  f n - ∑ i : Iio n, have : i < n := sorry; orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
termination_by _ n => n

but

noncomputable def gramSchmidt (f : ι → E) (n : ι) : E :=
  f n - ∑ i : Iio n, have : i < n := sorry; orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
termination_by _ n =>
  have := inst
  n

gives unknown identifier 'inst' at the have := inst line. Apparently, the full set of variables is available in the body of the definition, but once it is processed anything which was not referenced is not included in the context for the termination_by and other clauses

[Jeremy Tan]

Mario Carneiro said:

The following works:

variable {ι : Type _} [LinearOrder ι] [LocallyFiniteOrderBot ι] [inst : IsWellOrder ι (· < ·)]

attribute [local instance] IsWellOrder.toHasWellFounded

noncomputable def gramSchmidt (f : ι → E) (n : ι) : E :=
  have := inst
  f n - ∑ i : Iio n, have : i < n := sorry; orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
termination_by _ n => n

no it still gives unknown identifier 'inst' at the have := inst line

[Mario Carneiro]

note the modification to the variable line

[Jeremy Tan]

oh

[Mario Carneiro]

(this is the sort of situation where one wishes for the include command)

[Mario Carneiro]

another alternative is to put the [IsWellOrder ι (· < ·)] argument on the definition itself instead of in a variable

[Mario Carneiro]

i.e.

noncomputable def gramSchmidt [IsWellOrder ι (· < ·)] (f : ι → E) (n : ι) : E :=
  f n - ∑ i : Iio n, orthogonalProjection (𝕜 ∙ gramSchmidt f i) (f n)
termination_by _ n => n
decreasing_by exact mem_Iio.1 i.2

[Jeremy Tan]

OK, that works; I've just pushed it

[Jeremy Tan]

The next error I can't seem to fix is at gramSchmidtOrthonormalBasis:

noncomputable def gramSchmidtOrthonormalBasis : OrthonormalBasis ι 𝕜 E :=
  ((gramSchmidt_orthonormal' f).exists_orthonormalBasis_extension_of_card_eq h).some

the error being

application type mismatch
  Orthonormal.exists_orthonormalBasis_extension_of_card_eq h (gramSchmidt_orthonormal' f)
argument
  gramSchmidt_orthonormal' f
has type
  Orthonormal 𝕜 fun i ↦ gramSchmidtNormed 𝕜 f ↑i : Prop
but is expected to have type
  Orthonormal 𝕜 (restrict { i | gramSchmidtNormed 𝕜 f i ≠ 0 } ?m.424507) : Prop

In mathlib3 the restrict was applied automatically

[Jeremy Tan]

how to fix this?

[Jeremy Tan]

Anyone?