Identities to Equivalences in Graded Structures

Stream: general

[N Gelwan]

I have a dependent type Φ which takes arguments in a distributive lattice, e.g.

import Mathlib

variable
  [DistribLattice D]
  (F : D → Type)

Equality of terms in the lattice transports down Φ into equivalence of types, and a great many of the theorems that I'm trying to formalize implicitly utilize these equivalences as coercions, e.g.

variable
  (ψ : F x)
  (ϕ : F (x ⊔ y))


example : F (x ⊔ x) := ψ
example : F (y ⊔ x) := ϕ

I've been writing coercion instances ad-hoc for each of the theorems I've gotten to so far, but it's feeling pretty unwieldy. Lattice equality is decidable, right? That being said, can I leverage type-class resolution to automatically decide equality between lattice terms?

I don't know much about logic programming, or the implementation of the type-class resolution algorithm, but as far as I can tell I might only be able to use it to simplify terms with substitution, and that's not promising.

Anyone ever done anything like this? Am I missing a simpler way to do this?

[Trebor Huang]

Isn't there a similar problem with Nat-indexed stuff like graded rings? The general solution seems to be just developing enough API to move between various formalisms, for instance your D -> Type is equivalently a big universal type T with a function T -> D assigning each element its corresponding lattice point

[N Gelwan]

Good point; I'll take a look at what Mathlib has going on with its graded rings &c. tomorrow morning.

[Eric Wieser]

To that end, you may find https://www.repository.cam.ac.uk/items/1ca6b177-8773-47a6-8246-a26a948f5cfd helpful

[N Gelwan]

Ha! How appropriate.

[Kyle Miller]

It's not completely related, and I don't think it really helps, but just for sake of pointing out a nice idea to handle dependent types in algebra, here is a definition for a general version of chain complexes: https://github.com/leanprover-community/mathlib4/blob/5a809b6adb326ce351012b12a484544844277798//Mathlib/Algebra/Homology/HomologicalComplex.lean#L57-L61

The differential for a chain complex indexed by the integers is a map d i : X i -> X (i - 1) (or the other way), however this leads to dependent type issues since this fixes the latter term to being defeq to i - 1 rather than anything that equals i - 1.

The trick is to define d i j : X i -> X j for all i and j and then make it be 0 when j isn't equal to i - 1. This trick is possible because there's a default value d can take for invalid inputs -- the zero morphism.

[N Gelwan]

@Eric Wieser Wicked
Screenshot-2023-12-26-at-2.01.54-PM.png

[N Gelwan]

For those following and interested, I'll give a brief description of what Wieser and Zhang write.

First, they highlight the point that @Trebor Huang made, that there's an equivalence between "internally" and "externally" graded types: internal gradation is a map from a large type to the grade; and external gradation is a dependent type from the grade. They use externally graded types for discussion.

Using the construction of a graded semi-group as an example, they present 6 options for pushing an identity in the domain of an externally graded type to equivalence between components (quoting directly from the paper):

