Oi Habr.

Outro dia, fui a uma entrevista em uma empresa séria e lá eles me ofereceram para entregar uma lista simplesmente conectada. Infelizmente, essa tarefa levou toda a primeira rodada da entrevista e, no final da entrevista, o entrevistador disse que todo mundo estava doente hoje e, portanto, posso ir para casa. No entanto, todo o processo de solução desse problema, incluindo algumas opções para o algoritmo e sua subsequente discussão, bem como discussões sobre o que é a inversão da lista, estão abaixo do gato.

Resolvemos o problema

O entrevistador foi bastante simpático e amigável:

- Bem, primeiro vamos resolver esse problema: uma lista simplesmente conectada é fornecida, você precisa mudar isso.

- Eu vou fazer isso agora! E em que idioma é melhor fazer isso?

- Qual é o mais conveniente para você?

Eu entrevistei um desenvolvedor de C ++, mas para descrever os algoritmos nas listas, essa não é a melhor linguagem. Além disso, li em algum lugar que, nas entrevistas, você primeiro precisa oferecer uma solução ineficaz e, em seguida, melhorá-la sequencialmente. Abri o laptop, iniciei o vim e o intérprete e desenhei esse código:

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)

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

, - .