## Stream: new members

### Topic: Ignat

#### Ignat Insarov (Oct 03 2021 at 18:37):

Hello!

I like programming so naturally I want to program my Mathematics. Hopefully Lean can help me with that!

#### Ignat Insarov (Oct 03 2021 at 20:18):

Yo, so I have these overlapping instances:

class Same (φ: Type) := (same: φ → φ → ℙ)
def same {φ: Type} [Same φ]: φ → φ → ℙ := Same.same
notation x ≡ y := same x y
instance Same_thing (α: Type): Same α := Same.mk (λ x y, x = y)
instance Same_arrow (α β: Type) [Same β]: Same (α → β) := Same.mk (λ f₁ f₂, ∀ x, f₁ x ≡ f₂ x)
instance Same_proposition: Same ℙ := Same.mk (λ p q, p ↔ q)


What I want to say is that being same for functions means extensional equality, for propositions it is two way implication and for everything else equality. But I do not think it works — same seems to unfold into equality by default.

How can I make sure that more specific instances are preferred?

#### Eric Rodriguez (Oct 03 2021 at 20:27):

So as far as I understand, there is ways to do this (changing instance priority); however, I don't see why you'd want to do this at all! docs#funext and docs#propext may be interesting

#### Ignat Insarov (Oct 03 2021 at 20:31):

Yep, I reckon that I can add some axioms. I am really doing this for fun.

#### Eric Wieser (Oct 03 2021 at 20:51):

Instance priorities aren't that useful a tool from what I've seen - if you have multiple non-equal instance available, you can still end up with the "wrong" one. Most often we use priorities in mathlib simply for performance.

#### Yury G. Kudryashov (Oct 03 2021 at 20:55):

Generally we use instances for "canonical" structures.

#### Floris van Doorn (Oct 03 2021 at 21:02):

You have to be careful when going down this path, as other said. You can do it with priorities though: we're doing it in mathlib for docs#decidable, where docs#classical.prop_decidable is our catch-all.
The main thing you have to be careful about is that your statements are general enough. If you prove some theorem T about a type α with the Same_thing instance, you run into problems if you later apply T to ℙ, since for that type it generally will find the Same_proposition instance. The solution was to prove the statement T for an arbitrary instance, not just the Same_thing instance.

#### Ignat Insarov (Oct 03 2021 at 21:09):

So, another hardship is that Lean cannot infer an instance when I add some notations. See:

def ℙ := Prop
def Binary_Relation (α β: Type) := α → β → ℙ
notation α ~ β := Binary_Relation α β
def identity {α}: α ~ α := λ x y, x = y
def compose {α β γ}
: (α ~ β) → (β ~ γ) → (α ~ γ)
:= λ r₁ r₂, λ x z, ∃ y, (r₁ x y ∧ r₂ y z)
notation r₂ ∘ r₁ := compose r₁ r₂

theorem has_identity (α β): ∀ (r: α ~ β), ∀ x y, (r ∘ identity) x y ↔ r x y :=
begin
intros, unfold identity, unfold compose, split,
intro H, cases H with x' proof, cases proof, subst proof_left, apply proof_right,
intro H, existsi x, split,
reflexivity,
assumption,
end

class Same (φ: Type) := (same: φ → φ → ℙ)
def same {φ: Type} [Same φ]: φ → φ → ℙ := Same.same
notation x ≡ y := same x y
-- @[priority std.priority.default+1]
-- instance Same_thing (α: Type): Same α := Same.mk (λ x y, x = y)
instance Same_arrow (α β: Type) [Same β]: Same (α → β) := Same.mk (λ f₁ f₂, ∀ x, f₁ x ≡ f₂ x)
instance Same_proposition: Same ℙ := Same.mk (λ p q, p ↔ q)
#check (by apply_instance: Same (nat → bool → ℙ))
#check (by unfold Binary_Relation; apply_instance: Same (nat ~ bool))
theorem has_identity_fancy (α β): ∀ (r: α ~ β), (r ∘ identity) ≡ r :=
begin
sorry
end


The invocation of ≡ in the statement of the theorem has_identity_fancy is not working.

#### Ignat Insarov (Oct 03 2021 at 21:37):

No, it is not a dead end. I should add the type thing as a parameter to the theorem:

theorem has_identity_fancy (α β) [Same (α ~ β)]: ∀ (r: α ~ β), (r ∘ identity) ≡ r :=


— Then I can proceed to the proof.

