Zulip Chat Archive

Stream: general

Topic: rfl vs by reflexivity


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 16 2020 at 16:59):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 16 2020 at 17:00):

It's all in the doc.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 16 2020 at 17:05):

#mwe ?

view this post on Zulip Egbert Rijke (May 16 2020 at 17:09):

Here is my mwe

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 16 2020 at 17:13):

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

view this post on Zulip Patrick Massot (May 16 2020 at 17:13):

And replacing the whole calc by rfl works

view this post on Zulip Egbert Rijke (May 16 2020 at 17:14):

Ah that simplifies things :)

view this post on Zulip Patrick Massot (May 16 2020 at 17:14):

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

view this post on Zulip Egbert Rijke (May 16 2020 at 17:15):

Yes, using leanproject new ...

view this post on Zulip Patrick Massot (May 16 2020 at 17:15):

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

view this post on Zulip Egbert Rijke (May 16 2020 at 17:15):

Of course!

view this post on Zulip Patrick Massot (May 16 2020 at 17:16):

leanproject upgrade will do that

view this post on Zulip Egbert Rijke (May 16 2020 at 17:16):

Great!

view this post on Zulip Egbert Rijke (May 16 2020 at 17:16):

That's easy:)

view this post on Zulip Egbert Rijke (May 16 2020 at 17:16):

Thanks a lot!

view this post on Zulip Kevin Buzzard (May 16 2020 at 17:16):

Not just up?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 16 2020 at 17:17):

like you do

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 16 2020 at 17:19):

Oh sorry, it's upgrade-mathlib

view this post on Zulip Patrick Massot (May 16 2020 at 17:19):

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

view this post on Zulip Patrick Massot (May 16 2020 at 17:20):

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

view this post on Zulip Patrick Massot (May 16 2020 at 17:20):

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

view this post on Zulip Patrick Massot (May 16 2020 at 17:21):

Another trick: leanproject --help can help.

view this post on Zulip Egbert Rijke (May 16 2020 at 17:22):

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

view this post on Zulip Patrick Massot (May 16 2020 at 17:23):

I think the extension detects it and restarts lean

view this post on Zulip Egbert Rijke (May 16 2020 at 17:23):

Great!

view this post on Zulip Patrick Massot (May 16 2020 at 17:23):

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

view this post on Zulip Egbert Rijke (May 16 2020 at 17:24):

Ok thanks for your help:)

view this post on Zulip 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

view this post on Zulip Egbert Rijke (May 16 2020 at 17:55):

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

view this post on Zulip 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: May 10 2021 at 00:31 UTC