Naming Conventions

Stream: new members

[Alex Zhang]

protected def is_sym (A : matrix I I α) : Prop := Aᵀ = A

lemma is_sym_apply {A : matrix I I α} (h : A.is_sym) (i j : I) :
Aᵀ i j = A i j :=
by {simp [matrix.is_sym] at h, rw h}

lemma is_sym_ext {A : matrix I I α} :
(∀ i j, Aᵀ i j = A i j) → A.is_sym :=
by {intro h, ext, exact h i j}

lemma is_sym_iff (A : matrix I I α) : A.is_sym ↔ ∀ i j, Aᵀ i j = A i j :=
⟨is_sym_apply, is_sym_ext⟩

Are the three lemma names I gave consistent with the name conventions?

[Yakov Pechersky]

I wouldn't do protected def. I would call the first lemma is_sym.apply.

[Alex Zhang]

or perhaps

lemma is_sym_ext {A : matrix I I α} (h : A.is_sym) (i j : I) :
Aᵀ i j = A i j :=
by {simp [matrix.is_sym] at h, rw h}

lemma is_sym_of {A : matrix I I α} :
(∀ i j, Aᵀ i j = A i j) → A.is_sym :=
by {intro h, ext, exact h i j}

lemma is_sym_iff (A : matrix I I α) : A.is_sym ↔ ∀ i j, Aᵀ i j = A i j :=
⟨is_sym_ext, is_sym_of⟩

[Alex Zhang]

@Yakov Pechersky I did that because I think matrix.is_sym is parallel with some other .is_syms existing in mathlib. Some bridges can be then built.

[Yakov Pechersky]

I only found sym_sesq_form and sym_bilin_form with is_sym. Neither is protected afaik. The nice part of not protected is that open matrix will let you just say is_sym.

[Alex Zhang]

I am not sure whether there is any advantage of using the dot notation in this case.

[Yakov Pechersky]

Dot notation lets you write h.apply i j to mean Aᵀ i j = A i j when you have (h : A.is_sym) (i j : I)

[Alex Zhang]

oh, that's nice.

[Alex Zhang]

Which version of the lemma names is better do you think? @Yakov Pechersky @Eric Wieser when changing both to is_sym.

[Yakov Pechersky]

I could call the last one as is_sym.ext_iff. Where would you use it?

[Yakov Pechersky]

You can prove it just by rw [is_sym, matrix.ext_iff]

[Alex Zhang]

Yakov Pechersky said:

I could call the last one as is_sym.ext_iff. Where would you use it?

I think that is useful in many further theorems.

[Yakov Pechersky]

Sure, but since you know that A^T = A you could just rewrite that, you don't need to require it to be fully applied.

[Alex Zhang]

Yes. The three lemmas are very simple APIs anyway. I was just a little bit concerned about which names are better.

[Alex Zhang]

Modified according to your suggestion!

def is_sym (A : matrix I I α) : Prop := Aᵀ = A

lemma is_sym.ext_iff {A : matrix I I α} : A.is_sym ↔ ∀ i j, Aᵀ i j = A i j :=
by rw [is_sym, matrix.ext_iff]

lemma is_sym.apply {A : matrix I I α} (h : A.is_sym) (i j : I) :
Aᵀ i j = A i j := is_sym.ext_iff.1 h i j

lemma is_sym.ext {A : matrix I I α} :
(∀ i j, Aᵀ i j = A i j) → A.is_sym := is_sym.ext_iff.2

[Alex Zhang]

It will be useful to prove

def cir (v : fin n → α) : matrix (fin n) (fin n) α
| i j := v (i - j)

lemma cir_is_sym_ext_iff (v : fin n → α) :
(cir v).is_sym ↔ ∀ i j, v (j - i) = v (i - j) :=
by simp [is_sym.ext_iff, cir]

for example.

[Eric Wieser]

Why would you want to prove that and not (cir v).is_sym ↔ ∀ i, v i = v (-i)?

[Eric Wieser]

I'm not really sure any of these lemmas are worth having

[Yakov Pechersky]

You can make them, and then when you use them in a more complex lemma, we can see if there are good golfing strategies that retain expressability/comprehensability

[Eric Wieser]

The only lemma I'd want is is_sym.eq (h : A.is_sym) : Aᵀ = A := h for dot notation.

[Alex Zhang]

I was not careful enough, it should be (cir v).is_sym ↔ ∀ i, v (-i) = v i .

[Alex Zhang]

Eric Wieser said:

The only lemma I'd want is is_sym.eq (h : A.is_sym) : Aᵀ = A := h for dot notation.

Why is this useful? Why don't we just use unfold or simp or etc?

[Eric Wieser]

Because then you can do rw [h.eq]

[Eric Wieser]

see docs#commute.eq which is the same idea

[Alex Zhang]

OK. I see the point.