how to get output of a propositional function

Stream: new members

[Jordan Kloosterman]

I'm in my first proofs class and I was wanting to to the exercises in lean to build up my familiarity.

We learnt about propositions and predicates and on of the first questions involved the propositional function P="x = x^2" so that P(1) would turn into 1=1^2

This is as far as I got

def P(x : Int) :=
  x = x^2

example : P 0 := by --P(0)
  calc  -- error saying it has type 0 = 0^2 but was expecting type P 0
    0 = 0 := by rfl
    _ = 0 := by rfl
    _ = 0^2 := by ring

-- so I tried this one below

example : P 0 = true := by --P(0)
  calc
    P 0 = P 0 := by rfl
    _ = (0 = 0^2) := by rw[P 0] -- gives me an error inside the rw
    _ = (0 = 0) := by ring
    _ = true := by ring

I've mostly been doing exercises in the mechanics of proofs book, up to chapter 2.4 currently

Any help would be greatly appreciated.

[Ruben Van de Velde]

rw [P] without the argument works

[Ruben Van de Velde]

But then there's the issue that 0 is interpreted as a natural, and that ring doesn't quite work in this context:

import Mathlib.Tactic
def P(x : Int) :=
  x = x^2

example : P 0 = true := by --P(0)
  calc
    P 0 = P 0 := by rfl
    _ = ((0 : Int) = 0^2) := by rw[P] -- gives me an error inside the rw
    _ = ((0 : Int) = 0) := by ring_nf
    _ = true := by ring_nf

[Kevin Buzzard]

This also works and is closer to your original attempt (which is more idiomatic):

import Mathlib.Tactic
def P(x : Int) :=
  x = x^2

example : P 0 := by --P(0)
  calc  -- no error any more
    (0 : Int) = 0 := by rfl
    _ = 0 := by rfl
    _ = 0^2 := by ring

The point (as Ruben already noted) is that Lean will assume by default that 0 is a natural, not an integer. So you can just tell it that you mean the integer 0 and then Lean realises that everything else must be an integer for this to make sense.

[Kevin Buzzard]

I totally agree that the error "I was expecting a proof of 0=0^2 but you gave me a proof of 0=0^2" is not at all helpful. If it's any help, you can hover over the error message on the zeros, and see which ones are naturals and which ones are integers :-) (this does come up now and again; I wonder whether we should just make the natural zero and the integer zero different colours or something :-) )

[Jakub Nowak]

What about displaying 0 = 0^2 for nats, and (0 : Int) = 0^2 for ints? Basically, Lean should realize that 0 = 0^2 isn't parsed correctly without some type annotation somewhere. This is kinda what pp.analyze is supposed to be doing, if it wasn't broken.

[Jakub Nowak]

There was also proposal that error messages for rw etc, that say "got _ but expected _" should try to digest down where is the difference to the user. So in this instance it would point out for example that one has type @Eq.refl Nat .. and the other @Eq.refl Int .., and Nat and Int are different.

[Jakub Nowak]

Or maybe the real solution is to add section about reading error messages to Lean tutorials and teach people that context window is interactive and you should hover over stuff to check implicit arguments and types. IIrc that was something I had to learn myself.