Ignat

Stream: new members

[Ignat Insarov]

Hello!

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

[Ignat Insarov]

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]

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]

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

[Eric Wieser]

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]

Generally we use instances for "canonical" structures.

[Floris van Doorn]

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]

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]

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]

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

[Eric Rodriguez]

It should (?) then infer the instance regardless

[Ignat Insarov]

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

[Ignat Insarov]

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]

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

[Bryan Gin-ge Chen]

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

[Ignat Insarov]

Yes, I read it like three times already.

[Ignat Insarov]

I do not think it explains this situation.

[Ignat Insarov]

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]

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]

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

[Scott Morrison]

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

[Ignat Insarov]

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]

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

[Scott Morrison]

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

[Scott Morrison]

After that

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

will do what you want.

[Scott Morrison]

(After removing the @[derive Same].)

[Ignat Insarov]

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]

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]

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]

You are using an ancient version of Lean

[Patrick Massot]

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]

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