Equality of structures with types in fields

Stream: general

[Peter Nelson]

I'm having problems proving equality of somewhat simple structures without heq rearing its ugly head. To encapsulate some of them in a concrete question, how do I prove the following?

 structure test :=
  (t : Type)
  (f : t → ℤ)

def shift (T : test) : test := {
  t := T.t,
  f := λ x, T.f x + 1,
}

lemma shift_inj (T₁ T₂ : test) :
  shift T₁ = shift T₂ → T₁ = T₂ :=
  begin
    sorry,
  end

[Adam Topaz]

The standard answer is to try to avoid type equality.

A better option is to define morphisms for your structure, and construct isomorphisms instead of equalities.

[Adam Topaz]

In this particular case, you can probably use subst to prove your lemma

[Kenny Lau]

[not recommended]

import tactic data.int.basic

structure test :=
(t : Type)
(f : t → ℤ)

def shift (T : test) : test :=
{ t := T.t,
  f := λ x, T.f x + 1 }

lemma shift_inj (T₁ T₂ : test) (h : shift T₁ = shift T₂) : T₁ = T₂ :=
begin
  cases T₁, cases T₂,
  have : T₁_t = T₂_t := congr_arg test.t h, subst this,
  congr' 1,
  ext,
  refine add_right_cancel (_ : _ + 1 = _ + 1),
  change (shift ⟨T₁_t, T₁_f⟩).f x = (shift ⟨T₁_t, T₂_f⟩).f x,
  exact congr_fun (eq_of_heq $ congr_arg_heq test.f h) x,
end

[Peter Nelson]

Thanks! I take it from your answers that there is no idiomatic way to do such a thing.

I've certainly tried to avoid type equality - where I am is the result of a lot of agonising. This is part of a setting where 'equal' and 'isomorphic' are different, and being unable to rw with equal objects will be a serious problem for even the simplest things. My hope is that this ugliness will be confined to the proofs in an API.

[Kenny Lau]

what is the context?

[Adam Topaz]

If you don't bundle the type t then it's perfectly nice and easy to speak about equality of the associated f

[Peter Nelson]

The context is matroids. A matroid is a finite set E bundled with some extra structure, and a matroid M has minors, which are structures on subsets of E.

Two minors are equal if they are propeq structures on propeq subsets of E.

Two minors on different subsets F,F' of E might be isomorphic, while not being equal, if there is a structure-preserving bijection between F and F'.

Both isomorphism and equality are important concepts, but they aren't the same.

[Reid Barton]

And the bundled type is the subtype of the subset of E?

[Reid Barton]

If so this isn't going to work because you can't prove that different subsets of E yield unequal types

[Kenny Lau]

Reid Barton said:

If so this isn't going to work because you can't prove that different subsets of E yield unequal types

I'm not very sure about that

[Kenny Lau]

edit: never mind

[Peter Nelson]

We're implementing this differently, using a bespoke boolean algebra type that suits the structure. I don't know if the same issue holds there - I will need to discuss this with my coauthors.

In any case, I don't think one can argue that what I want is mathematically unnatural. If there is a better way to implement it I'd be happy to know it.

[Reid Barton]

It's unnatural to record a subset of E as a type

[Reid Barton]

because that "forgets the embedding into E"

[Reid Barton]

you can record it as a set E, or as a type with an injection to E (in which case isomorphism of the type+injection is what you call "equality")

[Peter Nelson]

We are using a type with injection.

If we use isomorphism to encode mathematical equality, then I anticipate very simple things (if a complicated theorem statement applies to one minor N, it applies to a minor N' with N = N') being unwieldy.

Also, how does one implement isomorphism in the mathematical sense, if isomorphism in lean is a stronger notion that corresponds to mathematical equality ?

