BC2f: Funkcje [TODO]


Require Import Arith.
Require Import Bool.
Require Import Equality.
Require Import FunctionalExtensionality.


W tym rozdziale zapoznamy się z najważniejszymi rodzajami funkcji. Trzeba przyznać na wstępie, że rozdział będzie raczej matematyczny (co wcale nie powinno cię odstraszać - matematyka jest świetna, a najbardziej praktyczną rzeczą w kosmosie jest dobra teoria).

Funkcje

Potrafisz już posługiwać się funkcjami. Mimo tego zróbmy krótkie przypomnienie.
Typ funkcji (niezależnych) z A w B oznaczamy przez A -> B. W Coqu funkcje możemy konstruować za pomocą abstrakcji (np. fun n : nat => n + n) albo za pomocą rekursji strukturalnej. Eliminować zaś możemy je za pomocą aplikacji: jeżeli f : A -> B oraz x : A, to f x : B.
Funkcje wyrażają ideę przyporządkowania: każdemu elementowi dziedziny funkcja przyporządkowuje element przeciwdziedziny. Jednak status dziedziny i przeciwdziedziny nie jest taki sam: każdemu elementowi dziedziny coś odpowiada, jednak mogą istnieć elementy przeciwdziedziny, które nie są obrazem żadnego elementu dziedziny.
Co więcej, w Coqu wszystkie funkcje są konstruktywne, tzn. mogą zostać obliczone. Jest to coś, co bardzo mocno odróżnia Coqa oraz rachunek konstrukcji (jego teoretyczną podstawę) od innych systemów formalnych.

Notation "f $ x" := (f x) (left associativity, at level 110, only parsing).
Notation "x |> f" := (f x) (right associativity, at level 60, only parsing).

Check plus (2 + 2) (3 + 3).
(* ===> 2 + 2 + (3 + 3) : nat *)

Check plus $ 2 + 2 $ 3 + 3.
(* ===> 2 + 2 + (3 + 3) : nat *)

Check (fun n : nat => n + n) 21.
(* ===> (fun n : nat => n + n) 21 : nat *)

Check 21 |> fun n : nat => n + n.
(* ===> (fun n : nat => n + n) 21 : nat *)

