rfl vs by reflexivity

Stream: general

[Egbert Rijke]

Sometimes by reflexivity does the job, whereas rfl isn't accepted. Can anyone tell the difference between the two?

[Kevin Buzzard]

The reflexivity tactic will close any goal of the form R a a where R is a relation tagged with the [refl] attribute

[Patrick Massot]

https://leanprover-community.github.io/mathlib_docs/tactics.html#refl%20/%20reflexivity

[Bhavik Mehta]

I think the difference you're observing is based on the relation in question - rfl will prove anything like a = a but reflexivity will work for any reflexive relation, not just equality

[Patrick Massot]

It's all in the doc.

[Egbert Rijke]

Kevin Buzzard said:

The reflexivity tactic will close any goal of the form R a a where R is a relation tagged with the [refl] attribute

But they even seem to differ when you're doing ordinary equational reasoning. I'm not working with more general relations at the moment.

[Kevin Buzzard]

#mwe ?

[Egbert Rijke]

Here is my mwe

[Egbert Rijke]

At the end there is an application of by reflexivity which can't be replaced by rfl

[Egbert Rijke]

PS, I'm still on 3.11 because I don't know how to update with elan. The install guide only told me how to install it, but not how to keep it up to date :P

[Patrick Massot]

Seems like an elaboration order issue. It works with by exact rfl

[Patrick Massot]

And replacing the whole calc by rfl works

[Egbert Rijke]

Ah that simplifies things :)

[Patrick Massot]

About your updating question, I need more context. Did you create a Lean project using leanproject?

[Egbert Rijke]

Yes, using leanproject new ...

[Patrick Massot]

And you want to upgrade to the latest shiny Lean+mathlib?

[Egbert Rijke]

Of course!

[Patrick Massot]

leanproject upgrade will do that

[Egbert Rijke]

Great!

[Egbert Rijke]

That's easy:)

[Egbert Rijke]

Thanks a lot!

[Kevin Buzzard]

Not just up?

[Patrick Massot]

That's when I'll get so addicted to it that he'll want to do it several times a day

[Patrick Massot]

like you do

[Egbert Rijke]

Actually, leanproject upgrade was countered by no such command exists. But leanproject up works, so I guess I might as well be an addict XD

[Patrick Massot]

Oh sorry, it's upgrade-mathlib

[Patrick Massot]

I've been addicted for too long, I forgot the long version

[Patrick Massot]

I need to add more synonyms. I already have upgrade-mathlib, update-mathlib and up

[Patrick Massot]

(because nobody can remember whether it's update or upgrade)

[Patrick Massot]

Another trick: leanproject --help can help.

[Egbert Rijke]

Do I need to restart vscode when I've upgraded lean, or is that not necessary?

[Patrick Massot]

I think the extension detects it and restarts lean

[Egbert Rijke]

Great!

[Patrick Massot]

(but restarting VScode just in case would have been faster than typing the question)

[Egbert Rijke]

Ok thanks for your help:)

[Jalex Stark]

Egbert Rijke said:

Here is my mwe

Why upload a file instead of copy-pasting the text? The latter should be easier for both you and the people who want to read your example?

namespace mwe

universes u v w

inductive list_of_length (A : Type u) : ℕ → Type u
| nil : list_of_length 0
| cons : ∀ (n : ℕ), A → list_of_length n → list_of_length (n+1)

namespace list_of_length

def head {A : Type u} :
    ∀ (n : ℕ), list_of_length A (n+1) → A
| n (cons n' a x) := a

def tail {A : Type u} :
    ∀ (n : ℕ), list_of_length A (n+1) → list_of_length A n
| n (cons n' a x) := x

def Matrix (m n : ℕ) (A : Type u) : Type u :=
list_of_length (list_of_length A n) m

def top_row {A : Type u} {m n : ℕ} :
    Matrix (m+1) n A → list_of_length A n :=
head m

def tail_rows {A : Type u} {m n : ℕ} :
    Matrix (m+1) n A → Matrix m n A :=
tail m

def cons_horizontal {A : Type u} :
    ∀ {m n : ℕ}, list_of_length A m → Matrix m n A → Matrix m (n+1) A
| 0 n nil M := nil
| (m+1) n (cons m' a x) M :=
    cons m (cons n a (top_row M)) (cons_horizontal x (tail_rows M))

theorem top_row_cons_horizontal {A : Type u} :
    ∀ {m n : ℕ} (x : list_of_length A (m+1)) (M : Matrix (m+1) n A),
    top_row (cons_horizontal x M) = cons n (head m x) (top_row M)
| m n (cons m' a x) (cons m'' y M) :=
    calc
    top_row (cons_horizontal (cons m' a x) (cons m'' y M))
        = cons n a y : rfl
    ... = cons n (head m (cons m' a x)) (top_row (cons m'' y M)) : by reflexivity

end list_of_length

end mwe

[Egbert Rijke]

Ok, I'll do that next time. Thanks!

[Bryan Gin-ge Chen]

You can also restart Lean without restarting VS Code by hitting ctrl+P and typing "Lean restart" into the command palette. You can assign a keybind to it by searching for the same thing in the VS Code keybinds.