rewrite goal

Stream: new members

[Thorsten Altenkirch]

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]

You need triple #backticks

[Thorsten Altenkirch]

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]

you can edit your posts too

[Mario Carneiro]

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

[Kevin Buzzard]

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

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

[Mario Carneiro]

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

[Mario Carneiro]

which is equivalent to Kevin's proof

[Mario Carneiro]

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]

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]

I am always looking for places to do cases on stuff

[Mario Carneiro]

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]

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

[Kevin Buzzard]

inb4 Mario

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

theorem cons : ¬ (tt = ff).

[Kevin Buzzard]

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

[Mario Carneiro]

Mario Carneiro said:

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

[Kevin Buzzard]

dammit I haven't got my glasses on

[Kevin Buzzard]

I missed the full stop :-)

[Kevin Buzzard]

touch\'e

[Kevin Buzzard]

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

[Thorsten Altenkirch]

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

[Mario Carneiro]

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