## Stream: general

### Topic: rfl vs by reflexivity

#### Egbert Rijke (May 16 2020 at 16:58):

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

#### Kevin Buzzard (May 16 2020 at 16:59):

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 (May 16 2020 at 16:59):

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

#### Bhavik Mehta (May 16 2020 at 17:00):

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 (May 16 2020 at 17:00):

It's all in the doc.

#### Egbert Rijke (May 16 2020 at 17:01):

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.

#mwe ?

Here is my mwe

#### Egbert Rijke (May 16 2020 at 17:10):

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

#### Egbert Rijke (May 16 2020 at 17:11):

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 (May 16 2020 at 17:13):

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

#### Patrick Massot (May 16 2020 at 17:13):

And replacing the whole calc by rfl works

#### Egbert Rijke (May 16 2020 at 17:14):

Ah that simplifies things :)

#### Patrick Massot (May 16 2020 at 17:14):

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

#### Egbert Rijke (May 16 2020 at 17:15):

Yes, using leanproject new ...

#### Patrick Massot (May 16 2020 at 17:15):

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

Of course!

#### Patrick Massot (May 16 2020 at 17:16):

leanproject upgrade will do that

Great!

That's easy:)

Thanks a lot!

#### Kevin Buzzard (May 16 2020 at 17:16):

Not just up?

#### Patrick Massot (May 16 2020 at 17:17):

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

like you do

#### Egbert Rijke (May 16 2020 at 17:18):

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 (May 16 2020 at 17:19):

Oh sorry, it's upgrade-mathlib

#### Patrick Massot (May 16 2020 at 17:19):

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

#### Patrick Massot (May 16 2020 at 17:20):

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

#### Patrick Massot (May 16 2020 at 17:20):

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

#### Patrick Massot (May 16 2020 at 17:21):

Another trick: leanproject --help can help.

#### Egbert Rijke (May 16 2020 at 17:22):

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

#### Patrick Massot (May 16 2020 at 17:23):

I think the extension detects it and restarts lean

Great!

#### Patrick Massot (May 16 2020 at 17:23):

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

#### Jalex Stark (May 16 2020 at 17:44):

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 :=

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 (May 16 2020 at 17:55):

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

#### Bryan Gin-ge Chen (May 16 2020 at 19:01):

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.

Last updated: Dec 20 2023 at 11:08 UTC