# Zulip Chat Archive

## 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.

Is this a dead end?

#### 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):

Yes, I read it like three times already.

#### 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