Induction on List

Stream: new members

[Peter Davidson]

Can anyone help me fill in the following sorry?

import Mathlib

namespace Rel

variable {α : Type*}

instance binary_rel_monoid : Monoid (Rel α α) where
  one := Eq
  mul := comp
  one_mul := comp_left_id
  mul_one := comp_right_id
  mul_assoc := comp_assoc

example (L : List (Rel α α)) : (L.prod).inv = (L.reverse.map inv).prod := by
  induction L with
  | nil =>
    exact inv_id
  | cons hd tl ih =>
    rw [List.prod_cons]
    sorry

I want to rewrite (hd * tl.prod).inv using Rel.inv_comp, but lean can't find the correct pattern to do this.

[Ruben Van de Velde]

import Mathlib

namespace Rel

variable {α : Type*}

instance binary_rel_monoid : Monoid (Rel α α) where
  one := Eq
  mul := comp
  one_mul := comp_left_id
  mul_one := comp_right_id
  mul_assoc := comp_assoc

theorem mul_def (a b : Rel α α) : a * b = a.comp b := rfl

example (L : List (Rel α α)) : (L.prod).inv = (L.reverse.map inv).prod := by
  induction L with
  | nil =>
    exact inv_id
  | cons hd tl ih =>
    rw [List.prod_cons]
    rw [mul_def, Rel.inv_comp]
    simp [mul_def, ih]

[Peter Davidson]

Thanks. It didn't occur to me to define the multiplication in this way. I guess I was assuming that it was somehow taken care of by the instance.

[Yakov Pechersky]

It's not defining it, it's exposing the spec of the definition you provided in the instance, as a lemma. That helps you rewrite and expose what the definition of multiplication is.

[Peter Davidson]

That makes sense. Is this a standard thing to do after creating such an instance? Or are there ways to work around it?

[Aaron Liu]

I think this is a standard thing to do after almost any definition, you can see that loogle "_def" has over 2000 results.

[Kenny Lau]

Peter Davidson said:

That makes sense. Is this a standard thing to do after creating such an instance? Or are there ways to work around it?

it is called the "API" in mathlib's philosophy; i.e. a set of lemmas so that you can actually use the definition.

[Kenny Lau]

if you're programming a calculator, and you implemented a square root function, then your job is done; but if you're programming in Lean, after you construct the square root function, you still need to prove the property sqrt (x * x) = x to be able to prove anything about it

[Peter Davidson]

Kenny Lau said:

if you're programming a calculator, and you implemented a square root function, then your job is done; but if you're programming in Lean, after you construct the square root function, you still need to prove the property sqrt (x * x) = x to be able to prove anything about it

That's a very helpful analogy. Thanks!

[Kenny Lau]

@Peter Davidson as another example, everyone knows that $\pi = 4\left( \dfrac11 - \dfrac13 + \dfrac15 - \dfrac17 + \cdots \right)$, but if you actually define it this way, and define $\sin x = x - \dfrac{x^3}{3!} + \dfrac{x^5}{5!} - \dfrac{x^7}{7!} + \cdots$, then you'll have a very hard time proving that $\sin \pi = 0$ :upside_down:

[Kenny Lau]

(note that instead mathlib has chosen for the definition of docs#Real.pi to be 2x where x in [1,2] such that cos(x) = 0)