Failing to prove that reversing a list reverses its order in Agda

Reverse.agda

open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary
open import Data.List
open import Data.List.Properties
open import Data.Unit hiding (_≤_)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Fin
open import Data.Nat as ℕ hiding (_≤_)

-- We parameterise the whole module over a type of list elements.
module Reverse (A : Set) where

-- Various ways to say that a function reverses its argument, or similar
-- properties.

-- Way #1: Three properties together characterise "reversal":
-- 1. reverse [] = []; it leaves empty list alone.
-- 2. reverse [x] = [x]; it leaves singletons alone.
-- 3. reverse (x ++ y) = reverse y ++ reverse x,
--    where (x ++ y) means concatenate x & y".
Reverses1 : (f : List A → List A) → Set
Reverses1 f = f [] ≡ []
            × (∀ x → f (x ∷ []) ≡ x ∷ [])
            × (∀ x y → f (x ++ y) ≡ f y ++ f x)

-- Way #2: Since any list has exactly one reversal, all list-reversing functions
-- have the same input/output behavior. So the property of reversing lists is
-- the same as the propety of "behaving like Data.List.reverse".
--
-- This is kinda boring, though.
Reverses2 : (f : List A → List A) → Set
Reverses2 f = ∀ L → f L ≡ reverse L

-- Way #3: As @haskell_cat suggested, we can require the lengths to be equal and
-- lookup to be inverted: the i'th element from the right of L should be the
-- i'th element from the left of (reverse L). This feels most "natural" to me,
-- but it involves indexing arithmetic, a thing Agda is... not great at.
inverse : ∀ n → Fin n → Fin n
inverse (suc n) zero = fromℕ n
inverse (suc n) (suc i) = suc (inverse n i)

lookup-from-end : (L : List A) → Fin (length L) → A
lookup-from-end L i = lookup L (inverse (length L) i)

Reverses3 : (f : List A → List A) → Set
Reverses3 f = ∀ L i
            → Σ[ samelen ∈ length (f L) ≡ length L ]
              (lookup (f L) i ≡ lookup-from-end L (subst Fin samelen i))

-- Property #4: Turns ascending lists into descending lists. There are actually
-- many ways of phrasing this third property alone. Also, while any reverse
-- function should satisfy this, there are other functions that do so (like the
-- function that always returns an empty list).
AscDescProperty : (f : List A → List A) → Set1
AscDescProperty f =
  -- For any binary relation ⊑ on elements and list L...
  -- (this is the bit that "parameterizes over order", IMO)
  ∀ (_⊑_ : Rel A lzero) (L : List A) →
  -- If L is ascending...
  (∀ i j → i ≤ j → lookup L i ⊑ lookup L j) →
  -- then (f L) is descending.
  (∀ i j → j ≤ i → lookup (f L) i ⊑ lookup (f L) j)

-- The trouble is proving that properties #1, #2, or #3 each imply property #4.
-- So far I have been unable to do this, although I'm confident it's possible.


-- ADDENDUM! Does the standard library reverse function satisfy properties
-- #1-#3? Let's see!

-- Property #1: check!
reverse-reverses1 : Reverses1 reverse
reverse-reverses1 = refl , (λ x → refl) , reverse-++-commute

-- Property #2 is just "behaving the same as the standard library reverse
-- function", so, yes.
reverse-reverses2 : Reverses2 reverse
reverse-reverses2 L = refl

-- Property #3, I haven't been able to prove yet, although I have some ideas.

-- And property #4, as I stated already, I haven't proven yet.