(Sub-)Types Are Not (Sub-)Sets

The correct abstraction is the one that lets me prove what I want, and the easier it is to prove, the more correct the abstraction is.

In my (admittedly short) time coding in Lean, the most difficult problem I've found by far is finding the correct formalization for the math I'm interested in. This post will detail one such instance of the problem, one that I seem destined to repeat -- but before I get to it, let me start by explaining why I run into it repeatedly.

Background

There's a certain aesthetic simplicity to not using more than you need, whether that's physical substances like ingredients for a recipe, or those of a mathematical nature, like the axioms used to prove a theorem. The fewer and weaker the axioms, the stronger and more impressive the result. Take, for instance, the typical calculus problem of finding the area below the curve y = x^2 where 0 \le x \le 1. Most of us would solve the definite integral

but such a quick and commonly known method is only well known because its underlying theory is so powerful as to be ubiquitous, so we are in effect crushing a nail with a sledgehammer. However, even the ancients knew how to calculate the area under this curve, several centuries before the advent of the calculus that we so easily take advantage of.

In Lean, the consequences of choosing the sledgehammer method are more keenly felt: why write hundreds (or thousands) of lines of code to develop calculus when there is a method that uses simpler tools?

All of this is my roundabout way of justifying the following: When a theory talks about subsets, the first tool I reach for is subtypes, despite Lean being powerful enough to encode ZFC.

However, one advantage of set theory is that it's easier to reason about \in than it is about : in type theory.

Lean

Consider the following statement: for predicates \phi(x), \psi(x) with one free variable over some set X,

With sets, it's fairly straightforward to show:

import Mathlib

universe u
variable (A : Type u) (X : Set A) (φ ψ : A -> Prop)

example : { x : A | φ x } = { x : A | ψ x } <-> ∀ x : A, φ x <-> ψ x := by
  apply Iff.intro
  . intro heq
    intro x
    apply Iff.intro
    . intro asm
      have : x ∈ { x | φ x } := asm
      rw [heq] at this
      exact this
    . intro asm
      have : x ∈ { x | ψ x } := asm
      rw [←heq] at this
      exact this
  . intro heqv
    apply Set.ext
    intro x
    apply heqv x

However, replacing subsets with subtypes is not so easy. One direction is disarmingly simple:

example (h : ∀ x : A, φ x <-> ψ x) : { x : A // φ x } = { x : A // ψ x } := by
  have : φ = ψ := by
    apply funext
    intro x
    apply propext
    apply h
  rw [this]
  done

It's the other that gives problems:

example (h : { x : A // φ x } = { x : A // ψ x }) : ∀ x : A, φ x <-> ψ x := by
  intro x
  apply Iff.intro
  . intro mp
    let xψ : { x : A // ψ x } := h ▸ ⟨x, mp⟩
    have : xψ.val = x := by rfl
/-
type mismatch
  HEq.rfl
has type
  HEq ?m.93344 ?m.93344 : Prop
but is expected to have type
   xψ.val = x : Prop
-/

example (h : { x : A // φ x } = { x : A // ψ x }) : ∀ x : A, φ x <-> ψ x := by
  intro x
  apply Iff.intro
  . intro mp
    let xφ : { x : A // φ x } := ⟨x, mp⟩
    rw [h] at xφ
    have : xφ.val = x := by rfl
/- same error as above -/

If either of those worked, we'd be able to extract a term with the same type as the goal and we'd be done. However, since equality between types is considered evil in lean, that means it won't be as straightfoward to prove as the previous example, if it's possible at all.