#### Eric Rodriguez (Oct 03 2021 at 21:38):

In Lean, it's also typical to be universe polymorphic, so you should use Type* pretty much everywhere you use Type

#### Eric Rodriguez (Oct 03 2021 at 21:38):

It should (?) then infer the instance regardless

#### Ignat Insarov (Oct 03 2021 at 21:41):

I do not think it does. I added stars everywhere but nothing happened.

#### Ignat Insarov (Oct 03 2021 at 21:44):

I am not sure I understand this. So, with [Same (α ~ β)] I tell Lean that the theorem accepts an instance as an argument. Any instance. But what I really want is for it to pick the specific definition of sameness, specifically λ x y, r₁ x y ↔ r₂ x y — I could not possibly prove anything until I have this specific formula in the goal.

#### Ignat Insarov (Oct 03 2021 at 21:51):

Is there some reference that explains how type class inference works from first principles?

#### Bryan Gin-ge Chen (Oct 03 2021 at 22:01):

I don't know if it qualifies as first principles, but the usual reference is chapter 10 of TPiL.

#### Ignat Insarov (Oct 04 2021 at 06:04):

I do not think it explains this situation.

#### Ignat Insarov (Oct 04 2021 at 06:12):

It says like:

Sometimes Lean can’t find an instance because the class is buried under a definition. … Alternatively, we can help Lean out by unfolding the definition.

So, in this case I should unfold the definition of ~, but how do I unfold anything in the statement of a theorem?

#### Scott Morrison (Oct 04 2021 at 06:36):

When you make a new definition of the form def X := Y, typeclasses which were available for Y are not available for X. You can "copy them across" using a @[derive] handler, e.g. @[derive T] def X := Y. If previously you had T Y available, this will make T X available.

#### Ignat Insarov (Oct 04 2021 at 06:41):

It says "failed to find a derive handler for"…

#### Scott Morrison (Oct 04 2021 at 06:46):

This will not work if T Y was not already available. Try posting a #mwe.

#### Ignat Insarov (Oct 04 2021 at 06:51):

Voilà:

def ℙ := Prop
class Same (φ: Type) := (same: φ → φ → ℙ)
def same {φ: Type} [Same φ]: φ → φ → ℙ := Same.same
notation x ≡ y := same x y
instance Same_arrow (α β: Type) [Same β]: Same (α → β) := Same.mk (λ f₁ f₂, ∀ x, f₁ x ≡ f₂ x)
instance Same_proposition: Same ℙ := Same.mk (λ p q, p ↔ q)

#check Same (nat → bool → ℙ)
@[derive Same] def Binary_Relation (α β: Type): Type := α → β → ℙ


#### Ignat Insarov (Oct 04 2021 at 06:53):

I am not sure if I am misinterpreting, but check seems to confirm that the instance exists.

#### Scott Morrison (Oct 04 2021 at 06:58):

I get unexpected token on your ≡. You need to replace the notation line with notation x ≡ y := same x y.

#### Scott Morrison (Oct 04 2021 at 06:59):

After that

instance (α β : Type) : Same (Binary_Relation α β) := by { dsimp [Binary_Relation], apply_instance }


will do what you want.

#### Scott Morrison (Oct 04 2021 at 06:59):

(After removing the @[derive Same].)

#### Ignat Insarov (Oct 04 2021 at 07:02):

Scott Morrison said:

I get unexpected token on your ≡. You need to replace the notation line with notation x ≡ y := same x y.

Works alright for me though, without any back ticks. Maybe this depends on the version of Lean. Lean (version 3.4.2, commit cbd2b6686ddb, Release)

#### Ignat Insarov (Oct 04 2021 at 07:02):

So the derive magic is not working. How can I get a similar magic but such that it can do the dsimp thing for me?

#### Ignat Insarov (Oct 04 2021 at 07:03):

I am also looking at this paper and it says that definitions may be marked as reducible. (Section 2.3.) Maybe I should mark my definition as reducible?

#### Patrick Massot (Oct 04 2021 at 07:04):

You are using an ancient version of Lean

#### Patrick Massot (Oct 04 2021 at 07:05):

Did you follow the instructions on https://leanprover-community.github.io/get_started.html#regular-install and https://leanprover-community.github.io/install/project.html ?

#### Ignat Insarov (Oct 04 2021 at 07:08):

No, I asked my package manager to get Lean 3 for me.

Last updated: Dec 20 2023 at 11:08 UTC