Solution to https://twitter.com/arntzenius/status/1034919539467677696

rev_asc_desc.v

Require Import Coq.Lists.List Coq.Relations.Relations Coq.Sorting.Sorted.
Require Import Coq.Program.Equality Psatz.

Lemma Sorted_iff_by_explicit_indices {A} {R: relation A} (l: list A):
  Sorted R l <-> forall n, (S n) < length l -> exists d,
    R (nth n l d) (nth (S n) l d).
Proof with (cbn in *; firstorder).
  split; induction l; intros.
  - unshelve esplit; contradict H0...
  - unshelve esplit; intuition; inversion H.
    induction n.
    + destruct H4...
    + intros...
      assert (S n < length l) by intuition.
      destruct (H5 n H6).
      do 2 rewrite (nth_indep l a x) by intuition.
      trivial.
  - intuition.
  - apply Sorted_cons.
    + apply IHl; intros.
      apply (H (S n))...
    + induction l...
      apply HdRel_cons.
      pose proof (H 0 ltac:(cbn;intuition))...
Qed.

Theorem rev_asc_desc {A} {R: relation A} (l: list A):
  (Sorted R l) -> (Sorted (transp _ R) (rev l)).
Proof.
  repeat rewrite Sorted_iff_by_explicit_indices.
  intros; destruct l.
  - contradict H0; firstorder.
  - rewrite rev_length in H0.
    set (L := length (a :: l)) in *.
    pose (m := L - S (S n)).
    assert ((S m) < L) by (unfold m; intuition).
    destruct (H m H1); exists x.
    do 2 rewrite rev_nth by intuition; fold L m.
    replace (L - S n) with (S m); unfold m; intuition.
Qed.