Bridge between Domino representations

This module provides equivalence functions between the two Domino representations used in the project:

1. WeightedSets.lean (DominoTilingsZ.Domino): Inductive type with horizontal/vertical constructors, using ℤ coordinates, with Set Domino for tilings
2. DominoTilings.lean (DominoTilings.Domino): Structure with cell1/cell2 fields, using ℕ coordinates, with Finset Domino for tilings

Design Rationale

The two representations were designed for different purposes:

• DominoTilingsZ uses ℤ coordinates for generality in weighted set theory and generating function calculations. The inductive type makes pattern matching on orientation natural.
• DominoTilings uses ℕ coordinates for finite rectangle tilings and faultfree classification. The structure representation is more flexible for adjacency conditions.

For rectangles with positive coordinates (the typical case), the representations are equivalent. This bridge enables theorem transfer between files when needed.

Main Definitions

• DominoBridge.toDominoZ: Convert a DominoTilings.Domino to DominoTilingsZ.Domino
• DominoBridge.toDominoN: Convert a DominoTilingsZ.Domino with positive coordinates to DominoTilings.Domino
• DominoBridge.hasPositiveCoords: Predicate for DominoTilingsZ.Domino having positive coords
• DominoBridge.cellsZ: The cells covered by a DominoTilings.Domino (cast to ℤ coordinates)

Main Results

• DominoBridge.toDominoZ_hasPositiveCoords: Converting from ℕ preserves positivity
• DominoBridge.toDominoZ_cells: Converting to ℤ preserves the set of cells
• DominoBridge.toDominoN_cells: Converting from ℤ preserves the set of cells

References

• Source files: FPS/WeightedSets.lean (DominoTilingsZ), Details/DominoTilings.lean (DominoTilings)

Tags

domino, tiling, bridge, equivalence

Coordinate conversion helpers

def DominoBridge.cellsZ (d : DominoTilings.Domino) : Set (ℤ × ℤ)

The cells covered by a DominoTilings.Domino, cast to ℤ coordinates. This allows comparison with DominoTilingsZ.Domino.toShape.

Equations

• DominoBridge.cellsZ d = {(↑d.cell1.1, ↑d.cell1.2), (↑d.cell2.1, ↑d.cell2.2)}

Conversion from DominoTilings.Domino to DominoTilingsZ.Domino

Note: We use DominoTilings.Domino.isHorizontal and DominoTilings.Domino.isVertical from DominoTilings.lean via dot notation (e.g., d.isHorizontal).

def DominoBridge.toDominoZ (d : DominoTilings.Domino) : DominoTilingsZ.Domino

Convert a DominoTilings.Domino to DominoTilingsZ.Domino.

The conversion uses the minimum coordinate as the anchor point:

• A horizontal domino becomes DominoTilingsZ.Domino.horizontal (min col) row
• A vertical domino becomes DominoTilingsZ.Domino.vertical col (min row)

Equations

• One or more equations did not get rendered due to their size.

Conversion from DominoTilingsZ.Domino to DominoTilings.Domino

def DominoBridge.hasPositiveCoords : DominoTilingsZ.Domino → Prop

A DominoTilingsZ.Domino has positive coordinates if all its cells have positive coordinates. This is the precondition for converting to DominoTilings.Domino (which uses ℕ coordinates).

Equations

• DominoBridge.hasPositiveCoords (DominoTilingsZ.Domino.horizontal i j) = (i ≥ 1 ∧ j ≥ 1)
• DominoBridge.hasPositiveCoords (DominoTilingsZ.Domino.vertical i j) = (i ≥ 1 ∧ j ≥ 1)

instance DominoBridge.instDecidablePredDominoHasPositiveCoords : DecidablePred hasPositiveCoords

Equations

• DominoBridge.instDecidablePredDominoHasPositiveCoords (DominoTilingsZ.Domino.horizontal i j) = inferInstanceAs (Decidable (i ≥ 1 ∧ j ≥ 1))
• DominoBridge.instDecidablePredDominoHasPositiveCoords (DominoTilingsZ.Domino.vertical i j) = inferInstanceAs (Decidable (i ≥ 1 ∧ j ≥ 1))

def DominoBridge.toDominoN (d : DominoTilingsZ.Domino) (hpos : hasPositiveCoords d) : DominoTilings.Domino

