a chain related by `≤` and a chain related by `<`

Stream: Is there code for X?

[Jujian Zhang]

I think the following is true: given a list l : list X and an irreflexive relation relation r on X such that list.chain' (λ x y, r x y ∨ x = y) l, i.e. l is a chain related by r disjoint with equality, then l.destutter is a chain related by r? In another word, is there a code for the sorry below?

example {X : Type*} [decidable_eq X] (l : list X) (r : X → X → Prop)
  [is_irrefl X r]
  (hl : list.chain' (λ x y, r x y ∨ x = y) l) :
  list.chain' r l.destutter :=  sorry

The mental model is taking r to be less than on integers, then l is $a_0 \le a_1 \le a_2 \le ... a_n$, then removing duplication should give you a list $b_0 < ... < b_m$.

[Yaël Dillies]

That looks like it should be easy by induction. But no I don't think we have it.

[Yaël Dillies]

Actually, your precise statement is wrong. If you replace dedup by destutter or assume transitivity of r, it becomes true again.

[Eric Rodriguez]

and destutter should have this lemma

[Eric Rodriguez]

docs#list.destutter

[Jujian Zhang]

Yaël Dillies said:

Actually, your precise statement is wrong. If you replace dedup by destutter or assume transitivity of r, it becomes true again.

Thanks for pointing out this, one of the application I need is that r being covby, so I can't assume transitivity of r, but destutter is a good idea!

[Yaël Dillies]

Ah I think what you really need is acyclicity, not transitivity.