Definiujemy typ

Inductive bintree : Set :=

  leaf : nat -> bintree

  | node : bintree -> bintree -> bintree.

"Obraz zwierciadlany” takiego drzewa otrzymujemy wymieniając lewe i prawe poddrzewa na każdym poziomie zagnieżdżenia (czyli rekursyjnie).

1. 1. Sformułuj to pojęcie indukcyjnym predykatem
   

Inductive is_mirror: bintree -> bintree -> Prop

2. 2. Skonstruuj metodą ekstrakcji program zwracający obraz zwierciadłowy argumentu (czyli sformułuj odpowiednie twierdzenie w Coq’u, przeprowadź dowód tego twierdzenia i zastosuj komendę Recursive Extraction (uwaga na konstrukcyjnść używanych typów!)).
   

3. 3. Zapisz rezultat  (commands Cd i Extraction odpowiednio sparametryzowane).
   

4. 4. Napisz program w Coq’u (Fixpoint) realizujący obraz zwierciadlany argumentu.
   

5. 5. Przeprowadź dowód jego poprawności.
   

6. 6. Wykonaj ekstracje tego programu i porównaj z rezultatem poprzedniej ekstrakcji. Co stwierdzasz? Czy potrafisz to sobie wytłumaczyć (kwalitatywnie)?