defining "type membership relation"

Stream: lean4

[Bulhwi Cha]

import Std.Tactic.RCases
import Mathlib.Init.Set

inductive Mem {α : Type u} : α → Type u → Prop where
  | intro (elem : α) {type : Type u} (eq : α = type) : Mem elem type

infix:50 " ∈ " => Mem

def isElem (elem : α) := Mem.intro elem rfl

example : 1 ∈ Nat             := isElem 1
example : true ∈ Bool         := isElem true
example : "Min Suha" ∈ String := isElem "Min Suha"
example : Nat ∈ Type          := isElem Nat

example : let subtype := {s : String // s.length > 5}
          (⟨"Na Sera", by simp⟩ : subtype) ∈ subtype := by apply isElem

-- type membership
example : ["Ha Yun", "Ryu Hari"] ∈ List String := isElem ["Ha Yun", "Ryu Hari"]

-- set membership
example : ["Ha Yun", "Ryu Hari"] ∈ {xs : List String | xs.length = 2 } :=
  show ["Ha Yun", "Ryu Hari"].length = 2
  from rfl

namespace Mem

-- every element is in exactly one type
theorem type_unique {α β : Type u} {x : α} (_h : x ∈ α) (h : x ∈ β) : α = β :=
  match h with
  | intro .(x) eq => eq

-- you can't prove this
example : ¬ "So Nagi" ∈ Nat := by
  intro h
  have is_string : "So Nagi" ∈ String := isElem "So Nagi"
  have String_eq_Nat : String = Nat   := type_unique is_string h
  sorry

-- corollary of `Mem.type_unique`
theorem mem_iff (a : α) (α' : Type _) : a ∈ α' ↔ α = α' := by
  constructor
  · rintro ⟨eq⟩
    rcases eq
    rfl
  · rintro ⟨⟩
    apply isElem

end Mem

[Bulhwi Cha]

I know there's no such thing as "type membership relation" in standard materials on type theory, but I tried defining it for fun and experimentation.

[Mario Carneiro]

You will not be able to prove the last sorry because Nat and String cannot be proven distinct

[Bulhwi Cha]

Right. That's my complaint about Lean's type theory.

[Mario Carneiro]

The usual way to fix this in concrete applications is to use an inductive indexing set and a map to types, and then use equality of indexes instead of equality of types

[Trebor Huang]

Actually, for every definable property in Lean, Nat and String never disagree. So I don't see any reason why they should be unequal. Do we want to prove two types are unequal for the sake of being unequal?

[Kevin Buzzard]

yes, I can count strings, so why not implement them like that :-)

[Bulhwi Cha]

Trebor Huang said:

Actually, for every definable property in Lean, Nat and String never disagree. So I don't see any reason why they should be unequal. Do we want to prove two types are unequal for the sake of being unequal?

I'd say they're just isomorphic.

[Kevin Buzzard]

The problem is that internally they could actually be equal. Because you can't rule that out, you can't prove they're not equal.

[Kyle Miller]

The type_unique theorem can be strengthened in a way.

lemma Mem_iff (a : α) (α' : Type _) : a ∈ α' ↔ α = α' := by
  constructor
  · rintro ⟨x, ⟨⟩⟩
    rfl
  · rintro ⟨⟩
    apply isElem

Here's another characterization of it:

def typeof (_a : α) := α

lemma Mem_iff' (a : α) (α' : Type _) : a ∈ α' ↔ typeof a = α' := by
  rw [typeof, ← Mem_iff]