Convert a DominoTilingsZ.Domino with positive coordinates to DominoTilings.Domino.

The conversion preserves the cells covered by the domino:

• A horizontal domino at (i, j) becomes a DominoTilings.Domino with cells (i, j) and (i+1, j)
• A vertical domino at (i, j) becomes a DominoTilings.Domino with cells (i, j) and (i, j+1)

Equations

• DominoBridge.toDominoN (DominoTilingsZ.Domino.horizontal i j) ⋯ = { cell1 := (i.toNat, j.toNat), cell2 := ((i + 1).toNat, j.toNat), distinct := ⋯, adjacent := ⋯ }
• DominoBridge.toDominoN (DominoTilingsZ.Domino.vertical i j) ⋯ = { cell1 := (i.toNat, j.toNat), cell2 := (i.toNat, (j + 1).toNat), distinct := ⋯, adjacent := ⋯ }

Round-trip properties

theorem DominoBridge.toDominoZ_hasPositiveCoords (d : DominoTilings.Domino) (h1 : d.cell1.1 ≥ 1) (h2 : d.cell1.2 ≥ 1) (h3 : d.cell2.1 ≥ 1) (h4 : d.cell2.2 ≥ 1) : hasPositiveCoords (toDominoZ d)

Converting DominoTilings.Domino to DominoTilingsZ.Domino produces positive coordinates when all cells are positive.

Cell preservation theorems

theorem DominoBridge.toDominoZ_cells (d : DominoTilings.Domino) : (toDominoZ d).toShape = cellsZ d

Converting DominoTilings.Domino to DominoTilingsZ.Domino preserves the set of cells (cast to ℤ).

This is the key theorem for theorem transfer between the two representations. It shows that the cells covered by a domino are the same regardless of which representation is used.

theorem DominoBridge.toDominoN_cells (d : DominoTilingsZ.Domino) (hpos : hasPositiveCoords d) : cellsZ (toDominoN d hpos) = d.toShape

Converting DominoTilingsZ.Domino to DominoTilings.Domino preserves the set of cells (cast to ℤ).

Canonical form for DominoTilings.Domino

The DominoTilings.Domino type allows the two cells to be in either order. For a canonical representation, we define a form where cell1 is always the "smaller" cell.

def DominoBridge.isCanonical (d : DominoTilings.Domino) : Prop

A DominoTilings.Domino is in canonical form if cell1 is the "smaller" cell:

• For horizontal dominos: cell1 has smaller column
• For vertical dominos: cell1 has smaller row

Equations

• DominoBridge.isCanonical d = if d.isHorizontal then d.cell1.1 < d.cell2.1 else d.cell1.2 < d.cell2.2

def DominoBridge.swap (d : DominoTilings.Domino) : DominoTilings.Domino

Swap the cells of a DominoTilings.Domino.

Equations

• DominoBridge.swap d = { cell1 := d.cell2, cell2 := d.cell1, distinct := ⋯, adjacent := ⋯ }

def DominoBridge.toCanonical (d : DominoTilings.Domino) : DominoTilings.Domino

Convert a DominoTilings.Domino to canonical form.

Equations

• DominoBridge.toCanonical d = if d.isHorizontal then if d.cell1.1 < d.cell2.1 then d else DominoBridge.swap d else if d.cell1.2 < d.cell2.2 then d else DominoBridge.swap d

theorem DominoBridge.toCanonical_cells (d : DominoTilings.Domino) : {(toCanonical d).cell1, (toCanonical d).cell2} = {d.cell1, d.cell2}

The cells of a domino in canonical form are the same as the original.

Rectangle correspondence

The two Rectangle definitions use different types:

• DominoTilings.Rectangle n m : Finset (ℕ × ℕ) - finite set of natural number pairs
• DominoTilingsZ.Rectangle n m : Set (ℤ × ℤ) - set of integer pairs

We establish that they correspond under the natural embedding ℕ → ℤ.

def DominoBridge.cellToZ (c : ℕ × ℕ) : ℤ × ℤ

Cast a cell from ℕ × ℕ to ℤ × ℤ.

Equations

• DominoBridge.cellToZ c = (↑c.1, ↑c.2)

