State three vectors are linearly dependent

Stream: new members

[Abdullah Uyu]

How can I rewrite my collinearity relation with the existing linear dependence in LinearAlgebra.LinearIndependent?

import Mathlib.LinearAlgebra.Projectivization.Basic
import Mathlib.LinearAlgebra.Projectivization.Independence

class ProjectiveGeometry (point : Type u) where
ell : point → point → point → Prop
l1  : ∀ a b, ell a b a
l2  : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q : point, ell q a c ∧ ell q b d

instance : ProjectiveGeometry (Projectivization K V) :=
⟨
fun X Y Z => ∃ k1 k2 k3 : K, ¬(k1 = 0 ∧ k2 = 0 ∧ k3 = 0) ∧
k1•X.rep + k2•Y.rep + k3•Z.rep = 0, -- This function should be rewritten.
sorry,
sorry,
sorry
⟩

[Abdullah Uyu]

import Mathlib.LinearAlgebra.Projectivization.Basic
import Mathlib.LinearAlgebra.Projectivization.Independence

class ProjectiveGeometry (point : Type u) where
ell : point → point → point → Prop
l1  : ∀ a b, ell a b a
l2  : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q : point, ell q a c ∧ ell q b d

instance : ProjectiveGeometry (Projectivization K V) :=
⟨
fun X Y Z => ¬ LinearIndependent K ![X.rep, Y.rep, Z.rep],
sorry,
sorry,
sorry
⟩

I think I figured it out, but there are some parts I don't quite get. I don't understand indexing types, and I couldn't find an explicit example of it. By mimicking the library, I wrote the above, but it does not work without !.

• Why is that?
• Also, does this state what I am intending?

[Ruben Van de Velde]

What do you mean by "work without !"?

[Abdullah Uyu]

Ruben Van de Velde said:

What do you mean by "work without !"?

