[ add ] well-foundedness of the lifting of a relation to `Maybe`?

[jamesmckinna]

Do we have anywhere:

• the binary relation constructor _<_ {A : Set a} (R : Rel A ℓ) : Rel (Maybe A) (a ⊔ ℓ) (naming?) defined by
  • nothing < just x
  • x R y → just x < just y
• proofs of its properties, incl. in particular
  • WellFounded R → WellFounded _<_

If not:

• where should it live?
• what should it be called?
• etc.

Elsewhere, this is the (_)⊥ lifting in (C)POs, but I don't seem to be able to find it.

Application: wellfoundedness of Strict lexicographic ordering on List, via uncons, mimicking/extending the corresponding argument for Vec.

[jwaldmann]

wellfoundedness of Strict lexicographic ordering on List

I would buy that for length-lexicographic - else, [1] > [0,1] > [0,0,1] > ..., no?

[jamesmckinna]

Oh... it may be that I need to go back to school, but my understanding of Data.List.Relation.Binary.Lex.Core, lines 32--36

data Lex {A : Set a} (P : Set)
         (_≈_ : Rel A ℓ₁) (_≺_ : Rel A ℓ₂) :
         Rel (List A) (a ⊔ ℓ₁ ⊔ ℓ₂) where
  base : P                             → Lex P _≈_ _≺_ []       []
  halt : ∀ {y ys}                      → Lex P _≈_ _≺_ []       (y ∷ ys)
  this : ∀ {x xs y ys} (x≺y : x ≺ y)   → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)
  next : ∀ {x xs y ys} (x≈y : x ≈ y)
         (xs<ys : Lex P _≈_ _≺_ xs ys) → Lex P _≈_ _≺_ (x ∷ xs) (y ∷ ys)

(with P = ⊥ to yield the Strict version...)
was that we would instead have [] < [1] < [0,1] < [0,0,1] no?

This suggest that there might very well be some dissonance between rewriting conventions regarding Lex, and what we have in the library?

[fredrikNordvallForsberg]

@jamesmckinna I don't think we have [1] < [0,1] with that definition, no? With P = ⊥ we cannot use base, halt does not apply because [1] is not empty, for this to apply we would need 1 < 0 which we do not have, and for next to apply we would need 1 = 0 which we again do not have.

One reasonable restriction I know is that the lexicographic order is wellfounded if we restrict to strictly decreasing lists, which in particular rules out @jwaldmann's counterexample above.

[jamesmckinna]

@fredrikNordvallForsberg oops! 🤦

[jwaldmann]

the definition of Lex is fine ("rewriting convention" is just writing y > x for x < y) but it does not keep wellfoundedness.

if we turn around the chain I mentioned, we get ... < [0,0,1] < [0,1] < [1] (each step using some next, and ultimately this) showing that [1] is not accessible?

Using next and this (but never base or halt) from https://agda.github.io/agda-stdlib/v2.2/Data.List.Relation.Binary.Lex.Core.html#949

[jamesmckinna]

Thanks everyone for the (re)schooling!

In an attempt to reverse out of this cul-de-sac, and cover my shame, let me loop back to the OP and ask: do we have the 'lifting monad' on pre-/partial orders defined anywhere? And: does it 'lift' the wellfoundedness property, or am I similarly mistaken as above?

[jwaldmann]

This "lifting" is a special case of disjoint sum: well-founded M1 + well-founded M2,
with each x in M1 less that each y in M2, and this is wf by lex-order on pairs, think (1,x) < (2, y). Your case is M1 = one element.

[jamesmckinna]

Hmm I was a bit hasty closing the issue, as the 'better' version of lifting via union also does not seem present in the library, IIUC. But given that I'm not currently about what I do and don't understand, I'd be happy to be pointed to it if it exists, or else for a PR which contributes it... ;-)

Finally: Relation.Binary.Construct.Add.Infimum.(Non)Strict based on Relation.Nullary.Construct.Add.Infimum.

See: #2683