Zulip Chat Archive

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.

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

#mwe ?

Egbert Rijke (May 16 2020 at 17:09):

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?

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

Of course!

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

leanproject upgrade will do that

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

Great!

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

That's easy:)

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

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

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

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

Egbert Rijke (May 16 2020 at 17:23):

Great!

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

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

Egbert Rijke (May 16 2020 at 17:24):

Ok thanks for your help:)

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