Given `A = B`, how to prove `a: A` also has type B in Lean 4

Question

I guess my question can be reduced to implementing this function:

def abEq (A B : Type) (a: A) (ab : A = B): B := sorry

I am new to Lean 4 and started learning from the official tutorial, currently I am at the chapter 7 (Inductive types).

I already know that substituting things in propositions given a certain equality is done using Eq.subst, and Eq.subst ab a is among the things I tried. My problem is that the type assertion a: A is not a proposition, and I have no idea how to proceed.

---

Why I am trying to do this

Perhaps I am suffering from an XY problem, so I thought including the following might help. In Lean, I am trying to define what I would define in set theory like this:

A signature is a pair $(Op, ar)$, where

• $Op$ is an arbitrary set of operations, and
• $ar\colon Op \to Nat$ a function giving their arities.

Let $Sig_{Op}$ be the set of all signatures with $Op$ as the set of operations, then \begin{align} arity\colon Sig_{Op} &\to Op \to Nat \\ (Op, ar) &\mapsto op \mapsto ar(op) \end{align} returns the arity of the operator $op$ in the signature $(Op, ar)$.

I came up with this:

def signature := (Op: Type) × (Op → Nat)

def sigOp (Op: Type) := { s: signature // s.fst = Op }

def arity {Op: Type} (op: Op) (s: sigOp Op): Nat := ...

but I am stuck implementing the function arity. s.val.snd op does not work, because s.val.snd expects an argument of type s.val.fst, while op has type Op. The value s carries a proof s.property: s.val.first = Op, but I don't know how to apply it. Is my problem in that I just don't know how to implement arity, or are my Lean definitions themselves wrong and I need to change them? If so, how?

Answer 1

[Note: Anyone reading this should also check Jason Rute's answer which shows how to do these things in Lean idiomatically.]

Indeed, you are experiencing the XY problem. You are not taking the advantage of dependent types, which you can do as shown below.

Regarding your problem X: one just has to perform a transport across equality, but in a universe:

def abEq (A B : Type) (a : A) (ab : A = B): B :=
  @eq.rec Type A (λ (X : Type), X) a B ab 

Namely, suppose we have:

• a type U
• element u : U
• a type family P : U → Type
• an element x : P u
• an element v : U
• equality e : u = v

Then eq.rec U u P x v e will produce an element of P v. We say that we transported x : P u to P v along e. If we set U := Type, u := A, P := λ X, X, x := a, v := B and e := ab then we get your example.

Now let's get onto problem Y.

I am including a fairly elaborate example of how to go about formalizing universal algebra because the classical treatment of universal algebra is not the right way to formalize the topic, but I see people falling into the trap repeatedly. In particular, one should not use natural numbers as arities – that creates a host of unecessary complications.

-- A signature has a type of operation symbols, and each symbol
-- has an arity. Improtantly, the arity is a type, not a number!
-- That is, if we want a symbol to have arity 3 we do not use
-- the number 3 but instead (any) type with 3 elements.
structure signature :=
  (symbol : Type) -- the type of operation symbols
  (arity : symbol → Type) -- the arities of symbols

namespace arity
  -- we define arities for constants, unary and binary symbols,
  -- as these are most common.

  inductive const : Type

  inductive unary : Type
    | u1 : unary -- the index of the only argument

  open unary

  inductive binary : Type
    | b1 : binary -- the index of the first argument
    | b2 : binary -- the index of the second argument

  open binary
end arity

-- the type of algebras for a given signature,
-- note that each symbol op is interpreted as a map which
-- takes a function (args : S.arity op → carrier) and returns
-- an element of the carrier. If the type S.arity op has
-- n elements, then args is (equivalent to) an n-tuple,
-- as it should be.
structure algebra (S : signature) :=
  (carrier : Type) -- the underlying carrier
  (act : Π (op : S.symbol), (S.arity op → carrier) → carrier)

-- Example: the free algebra generated by a signature S and a set X of generators

-- the carrier of the free algebra is the type of trees whose leaves are
-- the generators and the nodes are operation symbols
inductive tree (Leaf : Type) (Node : Type) (arity : Node → Type) : Type
| leaf : Leaf → tree -- the injection of generators into the tree algebra
| node : Π (t : Node), (arity t → tree) → tree

-- the free algebra on S generated by X
def free (S : signature) (X : Type) : algebra S :=
  { carrier := tree X S.symbol S.arity,
    act := tree.node }

-- the type of homomorphisms between two S-algebras
structure hom {S : signature} (X : algebra S) (Y : algebra S) :=
  (map : X.carrier → Y.carrier)
  (is_hom : Π (op : S.symbol) (args : S.arity op → X.carrier),
              map (X.act op args) = Y.act op (map ∘ args) )

-- composition of homomorphisms is a homomorphism
def hom_compose {S : signature} {X Y Z : algebra S}
                (g : hom Y Z) (f : hom X Y) : hom X Z :=
  { map := g.map ∘ f.map,
    is_hom := begin intros op args, simp [g.is_hom, f.is_hom] end
  }

-- example: the signature of a group

-- the type of symbols of a group
inductive group_symbol : Type
  | uni : group_symbol -- unit
  | inv : group_symbol -- inverse
  | mul : group_symbol -- multiplication

open group_symbol

def group : signature :=
  { symbol := group_symbol,
    arity := λ op, match op with
                   | uni := arity.const
                   | inv := arity.unary
                   | mul := arity.binary
                  end }

-- the group Z/3Z

-- the carrier of Z/3Z
inductive Z3_carrier : Type
  | z0 : Z3_carrier
  | z1 : Z3_carrier
  | z2 : Z3_carrier

open Z3_carrier

-- the inverse operation in Z/3Z
def Z3_inv : Z3_carrier → Z3_carrier
  | z0 := z0
  | z1 := z2
  | z2 := z1

-- addition in Z/3Z
def Z3_add : Z3_carrier → Z3_carrier → Z3_carrier
  | z0 z0 := z0
  | z0 z1 := z1
  | z0 z2 := z2
  | z1 z0 := z1
  | z1 z1 := z2
  | z1 z3 := z0
  | z2 z0 := z2
  | z2 z1 := z0
  | z2 z2 := z1

-- the group Z/3Z
def Z3 : algebra group :=
  { carrier := Z3_carrier,
    act := λ op,
             match op with
             | uni := λ args, z0
             | inv := λ args, Z3_inv (args arity.unary.u1)
             | mul := λ args, Z3_add (args arity.binary.b1) (args arity.binary.b2)
             end
  }

Answer 2

X

To amend Andrej's answer of your X problem, I would generally avoid Eq.rec (or any other Foo.rec recursors) as it is very low level and a bit tricky to use. (Although is is a great way to learn the underlying logic.)

In this case, this is already in Lean 4 as cast (with the order of the arguments in reverse of yours).

def abEq (A B : Type) (a : A) (ab : A = B): B :=
  cast ab a

Or even better, you can use the ▸ macro, which you can write using \t in VS Code.

def abEq (A B : Type) (a : A) (ab : A = B): B :=
  ab ▸ a

The macro is nice because it is flexible. Equality can be used in either direction. It can also be used for transitivity of equality and chaining equational reasoning:

theorem trans (A B C : Type) (ab : A = B) (bc : B = C) : A = C :=
  bc ▸ ab
theorem euclidean (A B C : Type) (ab : A = B) (ac : A = C) : B = C :=
  ab ▸ ac
def abcbEq (A B C : Type)  (a : A) (ab : A = B) (cb : C = B) : C :=
  cb ▸ ab ▸ a

Y

I don't claim to have a strong opinion like Andrej does about if Nat can be used as an arity. (I do however agree with him that a structure is better than using × if nothing more than readability.) To solve your stated Y problem (but with a structure), you can do it as follows.

structure Signature where
  (Op : Type)
  (arity: Op -> Nat)

def sigOp (Op: Type) := { s: Signature // s.Op = Op }

def arity {Op: Type} (op: Op) (s: sigOp Op): Nat :=
  let sign : Signature := s.val
  have h : sign.Op = Op := s.property
  sign.arity (h ▸ op)

Answer 3

My problem is that the type assertion a: A is not a proposition

This is indeed your problem, and it's not one that can be overcome. a : A is NOT a type in Lean or any other intensional, intrinsically typed theory, it's a judgment at the meta-level. So having a : A and A = B is not enough to express a : B, because the statement a : B is simply false.

This is because of the difference between propositional and definitional equality. The proof A = B is propositional equality: it's a type within Lean itself, and is based on what you can prove. However, a : A is based on definitional equality i.e syntactic equality up to normalization. So if a : A, then you have a : A' for any A' that is definitionally equal to A. But in general the two are not interchangable.

There are type theories where propositional and definitional equality are the same, these are called "extensional", and have a rule called "equality reflection that lets you exchange any two propositionally equal types in a judgment. But this makes type checking undecidable, as well as making it unsafe to normalize terms under binders. Nuprl is the most famous proof assistant based on this notion, but I'm sure there are others.

As for the XY problem, I suspect subst is in fact what you want, or possibly the more general J rule (I'm not sure what lean calls it), which basically lets you pattern match on the equality and turn a P x x refl into a P x y pf whenever pf : x = y.