ReverseReverse3 FIXED

Description

using a definition from haskell2010-1.1.1.0

Definitions (download)

module Definitions where

open import Data.List

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

myreverse : ∀ {a} {A : Set a} → List A → List A
myreverse {a}{A} xs = rev xs []

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 Rotsor 195 2015-02-01 06:52:20 JST
2 trigott 470 2014-11-15 07:48:13 JST
3 Lost_dog_ 764 2014-04-20 10:54:21 JST