reverse (reverse a) = a

reverse_reverse_neutral.idr

reverseT : List a -> List a -> List a
reverseT r [] = r
reverseT r (a::as) = reverseT (a::r) as

reverse : List a -> List a
reverse = reverseT []

total
reverseT_ends_ts : Proofs.reverseT ts as = Proofs.reverse as ++ ts
reverseT_ends_ts {ts} {as=[]} = Refl
reverseT_ends_ts {ts} {as=a::as} =
	replace {P=\v => reverseT (a :: ts) as = v ++ ts} (sym $ reverseT_ends_ts {ts=[a]}) $
	replace (appendAssociative (Proofs.reverse as) [a] ts) $
	reverseT_ends_ts {ts=a :: ts}

total
append_right_inductive_wrap : {c, l, r : List t} -> l = r -> l ++ c = r ++ c
append_right_inductive_wrap Refl = Refl

total
append_left_inductive_wrap : {c, l, r : List t} -> l = r -> c ++ l = c ++ r
append_left_inductive_wrap Refl = Refl

mutual
	total
	reverseT_prefix : Proofs.reverseT ts (as ++ bs) = Proofs.reverseT (Proofs.reverse as ++ ts) bs
	reverseT_prefix {ts} {as=[]} {bs} = Refl
	reverseT_prefix {ts} {as=a :: as} {bs} =
		replace
			{P=\v => v = Proofs.reverseT (Proofs.reverseT [a] as ++ ts) bs}
			(sym $ reverseT_ends_ts {ts=a::ts} {as=as ++ bs})
		$
		replace
			(sym $ reverseT_ends_ts {ts=Proofs.reverseT [a] as ++ ts} {as=bs})
		$
		replace
			{P=\v => Proofs.reverse (as ++ bs) ++ a :: ts = Proofs.reverse bs ++ v ++ ts}
			(sym $ reverseT_ends_ts {ts=[a]})
		$
		replace
			{P=\v => Proofs.reverse (as ++ bs) ++ a :: ts = Proofs.reverse bs ++ v}
			(appendAssociative (Proofs.reverse as) [a] ts)
		$
		replace
			(sym $ appendAssociative (Proofs.reverse bs) (Proofs.reverse as) (a::ts))
		$
		append_right_inductive_wrap {l=Proofs.reverse (as ++ bs)} {r=Proofs.reverse bs ++ Proofs.reverse as} {c=a::ts} $
		reverse_append_split

	total
	reverse_append_split : Proofs.reverse (as ++ bs) = Proofs.reverse bs ++ Proofs.reverse as
	reverse_append_split {as} {bs} =
		replace
			(reverseT_ends_ts {as=bs} {ts=Proofs.reverse as})
		$
		replace
			{P=\v => Proofs.reverse (as ++ bs) = Proofs.reverseT v bs}
			(appendNilRightNeutral (Proofs.reverse as))
		$
		reverseT_prefix

total
reverse_reverse_neutral : Proofs.reverse (Proofs.reverse as) = as
reverse_reverse_neutral {as=[]} = Refl
reverse_reverse_neutral {as=a :: as} =
	replace
		{P=\v => Proofs.reverse v = a::as}
		(sym $ reverseT_ends_ts {as=as} {ts=[a]})
	$
	replace
		{P=\v => v = a::as}
		(sym $ reverseT_prefix {as=Proofs.reverse as} {bs=[a]} {ts=[]})
	$
	append_left_inductive_wrap {c=[a]} $
	replace
		{P=\v => v = as}
		(sym $ appendNilRightNeutral (Proofs.reverse $ Proofs.reverse as))
	$
	reverse_reverse_neutral