哈Ha

前几天，我去了一家严肃的公司接受采访，他们在那里给我上交一个简单的清单。 不幸的是，此任务在整个采访的第一轮中进行，采访结束时，采访者说今天其他所有人都病了，所以我可以回家了。 然而，解决这个问题的整个过程，包括对算法的几个选择及其后续讨论，以及关于列表翻转的讨论，都应运而生。

我们解决问题

面试官非常友善：

- 好吧，让我们首先解决这个问题：给出一个简单的连接列表，您需要将其转过来。

-我现在就做！ 用哪种语言更好？

- 哪个更方便？

我采访了一位C ++开发人员，但是为了描述列表中的算法，这不是最好的语言。 另外，我在某个地方读到，您在面试时首先需要提供一个无效的解决方案，然后依次进行改进，因此我打开了笔记本电脑，启动了vim和解释器，并草绘了以下代码：

revDumb : List a -> List a
revDumb [] = []
revDumb (x :: xs) = revDumb xs ++ [x]

, , , - , , :

revOnto : List a -> List a -> List a
revOnto acc [] = acc
revOnto acc (x :: xs) = revOnto (x :: acc) xs

revAcc : List a -> List a
revAcc = revOnto []

— , , , .

- , . , ( ?) - , :

— , , , , , , , .

revsEq : (xs : List a) -> revAcc xs = revDumb xs

, :

— , case split .

— generate definition, case split, obvious proof search —

revsEq : (xs : List a) -> revAcc xs = revDumb xs
revsEq [] = Refl
revsEq (x :: xs) = ?revsEq_rhs_1

, , , :

— , , , . , , , :

revsEq : (xs : List a) -> revAcc xs = revDumb xs
revsEq [] = Refl
revsEq (x :: xs) = let rec = revsEq xs in ?wut

— ?wut,

  rec : revOnto [] xs = revDumb xs
--------------------------------------
wut : revOnto [x] xs = revDumb xs ++ [x]

— revDumb xs , rec. :

revsEq (x :: xs) = let rec = revsEq xs in
                   rewrite sym rec in ?wut

--------------------------------------
wut : revOnto [x] xs = revOnto [] xs ++ [x]

— c :

lemma1 : (x0 : a) -> (xs : List a) -> revOnto [x0] xs = revOnto [] xs ++ [x0]

generate definition, case split xs, obvious proof search

lemma1 : (x0 : a) -> (xs : List a) -> revOnto [x0] xs = revOnto [] xs ++ [x0]
lemma1 x0 [] = Refl
lemma1 x0 (x :: xs) = ?lemma1_rhs_2

— , . lemma1 x xs, lemma1 x0 xs. , , ,

lemma1 x0 (x :: xs) = let rec = lemma1 x xs in ?wut

?wut:

  rec : revOnto [x] xs = revOnto [] xs ++ [x]
--------------------------------------
wut : revOnto [x, x0] xs = revOnto [x] xs ++ [x0]

— revOnto [x] xs rec. :

lemma1 x0 (x :: xs) = let rec = lemma1 x xs in
                      rewrite rec in ?wut

— , :

--------------------------------------
wut : revOnto [x, x0] xs = (revOnto [] xs ++ [x]) ++ [x0]

— , . :

lemma1 x0 (x :: xs) = let rec = lemma1 x xs in
                      rewrite rec in
                      rewrite sym $ appendAssociative (revOnto [] xs) [x] [x0] in ?wut

— -:

--------------------------------------
wut : revOnto [x, x0] xs = revOnto [] xs ++ [x, x0]

— ! , , , . , , :

lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc

IDE . case split lst, acc, revOnto lst:

lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
lemma2 acc [] = Refl
lemma2 acc (x :: xs) = ?wut1

wut1

--------------------------------------
wut1 : revOnto (x :: acc) xs = revOnto [x] xs ++ acc

:

lemma2 acc (x :: xs) = let rec = lemma2 (x :: acc) xs in ?wut1

  rec : revOnto (x :: acc) xs = revOnto [] xs ++ x :: acc
--------------------------------------
wut1 : revOnto (x :: acc) xs = revOnto [x] xs ++ acc

rec:

lemma2 acc (x :: xs) = let rec = lemma2 (x :: acc) xs in
                       rewrite rec in ?wut1

--------------------------------------
wut1 : revOnto [] xs ++ x :: acc = revOnto [x] xs ++ acc

— - . , lemma1 , , lemma2 , lemma1 x xs , lemma2 [x] xs:

lemma2 acc (x :: xs) = let rec1 = lemma2 (x :: acc) xs in
                       let rec2 = lemma2 [x] xs in
                       rewrite rec1 in
                       rewrite rec2 in ?wut1

:

--------------------------------------
wut1 : revOnto [] xs ++ x :: acc = (revOnto [] xs ++ [x]) ++ acc

, :

lemma2 : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
lemma2 acc [] = Refl
lemma2 acc (x :: xs) = let rec1 = lemma2 (x :: acc) xs in
                       let rec2 = lemma2 [x] xs in
                       rewrite rec1 in
                       rewrite rec2 in 
                       rewrite sym $ appendAssociative (revOnto [] xs) [x] acc in Refl

— , lemma1 , , lemma2 lemma. , , , :

lemma : (acc, lst : List a) -> revOnto acc lst = revOnto [] lst ++ acc
lemma acc [] = Refl
lemma acc (x :: xs) = let rec1 = lemma (x :: acc) xs in
                      let rec2 = lemma [x] xs in
                      rewrite rec1 in
                      rewrite rec2 in 
                      rewrite sym $ appendAssociative (revOnto [] xs) [x] acc in Refl

revsEq : (xs : List a) -> revAcc xs = revDumb xs
revsEq [] = Refl
revsEq (x :: xs) = let rec = revsEq xs in
                   rewrite sym rec in lemma [x] xs

15, - , .

— , , - .

— , , . ! , ? ?!

— ! , ! , , ? « »? : xs — , xs' «» , , . !

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs

— , revDumb revAcc ( forall xs. revDumb xs = revAcc xs, , , , ), , , revDumb.

,

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs
revCorrect [] f init = Refl
revCorrect (x :: xs) f init = let rec = revCorrect xs f init in ?wut

:

  rec : foldl f init (revDumb xs) = foldr (flip f) init xs
--------------------------------------
wut : foldl f init (revDumb xs ++ [x]) = f (foldr (flip f) init xs) x

— :

revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                              rewrite sym rec in ?wut

--------------------------------------
wut : foldl f init (revDumb xs ++ [x]) = f (foldl f init (revDumb xs)) x

— revDumb xs . : f f, . :

foldlRhs : (f : b -> a -> b) ->
           (init : b) ->
           (x : a) ->
           (xs : List a) ->
           foldl f init (xs ++ [x]) = f (foldl f init xs) x

— , . :

foldlRhs : (f : b -> a -> b) ->
           (init : b) ->
           (x : a) ->
           (xs : List a) ->
           foldl f init (xs ++ [x]) = f (foldl f init xs) x
foldlRhs f init x [] = Refl
foldlRhs f init x (y :: xs) = foldlRhs f (f init y) x xs

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs
revCorrect [] f init = Refl
revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                              rewrite sym rec in foldlRhs f init x (revDumb xs)

— - ?
— . , .
— … , , . , , , , .

, - .