Zulip Chat Archive

Stream: new members

Topic: rewrite goal


view this post on Zulip Thorsten Altenkirch (Sep 21 2020 at 15:04):

I couldn't find a tactic to rewrite the current goal. I can use have but this seems to be a bit verbose. E.g. like in the following example
``
def is_tt : bool → Prop
| ff := false
| tt := true

-- BEGIN
theorem cons : ¬ (tt = ff) :=
begin
assume h,
have aux : is_tt ff,
rewrite← h,
constructor,
exact aux,
end

view this post on Zulip Johan Commelin (Sep 21 2020 at 15:04):

You need triple #backticks

view this post on Zulip Thorsten Altenkirch (Sep 21 2020 at 15:05):

Is there a tactic to rewrite the current goal? I can use have but this seems to be a bit verbose. E.g.


view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:06):

you can edit your posts too

view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:07):

rw will rewrite in the current goal. Could you give an example of what you would like to write?

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:08):

def is_tt : bool  Prop
| ff := false
| tt := true

-- BEGIN
theorem cons : ¬ (tt = ff) :=
begin
assume h,
cases h,
end

view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:08):

by the way you can prove this theorem using simply theorem cons : ¬ (tt = ff).

view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:08):

which is equivalent to Kevin's proof

view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:09):

but I can see you are going for the proof that doesn't use the builtin knowledge that cases has about injectivity of constructors

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:10):

Rewriting h : X = Y with X a variable can sometimes be done more powerfully in Lean by using subst h or cases h. If these work they might globally replace X by Y

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:10):

I am always looking for places to do cases on stuff

view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:10):

I would suggest presenting your proof like so:

def is_tt : bool  Prop
| ff := false
| tt := true

theorem cons : tt  ff :=
begin
  assume h,
  change is_tt ff,
  rw  h,
  trivial
end

view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:10):

you can also insert change true before the trivial to make it clearer

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:11):

inb4 Mario

def is_tt : bool  Prop
| ff := false
| tt := true

theorem cons : ¬ (tt = ff).

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:11):

@Thorsten Altenkirch the equation compiler can prove your theorem all by itself.

view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:11):

Mario Carneiro said:

by the way you can prove this theorem using simply theorem cons : ¬ (tt = ff).

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:12):

dammit I haven't got my glasses on

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:12):

I missed the full stop :-)

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:12):

touch\'e

view this post on Zulip Kevin Buzzard (Sep 21 2020 at 15:12):

My VS Code font is a lot bigger than my Zulip font :-)

view this post on Zulip Thorsten Altenkirch (Sep 21 2020 at 15:27):

I know that I can prove it directly but I just wanted to show how to prove it from basic principles.

view this post on Zulip Mario Carneiro (Sep 21 2020 at 15:34):

Kevin should be familiar with this from his blog post no confusion over no_confusion


Last updated: May 11 2021 at 22:14 UTC