BeiZero

В этой статье решаю задачу основанную на меме от Max Howell(создатель Homebrew), которого на собеседовании в Google заставляли инвертировать бинарное дерево, но он почему-то не смог

Google: 90% of our engineers use the software you wrote (Homebrew), but you can’t invert a binary tree on a whiteboard so fuck off.

Max Howell не смог, но я верю, что вы сможете! Рекомендую решать самостоятельно.

#agda #codewars

Хочется сказать, что функция инвертирования в задаче уже реализована и на самом деле мы будем доказывать, что дважды инвертированное дерево равно исходному дереву.

Импорты и определение модуля:

{-# OPTIONS --safe #-}
module Codewars.GoogleInterview where

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

Определение бинарного дерева:

data Tree (A : Set) : Set where
    leaf : A → Tree A
    branch : A → Tree A → Tree A → Tree A

Инвертирование дерева:

flipTree : {A : Set} → Tree A → Tree A
flipTree (leaf x) = leaf x
flipTree (branch x l r) = branch x (flipTree r) (flipTree l)

Доказывать будем по индукции, сначала рассмотрим случай листового узла, а потом случай ветви

flipTreeSym : {A : Set} → (t : Tree A) → t ≡ flipTree (flipTree t)
-- в случае листового узла равенство по определению
flipTreeSym (leaf a) = refl
flipTreeSym (branch x l r) = 
    -- доказывать будет удобнее показывая, что flipTree (flipTree t) ≡ t, а не наоборот, используем sym
    sym (
        -- применим flipTree к ветви
        flipTree (flipTree(branch x l r)) ≡⟨⟩
        -- и еще раз
        flipTree (branch x (flipTree r) (flipTree l)) ≡⟨⟩
        -- теперь можем применить предположение индукции к левому поддереву
        branch x (flipTree(flipTree l)) (flipTree(flipTree r)) ≡⟨ 
            cong (λ a → branch x a (flipTree(flipTree r))) (sym(flipTreeSym l)) 
        ⟩ 
        -- а теперь к правому
        branch x l (flipTree(flipTree r)) ≡⟨ 
            cong (λ a → branch x l a) (sym(flipTreeSym r)) 
        ⟩ 
        -- ч.т.д.
        branch x l r ∎
    )