ReverseReverse3

Description

using a definition from haskell2010-1.1.1.0

Definitions (download)

module Definitions where

open import Data.List

myreverse : ∀ {a} {A : Set a} → List A → List A
myreverse {a}{A} xs = rev xs []
  where
    rev : List A → List A → List A
    rev []       a = a
    rev (x ∷ xs) a = rev xs (x ∷ a)

Theorem (download)

module Theorem where

open import Definitions

open import Data.List
open import Relation.Binary.PropositionalEquality

postulate
  revrev : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs

Verifier

module Verifier where

open import Definitions
open import Theorem

open import Data.List
open import Relation.Binary.PropositionalEquality

verify : ∀ {a} {A : Set a} (xs : List A) → myreverse (myreverse xs) ≡ xs
verify = revrev

Proofs

Rank Prover Size Date