Base positions

In this file, we define position functions for atoms, litters, and near-litters.

Main declarations

• ConNF.instPositionLitter: The position function for litters.
• ConNF.instPositionAtom: The position function for atoms.
• ConNF.instPositionNearLitter: The position function for near-litters.

TODO: These position functions are very simple to define but might not have all the required properties (e.g. joint injectivity, positions of litters compared to their near-litters). We should investigate this later, once we know precisely what is needed. The properties of the position function on litters allows for a concise description of the fuzz map condition.

instance ConNF.instPositionLitter [ConNF.Params] : ConNF.Position ConNF.Litter

Equations

• ConNF.instPositionLitter = { pos := { toFun := ConNF.funOfDeny ⋯ (fun (L : ConNF.Litter) => {L.ν}) ⋯, inj' := ⋯ } }

theorem ConNF.Litter.lt_pos [ConNF.Params] (L : ConNF.Litter) : L.ν < ConNF.pos L

instance ConNF.instPositionAtom [ConNF.Params] : ConNF.Position ConNF.Atom

Equations

• ConNF.instPositionAtom = { pos := { toFun := ConNF.funOfDeny ⋯ (fun (a : ConNF.Atom) => {ConNF.pos aᴸ}) ⋯, inj' := ⋯ } }

theorem ConNF.Atom.pos_litter_lt_pos [ConNF.Params] (a : ConNF.Atom) : ConNF.pos aᴸ < ConNF.pos a

instance ConNF.instPositionNearLitter [ConNF.Params] : ConNF.Position ConNF.NearLitter

Equations

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

theorem ConNF.NearLitter.pos_litter_lt_pos [ConNF.Params] (N : ConNF.NearLitter) : ConNF.pos Nᴸ < ConNF.pos N

theorem ConNF.NearLitter.pos_atom_lt_pos [ConNF.Params] (N : ConNF.NearLitter) (a : ConNF.Atom) (h : a ∈ symmDiff Nᴬ Nᴸᴬ) : ConNF.pos a < ConNF.pos N