wellfoundedness of Strict lexicographic ordering on List

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

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?

@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.

@fredrikNordvallForsberg oops! 🤦

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

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?

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.

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.

Modulo:

• merge of [ add ] wellfoundedness of Relation.Binary.Construct.Add.Infimum.Strict #2683
• fixing the termination checker to unwind the mutual dependency, and observing that recursion is on shorter sublists (!?)

the following should actually work (?), by analogy with Vec:

  module _ (≈-trans : Transitive _≈_) (≺-respʳ : _≺_ Respectsʳ _≈_ ) (≺-wf : WellFounded _≺_)
    where

    private
      _≺×ₗₑₓ<′_ : Rel (A × List A) _
      _≺×ₗₑₓ<′_ = ×-Lex _≈_ _≺_ _<_

      _≺×ₗₑₓ<_ : Rel (List A) _
      _≺×ₗₑₓ<_ = _<₋_ _≺×ₗₑₓ<′_ on uncons
    
      <⇒≺×ₗₑₓ< : _<_ ⇒ _≺×ₗₑₓ<_
      <⇒≺×ₗₑₓ< halt           = ⊥₋<[ _ , _ ]
      <⇒≺×ₗₑₓ< (this x≺y)     = [ inj₁ x≺y ]
      <⇒≺×ₗₑₓ< (next x≈y y<x) = [ inj₂ (x≈y , y<x) ]

    <-wellFounded : WellFounded _<_
    ≺×ₗₑₓ<-wellFounded : WellFounded _≺×ₗₑₓ<_

    <-wellFounded []         = acc λ ys<[] → contradiction ys<[] xs≮[]
    <-wellFounded xs@(_ ∷ _) = Subrelation.wellFounded <⇒≺×ₗₑₓ< ≺×ₗₑₓ<-wellFounded xs
    
    ≺×ₗₑₓ<-wellFounded = On.wellFounded uncons (<₋-wellFounded _≺×ₗₑₓ<′_ (×-wellFounded' ≈-trans ≺-respʳ ≺-wf <-wellFounded))

Comments welcome.