def snoc : list A $$ A $$ list A

$|[]$ a :$=[$a$]$

$|($a :: as$)$ b :$=$ a :: $($snoc as b$)$

def rev : list A $$ list A

$|[]$ :$=[]$

$|($a :: as$)$ :$=$ snoc $($rev as$)$ a

$/-$

Our implementation of rev is inefficient: it has O$($n$^2)$ complexity.

The definition below $($called fastrev$)$ is efficient, having only O$($n$)$ complexity.

It uses an auxilliary function revaux which accumulates the reversed

list in a $2$nd variable.

$-/$

def revaux : list A $$ list A $$ list A

$|[]$ bs :$=$ bs

$|($a :: as$)$ bs :$=$ revaux as $($a :: bs$)$

def fastrev $($l : list A$)$ : list A

:$=$ revaux l $[]$

#reduce fastrev $[1,2,3]$

end revDefn

namespace ex$07$

open revDefn

$/----$ Do not add$/$change anything above this line $----/$

$/-$

However we would like to show that fast rev and rev do the same thing.

You'll need to establish a lemma about revaux $($hint: try writing

down a precise specification of what revaux does$).$

You may use the fact that lists with $++$ form a monoid

$($just copy the proofs from the lecture$).$

$-/$

open nat

def append : list A $$ list A $$ list A

$|[]$ bs :$=$ bs

$|($a :: as$)$ bs :$=$ a :: $($append as bs$)$

local notation $($name :$=$ append$)$ as $++$ bs :$=$ append as bs

theorem rneutr : $$ as : list A$,$

as $++$ nil $=$ as :$=$

begin

assume as$,$

induction as with a as$\text{'}$ ih$,$

reflexivity,

dsimp $[$append$],$

rewrite ih$,$

end

lemma lem$1$ : $($as bs : list A$),$ revaux as bs $=($rev as$)++$ bs :$=$

begin

assume as bs$,$

end

theorem fastrev$\_$thm : $$ as : list A $,$ fastrev as $=$ rev as :$=$

begin

sorry,

end