open list

set$\_$option pp$.$structure$\_$projections false

variables $\{$A B C : Type$\}$

$/-$

In the lecture we have introduced the function reverse

$($and the auxilliary function snoc$)$

$-/$

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

$/-$

Part $1$ :

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

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

It uses an auxillary 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]$

$/-$

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

You need to establish a lemma about revaux which you can rpve by induction.

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

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

$-/$

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

begin

sorry,

end $-$ i have to prove this but without using tactics such as intros, simp, list.append$\_$nil etc