Sorry, just realizing the sentence is a bit awkward (: I initially didn't put the exclamation mark before the list, and it didn't work.

[Abdullah Uyu]

Ruben Van de Velde said:

What do you mean by "work without !"?

But if you ask the error, it's

typeclass instance problem is stuck, it is often due to metavariables
  Module K (?m.2765 X Y Z)

[Eric Wieser]

[x, y, z] is a List _, ![x, y, z] is a Fin 3 -> _. They're completely different to Lean, which is why you can't just expect it to work without the !

[Abdullah Uyu]

Eric Wieser said:

[x, y, z] is a List _, ![x, y, z] is a Fin 3 -> _. They're completely different to Lean, which is why you can't just expect it to work without the !

OK understood. Now I realize I can actually directly use the collinearity condition Projectivization.Independent instead of LinearIndependent. But the following does not type check:

fun X Y Z => ¬ Projectivization.Independent ![X, Y, Z],

it gives:

error: (deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

[Abdullah Uyu]

Meahwhile I am trying to write the proper indexing function instead of using the converter !.

[Abdullah Uyu]

I think there is another problem here, because I get the same error above with the following indexing function:

def index (X Y Z : Projectivization K V) : Fin 3 → Projectivization K V :=
fun i : Fin 3 => match i with
| 0 => X
| 1 => Y
| 2 => Z

[Abdullah Uyu]

I use the indexing function above like this:

fun X Y Z => ¬ Projectivization.Independent (index X Y Z),

[Eric Wieser]

Can you make a mwe?

[Abdullah Uyu]

Of course, give me a second.

[Abdullah Uyu]

import Mathlib.LinearAlgebra.Projectivization.Basic
import Mathlib.LinearAlgebra.Projectivization.Independence

variable [DivisionRing K] [AddCommGroup V] [Module K V]

def index (X Y Z : Projectivization K V) : Fin 3 → Projectivization K V :=
fun i : Fin 3 => match i with
| 0 => X
| 1 => Y
| 2 => Z

class ProjectiveGeometry (point : Type u) where
ell : point → point → point → Prop
l1  : ∀ a b, ell a b a
l2  : ∀ a b p q, ell a p q → ell b p q → p ≠ q → ell a b p
l3  : ∀ a b c d p, ell p a b → ell p c d → ∃ q : point, ell q a c ∧ ell q b d

instance : ProjectiveGeometry (Projectivization K V) :=
  ⟨
  fun X Y Z => ¬ Projectivization.Independent (index X Y Z),
  sorry,
  sorry,
  sorry
  ⟩

Here @Eric Wieser

[Abdullah Uyu]

Eric Wieser said:

Can you make a mwe?

Sorry, I actually get the following error, not the one above; I though it's the same:

error: (deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the
limit)

[Abdullah Uyu]

The former is complaining about isDefEq, the latter whnf.

[Eric Wieser]

The error message is super unhelpful, but the problem is that docs#Projectivization.Independent needs K to be a Field

[Eric Wieser]

I found this out by adding (K := K) before (index X Y Z)

[Eric Wieser]

Lean is concluding that you must be talking about some other field, and so goes on a wild goose chase trying to find out which one before timing out. If you remind it you definitely want K then it fails quickly

[Abdullah Uyu]

Eric Wieser said:

I found this out by adding (K := K) before (index X Y Z)

Do you mean like this?

fun X Y Z => ¬ Projectivization.Independent (K := K) (index X Y Z),

This gives me the same error, do you also change the definition of index?

[Abdullah Uyu]

Eric Wieser said:

Lean is concluding that you must be talking about some other field, and so goes on a wild goose chase trying to find out which one before timing out. If you remind it you definitely want K then it fails quickly

This is funny :big_smile:

[Abdullah Uyu]

But in any case, I may abandon DivisionRing and use Field. The other option may be to generalize Independent for DivisionRing.

[Abdullah Uyu]

@Michael Blyth Why is Projectivization.Independent for Field but not generally for DivisionRing? Would it be hard to generalize?

[Abdullah Uyu]

Eric Wieser said:

Lean is concluding that you must be talking about some other field, and so goes on a wild goose chase trying to find out which one before timing out. If you remind it you definitely want K then it fails quickly

I changed Field to DivisionRing in Projectivization.Independence and it compiled. That was too easy, am I missing something here? :smiley:

[Eric Wieser]

I was going to suggest you try that and see what happened :)

[Notification Bot]

Abdullah Uyu has marked this topic as resolved.

[Eric Wieser]

@Abdullah Uyu, can you make a PR with that change?

[Abdullah Uyu]

Eric Wieser said:

Abdullah Uyu, can you make a PR with that change?

Sure, will look into it when I get a chance to sit before my laptop.

[Eric Wieser]

Would it be hard to generalize?

One thing to watch out for is that sometimes a Lean generalization is meaningless mathematically, even if it compiles; for example, docs#BilinForm does not need the ring to be commutative, but in practice the definition is only the right one when it is.

[Abdullah Uyu]

That is interesting.

Eric Wieser said:

Would it be hard to generalize?

One thing to watch out for is that sometimes a Lean generalization is meaningless mathematically, even if it compiles; for example, docs#BilinForm does not need the ring to be commutative, but in practice the definition is only the right one when it is.

[Abdullah Uyu]

Eric Wieser said:

Abdullah Uyu, can you make a PR with that change?

Alright, I should follow this https://leanprover-community.github.io/contribute/index.html right? It talks about some permission, do I need it?

[Abdullah Uyu]

I guess that is the procedure. My github username is oneofvalts.

[Notification Bot]

Abdullah Uyu has marked this topic as unresolved.

[Eric Wieser]

Abdullah Uyu said:

I guess that is the procedure. My github username is oneofvalts.

Invite sent!

[Abdullah Uyu]

Eric Wieser said:

Abdullah Uyu said:

I guess that is the procedure. My github username is oneofvalts.

Invite sent!

Thank you, just created the PR. I am fairly new to this procedure, so I hope it is OK.