(I'm certainly not arguing that my implementation is natural, by the way - just that what I want out of 'equal' is).

[Reid Barton]

I think you found that things became even more unwieldy when you tried to use equality of types :upside_down:

[Reid Barton]

There's isomorphism over E as well as isomorphism over an isomorphism of E.

[Peter Nelson]

Hard to argue with that. Again, I'm (perhaps naively) hoping to hide this in an API and leave a reasonable user-facing interface.

[Adam Topaz]

IMO the natural thing to do is to mimic the way, e.g., groups and bundled subgroups are defined in mathlib. This should certainly work for the mathematical definition of matroids that I know...

[Adam Topaz]

Oh sorry, I see it's more complicated since there is some localization going on when defining a "minor" of a matroid. But it can still be done using some inductive type, I guess.

[Reid Barton]

Assuming that what you want to express is indeed mathematically reasonable, then it isn't equality of types.

[Reid Barton]

"Two subsets of $E$ are equal if they have the same elements" and "two subobjects $f : A \hookrightarrow E$, $g : B \hookrightarrow E$ are 'equal' if they have the same image / (equivalently) there is an isomorphism $i : A \to B$ which commutes with $f$ and $g$" are reasonable. "Two subobjects $f : A \hookrightarrow E$, $g : B \hookrightarrow E$ are equal if $A = B$ and $f = g$" is not.

[Reid Barton]

In particular, $A = B$ will frequently be independent of Lean.

[Reid Barton]

What we've learned from the category library is that usually the best way to deal with an equality of objects (containing types) is to turn it into an isomorphism

[Kevin Buzzard]

Just to give some idea of what lean can't do, $\mathbb{N}=\mathbb{Z}$ can neither be proved nor disproved in Lean. Equality of types is a strange thing in dependent type theory. The moment a subobject turns into a type of its own, the naive idea of equality becomes much more intractable.

[Riccardo Brasca]

But we can prove that they are not isomorphic as semirings (or ordered sets or whatever structure we care about), right?

[Reid Barton]

Isomorphism is not a problem

[Reid Barton]

The problem is if two structures are isomorphic, but not obviously equal--then whether they are actually equal will be undecidable

[Riccardo Brasca]

But it is something we usually don't care that much doing mathematics, right? Like if its true that $\pi = \exp \colon \mathbf{C} \to \mathbf{C}$ in usual set theory? I mean, both objects are sets, so the statement is meaningful (but false I think...). I apologize if what I am sating is nonsense, I have a very naive understanding of foundations.

[Kevin Buzzard]

This is type theory but it's the same sort of thing, yes. There are "weird" questions which don't make any mathematical sense but which you happen to be able to ask anyway. You could imagine that there could in theory be a way of setting up mathematics in set theory such that $\pi=\exp$ as sets. Similarly there is a way of setting up maths in type theory such that $\mathbb{N}=\mathbb{Z}$ as types, but that one would only discover this by "unfolding too much".

[Mario Carneiro]

I think $\pi\ne\exp$ because $\pi\in\{\pi\}\in(\pi,e^\pi)\in\exp$

[Mario Carneiro]

oh, unless $\pi\in\mathbb{R}$ where $\mathbb{C}=\mathbb{R}\times\mathbb{R}$, but in that case $\pi_\mathbb{R}\in\{\pi_\mathbb{R}\}\in(\pi_\mathbb{R},0)=\pi$ and the rest is as before

[Riccardo Brasca]

Except that a function $f \colon X \to Y$ is more than a subset $S \subset X \times Y$ such that blah blah I think: $f$ must "know" its codomain, and if I just give you $S = {(0,1), (1,2), \ldots}$ how can you know whether I am talking about $f \colon \mathbf{N} \to \mathbf{N}$ or $f \colon \mathbf{N} \to \mathbf{N}^+$? So probably $f$ is the inclusion $S \hookrightarrow X \times Y$.

[Riccardo Brasca]

OK, time to find something more interesting for a Sunday morning...

[Riccardo Brasca]

Nice proof BTW!

[Kevin Buzzard]

Yeah, get back to commutative algebra :-)

[Dean Young]

Can anyone help with this sorry I need to fill in? How do I split the structure and then apply equalities?

structure Person where
  name : String
  age : Nat

def alice : Person :=
{
  name := "Ali" ++ "ce",
  age := 30
}

def alice₂ : Person :=
{
  name := "Alice",
  age := 29+1
}

theorem alice_eq_alice₂ : alice = alice₂ := sorry

[Dean Young]

I am in lean 4.

[Yury G. Kudryashov]

Does rfl work?

[Yury G. Kudryashov]

More generally, you can tag your structure with @[ext].

[Yury G. Kudryashov]

This will generate a lemma p.name = q.name -> p.age = q.age -> p = q

[Dean Young]

I need the generality since this isn't a complete example. Here is my code:

def n : Int := 1


def reflexivity {X : Type} {x : X} (p : x = x) := Eq.refl p


