## Stream: new members

### Topic: rewrite goal

#### 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

#### Johan Commelin (Sep 21 2020 at 15:04):

You need triple #backticks

#### 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.




#### Mario Carneiro (Sep 21 2020 at 15:06):

you can edit your posts too

#### 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?

#### 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


#### Mario Carneiro (Sep 21 2020 at 15:08):

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

#### Mario Carneiro (Sep 21 2020 at 15:08):

which is equivalent to Kevin's proof

#### 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

#### 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

#### Kevin Buzzard (Sep 21 2020 at 15:10):

I am always looking for places to do cases on stuff

#### 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


#### Mario Carneiro (Sep 21 2020 at 15:10):

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

#### Kevin Buzzard (Sep 21 2020 at 15:11):

inb4 Mario

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

theorem cons : ¬ (tt = ff).


#### Kevin Buzzard (Sep 21 2020 at 15:11):

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

#### 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).

#### Kevin Buzzard (Sep 21 2020 at 15:12):

dammit I haven't got my glasses on

#### Kevin Buzzard (Sep 21 2020 at 15:12):

I missed the full stop :-)

touch\'e

#### Kevin Buzzard (Sep 21 2020 at 15:12):

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

#### 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.

#### 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