1 ≠ -1 in ℤˣ?

Stream: Is there code for X?

[Alex Kontorovich]

This one is quite stupid. Help please?

example : (1 : ℤˣ) ≠ -1 :=
begin
  sorry,
end

[Adam Topaz]

I'm not next to Lean, but will dec_trivial do it?

[Julian Berman]

Seems like yes -- and hint looks like it indeed suggests dec_trivial (saying it solves the goal) which is sometimes a good thing to try for silly looking things.

[Ruben Van de Velde]

I would have tried norm_num

[Junyan Xu]

example : (1 : ℤˣ) ≠ -1 := λ h, by cases h

[Adam Topaz]

The ultimate golf:

example : (1 : ℤˣ) ≠ -1 .

[Alex Kontorovich]

What is that??? The dot does something like dec_trivial?...

[Junyan Xu]

A single dot generates the same term as my version, which is much longer than the term generated by dec_trivial (when printed with set_option pp.implicit true. dec_trivial uses existing instances so it only needs to check the units.val agree, but it might take more time to find those instances.

[Martin Dvořák]

Is there a documentation for . please?

[Junyan Xu]

example : (1 : ℤˣ) ≠ -1 . is a pattern matching proof but since there's no pattern to be matched you need to append a dot.

[Junyan Xu]

The same reason as why cases h solves the goal (because it generates zero goals).

[Jason Rute]

I would also like to see the dot proofs explained better in documentation or a blog post. Does something like this also work for Lean 4?

[Antoine Chambert-Loir]

While dec_trivial and other easy proofs exist, I had to make a proof by contradiction in permutation group theory, where the contradiction came from 1 \neq -1. Therefore, I believe that it should be in mathlib so that we can apply it and get the contradiction.

[Junyan Xu]

The dot (period) has the effect of instructing Lean to stop parsing (and possibly more), which is also useful when e.g. you are writing a new proof but want to keep the old proof around without commenting it out: you can insert a period (surrounded by one whitespace each side) between the new proof and the old proof, and then the old proof won't interfere with the new proof. (Mostly useful for term-mode proofs.)

[Junyan Xu]

where the contradiction came from 1 \neq -1

If you have h : 1 = -1 in the context, you can just do cases h to close the goal (or apply absurd h, dec_trivial). But maybe I didn't imagine your situation correctly.

[Antoine Chambert-Loir]

I'll check if that suffices!

[Mario Carneiro]

Jason Rute said:

I would also like to see the dot proofs explained better in documentation or a blog post. Does something like this also work for Lean 4?

Lean 4 doesn't support exactly this syntax, but since I like this proof so much I added a similar syntax for it. With Std.Tactic.NoMatch you can write

example : (1 : ℤˣ) ≠ -1 := fun.

to similar effect.

[Mario Carneiro]

There isn't that much to explain: it's an empty pattern match, exactly the same as other equation compiler definitions except there are zero match arms

[Julian Berman]

They're called auto_params in case it's helpful for searching (I thought I remembered a thread where I asked about them and got linked something in TPiL but seems I'm misremembering)

[Mario Carneiro]

that's the wrong "dot proof"

[Julian Berman]

Oh is it? Like they're not related to the ones in structures?

[Mario Carneiro]

you are thinking of (x : A . tac) syntax