Najważniejszą rzeczą, jaką możemy zrobić z funkcją, jest zaaplikowanie jej do argumentu. Jest to tak częsta operacja, że zdefiniujemy sobie dwie notacje, które pozwolą nam zaoszczędzić kilka stuknięć w klawiaturę.
Notacja $ (pożyczona z języka Haskell) będzie nam służyć do niepisania nawiasów: jeżeli argumentami funkcji będą skomplikowane termy, zamiast pisać wokół nich parę nawiasów, będziemy mogli wstawić tylko jeden symbol dolara "$". Dzięki temu zamiast 2n nawiasów napiszemy tylko n znaków "$" (choć trzeba przyznać, że będziemy musieli pisać więcej spacji).
Notacja |> (pożyczona z języka F#) umożliwi nam pisanie aplikacji w odwrotnej kolejności. Dzięki temu będziemy mogli np. pomijać nawiasy w abstrakcji. Jako, że nie da się zrobić notacji w stylu "x f", jest to najlepsze dostępne nam rozwiązanie.

Definition comp
  {A B C : Type} (f : A -> B) (g : B -> C) : A -> C :=
    fun x : A => g (f x).

Notation "f .> g" := (comp f g) (left associativity, at level 40).

Drugą najważniejszą operacją, jaką możemy wykonywać na funkcjach, jest składanie. Jedynym warunkiem jest aby przeciwdziedzina pierwszej funkcji była taka sama, jak dziedzina drugiej funkcji.

Lemma comp_assoc :
  forall (A B C D : Type) (f : A -> B) (g : B -> C) (h : C -> D),
    (f .> g) .> h = f .> (g .> h).

Składanie funkcji jest łączne. Zagadka: czy jest przemienne?
Uwaga techniczna: jeżeli prezentuję jakieś twierdzenie bez dowodu, to znaczy, że dowód jest ćwiczeniem.

Definition id {A : Type} : A -> A := fun x : A => x.

Najważniejszą funkcją w całym kosmosie jest identyczność. Jest to funkcja, która nie robi zupełnie nic. Jej waga jest w tym, że jest ona elementem neutralnym składania funkcji.

Lemma id_left :
  forall (A B : Type) (f : A -> B), id .> f = f.

Lemma id_right :
  forall (A B : Type) (f : A -> B), f .> id = f.

Definition const {A B : Type} (b : B) : A -> B := fun _ => b.

Funkcja stała to funkcja, która ignoruje swój drugi argument i zawsze zwraca pierwszy argument.

Definition flip
  {A B C : Type} (f : A -> B -> C) : B -> A -> C :=
    fun (b : B) (a : A) => f a b.

flip to całkiem przydatny kombinator (funkcja wyższego rzędu), który zamienia miejscami argumenty funkcji dwuargumentowej.

Fixpoint iter {A : Type} (n : nat) (f : A -> A) : A -> A :=
match n with
| 0 => id
| S n' => f .> iter n' f
end.

Ostatnim przydatnim kombinatorem jest iter. Służy on do składania funkcji samej ze sobą n razy. Oczywiście funkcja, aby można ją było złożyć ze sobą, musi mieć identyczną dziedzinę i przeciwdziedzinę.

Aksjomat ekstensjonalności

Ważną kwestią jest ustalenie, kiedy dwie funkcje są równe. Zacznijmy od tego, że istnieją dwie koncepcje równości:

Print eq.
(* ===>
    Inductive eq (A : Type) (x : A) : A -> Prop :=
    | eq_refl : x = x
*)


Podstawowym i domyślnym rodzajem równości w Coqu jest równość intensjonalna, której właściwości już znasz. Każda funkcja, na mocy konstruktora eq_refl, jest równa samej sobie. Prawdą jest też mniej oczywisty fakt: każda funkcja jest równa swojej η-ekspansji.

Lemma eta_expansion :
  forall (A B : Type) (f : A -> B), f = fun x : A => f x.
Proof. reflexivity. Qed.

Print Assumptions eta_expansion.
(* ===> Closed under the global context *)

η-ekspansja funkcji f to nic innego, jak funkcja anonimowa, która bierze x i zwraca f x. Nazwa pochodzi od greckiej litery η (eta). Powyższe twierdzenie jest trywialne, gdyż równość zachodzi na mocy konwersji.
Warto podkreślić, że jego prawdziwość nie zależy od żadnych aksjomatów. Stwierdzenie to możemy zweryfikować za pomocą komendy Print Assumptions, która wyświetla listę aksjomatów, które zostały wykorzystane w definicji danego termu. Napis "Closed under the global context" oznacza, że żadnego aksjomatu nie użyto.

Lemma plus_1_eq :
  (fun n : nat => 1 + n) = (fun n : nat => n + 1).
Proof.
  trivial.
  Fail rewrite Nat.add_comm. (* No i co teraz? *)
Abort.

Równość intensjonalna ma jednak swoje wady. Główną z nich jest to, że jest ona bardzo restrykcyjna. Widać to dobrze na powyższym przykładzie: nie jesteśmy w stanie udowodnić, że funkcje fun n : nat => 1 + n oraz fun n : nat => n + 1 są równe, gdyż zostały zdefiniowane za pomocą innych termów. Mimo, że termy te są równe, to nie są konwertowalne, a zatem funkcje też nie są konwertowalne. Nie znaczy to jednak, że nie są równe — po prostu nie jesteśmy w stanie w żaden sposób pokazać, że są.

Require Import FunctionalExtensionality.

Check @functional_extensionality.
(* ===> @functional_extensionality
          : forall (A B : Type) (f g : A -> B),
              (forall x : A, f x = g x) -> f = g *)


Z tarapatów wybawić nas może jedynie aksjomat ekstensjonalności dla funkcji, zwany w Coqu functional_extensionality (dla funkcji, które nie są zależne) lub functional_extensionality_dep (dla funkcji zależnych).
Aksjomat ten głosi, że f i g są równe, jeżeli są równe dla wszystkich argumentów. Jest on bardzo użyteczny, a przy tym nie ma żadnych smutnych konsekwencji i jest kompatybilny z wieloma innymi aksjomatami. Z tych właśnie powodów jest on jednym z najczęściej używanych w Coqu aksjomatów. My też będziemy go wykorzystywać.

Lemma plus_1_eq :
  (fun n : nat => 1 + n) = (fun n : nat => n + 1).
Proof.
  extensionality n. rewrite Nat.add_comm. trivial.
Qed.

Sposób użycia aksjomatu jest banalnie prosty. Jeżeli mamy cel postaci f = g, to taktyka extensionality x przekształca go w cel postaci f x = g x, o ile tylko nazwa x nie jest już wykorzystana na coś innego.
Dzięki zastosowaniu aksjomatu nie musimy już polegać na konwertowalności termów definiujących funkcje. Wystarczy udowodnić, że są one równe. W tym przypadku robimy to za pomocą twierdzenia Nat.add_comm.

Ćwiczenie

Użyj aksjomatu ekstensjonalności, żeby pokazać, że dwie funkcje binarne są równe wtedy i tylko wtedy, gdy ich wartości dla wszystkich argumentów są równe.

Lemma binary_funext :
  forall (A B C : Type) (f g : A -> B -> C),
    f = g <-> forall (a : A) (b : B), f a b = g a b.

Odwrotności i izomorfizmy (TODO)

W tym podrozdziale zajmiemy się pojęciem funkcji odwrotnej i płynącą z niego mądrością.

Definition has_preinverse {A B : Type} (f : A -> B) : Type :=
  {g : B -> A | forall b : B, f (g b) = b}.

Definition has_postinverse {A B : Type} (f : A -> B) : Type :=
  {g : B -> A | forall a : A, g (f a) = a}.

Intuicja jest dość prosta: wiemy ze szkoły, że na liczbach całkowitych odejmowanie jest odwrotnością dodawania (np. a + b - b = a), tzn. jeżeli do a dodamy b, a potem odejmiemy b, to znowu mamy a. Podobnie w liczbach rzeczywistych mnożenie przez liczbę niezerową ma odwrotność w postaci dzielenia, np. (x * y) / y = x.
Oczywiście pojęcie odwrotności dotyczy nie tylko działań na liczbach, ale także dowolnych funkcji - g jest odwrotnością f, gdy odwraca ono działanie f dla dowolnego argumentu a, tzn. najpierw mamy a, potem aplikujemy f i mamy f a, zaś na koniec aplikujemy g i znów mamy a, czyli g (f a) = a. To właśnie jest napisane w definicji has_postinverse.
No właśnie - powyższy opis jest opisem postodwrotności. Nazwa wynika z kolejności - g jest postodwrotnością f, gdy najpierw aplikujemy f, a potem odwracamy jego działanie za pomocą g (po łacinie "post" znaczy "po", np. "post meridiem" znaczy "po południu").
Analogicznie, choć może nieco mniej intuicyjnie, prezentuje się definicja preodwrotności (po łacinie "prae" znaczy "przed"). g jest preodwrotnością f, gdy f jest postodwrotnością g. Innymi słowy: f ma preodwrotność, jeżeli odwraca ono działanie jakiejś funkcji.
Dobra, wystarczy gadania. Czas na ćwiczenia.

Ćwiczenie

Pokaż, że odjęcie n jest postodwrotnością dodania n. Czy jest także preodwrotnością?

Lemma plus_n_has_postinverse_sub_n :
  forall n : nat,
    has_postinverse (plus n).


Zauważ, że sortem has_preinverse i has_postinverse jest Type, nie zaś Prop. Jest tak dlatego, że o ile stwierdzenie "f jest pre/post odwrotnością g" jest zdaniem, to posiadanie odwrotności już nie, gdyż dana funkcja może mieć wiele różnych odwrotności.

Ćwiczenie

Rozważmy funkcję app [1; 2; 3], która dokleja na początek listy liczb naturalnych listę [1; 2; 3]. Znajdź dwie różne jej postodwrotności (nie musisz formalnie dowodzić, że są różne - wystarczy nieformalny argument). Czy funkcja ta ma preodwrotność?

From Typonomikon Require Export D5.


Ćwiczenie

Czasem funkcja może mieć naprawdę dużo odwrotności. Pokaż, że funkcja cons x dla x : A ma ich nieskończenie wiele. Nie musisz dowodzić, że odwrotności są różne (ani że jest ich dużo), jeżeli widać to na pierwszy rzut oka.


Ćwiczenie

Dla listowych funkcji widzieliśmy postodwrotności, ale nie widzieliśmy preodwrotności. Może więc preodwrotności nie istnieją? Otóż nie tym razem!
Dla jakich n funkcja cycle n ma (pre/post)odwrotność?

Definition uncycle {A : Type} (n : nat) (l : list A) : list A :=
  cycle (length l - n) l.

Lemma cycle_has_preinverse :
  forall (A : Type) (n : nat),
    has_preinverse (@cycle A n).
Proof.
  intros. red.
  exists (uncycle n).
  unfold uncycle, cycle.
Abort.

Definition isomorphism {A B : Type} (f : A -> B) : Type :=
  {g : B -> A | (forall a : A, g (f a) = a) /\
                (forall b : B, f (g b) = b)}.

Lemma iso_has_preinverse :
  forall {A B : Type} {f : A -> B},
    isomorphism f -> has_preinverse f.

Lemma iso_has_postinverse :
  forall {A B : Type} {f : A -> B},
    isomorphism f -> has_postinverse f.

Lemma both_inverses_isomorphism :
  forall {A B : Type} {f : A -> B},
    has_preinverse f -> has_postinverse f -> isomorphism f.

Skracalność (TODO)

Tutaj o lewej i prawej skracalności, czyli mono- i epi- morfizmy.

Definition precancellable {A B : Type} (f : A -> B) : Prop :=
  forall (X : Type) (g h : B -> X), f .> g = f .> h -> g = h.

Definition postcancellable {A B : Type} (f : A -> B) : Prop :=
  forall (X : Type) (g h : X -> A), g .> f = h .> f -> g = h.

Lemma has_preinverse_precancellable :
  forall {A B : Type} {f : A -> B},
    has_preinverse f -> precancellable f.

Lemma has_postinverse_postcancellable :
  forall {A B : Type} {f : A -> B},
    has_postinverse f -> postcancellable f.

Injekcje


Definition injective {A B : Type} (f : A -> B) : Prop :=
  forall x x' : A, f x = f x' -> x = x'.

Objaśnienia zacznijmy od nazwy. Po łacinie "iacere" znaczy "rzucać", zaś "in" znaczy "w, do". W językach romańskich samo słowo "injekcja" oznacza zaś zastrzyk. Bliższym matematycznemu znaczeniu byłoby jednak tłumaczenie "wstrzyknięcie". Jeżeli funkcja jest injekcją, to możemy też powiedzieć, że jest "injektywna". Inną nazwą jest "funkcja różnowartościowa". Na wiki można zapoznać się z obrazkami poglądowymi.
Podstawowa idea jest prosta: jeżeli funkcja jest injekcją, to identyczne jej wartości pochodzą od równych argumentów.
Przekonajmy się na przykładzie.

Goal injective (fun n : nat => 2 + n).
Proof.
  unfold injective; intros. destruct x, x'; cbn in *.
    trivial.
    inversion H.
    inversion H.
    inversion H. trivial.
Qed.

Funkcja fun n : nat => 2 + n, czyli dodanie 2 z lewej strony, jest injekcją, gdyż jeżeli 2 + n = 2 + n', to rozwiązując równanie dostajemy n = n'. Jeżeli wartości funkcji są równe, to argumenty również muszą być równe.
Zobaczmy też kontrprzykład.

Goal ~ injective (fun n : nat => n * n - n).
Proof.
  unfold injective, not; intros.
  specialize (H 0 1). cbn in H. specialize (H eq_refl). inversion H.
Qed.

Funkcja f(n) = n^2 - n nie jest injekcją, gdyż mamy zarówno f(0) = 0 jak i f(1) = 0. Innymi słowy: są dwa nierówne argumenty (0 i 1), dla których wartość funkcji jest taka sama (0).
A oto alternatywna definicja.

Definition injective' {A B : Type} (f : A -> B) : Prop :=
  forall x x' : A, x <> x' -> f x <> f x'.

Głosi ona, że funkcja injektywna to funkcja, która dla różnych argumentów przyjmuje różne wartości. Innymi słowy, injekcja to funkcja, która zachowuje relację <>. Przykład 1 możemy sparafrazować następująco: jeżeli n jest różn od n', to wtedy 2 + n jest różne od 2 + n'.
Definicja ta jest równoważna poprzedniej, ale tylko pod warunkiem, że przyjmiemy logikę klasyczną. W logice konstruktywnej pierwsza definicja jest lepsza od drugiej.

Ćwiczenie

Pokaż, że injective jest mocniejsze od injective'. Pokaż też, że w logice klasycznej są one równoważne.

Lemma injective_injective' :
  forall (A B : Type) (f : A -> B),
    injective f -> injective' f.

Lemma injective'_injective :
  (forall P : Prop, ~ ~ P -> P) ->
  forall (A B : Type) (f : A -> B),
    injective' f -> injective f.

Udowodnij, że różne funkcje są lub nie są injektywne.

Lemma id_injective :
  forall A : Type, injective (@id A).

Lemma S_injective : injective S.

Lemma const_unit_inj :
  forall (A : Type) (a : A),
    injective (fun _ : unit => a).

Lemma add_k_left_inj :
  forall k : nat, injective (fun n : nat => k + n).

Lemma mul_k_inj :
  forall k : nat, k <> 0 -> injective (fun n : nat => k * n).

Lemma const_2elem_not_inj :
  forall (A B : Type) (b : B),
    (exists a a' : A, a <> a') -> ~ injective (fun _ : A => b).

Lemma mul_k_0_not_inj :
  ~ injective (fun n : nat => 0 * n).

Lemma pred_not_injective : ~ injective pred.

Jedną z ważnych właściwości injekcji jest to, że są składalne: złożenie dwóch injekcji daje injekcję.

Lemma inj_comp :
  forall (A B C : Type) (f : A -> B) (g : B -> C),
    injective f -> injective g -> injective (f .> g).

Ta właściwość jest dziwna. Być może kiedyś wymyślę dla niej jakąś bajkę.

Lemma LOLWUT :
  forall (A B C : Type) (f : A -> B) (g : B -> C),
    injective (f .> g) -> injective f.

Na zakończenie należy dodać do naszej interpretacji pojęcia "injekcja" jeszcze jedną ideę. Mianowicie jeżeli istnieje injekcja f : A -> B, to ilość elementów typu A jest mniejsza lub równa liczbie elementów typu B, a więc typ A jest w pewien sposób mniejszy od B.
f musi przyporządkować każdemu elementowi A jakiś element B. Gdy elementów A jest więcej niż B, to z konieczności któryś z elementów B będzie obrazem dwóch lub więcej elementów A.
Wobec powyższego stwierdzenie "złożenie injekcji jest injekcją" możemy zinterpretować po prostu jako stwierdzenie, że relacja porządku, jaką jest istnienie injekcji, jest przechodnia. (TODO: to wymagałoby relacji jako prerekwizytu).

Ćwiczenie

Udowodnij, że nie istnieje injekcja z bool w unit. Znaczy to, że bool ma więcej elementów, czyli jest większy, niż unit.

Lemma no_inj_bool_unit :
  ~ exists f : bool -> unit, injective f.

Pokaż, że istnieje injekcja z typu pustego w każdy inny. Znaczy to, że Empty_set ma nie więcej elementów, niż każdy inny typ (co nie powinno nas dziwić, gdyż Empty_set nie ma żadnych elementów).

Lemma inj_Empty_set_A :
  forall A : Type, exists f : Empty_set -> A, injective f.

Surjekcje

Drugim ważnym rodzajem funkcji są surjekcje.

Definition surjective {A B : Type} (f : A -> B) : Prop :=
    forall b : B, exists a : A, f a = b.

I znów zacznijmy od nazwy. Po francusku "sur" znaczy "na", zaś słowo "iacere" już znamy (po łac. "rzucać"). Słowo "surjekcja" moglibyśmy więc przetłumaczyć jako "pokrycie". Tym bowiem w istocie jest surjekcja — jest to funkcja, która "pokrywa" całą swoją przeciwdziedzinę.
Owo "pokrywanie" w definicji wyraziliśmy w ten sposób: dla każdego elementu b przeciwdziedziny B istnieje taki element a dziedziny A, że f a = b.
Zobaczmy przykład i kontrprzykład.

Lemma pred_surjective : surjective pred.
Proof.
  unfold surjective; intros. exists (S b). cbn. trivial.
Qed.

Powyższe twierdzenie głosi, że "funkcja pred jest surjekcją", czyli, parafrazując, "każda liczba naturalna jest poprzednikiem innej liczby naturalnej". Nie powinno nas to zaskakiwać, wszakże każda liczba naturalna jest poprzednikiem swojego następnika, tzn. pred (S n) = n.

Lemma S_not_surjective : ~ surjective S.
Proof.
  unfold surjective; intro. destruct (H 0). inversion H0.
Qed.

Surjekcją nie jest za to konstruktor S. To również nie powinno nas dziwić: istnieje przecież liczba naturalna, która nie jest następnikiem żadnej innej. Jest nią oczywiście zero.
Surjekcje cieszą się właściwościami podobnymi do tych, jakie są udziałem injekcji.

Ćwiczenie

Pokaż, że złożenie surjekcji jest surjekcją. Udowodnij też "dziwną właściwość" surjekcji.

Lemma sur_comp :
  forall (A B C : Type) (f : A -> B) (g : B -> C),
    surjective f -> surjective g -> surjective (f .> g).

Lemma LOLWUT_sur :
  forall (A B C : Type) (f : A -> B) (g : B -> C),
    surjective (f .> g) -> surjective g.

Ćwiczenie

Zbadaj, czy wymienione funkcje są surjekcjami. Sformułuj i udowodnij odpowiednie twierdzenia.
Funkcje: identyczność, dodawanie (rozważ zero osobno), odejmowanie, mnożenie (rozważ 1 osobno).


Tak jak istnienie injekcji f : A -> B oznacza, że A jest mniejszy od B, gdyż ma mniej (lub tyle samo) elementów, tak istnieje surjekcji f : A -> B oznacza, że A jest większy niż B, gdyż ma więcej (lub tyle samo) elementów.
Jest tak na mocy samej definicji: każdy element przeciwdziedziny jest obrazem jakiegoś elementu dziedziny. Nie jest powiedziane, ile jest tych elementów, ale wiadomo, że co najmniej jeden.
Podobnie jak w przypadku injekcji, fakt że złożenie surjekcji jest surjekcją możemy traktować jako stwierdzenie, że porządek, jakim jest istnienie surjekcji, jest przechodni. (TODO)

Ćwiczenie

Pokaż, że nie istnieje surjekcja z unit w bool. Oznacza to, że unit nie jest większy niż bool.

Lemma no_sur_unit_bool :
  ~ exists f : unit -> bool, surjective f.

Pokaż, że istnieje surjekcja z każdego typu niepustego w unit. Oznacza to, że każdy typ niepusty ma co najmniej tyle samo elementów, co unit, tzn. każdy typ nie pusty ma co najmniej jeden element.

Lemma sur_A_unit :
  forall (A : Type) (nonempty : A), exists f : A -> unit, surjective f.

Bijekcje



Definition bijective {A B : Type} (f : A -> B) : Prop :=
  injective f /\ surjective f.

Po łacinie przedrostek "bi-" oznacza "dwa". Bijekcja to funkcja, która jest zarówno injekcją, jak i surjekcją.

Lemma id_bij : forall A : Type, bijective (@id A).
Proof.
  split; intros.
    apply id_injective.
    apply id_sur.
Qed.

Lemma S_not_bij : ~ bijective S.
Proof.
  unfold bijective; intro. destruct H.
  apply S_not_surjective. assumption.
Qed.

Pozostawię przykłady bez komentarza — są one po prostu konsekwencją tego, co już wiesz na temat injekcji i surjekcji.
Ponieważ bijekcja jest surjekcją, to każdy element jej przeciwdziedziny jest obrazem jakiegoś elementu jej dziedziny (obraz elementu x to po prostu f x). Ponieważ jest injekcją, to element ten jest unikalny.
Bijekcja jest więc taką funkcją, że każdy element jej przeciwdziedziny jest obrazem dokładnie jednego elementu jej dziedziny. Ten właśnie fakt wyraża poniższa definicja alternatywna.
TODO: exists! nie zostało dotychczas opisane, a chyba nie powinno być opisane tutaj.

Definition bijective' {A B : Type} (f : A -> B) : Prop :=
  forall b : B, exists! a : A, f a = b.

Ćwiczenie

Udowodnij, że obie definicje są równoważne.

Lemma bijective_bijective' :
  forall (A B : Type) (f : A -> B),
    bijective f <-> bijective' f.

Ćwiczenie


Fixpoint unary (n : nat) : list unit :=
match n with
| 0 => []
| S n' => tt :: unary n'
end.

Funkcja unary reprezentuje liczbę naturalną n za pomocą listy zawierającej n kopii termu tt. Udowodnij, że unary jest bijekcją.

Lemma unary_bij : bijective unary.

Jak już powiedzieliśmy, bijekcje dziedziczą właściwości, które mają zarówno injekcje, jak i surjekcje. Wobec tego możemy skonkludować, że złożenie bijekcji jest bijekcją. Nie mają one jednak "dziwnej własciwości".
TODO UWAGA: od teraz twierdzenia, które pozostawię bez dowodu, z automatu stają się ćwiczeniami.

Lemma bij_comp :
  forall (A B C : Type) (f : A -> B) (g : B -> C),
    bijective f -> bijective g -> bijective (f .> g).

Bijekcje mają też interpretacje w idei rozmiaru oraz ilości elementów. Jeżeli istnieje bijekcja f : A -> B, to znaczy, że typy A oraz B mają dokładnie tyle samo elementów, czyli są "tak samo duże".
Nie powinno nas zatem dziwić, że relacja istnienia bijekcji jest relacją równoważności:

Ćwiczenie

Jeżeli między A i B istnieje bijekcja, to mówimy, że A i B są równoliczne (ang. equipotent). Pokaż, że relacja równoliczności jest relacją równoważności. TODO: prerekwizyt: relacje równoważności

Definition equipotent (A B : Type) : Prop :=
  exists f : A -> B, bijective f.

Notation "A ~~ B" := (equipotent A B) (at level 10).

Równoliczność A i B będziemy oznaczać przez A ~ B. Nie należy notacji ~ mylić z notacją ~ oznaczającej negację logiczną. Ciężko jednak jest je pomylić, gdyż pierwsza zawsze bierze dwa argumenty, a druga tylko jeden.

Lemma equipotent_refl :
  forall A : Type, A ~~ A.

Lemma equipotent_sym :
  forall A B : Type, A ~~ B -> B ~~ A.

Lemma equipotent_trans :
  forall A B C : Type, A ~~ B -> B ~~ C -> A ~~ C.

Inwolucje


Definition involutive {A : Type} (f : A -> A) : Prop :=
  forall x : A, f (f x) = x.

Kolejnym ważnym (choć nie aż tak ważnym) rodzajem funkcji są inwolucje. Po łacinie "volvere" znaczy "obracać się". Inwolucja to funkcja, która niczym Chuck Norris wykonuje półobrót — w tym sensie, że zaaplikowanie jej dwukrotnie daje cały obrót, a więc stan wyjściowy.
Mówiąc bardziej po ludzku, inwolucja to funkcja, która jest swoją własną odwrotnością. Spotkaliśmy się już z przykładami inwolucji: najbardziej trywialnym z nich jest funkcja identycznościowa, bardziej oświecającym zaś funkcja rev, która odwraca listę — odwrócenie listy dwukrotnie daje wyjściową listę. Inwolucją jest też negb.

Lemma id_inv :
  forall A : Type, involutive (@id A).

Lemma rev_rev :
  forall A : Type, involutive (@rev A).

Lemma negb_inv : involutive negb.

Żeby nie odgrzewać starych kotletów, przyjrzyjmy się funkcji weird.

Fixpoint weird {A : Type} (l : list A) : list A :=
match l with
| [] => []
| [x] => [x]
| x :: y :: t => y :: x :: weird t
end.

Lemma weird_inv :
  forall A : Type, involutive (@weird A).

Funkcja ta zamienia miejscami bloki elementów listy o długości dwa. Nietrudno zauważyć, że dwukrotne takie przestawienie jest identycznością. UWAGA TODO: dowód wymaga specjalnej reguły indukcyjnej.

Lemma flip_inv :
  forall A : Type, involutive (@flip A A A).

Inwolucją jest też kombinator flip, który poznaliśmy na początku rozdziału. Przypomnijmy, że zamienia on miejscami argumenty funkcji binarnej. Nie dziwota, że dwukrotna taka zamiana daje oryginalną funkcję.

Goal ~ involutive (@rev nat .> weird).

Okazuje się, że złożenie inwolucji wcale nie musi być inwolucją. Wynika to z faktu, że funcje weird i rev są w pewien sposób niekompatybilne — pierwsze wywołanie każdej z nich przeszkadza drugiemu wywołaniu drugiej z nich odwrócić efekt pierwszego wywołania.

Lemma comp_inv :
  forall (A : Type) (f g : A -> A),
    involutive f -> involutive g -> f .> g = g .> f -> involutive (f .> g).

Kryterium to jest rozstrzygające — jeżeli inwolucje komutują ze sobą (czyli są "kompatybilne", f .> g = g .> f), to ich złożenie również jest inwolucją.

Lemma inv_bij :
  forall (A : Type) (f : A -> A), involutive f -> bijective f.

Ponieważ każda inwolucja ma odwrotność (którą jest ona sama), każda inwolucja jest z automatu bijekcją.


Ćwiczenie

Rozważmy funkcje rzeczywiste f(x) = ax^n, f(x) = ax^(-n), f(x) = sin(x), f(x) = cos(x), f(x) = a/x, f(x) = a - x, f(x) = e^x. Które z nich są inwolucjami?

Uogólnione inwolucje

Pojęcie inwolucji można nieco uogólnić. Żeby to zrobić, przeformułujmy najpierw definicję inwolucji.

Definition involutive' {A : Type} (f : A -> A) : Prop :=
  f .> f = id.

Nowa definicja głosi, że inwolucja to taka funkcja, że jej złożenie ze sobą jest identycznością. Jeżeli funkcje f .> f i id A zaaplikujemy do argumentu x, otrzymamy oryginalną definicję. Nowa definicja jest równoważna starej na mocy aksjomatu ekstensjonalności dla funkcji.

Lemma involutive_involutive' :
  forall (A : Type) (f : A -> A), involutive f <-> involutive' f.

Pójdźmy o krok dalej. Zamiast składania .> użyjmy kombinatora iter 2, który ma taki sam efekt.

Definition involutive'' {A : Type} (f : A -> A) : Prop :=
  iter f 2 = id.

Lemma involutive'_involutive'' :
  forall (A : Type) (f : A -> A),
    involutive' f <-> involutive'' f.

Droga do uogólnienia została już prawie przebyta. Nasze dotychczasowe inwolucje nazwiemy uogólnionymi inwolucjami rzędu 2. Definicję uogólnionej inwolucji otrzymamy, zastępując w definicji 2 przez n.

Definition gen_involutive
  {A : Type} (n : nat) (f : A -> A) : Prop :=
    iter f n = id.

Nie żeby pojęcie to było jakoś szczególnie często spotykane lub nawet przydatne — wymyśliłem je na poczekaniu. Spróbujmy znaleźć jakąś uogólnioną inwolucję o rzędzie większym niż 2.

Fixpoint weirder {A : Type} (l : list A) : list A :=
match l with
| [] => []
| [x] => [x]
| [x; y] => [x; y]
| x :: y :: z :: t => y :: z :: x :: weirder t
end.

Compute weirder [1; 2; 3; 4; 5].
(* ===> = 2; 3; 1; 4; 5 : list nat *)

Compute iter weirder 3 [1; 2; 3; 4; 5].
(* ===> = 1; 2; 3; 4; 5 : list nat *)

Lemma weirder_inv_3 :
  forall A : Type, gen_involutive 3 (@weirder A).

Idempotencja


Definition idempotent {A : Type} (f : A -> A) : Prop :=
  forall x : A, f (f x) = f x.

Kolejnym rodzajem funkcji są funkcje idempotente. Po łacinie "idem" znaczy "taki sam", zaś "potentia" oznacza "moc". Funkcja idempotentna to taka, której wynik jest taki sam niezależnie od tego, ile razy zostanie zaaplikowana.
Przykłady można mnożyć. Idempotentne jest wciśnięcie guzika w windzie — jeżeli np. wciśniemy "2", to po wjechaniu na drugi piętro kolejne wciśnięcia guzika "2" nie będą miały żadnego efektu.
Idempotentne jest również sortowanie. Jeżeli posortujemy listę, to jest ona posortowana i kolejne sortowania niczego w niej nie zmienią. Problemem sortowania zajmiemy się w przyszłych rozdziałach.

Lemma id_idem :
  forall A : Type, idempotent (@id A).

Lemma const_idem :
  forall (A B : Type) (b : B), idempotent (const b).

Lemma take_idem :
  forall (A : Type) (n : nat), idempotent (@take A n).

Identyczność jest idempotentna — niezrobienie niczego dowolną ilość razy jest wszakże ciągle niezrobieniem niczego. Podobnież funkcja stała jest idempotentna — zwracanie tej samej wartości daje zawsze ten sam efekt, niezależnie od ilości powtórzeń.
Ciekawszym przykładem, który jednak nie powinien cię zaskoczyć, jest funkcja take dla dowolnego n : nat. Wzięcie n elementów z listy l daje nam listę mającą co najwyżej n elementów. Próba wzięcia n elementów z takiej listy niczego nie zmieni, gdyż jej długość jest mniejsza lub równa ilości elementów, które chcemy wziąć.

Lemma comp_idem :
  forall (A : Type) (f g : A -> A),
    idempotent f -> idempotent g -> f .> g = g .> f ->
      idempotent (f .> g).

Jeżeli chodzi o składanie funkcji idempotentnych, sytuacja jest podobna do tej, jaka jest udziałem inwolucji.