def symmetry {X : Type} {x : X} {y : X}  (p : x = y) := Eq.symm p


def transitivity {X : Type} {x : X} {y : X} {z : X} (p : x = y) (q : y = z) := Eq.trans p q


def extensionality (f g : X → Y) (p : (x:X) → f x = g x) : f = g := funext p


def equal_arguments {X : Type} {Y : Type} {a : X} {b : X} (f : X → Y) (p : a = b) : f a = f b := congrArg f p

def equal_functions {X : Type} {Y : Type} {f₁ : X → Y} {f₂ : X → Y} (p : f₁ = f₂) (x : X) : f₁ x = f₂ x := congrFun p x


-- A category C consists of:
structure category.{u₀,v₀} where
  Obj : Type u₀
  Hom : Obj → Obj → Type v₀
  Idn : (X:Obj) → Hom X X
  Cmp : (X:Obj) → (Y:Obj) → (Z:Obj) → (_:Hom X Y) → (_:Hom Y Z) → Hom X Z
  Id₁ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X Y Y f (Idn Y) = f
  Id₂ : (X:Obj) → (Y:Obj) → (f:Hom X Y) →
    Cmp X X Y (Idn X) f = f
  Ass : (W:Obj) → (X:Obj) → (Y:Obj) → (Z:Obj) → (f:Hom W X) → (g:Hom X Y) → (h:Hom Y Z) →
    (Cmp W X Z) f (Cmp X Y Z g h) = Cmp W Y Z (Cmp W X Y f g) h


-- Notation for the identity map which infers the category:
def identity_map (C : category) (X : C.Obj) := C.Idn X
notation "𝟙_(" C ")" => identity_map C

def Idn {C : category} (X : C.Obj) := C.Idn X
notation "𝟙" X => Idn X

