Using option to define operators

Stream: maths

[Max Bobbin]

If I were to define an operator like division whose output is option how can I unify the operator with the has_div class? For instance, as a mwe, if I wanted to define division for the rational numbers as

def rat.div2 : ℚ → ℚ → option ℚ
| a b := ite (b ≠ 0) (option.some (a * b⁻¹)) option.none

I felt like option.get was in the right direction, but I couldn't get it to work.

instance rat.has_div2 : has_div ℚ := option.get rat.div2

I've been playing around with this idea when defining addition for my dimensional analysis project so I didn't have to use a junk value.

[Patrick Johnson]

To avoid using an option or a junk value:

def rat.div2 : ℚ → ℚ → ℚ :=
classical.epsilon $ λ f, ∀ a b, b ≠ 0 → f a b = a * b⁻¹

[Patrick Johnson]

If you want to keep the option and use your original definition, then you can't avoid having a junk value. In that case, docs#option.get_or_else is the function you want.

[Max Bobbin]

interesting. I'm not interested in keeping the option, I wasn't aware of this way. Thanks!

[Eric Wieser]

docs#classical.epsilon is a junk value too

[Patrick Johnson]

Technically yes, but more subtle. It's actually a junk function of a in this case (when b=0, you get a potentially different result for each a). It's better than an explicit junk value because you can't accidentally prove an intuitively wrong theorem.

[Eric Wieser]

Ah I missed that the epsilon was happening on the space of functions

[Eric Wieser]

I'm not sure whether I fully agree with your second sentence; certainly many intuitively wrong theorems are out of reach, but are you sure all of them are?

[Patrick Johnson]

I mean you can't prove div2 1 0 = 0 for instance.

[Max Bobbin]

Been trying to use the classical.epsilon, but I don't think I understand fully how to use the classical.choice to close the goal. I was able to close the goal of the if statement, but the else statement which uses classical.choice is tripping me up. I wanted to know if anyone had any advice on working with classical.choice? I attached the code I'm working on below just so you can see what I did.

--supporting stuff
import data.rat.basic
def dimension (α : Type u) := α → ℚ

namespace dimension
def dimensionless (α) : dimension α := λ i, 0
instance {α} : has_one (dimension α) := ⟨dimension.dimensionless α⟩
instance {α} : nonempty (dimension α) := has_one.nonempty
protected noncomputable def add {α} [decidable_eq (dimension α)]: dimension α → dimension α → dimension α := classical.epsilon $ λ f, ∀ a b, a = b → f a b = a

--code I'm working on
example {α} (a : dimension α) [decidable_eq (dimension α)]: a.add a = a :=
begin
  simp [dimension.add, classical.epsilon, classical.strong_indefinite_description],
  split_ifs,
  simp,
  rcases (classical.indefinite_description _ h) with ⟨H,H2⟩,
  rw ← H2 a a,
  finish,
  refl,
  simp,
  push_neg at h,
  specialize h dimension.add,
  cases h with a h,
  cases h with b h,
  cases h with h1 h,
end

[Patrick Johnson]

When proving things that involve classical epsilon, you need to prove that at least one object exists that satisfies the epsilon condition. In this case, you need to prove that there exists function f such that f a b = a

example {α} (a : dimension α) [decidable_eq (dimension α)] : a.add a = a :=
begin
  generalize hb : a = b, symmetry' at hb,
  nth_rewrite 1 hb, revert b a hb, unfold dimension.add,
  apply classical.epsilon_spec (⟨λ a _, a, λ _ _ _, rfl⟩ :
    ∃ (f : dimension α → dimension α → dimension α), ∀ a b, a = b → f a b = a),
end

[Max Bobbin]

Ahhh, I see. I wasn't aware of a couple the ability to use a couple of the tactics like that. Thank you