Answering someone's question from WeChat

List-rev-ind.agda

{-# OPTIONS --cubical --safe #-}

open import Cubical.Foundations.Prelude
open import Cubical.Data.List

private variable X : Type

rev-ind : (P : List X → Type)
  → P []
  → (∀ x xs → P xs → P (xs ∷ʳ x))
  → (xs : List X) → P xs
rev-ind P bc ic [] = bc
-- this is filled by pressing Ctrl-C Ctrl-A, I didn't review it
-- maybe there is a better implementation
rev-ind P bc ic (x ∷ xs) = rev-ind (λ z → P (x ∷ z)) (ic x [] bc) (λ x xs → ic x (_ ∷ xs)) xs


-- parameters are written here so they're all fixed in the following definitions
module _ {A : Type} {a : A} where
  -- random theorem that is probably not suitable for rev-ind
  demo : (xs : List A) → xs ++ [ a ] ≡ rev (a ∷ rev xs)
  demo = rev-ind
    -- the motive, created by "copying" the goal
    -- and rename xs to the parameter
    -- no need of those implicit parameters
    (λ z → z ++ [ a ] ≡ rev (a ∷ rev z))
    -- base case is just refl
    refl
    -- I don't see how to fill this, but I don't think you need this either
    {!!}