-- Notation for composition which infers the category and objects:
def composition (C : category) {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘_(" C ")" f => composition C f g

def Cmp {C : category} {X : C.Obj} {Y : C.Obj} {Z : C.Obj} (f : C.Hom X Y) (g : C.Hom Y Z) : C.Hom X Z := C.Cmp X Y Z f g
notation g "∘" f => Cmp f g


-- obtaining a morphism from an equality
def Map (C : category) {X : C.Obj} {Y : C.Obj} (p : X = Y) : C.Hom X Y := by
subst p
exact C.Idn X


-- definition of an isomorphism from X to Y
structure isomorphism (C : category) (X : C.Obj) (Y : C.Obj) where
  Fst : C.Hom X Y
  Snd : C.Hom Y X
  Id₁ : (C.Cmp X Y X Fst Snd) = C.Idn X
  Id₂ : (C.Cmp Y X Y Snd Fst) = C.Idn Y


-- notation for isomorphisms from X to Y (≅)
notation X "≅_(" C ")" Y => isomorphism C X Y


-- defining the inverse of an isomorphism between objects X and Y
def inverse {C : category} {X : C.Obj} {Y : C.Obj} (f : X ≅_(C) Y) : Y ≅_(C) X := {Fst := f.Snd, Snd := f.Fst, Id₁ := f.Id₂, Id₂ := f.Id₁}


-- notation for inverse : isos from X to Y to isos from Y to X
notation f "⁻¹" => inverse f


-- definition of a functor
structure functor (C : category) (D : category) where
   Obj : ∀(_ : C.Obj),D.Obj
   Hom : ∀(X : C.Obj),∀(Y : C.Obj),∀(_ : C.Hom X Y),D.Hom (Obj X) (Obj Y)
   Idn : ∀(X : C.Obj),Hom X X (C.Idn X) = D.Idn (Obj X)
   Cmp : ∀(X : C.Obj),∀(Y : C.Obj),∀(Z : C.Obj),∀(f : C.Hom X Y),∀(g : C.Hom Y Z),
   D.Cmp (Obj X) (Obj Y) (Obj Z) (Hom X Y f) (Hom Y Z g) = Hom X Z (C.Cmp X Y Z f g)


-- definition of the identity functor on objects
def CatIdnObj (C : category) :=
fun(X : C.Obj)=>
X

-- definition of the identity functor on morphisms
def CatIdnMor (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
f

-- proving the identity law for the identity functor
def CatIdnIdn (C : category) :=
fun(X : C.Obj)=>
Eq.refl (C.Idn X)

-- proving the compositionality law for the identity functor
def CatIdnCmp (C : category) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
Eq.refl (C.Cmp X Y Z f g)


-- defining the identity functor
def CatIdn (C : category) : functor C C :=
{Obj := CatIdnObj C, Hom := CatIdnMor C, Idn := CatIdnIdn C, Cmp := CatIdnCmp C}


-- defining the composition G ∘_(Cat) F on objects
def CatCmpObj (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
(G.Obj (F.Obj X))

-- defining the composition G ∘_(Cat) F on morphisms
def CatCmpHom (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(f : C.Hom X Y)=>
(G.Hom) (F.Obj X) (F.Obj Y) (F.Hom X Y f)

-- proving the identity law for the composition G ∘_(Cat) F
def CatCmpIdn (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
Eq.trans (congrArg (G.Hom (F.Obj X) (F.Obj X)) (F.Idn X) ) (G.Idn (F.Obj X))

-- proving the compositionality law for the composition G ∘_(Cat) F
def CatCmpCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) :=
fun(X : C.Obj)=>
fun(Y : C.Obj)=>
fun(Z : C.Obj)=>
fun(f : C.Hom X Y)=>
fun(g : C.Hom Y Z)=>
((Eq.trans)
(G.Cmp (F.Obj X) (F.Obj Y) (F.Obj Z) (F.Hom X Y f) (F.Hom Y Z g))
(congrArg (G.Hom  (F.Obj X) (F.Obj Z)) (F.Cmp X Y Z f g)))

-- defining the composition in the category Cat
def CatCmp (C : category) (D : category) (E : category) (F : functor C D) (G : functor D E) : functor C E :=
{Obj := CatCmpObj C D E F G, Hom := CatCmpHom C D E F G,Idn := CatCmpIdn C D E F G, Cmp := CatCmpCmp C D E F G}


-- proving Cat.Id₁
def CatId₁ (C : category) (D : category) (F : functor C D) : ((CatCmp C D D) F (CatIdn D) = F) := Eq.refl F

-- Proof of Cat.Id₂
def CatId₂ (C : category) (D : category) (F : functor C D) : ((CatCmp C C D) (CatIdn C) F = F) := Eq.refl F

-- Proof of Cat.Ass
def CatAss (B : category) (C : category) (D : category) (E : category) (F : functor B C) (G : functor C D) (H : functor D E) : (CatCmp B C E F (CatCmp C D E G H) = CatCmp B D E (CatCmp B C D F G) H) :=
Eq.refl (CatCmp B C E F (CatCmp C D E G H))


-- The category of categories
universe u
universe v
def Cat : category := {Obj := category.{u, v}, Hom := functor, Idn := CatIdn, Cmp := CatCmp, Id₁:= CatId₁, Id₂:= CatId₂, Ass := CatAss}


def SetObj := Type

def SetHom (X : SetObj) (Y : SetObj) : Type := X → Y

def SetIdn (X : SetObj) : (SetHom X X) := λ (x : X) => x


def SetCmp (X : SetObj) (Y : SetObj) (Z : SetObj) (f : SetHom X Y) (g : SetHom Y Z) : SetHom X Z := λ (x : X) => (g (f x))


def SetId₁ (X : SetObj) (Y : SetObj) (f : SetHom X Y) : (SetCmp X Y Y f (SetIdn Y)) = f := funext (λ _ => rfl)

def SetId₂ (X : SetObj) (Y : SetObj) (f : SetHom X Y) : (SetCmp X X Y (SetIdn X) f) = f := rfl

def SetAss (W : SetObj) (X : SetObj) (Y : SetObj) (Z : SetObj) (f : SetHom W X) (g : SetHom X Y) (h : SetHom Y Z) : (SetCmp W X Z f (SetCmp X Y Z g h)) = (SetCmp W Y Z (SetCmp W X Y f g) h) := funext (λ _ => rfl)


def Set : category := {Obj := SetObj, Hom := SetHom, Idn := SetIdn, Cmp := SetCmp, Id₁ := SetId₁, Id₂ := SetId₂, Ass := SetAss}


--  defining the functor Opp : Cat.{u,v} →_(Cat) Cat.{u,v} on objects (ᵒᵖ)
def OppObj (C : Cat.Obj) : Cat.Obj := {
  Obj := C.Obj,
  Hom := λ X Y => C.Hom Y X,
  Idn := λ X => C.Idn X,
  Cmp := λ X Y Z f g => C.Cmp Z Y X g f,
  Id₁ := λ X Y f => C.Id₂ Y X f,
  Id₂ := λ X Y f => C.Id₁ Y X f,
  Ass := λ W X Y Z f g h => Eq.symm (C.Ass Z Y X W h g f)
}


notation C "ᵒᵖ" => OppObj C


-- defining ᵒᵖ on functors
def OppHom (C : Cat.Obj) (D : Cat.Obj) (F : Cat.Hom C D) : (Cat.Hom (OppObj C) (OppObj D)) := {
  Obj := λ X => F.Obj X,
  Hom := λ X Y f => F.Hom Y X f,
  Idn := λ X => F.Idn X,
  Cmp := λ X Y Z f g => F.Cmp Z Y X g f
}


-- proving the identity law for the functor Opp : Cat →_(Cat) Cat
def OppIdn (C : Cat.Obj) : (OppHom C C (Cat.Idn C)) = Cat.Idn (OppObj C) := rfl

-- proving the compositionality law for the functor Opp : Cat →_(Cat) Cat
def OppCmp (C : Cat.Obj) (D : Cat.Obj) (E : Cat.Obj) (F : Cat.Hom C D) (G : Cat.Hom D E) : (Cat.Cmp (OppObj C) (OppObj D) (OppObj E) (OppHom C D F) (OppHom D E G)) = OppHom C E (Cat.Cmp C D E F G ):= Eq.refl (OppHom C E (Cat.Cmp C D E F G ))


def Opp : (Cat.Hom Cat.{u,v} Cat.{u,v}) := {
  Obj := OppObj,
  Hom := OppHom,
  Idn := OppIdn,
  Cmp := OppCmp
}


-- Opp is an involution
def OppInv : (Cat.Cmp Cat.{u,v} Cat.{u,v} Cat.{u,v} Opp Opp) = (Cat.Idn Cat.{u,v}) := (Eq.refl (Cat.Idn Cat.{u,v}))


-- defining the objects of the PrdCatObj C D
def PrdCatObjObj (C : category) (D : category) := (D.Obj) × (C.Obj)

-- defining the morphisms of PrdCatObj C D
def PrdCatObjHom (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) := (D.Hom X.1 Y.1) × (C.Hom X.2 Y.2)

-- defining the identity functor on an object in C × D
def PrdCatObjIdn (C : category) (D : category) (X : PrdCatObjObj C D) := ((D.Idn X.1),(C.Idn X.2))

-- defining the composition on morphisms in C × D
def PrdCatObjCmp (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (Z : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) (g : PrdCatObjHom C D Y Z) : PrdCatObjHom C D X Z := (D.Cmp X.1 Y.1 Z.1 f.1 g.1, C.Cmp X.2 Y.2 Z.2 f.2 g.2)


-- proving the first identity law for morphisms in C ×_Cat D
theorem PrdCatObjId₁ (C : category) (D : category) (X : PrdCatObjObj C D) (Y : PrdCatObjObj C D) (f : PrdCatObjHom C D X Y) :
  PrdCatObjCmp C D X Y Y f (PrdCatObjIdn C D Y) = f := by
match f1, f2 with
| f1 => f.1
| f2 => f.2
cases PrdCatObjCmp C D X Y Y f (PrdCatObjIdn C D Y)
rw [Eq.symm (C.Id₂ X.2 Y.2 f.2)]
--rw [Eq.symm (D.Id₂ X.1 Y.1 f.1)]
sorry

[Dean Young]

that @[ext] is perfect but I can't quite see how to use it... what does the lemma get named and where do you put the @[ext]...

[Mario Carneiro]

on the structure(s)

[Mario Carneiro]

the lemma is named MyStruct.ext

[Dean Young]

so, right before structure keyword?

[Dean Young]

wow this is perfect thanks

[Dean Young]

I get unknown attribute [ext] in lean 4.

[Mario Carneiro]

import Std

[Kyle Miller]

If you have mathlib4 loaded up, you can find a file that uses @[ext], and in VS Code right click it and do "go to definition" to see what you might need to import.

[Eric Wieser]

I need the generality since this isn't a complete example.

I'm pretty sure this no longer counts as a #mwe!