rewrite propositions with types

Stream: general

[Siyuan Yan]

I'm new to lean, and this is an example from the tutorials:

def even_fun (f : ℝ → ℝ) := ∀ x, f (-x) = f x

def odd_fun (f : ℝ → ℝ) := ∀ x, f (-x) = -f x

example (f g : ℝ → ℝ) : even_fun f → even_fun g →  even_fun (f + g) :=
begin
  sorry,
end

instead of defs and ... → ... → ..., how do I make a type for even function? This is want I want to write:

example (f g : EvenFunction ℝ ℝ) : ??? :=
begin
  sorry,
end

Moreover, what should I write at the ??? part to claim that f + g still has type EvenFunction ℝ ℝ?

[Julian Berman]

Did you already write EvenFunction? How did you define it? Or is that part of the question as well?

[Siyuan Yan]

That's part of the question :smile:

[Julian Berman]

I am not at a level too much beyond where you are, but part of what you're asking might have to do with glossary#bundled-vs-unbundled.

You can define a simple type which is a function along with a proof that it's even via e.g.:

import data.real.basic

def even_fun (f : ℝ → ℝ) := ∀ x, f (-x) = f x

def odd_fun (f : ℝ → ℝ) := ∀ x, f (-x) = -f x

structure even_function :=
(to_fun : ℝ → ℝ)
(is_even_to_fun : even_fun to_fun)

def even_function.add : even_function → even_function → even_function := λ f g, ⟨f.to_fun + g.to_fun, begin
end⟩

instance : has_add  even_function := ⟨add⟩

variables (f g : even_function)
#check f + g

but now you see you may need to teach lean even how to add those (which involves filling in the proof you were talking about).

[Kevin Buzzard]

In type theory, if you make a new type EvenFunction ℝ ℝ then there are two issues: firstly if f has type EvenFunction ℝ ℝ then it will not have type ℝ → ℝ, in other words it definitely will not be a function from ℝ to ℝ. You will be able to tell Lean to interpret it as a function from the reals to the reals, but it will add a little up-arrow in front of it -- this will be an "invisible function" from the type EvenFunction ℝ ℝ to the type ℝ → ℝ, just like in Lean there are invisible functions from the naturals to the integers to the rationals to the reals to the complexes, from the rationals to the 37-adic numbers etc etc. And second it will not be a theorem that f + g still has type EvenFunction ℝ ℝ -- the assertion that a term has a given type is just some inbuilt thing in type theory, it's not something you can prove. So if you do it this way then the assertion will still have the same content but it will be wrapped up differently -- it will be a definition of an addition on the type EvenFunction ℝ ℝ, and then a theorem that f+g, when interpreted via the "invisible function", or coercion, and evaluated at a real x, will equal the coercion of f evaluated at x, add the coercion of g evaluated at x. So it's all the same information but packaged up in a totally different way.

To make the coercion in Lean 3 you need to know about has_coe_to_fun and to make the addition you need to know about the has_add typeclass.

[Siyuan Yan]

@Julian Berman @Kevin Buzzard thanks! those are two different approaches. I was more thinking in line with Kevin. Interesting to know structure exists too!

[Siyuan Yan]

actually maybe not too different? structure seems to be a "frontend" for defining inductive types?

[Kevin Buzzard]

You can read about structures in chapter 9 of #tpil