ReverseReverse1

Description

a simple reverse definition.

Definitions (download)

module Definitions where

open import Data.List

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

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
1 Lost_dog_ 325 2014-04-20 10:43:16 JST
2 trigott 645 2014-05-28 00:34:29 JST