Dôkaz indukciou a funkcie vyššieho rádu

Odporúčané zdroje

Potrebné knižnice

From Stdlib Require Import Arith.PeanoNat Lists.List Bool.Bool.
Import ListNotations.

Import poskytuje lemy o nat, zoznamy, boolovské operácie a zápis zoznamov [1; 2; 3]. Nasledujúce samostatné ukážky predpokladajú tieto importy.

Dôkazy

Dôkaz indukciou

Typ nat je induktívne definovaný dvoma konštruktormi. Príkaz Print nat. zobrazí jeho definíciu:

Print nat.

Skrátený výstup:

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

Každé prirodzené číslo je teda buď O (nula), alebo má tvar S n' pre menšie číslo n'. Dôkaz všeobecného tvrdenia sleduje práve tieto dva spôsoby konštrukcie čísla.

Formálne vyjadrenie indukcie

Nech P : nat -> Prop priraďuje každému prirodzenému číslu tvrdenie. Princíp indukcie možno zapísať ako implikáciu:

(P 0 ∧ (∀n : nat, P n → P (S n))) → ∀n : nat, P n

Ako odvodzovacie pravidlo vyzerá ten istý princíp takto; nad čiarou sú dve premisy, pod ňou záver:

P 0        ∀n : nat, P n → P (S n)
----------------------------------  (indukcia nad nat)
          ∀n : nat, P n

Prvá premisa je základný prípad. Druhá je indukčný krok: pre ľubovoľné n treba ukázať, že z P n vyplýva P (S n). Záver potom hovorí, že vlastnosť platí pre všetky prirodzené čísla.

Súvislosť s modus ponens

Pri indukcii používame aj pravidlo modus ponens: ak platí A a zároveň vieme, že z A vyplýva B, môžeme odvodiť B.

A       A → B
-------------  (modus ponens)
      B

Ak už máme základný prípad a všeobecný indukčný krok, môžeme ho špecializovať postupne na 0, S 0 a ďalšie konkrétne čísla. V každom z týchto jednotlivých prechodov použijeme modus ponens:

P 0       P 0 → P (S 0)
-----------------------  (modus ponens)
        P (S 0)

P (S 0)   P (S 0) → P (S (S 0))
--------------------------------  (modus ponens)
          P (S (S 0))

Tento reťazec názorne ukazuje, čo znamená indukčný krok pri konkrétnych číslach. Konečný počet použití modus ponens však dá iba konečný počet prípadov. Všeobecný záver ∀n, P n poskytuje indukčné pravidlo viazané na konštruktory O a S typu nat.

