formation

Stream: new members

[Alex Zhang]

Is there a way to state an example or theorem asserting that a certain object has a certain type?
For example, I first import data.real.basic, then is there a way to write an example or theorem in Lean asserting that 5 has type \R?

[Eric Wieser]

example : ℝ := 5

[Eric Wieser]

But this doesn't mean "5 has type ℝ", it means "lean can parse the syntax 5 into a term of type \R"

[Johan Commelin]

@Alex Zhang The kernel can check that certain expressions have a certain type. But you cannot prove this.

[Eric Wieser]

If you really want a "proof", you could do something like

def typeof {T : Sort*} (t : T) : Sort* := T

example : typeof 5 = ℕ := rfl

[Eric Wieser]

But note that if lean doesn't have a hint about how to interpret 5, it chooses nat not real!

[Alex Zhang]

I don't quite know how to introduce a new function in the proof of a theorem.
For example, in the following code, how can I define f to the following function:
f x = g x if x<=10
f x = 1 if 11 <= x <= 20
f x = 0 o/w

example (g : ℕ → ℕ):true :=
begin
  let f : ℕ → ℝ :=

end

[Alex Zhang]

I can do this by using a new {} block with by_cases, but this way seems clumsy...

[Ruben Van de Velde]

  let f : ℕ → ℝ := λ n, if n ≤ 10 then g n else if n ≤ 20 then 1 else 0,