theorem DominoBridge.rectangle_correspondence (n m : ℕ) : cellToZ '' ↑(DominoTilings.Rectangle n m) = DominoTilingsZ.Rectangle n m

The image of DominoTilings.Rectangle under cellToZ equals DominoTilingsZ.Rectangle as sets of ℤ × ℤ.

Documentation: Relationship between representations

Key differences between the two Domino types:

Aspect	DominoTilingsZ.Domino	DominoTilings.Domino
Coordinates	ℤ × ℤ	ℕ × ℕ
Representation	Inductive (horizontal/vertical)	Structure (cell1, cell2)
Anchor	Explicit position parameter	Implicit via cells
Orientation	Explicit in constructor	Derived from cell positions

When to use each representation:

• DominoTilingsZ: Use when working with generating functions, weighted sets, or when you need to pattern match on orientation. The ℤ coordinates allow for translations that may temporarily go negative.

• DominoTilings: Use when working with finite tilings of rectangles, especially when you need to reason about cell membership in finsets. The structure representation is more flexible for adjacency conditions.

Bridging tilings:

To bridge between DominoTilingsZ.Tiling S and DominoTilings.DominoTiling n m, use:

1. toDominoZ / toDominoN for individual domino conversion
2. toDominoZ_cells / toDominoN_cells for cell preservation
3. rectangle_correspondence for shape correspondence

Tiling equivalence infrastructure

We develop the machinery to convert between DominoTilings.DominoTiling n m and DominoTilingsZ.Tiling (Rectangle n m). This requires:

1. Converting the set of dominos (Finset vs Set)
2. Preserving the disjointness property
3. Preserving the covering property

Converting a DominoTiling to a Tiling

def DominoBridge.dominoFinsetToSet (ds : Finset DominoTilings.Domino) : Set DominoTilingsZ.Domino

Convert a Finset of DominoTilings.Domino to a Set of DominoTilingsZ.Domino.

Equations

• DominoBridge.dominoFinsetToSet ds = {x : DominoTilingsZ.Domino | ∃ d ∈ ds, DominoBridge.toDominoZ d = x}

theorem DominoBridge.DominoTiling_dominos_pos {n m : ℕ} (T : DominoTilings.DominoTiling n m) (d : DominoTilings.Domino) (hd : d ∈ T.dominos) : d.cell1.1 ≥ 1 ∧ d.cell1.2 ≥ 1 ∧ d.cell2.1 ≥ 1 ∧ d.cell2.2 ≥ 1

The dominos in a DominoTiling have positive coordinates (cell coords ≥ 1).

theorem DominoBridge.toDominoZ_pairwise_disjoint {n m : ℕ} (T : DominoTilings.DominoTiling n m) : (dominoFinsetToSet T.dominos).PairwiseDisjoint DominoTilingsZ.Domino.toShape

Converting a DominoTiling preserves pairwise disjointness.

theorem DominoBridge.toDominoZ_cover {n m : ℕ} (T : DominoTilings.DominoTiling n m) : ⋃ d ∈ dominoFinsetToSet T.dominos, d.toShape = DominoTilingsZ.Rectangle n m

Converting a DominoTiling preserves the covering property.

def DominoBridge.toTilingZ {n m : ℕ} (T : DominoTilings.DominoTiling n m) : DominoTilingsZ.Tiling (DominoTilingsZ.Rectangle n m)

Convert a DominoTiling to a Tiling.

Equations

• DominoBridge.toTilingZ T = { dominos := DominoBridge.dominoFinsetToSet T.dominos, pairwise_disjoint := ⋯, cover := ⋯ }

Dominos in a Tiling of a rectangle have positive coordinates

theorem DominoBridge.Tiling_dominos_pos {n m : ℕ} (T : DominoTilingsZ.Tiling (DominoTilingsZ.Rectangle n m)) (d : DominoTilingsZ.Domino) (hd : d ∈ T.dominos) : hasPositiveCoords d

Dominos in a Tiling of a rectangle have positive coordinates.

theorem DominoBridge.toDominoN_injective {d1 d2 : DominoTilingsZ.Domino} (hpos1 : hasPositiveCoords d1) (hpos2 : hasPositiveCoords d2) (heq : toDominoN d1 hpos1 = toDominoN d2 hpos2) : d1 = d2

toDominoN is injective on dominos with positive coordinates.