V samotnom dôkaze indukčného kroku predpokladáme IH : P n' pre ľubovoľné n' a dokazujeme P (S n'). Tento lokálny predpoklad sa nazýva indukčná hypotéza. Tvrdenie ∀n, P n → P (S n) je naopak celý indukčný krok, nie indukčná hypotéza. Ak v kroku máme implikáciu P n' → P (S n'), môžeme ju s IH použiť podľa modus ponens.

Pre vlastnosť P n := n + 0 = n dostávame konkrétnu podobu pravidla:

0 + 0 = 0       ∀n : nat, n + 0 = n → S n + 0 = S n
----------------------------------------------------  (indukcia nad nat)
                   ∀n : nat, n + 0 = n

V nasledovníkovej vetve je indukčná hypotéza IH : n' + 0 = n' a cieľ S n' + 0 = S n'. Podľa definície sčítania sa ľavá strana zjednoduší na S (n' + 0); použitím IH dostaneme S n'. Nižšie uvidíme presne tieto výrazy v dôkazovom stave Rocqu.

destruct a induction

destruct n rozdelí cieľ podľa konštruktorov na prípady O a S n'. V druhej vetve nedostaneme informáciu o platnosti skúmanej vlastnosti pre n'. induction n vytvorí rovnaké štrukturálne prípady, ale vo vetve S n' pridá indukčnú hypotézu. Preto sa destruct hodí na priamu analýzu prípadov, zatiaľ čo pri tvrdeniach o rekurzívnych definíciách často potrebujeme induction. Rovnaký rozdiel sa uplatňuje aj pri zoznamoch a iných induktívnych typoch.

Príklad: 0 + n a n + 0

Definícia Nat.add sa rozvetvuje podľa prvého argumentu: 0 + n sa zjednoduší priamo, ale pri premennej n sa n + 0 bez ďalších informácií nerozbalí.

Theorem plus_O_n' : forall n : nat, 0 + n = n.
Proof.
  intro n.
  (* n : nat
     ============================
     0 + n = n *)
  simpl.
  (* n : nat
     ============================
     n = n *)
  reflexivity.
Qed.

Po intro n je v komentári viditeľný cieľ 0 + n = n; simpl ho zmení na n = n, čo uzatvorí reflexivity. Pri obrátenom poradí argumentov potrebujeme indukciu:

Theorem plus_n_O : forall n : nat, n + 0 = n.
Proof.
  intro n.
  (* n : nat
     ============================
     n + 0 = n *)
  induction n as [| n' IH].
  (* 2 ciele:
     1. ============================
        0 + 0 = 0

     2. n' : nat
        IH : n' + 0 = n'
        ============================
        S n' + 0 = S n' *)
  - simpl. reflexivity.
  - (* n' : nat
       IH : n' + 0 = n'
       ============================
       S n' + 0 = S n' *)
    simpl.
    (* n' : nat
       IH : n' + 0 = n'
       ============================
       S (n' + 0) = S n' *)
    rewrite IH.
    (* n' : nat
       IH : n' + 0 = n'
       ============================
       S n' = S n' *)
    reflexivity.
Qed.

Komentáre sledujú stav po intro, rozdelenie na dva podciele po induction, zjednodušenie nasledovníkovej vetvy a jej prepísanie pomocou IH. V základnom prípade sa 0 + 0 vypočíta priamo.

Abstraktná podoba indukčného princípu

Check nat_ind.

Podstatná časť typu je:

nat_ind :
  forall P : nat -> Prop,
    P 0 ->
    (forall n : nat, P n -> P (S n)) ->
    forall n : nat, P n

nat_ind je eliminátor odvodený z definície nat: z dôkazu základného prípadu a funkcie realizujúcej indukčný krok zostaví dôkaz pre ľubovoľné n. Nasledujúca lema má ten istý obsah. Jej dôkaz pomocou induction ilustruje použitie indukčného princípu; nie je jeho nezávislým odvodením.

Lemma induction_principle :
  forall (P : nat -> Prop),
    P 0 ->
    (forall n, P n -> P (S n)) ->
    forall n, P n.
Proof.
  intros P H0 Hstep n.
  (* P : nat -> Prop
     H0 : P 0
     Hstep : forall n : nat, P n -> P (S n)
     n : nat
     ============================
     P n *)
  induction n as [| n' IH].
  - (* P : nat -> Prop
       H0 : P 0
       Hstep : forall n : nat, P n -> P (S n)
       ============================
       P 0 *)
    exact H0.
  - (* P : nat -> Prop
       H0 : P 0
       Hstep : forall n : nat, P n -> P (S n)
       n' : nat
       IH : P n'
       ============================
       P (S n') *)
    apply Hstep.
    (* P : nat -> Prop
       H0 : P 0
       Hstep : forall n : nat, P n -> P (S n)
       n' : nat
       IH : P n'
       ============================
       P n' *)
    exact IH.
Qed.

Po intros je v kontexte H0 : P 0 a Hstep : forall n, P n -> P (S n). V základnej vetve exact H0 uzatvorí cieľ P 0. Vo vetve nasledovníka je navyše IH : P n'; apply Hstep zmení cieľ P (S n') na P n', ktorý uzatvorí exact IH.

Taktika exact

exact H uzatvorí cieľ, ak má term H požadovaný typ. Komentár v dôkaze identity zachytáva stav po intros P H:

Theorem identity : forall P : Prop, P -> P.
Proof.
  intros P H.
  (* P : Prop
     H : P
     ============================
     P *)
  exact H.
Qed.

Term H je dôkazom presne toho tvrdenia, ktoré je cieľom. Po exact H neostáva ďalší podcieľ.

Taktika apply

Ak máme H2 : P -> Q a cieľ Q, apply H2 ponechá ako nový cieľ predpoklad P.

Theorem modus_ponens :
  forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
  intros P Q H1 H2.
  (* P, Q : Prop
     H1 : P
     H2 : P -> Q
     ============================
     Q *)
  apply H2.
  (* P, Q : Prop
     H1 : P
     H2 : P -> Q
     ============================
     P *)
  exact H1.
Qed.

Komentáre ukazujú, ako apply H2 zmení cieľ Q na P. exact H1 uzatvorí nový cieľ. Taktika apply tak rozloží použitie implikácie na potrebnú premisu.

Taktika rewrite

Ak H : a = b, potom rewrite H prepíše vhodný výskyt a na b v cieli. rewrite <- H postupuje opačným smerom. Rovnosť sa pritom spravidla použije na výskyt v aktuálnom cieli; neslúži ako príkaz na globálnu zmenu definície.

Nasledujúci príklad používa už dokázanú lemu plus_n_O:

Theorem rewrite_example : forall n : nat, n + 0 = n.
Proof.
  intro n.
  (* n : nat
     ============================
     n + 0 = n *)
  rewrite plus_n_O.
  (* n : nat
     ============================
     n = n *)
  reflexivity.
Qed.

Užitočnejšia je rovnosť vo vnútri väčšieho výrazu:

Theorem add_zero_inside :
  forall n : nat, (n + 0) + 1 = n + 1.
Proof.
  intro n.
  (* n : nat
     ============================
     n + 0 + 1 = n + 1 *)
  rewrite plus_n_O.
  (* n : nat
     ============================
     n + 1 = n + 1 *)
  reflexivity.
Qed.

Komentáre pri taktikách ukazujú premenu cieľa (n + 0) + 1 = n + 1 na n + 1 = n + 1. Keby sme chceli prepísať opačným smerom, zapísali by sme rewrite <- plus_n_O, no museli by sme dávať pozor na vhodný výskyt.

Výber výskytu pri komutativite

Check Nat.add_comm.

Lema má typ forall n m : nat, n + m = m + n. Pri všeobecnom rewrite Nat.add_comm môže Rocq zvoliť väčší podvýraz, než sme zamýšľali:

Theorem plus_rearrange_firsttry : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  (* n, m, p, q : nat
     ============================
     n + m + (p + q) = m + n + (p + q) *)
  rewrite Nat.add_comm.
  (* n, m, p, q : nat
     ============================
     p + q + (n + m) = m + n + (p + q) *)
Abort.

Komentár po taktike zachytáva stav v Rocqu 9.2: prepísal celý vonkajší súčet na ľavej strane. Argumenty lemy môžeme špecializovať explicitne:

Theorem plus_rearrange_direct : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  rewrite (Nat.add_comm n m).
  (* n, m, p, q : nat
     ============================
     m + n + (p + q) = m + n + (p + q) *)
  reflexivity.
Qed.

Taktika assert a lokálna lema

assert (H : T) zavedie pomenovaný medzivýsledok. Najprv treba dokázať T; potom možno H : T použiť v pôvodnom cieli. To sa hodí, keď medzivýsledok spresňuje ďalší postup alebo ho chceme použiť viackrát. Nie je to jediný spôsob cieleného prepísania.

Theorem mult_0_plus' : forall n m : nat,
  (n + 0 + 0) * m = n * m.
Proof.
  intros n m.
  assert (H : n + 0 + 0 = n).
  (* 2 ciele:
     1. n, m : nat
        ============================
        n + 0 + 0 = n

     2. n, m : nat
        H : n + 0 + 0 = n
        ============================
        (n + 0 + 0) * m = n * m *)
  { rewrite plus_n_O. rewrite plus_n_O. reflexivity. }
  (* n, m : nat
     H : n + 0 + 0 = n
     ============================
     (n + 0 + 0) * m = n * m *)
  rewrite H.
  (* n, m : nat
     H : n + 0 + 0 = n
     ============================
     n * m = n * m *)
  reflexivity.
Qed.

Komentár po assert zachytáva oba podciele. Zložené zátvorky { ... } ohraničujú dôkaz medzivýsledku. Po jeho uzavretí zostáva druhý cieľ; rewrite H v ňom zmení ľavý činiteľ na n.

Rovnaký postup môžeme použiť pri komutativite:

Theorem plus_rearrange : forall n m p q : nat,
  (n + m) + (p + q) = (m + n) + (p + q).
Proof.
  intros n m p q.
  assert (H : n + m = m + n).
  (* 2 ciele:
     1. n, m, p, q : nat
        ============================
        n + m = m + n

     2. n, m, p, q : nat
        H : n + m = m + n
        ============================
        n + m + (p + q) = m + n + (p + q) *)
  { apply Nat.add_comm. }
  rewrite H.
  (* n, m, p, q : nat
     H : n + m = m + n
     ============================
     m + n + (p + q) = m + n + (p + q) *)
  reflexivity.
Qed.

Po assert treba najskôr dokázať n + m = m + n. V druhom cieli je už H : n + m = m + n, takže rewrite H vyberie požadovaný vnútorný súčet. Pri jedinom použití je kratšie rewrite (Nat.add_comm n m).

rewrite s podmienenou rovnosťou

Lema môže mať tvar H : P -> a = b. Aby Rocq mohol použiť rovnosť, musí súčasne získať dôkaz premisy P. Taktika preto môže vytvoriť ďalší podcieľ:

Theorem conditional_rewrite :
  forall (P : Prop) (a b : nat),
    (P -> a = b) -> P -> a + 1 = b + 1.
Proof.
  intros P a b H HP.
  (* P : Prop
     a, b : nat
     H : P -> a = b
     HP : P
     ============================
     a + 1 = b + 1 *)
  rewrite H.
  (* 2 ciele:
     1. P : Prop
        a, b : nat
        H : P -> a = b
        HP : P
        ============================
        b + 1 = b + 1

     2. P : Prop
        a, b : nat
        H : P -> a = b
        HP : P
        ============================
        P *)
  - reflexivity.
  - exact HP.
Qed.

Komentár ukazuje nový cieľ P vytvorený po rewrite H; uzatvára ho exact HP. V úlohe plus_leb_compat_l má podobnú úlohu indukčná hypotéza: podmienené prepísanie môže vyžiadať dôkaz predpokladu o porovnaní.

Taktika replace

replace t1 with t2 nahradí vybraný výskyt t1 výrazom t2 a vytvorí povinnosť dokázať t2 = t1. Smer tejto pomocnej rovnosti treba pri použití lemy skontrolovať.

Theorem replace_example :
  forall n : nat, (n + 0) + 1 = n + 1.
Proof.
  intro n.
  (* n : nat
     ============================
     n + 0 + 1 = n + 1 *)
  replace (n + 0) with n.
  (* 2 ciele:
     1. n : nat
        ============================
        n + 1 = n + 1

     2. n : nat
        ============================
        n = n + 0 *)
  - reflexivity.
  - symmetry.
    (* n : nat
       ============================
       n + 0 = n *)
    apply plus_n_O.
Qed.

Komentár po replace zachytáva hlavný cieľ a pomocnú rovnosť. Taktika symmetry otočí cieľ a = b na b = a. Tu zmení n = n + 0 na n + 0 = n, čo je presne tvar lemy plus_n_O. Taktike symmetry sa podrobnejšie budeme venovať neskôr. Taktika replace je vhodná, keď chceme najskôr zvoliť tvar výrazu a rovnosť dokazovať oddelene.

Formálny a neformálny dôkaz

Neformálny dôkaz komunikuje matematickú myšlienku prirodzeným jazykom a môže vynechať rutinné medzikroky. Formálny dôkaz v Rocqu zostavuje dôkazový term. Jadro systému kontroluje, či má tento term typ zodpovedajúci formulovanému tvrdeniu vzhľadom na použité definície, axiómy a logický základ systému. Aj pri úspešnej kontrole však môžeme nesprávne formulovať špecifikáciu alebo dokazovať iné tvrdenie, než sme zamýšľali.

Pri dôkaze forall n, n + 0 = n možno neformálny indukčný krok zapísať takto. Predpokladajme IH : n' + 0 = n' a uvažujme prípad n = S n'. Potom:

S n' + 0
= S (n' + 0)    podľa definície sčítania
= S n'          podľa indukčnej hypotézy

Základný prípad 0 + 0 = 0 plynie priamo z definície sčítania. Formálny dôkaz je uvedený vyššie v leme plus_n_O: simpl realizuje prvú rovnosť a rewrite IH druhú. V dôkazovom stave je pritom viditeľný lokálny kontext, cieľ a po taktike prípadné nové podciele.

Funkcie vyššieho rádu

Funkcia vyššieho rádu prijíma funkciu ako argument alebo ju vracia ako výsledok. V Galline sú funkcie termy, preto ich možno odovzdávať ďalším funkciám. Príklad doit2times aplikuje funkciu typu X -> X dvakrát:

Definition doit2times {X : Type} (f : X -> X) (x : X) : X :=
  f (f x).

Check @doit2times.
Definition succ (n : nat) : nat := n + 1.
Compute doit2times succ 1.
Compute doit2times (fun x : nat => x + 1) 1.

Example test_doit2times : doit2times succ 1 = 3.
Proof. reflexivity. Qed.

Check @doit2times ukáže explicitný typový parameter X; oba výpočty vrátia 3. Zápis fun x : nat => x + 1 vytvorí anonymnú funkciu.

Štandardná knižnica poskytuje tieto funkcie. Ich vlastné definície nižšie slúžia na vysvetlenie rekurzívneho spracovania zoznamu a majú odlišné názvy, aby nekolidovali s knižnicou:

Check List.filter.
Check List.map.
Check List.fold_right.

filter

filter dostáva argumenty v tomto poradí: najprv test test : X -> bool, potom zoznam l : list X. Výsledkom je zoznam práve tých prvkov, pre ktoré test vráti true.

Fixpoint my_filter {X : Type} (test : X -> bool) (l : list X)
    : list X :=
  match l with
  | [] => []
  | head :: tail =>
      if test head then head :: my_filter test tail
      else my_filter test tail
  end.

Compute my_filter Nat.even [1; 2; 3; 4; 5; 6].

Výsledok je [2; 4; 6] : list nat. Nat.even : nat -> bool je výpočtový test párnosti; Nat.odd testuje nepárnosť. Test nie je tvrdením typu Prop, ale funkciou vracajúcou bool. Výpis Print Nat.even. ukazuje vetvy 0, S 0 a S (S n'); v poslednej vetve funkcia pokračuje na n'. Tento tvar využijeme pri dôkaze even_S.

map

map aplikuje f : X -> Y na každý prvok zoznamu typu list X a vytvorí list Y. Typ výsledného prvku sa teda môže od typu vstupného prvku líšiť.

Fixpoint my_map {X Y : Type} (f : X -> Y) (l : list X)
    : list Y :=
  match l with
  | [] => []
  | head :: tail => f head :: my_map f tail
  end.

Compute my_map (fun x => x + 5) [4; 0; 5; 6; 9].
Compute my_map Nat.odd [4; 0; 5; 6; 9].
Compute my_map (fun n => [Nat.even n; Nat.odd n]) [4; 0; 5; 6; 9].

Výsledky sú postupne [9; 5; 10; 11; 14], [false; false; true; false; true] a [[true; false]; [true; false]; [false; true]; [true; false]; [false; true]]. V posledných dvoch prípadoch sa typ prvku mení z nat na bool, respektíve list bool.

fold_right

Pravostranný fold prijíma kombinujúcu funkciu f : X -> Y -> Y, zoznam l : list X a počiatočnú hodnotu b : Y. V rekurzívnom prípade najprv spracuje chvost a potom použije f na hlavu a výsledok chvosta:

Fixpoint my_fold_right {X Y : Type}
    (f : X -> Y -> Y) (l : list X) (b : Y) : Y :=
  match l with
  | [] => b
  | h :: t => f h (my_fold_right f t b)
  end.

Preto výraz my_fold_right Nat.add [1; 2; 3; 4] 0 zodpovedá zátvorkovaniu 1 + (2 + (3 + (4 + 0))). b je výsledok pre prázdny zoznam; v pravostrannom folde sa vkladá na pravý koniec výrazu. Toto poradie sa líši od fold_left, ktorý poskytuje aj štandardná knižnica.

Compute my_fold_right Nat.add [1; 2; 3; 4] 0.
Compute my_fold_right andb [true; true; true; true] false.
Compute my_fold_right andb [true; true; true; true] true.
Compute my_fold_right andb [true; true; false; true] true.
Compute my_fold_right Nat.mul [1; 2; 3; 4] 1.
Compute my_fold_right Nat.mul [1; 2; 3; 4] 0.

Výsledky sú 10, false, true, false, 24 a 0. Pri andb je neutrálna hodnota true; počiatočné false spôsobí false aj vtedy, keď sú všetky prvky zoznamu pravdivé. Podobne má súčin neutrálnu hodnotu 1, nie 0.

Typy X a Y nemusia byť rovnaké. Pri nasledujúcom príklade je X = nat a Y = list bool:

Compute my_fold_right
  (fun n acc => Nat.even n :: acc)
  [1; 2; 3; 4]
  [].

Výsledok je [false; true; false; true]. Pri sčítaní dĺžok vnútorných zoznamov je X = list nat, Y = nat; pri ich zreťazení je X = list nat, Y = list nat:

Compute my_fold_right
  (fun l acc => length l + acc)
  [[1]; []; [2; 3; 2]; [4]]
  0.
Compute my_fold_right
  (fun l acc => l ++ acc)
  [[1]; [2; 3]; [4]]
  [].

Výsledky sú 5 a [1; 2; 3; 4]. Všeobecný typ my_fold_right je (X -> Y -> Y) -> list X -> Y -> Y s implicitnými parametrami X a Y. Knižničná List.fold_right má iné poradie posledných dvoch argumentov: List.fold_right f b l. Pri jej použití teda zapisujeme najprv počiatočnú hodnotu b a až potom zoznam l.

Boolovské testy a logické tvrdenia

bool je dátový typ s hodnotami true a false; boolovské testy možno vyhodnotiť pomocou Compute a použiť v if. Prop je univerzum logických tvrdení. Term typu P : Prop je dôkazom tvrdenia P, nie výsledkom boolovského testu.

Compute (3 <=? 5).
Check (3 <=? 5).
Check (3 <= 5).

Prvé dva príkazy vrátia true : bool, respektíve typ bool; tretí vypíše typ Prop. Samotné tvrdenie 3 <= 5 môže mať dôkaz, ale nie je boolovskou hodnotou true.

Ďalšie výpočtové operácie sú negb b, andb b1 b2 a orb b1 b2 (tiež zápisy b1 && b2 a b1 || b2). Logické spojky v Prop sú ~ P, P /\ Q, P \/ Q, P -> Q a P <-> Q. Nezamieňajme výpočtový výsledok n <=? m = true s tvrdením n <= m; súvis medzi nimi možno dokázať pomocou knižničných lém.

Compute (5 =? 3).
Compute (4 <? 4).
Compute (andb true false).
Compute (orb true false).
Compute (negb true).

Výsledky sú postupne false, false, false, true a false. Tieto rozdiely sa využívajú aj v úlohách s =?, <=?, Nat.even, andb a orb.

Samostatné úlohy

Základné indukčné dôkazy

Úlohy 3.1–3.7 využívajú rozbalenie rekurzívnej definície, základný prípad a indukčný krok. Pri komutativite sčítania môže pomôcť pomocná lema pre n + S m.

Theorem minus_n_n : forall n : nat,
  minus n n = 0.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem mul_0_r : forall n : nat,
  n * 0 = 0.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem mult_n_1 : forall n : nat,
  n * 1 = n.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + S m.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem add_comm : forall n m : nat,
  n + m = m + n.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem add_assoc : forall n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Fixpoint double (n : nat) : nat :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Lemma double_plus : forall n : nat,
  double n = n + n.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Kombinovanie lém a pokročilejšie dôkazy

Úlohy 3.8–3.10 vyžadujú kombinovanie indukcie s už dokázanými pomocnými tvrdeniami.

Theorem even_S : forall n : nat,
  Nat.even (S n) = negb (Nat.even n).
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem add_shuffle3 : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem mul_comm : forall m n : nat,
  m * n = n * m.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Boolovské funkcie a porovnania

Úlohy 3.11–3.17 pracujú s výsledkami typu bool. Rovnosti v ich formuláciách sú však tvrdenia typu Prop, ktoré treba dokázať.

Theorem plus_leb_compat_l : forall n m p : nat,
  (n <=? m) = true ->
  ((p + n) <=? (p + m)) = true.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem leb_refl : forall n : nat,
  (n <=? n) = true.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem zero_neqb_S : forall n : nat,
  (0 =? S n) = false.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem andb_false_r : forall b : bool,
  andb b false = false.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem S_neqb_0 : forall n : nat,
  (S n =? 0) = false.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem mult_1_l : forall n : nat,
  1 * n = n.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem all3_spec : forall b c : bool,
  orb (andb b c) (orb (negb b) (negb c)) = true.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Pokročilejšie algebraické dôkazy

Úlohy 3.18–3.20 nadväzujú na predchádzajúce lemy o sčítaní a násobení.

Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = n * p + m * p.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem mult_assoc : forall n m p : nat,
  n * (m * p) = (n * m) * p.
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Theorem add_shuffle3' : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
  (* Doplňte dôkaz. *)
Admitted.

Funkcie vyššieho rádu – dobrovoľné kontrolné úlohy

Nasledujúce krátke úlohy dopĺňajú dôkazové zadanie. Riešenia píšte pomocou knižničných funkcií; ich implementácie my_map, my_filter a my_fold_right vyššie slúžia na porozumenie ich správaniu.

Zhrnutie

Indukčný princíp nad nat vychádza z konštruktorov O a S. destruct vytvorí prípady podľa konštruktorov; induction navyše poskytne v rekurzívnej vetve indukčnú hypotézu. Pri dôkaze treba rozlišovať základný prípad, všeobecný indukčný krok a konkrétny predpoklad IH v lokálnom kontexte. Dôkazový stav ukazuje dostupné hypotézy a aktuálny cieľ.

Taktiky exact, apply, rewrite, assert a replace používajú dôkazy a rovnosti odlišným spôsobom; niektoré z nich vytvárajú nové podciele. Formálny dôkaz kontroluje Rocq vzhľadom na presne zapísané tvrdenie, kým neformálny dôkaz vyjadruje tú istú argumentáciu stručnejšie. Boolovské testy vracajú hodnoty typu bool; matematické tvrdenia patria do Prop. Funkcie vyššieho rádu filter, map a fold_right spracúvajú zoznamy pomocou funkčných argumentov, pričom fold_right skladá výsledok sprava.