1. Use heterogenous equality (denoted ==), which allows us to express equality
   between distinct types (ex.

2. Express the equality in terms of sigma types or dependent pairs, denoted
   Σ i, A i (ex).

3. Express the grading constraint as an equality on sigma types (ex).

4. Provide an explicit proof that the equality is type correct using the recursor
   for equality, eq.rec (ex).

5. Store a canonical map between objects of the “same” grade to use instead
   of using eq.rec, to allow better definitional control (ex).

6. Take an additional index into mul (they're talking about a graded semigroup) and a proof that it is equal to i + j (ex).

[Eric Wieser]

In retrospect I think 5 was in fact the better design, and we're now in a good place to do the refactor and evaluate if it makes things simpler

[N Gelwan]

Ah, good to know. I'll start with that in my toy problem.

[N Gelwan]

This is what I ended up with:

import Mathlib


namespace ValuationAlgebras


variable
  {ι : Type*}
  [Lattice ι]
  (A : ι → Type*)


def Principal [Lattice ι] (i : ι) := { j : ι // j ≤ i }


instance [Lattice ι] (i : ι) : CoeOut (Principal i) ι where
  coe j := j.val


class ValuationAlgebra where
  /-- Cast terms of one grade to another when those grades can be equated -/
  cast (h : i = j) : A i → A j
  /-- Reflexivity casts to the identity -/
  cast_rfl (x : A i) : cast rfl x = x
  /-- Inter-grade multiplication -/
  mul : A i → A j → A (i ⊔ j)
  /-- Inter-grade multiplication is commutative -/
  mul_comm (x : A i) (y : A j) : cast sup_comm (mul x y) = mul y x
  /-- Inter-grade multiplication is associative -/
  mul_assoc (x : A i) (y : A j) (z : A k) : cast sup_assoc (mul (mul x y) z) = mul x (mul y z)
  /-- Each grade has a `one` -/
  one i : A i
  /-- Intra-grade multiplication by the grade's `one` is the identity -/
  mul_one (x : A i) : cast sup_idem (mul x (one i)) = x
  /-- Inter-grade multiplication of `one` elements produces a `one` element -/
  mul_one_one : mul (one i) (one j) = one (i ⊔ j)
  /-- Marginalization over sub-grades -/
  margin : A i → (j : Principal i) → A j
  /-- Marginalization respects transitivity of sub-grades -/
  margin_trans (x : A i) (j : Principal i) (k : Principal (j : ι)) : margin (margin x j) k = margin x ⟨k, le_trans k.property j.property⟩
  /-- Marginalization distributes across multiplication in a particular way -/
  margin_mul (x : A i) (y : A j) : margin (mul x y) ⟨i, le_sup_left⟩ = cast sup_inf_self (mul x (margin y ⟨i ⊓ j, inf_le_right⟩))

The last two properties have a kind of gnarly declaration (made marginally better if we declare a instance [Lattice ι] (i : ι) : Lattice (Principal i) and promise to propagate annoying manual dependent constructions all over the place, but that's really because of the nasty dependent type of ValuationAlgebra.margin.

I wonder if I can apply some of the abstractive principles we used here in grading algebras to treat a lattice of principal ideals. I'll give it a shot later.

Haven't put this to use, yet. I'll drop an update about ease-of-use later as well.

[N Gelwan]

Ended up having to add a bunch of cast identities:

import Mathlib


namespace ValuationAlgebras


variable
  {D : Type*}
  [DistribLattice D]
  (Φ : D → Type*)


class ValuationAlgebra where
  /-- Cast terms of one grade to another when those grades can be equated -/
  cast (p : x = y) : Φ x → Φ y
  /-- Reflexivity casts to the identity -/
  cast_rfl : ∀ φ : Φ x, cast rfl φ = φ
  /-- Casting across the symmetry of equality produces inverses -/
  cast_symm : ∀ φ : Φ x, ∀ ψ : Φ y, ∀ p : x = y, (cast p φ) = ψ ↔ φ = (cast (Eq.symm p) ψ)
  /-- Casting across two equalities is casting across their transitivity -/
  cast_trans : ∀ φ : Φ x, ∀ p : x = y, ∀ q : y = z, cast q (cast p φ) = cast (Eq.trans p q) φ
  /-- Inter-grade multiplication -/
  mul : Φ x → Φ y → Φ (x ⊔ y)
  /-- Inter-grade multiplication is commutative -/
  mul_comm : ∀ φ : Φ x, ∀ ψ : Φ y, mul φ ψ = cast sup_comm (mul ψ φ)
  /-- Inter-grade multiplication is associative -/
  mul_assoc : ∀ φ : Φ x, ∀ ψ : Φ y, ∀ ϕ : Φ z, cast sup_assoc (mul (mul φ ψ ) ϕ) = mul φ (mul ψ ϕ)
  /-- Casting respects multiplication -/
  cast_mul : ∀ φ : Φ x, ∀ ψ : Φ y, ∀ p : x = z, mul (cast p φ) ψ = cast (congrArg (· ⊔ y) p) (mul φ ψ)
  /-- Each grade has a `one` -/
  one x : Φ x
  /-- Intra-grade multiplication by the grade's `one` is the identity -/
  mul_one (φ : Φ x) : φ = cast sup_idem (mul φ (one x))
  /-- Inter-grade multiplication of `one` elements produces a `one` element -/
  mul_one_one : mul (one x) (one y) = one (x ⊔ y)
  /-- Marginalization over sub-grades -/
  margin (φ : Φ x) (y : D) (p : y ≤ x) : Φ y
  /-- Marginalization respects reflexivity of sub-grades -/
  margin_refl : ∀ φ : Φ x, margin φ x (le_refl x) = φ
  /-- Marginalization respects transitivity of sub-grades -/
  margin_trans : ∀ φ : Φ x, ∀ y z : D, ∀ p : z ≤ y, ∀ q : y ≤ x, margin φ z (le_trans p q) = margin (margin φ y q) z p
  /-- Marginalization distributes across multiplication in a particular way -/
  margin_mul : ∀ φ : Φ x, ∀ ψ : Φ y, margin (mul φ ψ) x le_sup_left = cast sup_inf_self (mul φ (margin ψ (x ⊓ y) inf_le_right))
  /-- Casting respects marginalization when a grade is cast -/
  cast_margin_le_of_eq : ∀ φ : Φ x, ∀ y z : D, ∀ p : y ≤ x, ∀ q : z = x, margin φ y p = margin (cast q.symm φ) y (le_of_le_of_eq p q.symm)
  /-- Casting respects marginalization when a sub-grade is cast -/
  cast_margin_eq_of_le : ∀ φ : Φ x, ∀ y z : D, ∀ p : y ≤ x, ∀ q : z = y, margin φ y p = cast q (margin φ z (le_of_eq_of_le q p))

I have a couple of proofs formalized but am starting to grind to a halt on the third. There's a substantial overhead to managing the casting; I'm constantly pulling it out of sub-terms with cast_mul, cast_margin_le_of_eq, and cast_margin_eq_of_le, consolidating casts with cast_trans, and bouncing them around with cast_symm derivatives.

With the proof I'm currently working on I've finally hit a wall and might have to re-examine the approach. I'll admit that I don't have a handle on how to get the most out of the proof system so there might be some more juice I can squeeze without having to build or tear-down any machinery.

[Eric Wieser]

I don't think you need to add all those extra axioms for cast; they follow from cast_rfl:

import Mathlib


namespace ValuationAlgebras


variable
  {D : Type*}
  [DistribLattice D]
  (Φ : D → Type*)


class ValuationAlgebra where
  /-- Cast terms of one grade to another when those grades can be equated -/
  cast (p : x = y) : Φ x → Φ y
  /-- Reflexivity casts to the identity -/
  cast_rfl : ∀ φ : Φ x, cast rfl φ = φ

variable [ValuationAlgebra Φ]

/-- Casting across the symmetry of equality produces inverses -/
theorem ValuationAlgebra.cast_symm (φ : Φ x) (ψ : Φ y) (p : x = y) : (cast p φ) = ψ ↔ φ = (cast (Eq.symm p) ψ) := by
  cases p
  rw [cast_rfl, cast_rfl]

/-- Casting across two equalities is casting across their transitivity -/
theorem ValuationAlgebra.cast_trans (φ : Φ x) (p : x = y) (q : y = z) : cast q (cast p φ) = cast (Eq.trans p q) φ := by
  cases p
  cases q
  rw [cast_rfl, cast_rfl]

[N Gelwan]

Ah, I was wondering whether they were superfluous! Thanks for the tip.

[Eric Wieser]

I think you can drop cast_margin_le_of_eq and cast_margin_eq_of_le for the same reason

[Eric Wieser]

One thing that I think you do is build a type akin to GradedMonoid, and put a CommSemigroup structure on it using your Mul fields

[Eric Wieser]

Then whenever you need to do algebraic manipulation, you can switch to that type

[N Gelwan]

The annoying thing about this structure is that the grade of an element is almost always relevant when you're marginalizing, since the signature of that function is dependent on the grade. Such a pain.

I'm going to see how much mileage I can get out of your suggestion, though.

[N Gelwan]

Oh, I just found out about ▸. @Eric Wieser is there any reason to prefer using the ad-hoc cast method over this, ex.

class ValuationAlgebra where
  /-- Inter-grade multiplication -/
  mul : Φ x → Φ y → Φ (x ⊔ y)
  /-- Inter-grade multiplication is commutative -/
  mul_comm (φ : Φ x) (ψ : Φ y) : mul φ ψ = (sup_comm : x ⊔ y = y ⊔ x) ▸ (mul ψ φ)

[Eric Wieser]

Yes, the advantage of the custom cast is that when you make instances of this class, you can choose a cast that is nicer to prove things with.

[Eric Wieser]

It's only when you're in the abstract setting that it makes no difference

[N Gelwan]

Oh man, the triangle has so much useful machinery built-in (seems like it is automatically applying symmetry arguments?). I've got to explore whether it will be more productive to use this, given that I'm not writing a production-grade library or anything.

[N Gelwan]

Oh, but your point is a matter of semantics. Ok, I'll check ahead in the work I'm formalizing and see if I'm pursuing too deep a level of abstraction right now, gauge whether I'll actually be working with some nice concrete structures.

[N Gelwan]

Thanks for the tips, again.

[Kyle Miller]

Eric Wieser said:

Yes, the advantage of the custom cast is that when you make instances of this class, you can choose a cast that is nicer to prove things with.

In particular, it keeps the cast focused on a particular index. If you use triangle (a.k.a. Eq.rec) this is an unrestricted cast and it's hard (or maybe impossible?) to write lemmas you can be sure can apply with simp or rw. With cast, you can write the casts as algebraic rules.

[Kyle Miller]

If there's no reason for each class instance to have a custom cast, you might consider doing this instead:

def ValuationAlgebra.cast {Φ : D → Type*} [ValuationAlgebra Φ] (a : Φ x) (h : x = y) : Φ y :=
  h ▸ a