Ďalšie taktiky

Obsah

Kapitola nadväzuje na dokazovanie vlastností prirodzených čísel a zoznamov. Rozšírime súbor taktík a ukážeme, ako pri ich výbere vychádzať z tvaru cieľa a dostupných hypotéz. Osobitnú pozornosť venujeme zachovaniu informácií pri rozbore výrazov a príprave indukčného predpokladu, ktorý možno použiť v rekurzívnom kroku.

• apply, symmetry, transitivity
• injection, discriminate, contradiction
• Práca s kontextom: simpl in, apply ... in, specialize
• unfold, subst, remember, generalize dependent
• f_equal, admit, assumption, try, repeat, operátor ;

Potrebné knižnice

Príklady v blokoch rocq možno vykonať postupne v jednom súbore; schematické zápisy sú označené ako text. Príklad admit_example je zámerne nedokončený.

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

Ďalšie taktiky

Taktika apply

Taktika apply porovná cieľ so záverom použitého tvrdenia a pokúsi sa odvodiť jeho argumenty. Z predpokladov, ktoré ešte treba dokázať, vytvorí nové podciele. Ak dostupná hypotéza priamo dokazuje cieľ, apply ho uzavrie, ako v nasledujúcom príklade.

Theorem apply_ex1 : forall (n m : nat),
  n = m -> n = m.
Proof.
  intros n m eq.
  (* eq : n = m
     ============================
     n = m *)

  apply eq.
Qed.

Taktika symmetry

Niekedy potrebujeme využiť predpoklad rovnosti, ale jeho strany sú obrátené oproti cieľovej rovnosti.

Taktika symmetry transformuje cieľ x = y na ekvivalentný cieľ y = x. Tým umožní priamu aplikáciu dostupného predpokladu alebo vety.

Theorem apply_ex2 : forall (n m : nat),
  m = n -> n = m.
Proof.
  intros n m eq. (* apply eq zlyháva *)
  (* eq : m = n
     ============================
     n = m *)

  symmetry.
  (* ============================
     Otočíme smer rovnosti v cieli

     eq : m = n
     ============================
     m = n *)

  apply eq.
Qed.

Tranzitívnosť a apply ... with

Tranzitívnosť rovnosti

Z rovností x = y a y = z vyplýva x = z. Najprv tento krok vykonáme dvoma prepísaniami pomocou rewrite.

Example transitivity_eq_example : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros.
  (* H : [a; b] = [c; d]
     H0 : [c; d] = [e; f]
     ============================
     [a; b] = [e; f] *)

  rewrite H.
  (* ============================
     [c; d] = [e; f] *)

  rewrite H0.
  (* ============================
     [e; f] = [e; f] *)

  reflexivity.
Qed.

Všeobecná veta o tranzitívnosti

Theorem transitivity_eq : forall {X:Type} (x y z : X),
  x = y -> y = z -> x = z.
Proof.
  intros X x y z eq1 eq2. rewrite eq1. rewrite eq2.
  reflexivity.
Qed.

Použitie vlastnej vety s apply ... with

Pri aplikácii transitivity_eq na cieľ [a; b] = [e; f] možno určiť x a z, ale medzičlánok y sa v závere vety nevyskytuje. Preto ho zadáme explicitne pomocou with (y := [c; d]). Predpoklady vety sa stanú dvoma podcieľmi.

Example transitivity_eq_example' : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros.
  (* H : [a; b] = [c; d]
     H0 : [c; d] = [e; f]
     ============================
     [a; b] = [e; f] *)

  apply transitivity_eq with (y:=[c;d]).
  - (* ============================
       Prvý podcieľ: prvá rovnosť x = y
       ...
       ============================
       [a; b] = [c; d] *)
    apply H.

  - (* ============================
       Druhý podcieľ: druhá rovnosť y = z
       ...
       ============================
       [c; d] = [e; f] *)
    apply H0.
Qed.

Ekvivalentný dôkaz pomocou taktiky transitivity

Taktika transitivity t vytvorí z cieľa x = z podciele x = t a t = z. V tomto príklade teda dosiahneme rovnaké rozdelenie ako aplikáciou vlastnej vety.

Example transitivity_eq_example'' : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros.
  transitivity [c;d].
  (* ============================
     Taktika transitivity automaticky vytvorí dva podciele:
     1. [a; b] = [c; d]
     2. [c; d] = [e; f] *)

  - apply H.
  - apply H0.
Qed.

Injektívnosť a disjunktnosť konštruktorov

Pripomeňme si tvar knižničnej definície prirodzených čísel; v spoločnom súbore ju znova nedeklarujeme:

Inductive nat : Type :=
  | O
  | S (n : nat).

Z tejto definície vyplýva, že každý prvok je buď O, alebo má tvar S n. Okrem toho platí:

• S je injektívny konštruktor: ak S n = S m, tak n = m
• Konštruktory O a S sú disjunktné: O <> S n pre každé n

Podobne pri iných induktívnych typoch:

• pri zoznamoch je cons injektívny a nil je odlišný od každého neprázdneho zoznamu
• pri bool sú true a false rôzne

Taktika injection

Najprv dokážeme injektívnosť konštruktora S pomocou funkcie pred, ktorá zo S n vypočíta n.

Theorem S_injective : forall (n m : nat),
  S n = S m ->
  n = m.
Proof.
  intros n m H.
  assert (H2 : n = pred (S n)) by reflexivity.
  rewrite H2. rewrite H. simpl. reflexivity.
Qed.

Taktika injection využije injektívnosť konštruktorov v rovnosti v hypotéze. Z H : S n = S m získame n = m. Odlišnú úlohu má neskoršia taktika f_equal: cieľ S n = S m zredukuje na dokazovanie n = m.

Theorem S_injective' : forall (n m : nat),
  S n = S m ->
  n = m.
Proof.
  intros n m H.
  (* H : S n = S m
     ============================
     n = m *)

  injection H as Hnm.
  (* ============================
     Použijeme injektívnosť S: zo S n = S m vyplýva n = m.

     Hnm : n = m
     ============================
     n = m *)

  apply Hnm.
Qed.

Theorem injection_ex1 : forall (n m o : nat),
  [n;m] = [o;o] ->
  n = m.
Proof.
  intros n m o H.
  (* H : [n; m] = [o; o]
     ============================
     n = m *)

  injection H as H1 H2.
  (* ============================
     Injektívnosť cons použijeme aj na vnorené konštruktory.
     Získame rovnosti zodpovedajúcich prvkov:

     H1 : n = o
     H2 : m = o
     ============================
     n = m *)

  rewrite H1. rewrite H2. reflexivity.
Qed.

Taktika discriminate

Hodnoty vytvorené rôznymi konštruktormi toho istého induktívneho typu sa nemôžu rovnať. Preto sú rovnosti O = S n a true = false nemožné.

Taktika discriminate H využije takúto nemožnú rovnosť v hypotéze H a uzavrie aktuálny cieľ. Z nemožného predpokladu môžeme odvodiť ľubovoľné tvrdenie.

Príklad so sporným predpokladom false = true:

Theorem discriminate_ex1 : forall (n m : nat),
  false = true ->
  n = m.
Proof.
  intros n m contra.
  (* ============================
     false a true sú rôzne konštruktory → spor

     contra : false = true
     ============================
     n = m *)

  discriminate contra.
Qed.

Príklad: protirečenie S n = 0.

Theorem discriminate_ex2 : forall (n : nat),
  S n = O ->
  2 + 2 = 5.
Proof.
  intros n contra.
  (* ============================
     S n a O sú rôzne konštruktory → zo sporu vyplýva čokoľvek

     contra : S n = O
     ============================
     2 + 2 = 5 *)

  discriminate contra.
Qed.

Taktika contradiction

Taktika contradiction uzavrie cieľ, ak v kontexte rozpozná logický spor, napríklad HP : P spolu s HnP : ~P, alebo priamo Hfalse : False. Nie je všeobecným postupom na automatické odvodenie ľubovoľného zložitého sporu.

Príklad s tvrdením a jeho negáciou:

Theorem contradiction_ex1 : forall (P Q : Prop),
  P -> ~P -> Q.
Proof.
  intros P Q HP HnP.
  (* ============================
     Máme P aj ~P → spor

     HP : P
     HnP : ~P  (teda P -> False)
     ============================
     Q *)

  contradiction.
Qed.

Nasledujúci príklad má síce v názve contradiction, ale používa discriminate, pretože predpokladom je nemožná rovnosť konštruktorov:

Theorem contradiction_ex2 : forall (n : nat),
  S n = O -> 3 = 4.
Proof.
  intros n H.
  discriminate.
Qed.

Niekedy treba nemožnú rovnosť najprv pripraviť. Po prepísaní H2 pomocou H1 dostaneme true = false, na čo použijeme discriminate:

Theorem contradiction_ex3 : forall b : bool,
  b = true -> b = false -> 0 = 1.
Proof.
  intros b H1 H2.
  rewrite H1 in H2.
  discriminate H2.
Qed.

Oba postupy využívajú princíp ex falso quodlibet: z False možno odvodiť ľubovoľné tvrdenie. Rozdiel spočíva v tom, z akých hypotéz spor získame.

Použitie taktík na hypotézy

Postup od hypotéz a postup od cieľa

Pri dokazovaní môžeme vychádzať z cieľa alebo odvodzovať dôsledky dostupných hypotéz. Viaceré taktiky majú varianty pre obe situácie.

• simpl in H zjednoduší hypotézu H v kontexte.
• apply L in H použije implikáciu L : X -> Y na hypotézu H : X a nahradí ju za Y. To je tzv. forward reasoning.

Naopak apply L je backward reasoning: ak chceme dokázať Y, stačí dokázať X.

Príklad s simpl in H.

Theorem S_inj : forall (n m : nat) (b : bool),
  ((S n) =? (S m)) = b ->
  (n =? m) = b.
Proof.
  intros n m b H.
  simpl in H.
  (* H : (n =? m) = b
     ============================
     (n =? m) = b *)
  apply H.
Qed.

Pri apply ... in postupujeme od hypotézy k jej dôsledku:

Theorem silly4 : forall (n m p q : nat),
  (n = m -> p = q) -> m = n -> q = p.
Proof.
  intros n m p q EQ H.
  symmetry in H.
  (* H : n = m *)
  apply EQ in H.
  (* H : p = q *)
  symmetry in H.
  apply H.
Qed.

Taktika specialize

Taktika specialize umožňuje konkretizovať príliš všeobecnú hypotézu dosadením konkrétnej hodnoty do jej kvantifikátora.

Ak máme H : forall x : T, P x, potom specialize H with (x := e) nahradí lokálnu hypotézu H hypotézou H : P e. Výraz e musí mať typ T.

V nasledujúcom príklade všeobecný predpoklad platí aj pre m = 1. Po tomto dosadení môžeme využiť rovnosť 1 * n = n.

Search (1 * _).
(* Nájdenie pomocnej vety PeanoNat.Nat.mul_1_l:
PeanoNat.Nat.mul_1_l: forall n : nat, 1 * n = n *)

Príklad: dosadíme m := 1.

Theorem specialize_example: forall n,
     (forall m, m * n = 0) ->
     n = 0.
Proof.
  intros n H.
  (* n : nat
     H : forall m : nat, m * n = 0
     ============================
     n = 0 *)

  specialize H with (m := 1).
  (* n : nat
     H : 1 * n = 0
     ============================
     n = 0 *)

  rewrite PeanoNat.Nat.mul_1_l in H.
  apply H.
Qed.

Špecializácia globálnej vety

Pomocná veta.

Theorem trans_eq :
  forall (X:Type) (x y z : X), x = y -> y = z -> x = z.
Proof.
  intros X x y z eq1 eq2.
  rewrite -> eq1. rewrite -> eq2. reflexivity.
Qed.

Príkaz specialize trans_eq with (y := [c; d]) as H vytvorí novú lokálnu hypotézu H so zvoleným medzičlánkom. Globálna veta trans_eq zostáva nezmenená; na rozdiel od predchádzajúceho príkladu teda nenahrádzame existujúcu lokálnu hypotézu.

Example trans_eq_example''' : forall (a b c d e f : nat),
     [a;b] = [c;d] ->
     [c;d] = [e;f] ->
     [a;b] = [e;f].
Proof.
  intros a b c d e f eq1 eq2.
  (* eq1 : [a; b] = [c; d]
     eq2 : [c; d] = [e; f]
     ============================
     [a; b] = [e; f] *)

  specialize trans_eq with (y := [c;d]) as H.
  (* eq1 : [a; b] = [c; d]
     eq2 : [c; d] = [e; f]
     H :
      forall x z : list nat,
      x = [c; d] -> [c; d] = z -> x = z
     ============================
     [a; b] = [e; f] *)

  apply H.
  - apply eq1.
  - apply eq2.
Qed.

Taktika unfold

Explicitné rozbalenie definícií

Taktika unfold explicitne rozbalí zvolenú transparentnú definíciu. Taktika simpl zjednodušuje pomocou redukčných pravidiel a podľa výrazu môže tiež rozbaľovať definície, ale nerozbalí vždy všetko. Pri square chceme odkryť násobenie, aby sme mohli použiť jeho asociatívnosť a komutatívnosť.

Definícia funkcie square.

Definition square n := n * n.

Príklad s explicitným rozbalením square:

Lemma square_mult :
  forall n m, square (n * m) = square n * square m.
Proof.
  intros n m.
  simpl.
  (* ============================
     V tomto cieli simpl ponechá square nerozbalenú.

     n, m : nat
     ============================
     square (n * m) = square n * square m *)


  unfold square.  (* manuálne rozbalenie definície *)
  (* ============================
     Manuálne rozbalenie definície.

     n, m : nat
     ============================
     n * m * (n * m) = n * n * (m * m) *)

  rewrite PeanoNat.Nat.mul_assoc.
  (* ============================
     n * m * n * m = n * n * (m * m) *)

  assert (H: n * m * n = n * n * m).
    { rewrite PeanoNat.Nat.mul_comm.
      apply PeanoNat.Nat.mul_assoc. }
  (* H : n * m * n = n * n * m
     ============================
     n * m * n * m = n * n * (m * m) *)

  rewrite H.
  rewrite PeanoNat.Nat.mul_assoc.
  reflexivity.
Qed.

Automatické rozbalenie jednoduchej funkcie

Definícia foo vracia konštantu, preto ju simpl rozbalí aj bez znalosti argumentu.

Definition foo (x: nat) := 5.

Fact silly_fact_1 : forall m, foo m + 1 = foo (m + 1) + 1.
Proof.
  intros m. simpl. reflexivity.
Qed.

Funkcia s rozborom argumentu

V definícii bar rozhoduje o redukcii tvar argumentu. Rozborom m sprístupníme príslušnú vetvu match.

Definition bar x :=
  match x with
  | O => 5
  | S _ => 5
  end.

Riešenie pomocou destruct.

Fact silly_fact_2 : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  destruct m as [|n] eqn:E.
  - (* ============================
       Prvá vetva: m = 0

       m : nat
       E : m = 0
       ============================
       bar 0 + 1 = bar (0 + 1) + 1 *)

    simpl. reflexivity.
  - (* ============================
       Druhá vetva: m = S n

       m, n : nat
       E : m = S n
       ============================
       bar (S n) + 1 = bar (S n + 1) + 1 *)

    simpl. reflexivity.
Qed.

Riešenie pomocou unfold + destruct.

Fact silly_fact_2' : forall m, bar m + 1 = bar (m + 1) + 1.
Proof.
  intros m.
  unfold bar.  (* explicitné rozbalenie definície *)
  destruct m eqn:E.
  - reflexivity.
  - reflexivity.
Qed.

Taktika subst

Taktika subst slúži na nahradenie premenných ich známymi hodnotami podľa rovností v kontexte.

Z vhodnej rovnosti x = t alebo t = x, kde x je premenná a t neobsahuje x, môže subst nahradiť x výrazom t v cieli aj v závislých hypotézach. Odstráni pritom premennú x aj použitú rovnosť. Zápis subst x určí premennú; samotné subst spracuje vhodné rovnosti automaticky.

Lemma subst_example_1 :
  forall (x y : nat), x = y -> x + 1 = y + 1.
Proof.
  intros x y H.
  (* x, y : nat
     H : x = y
     ============================
     x + 1 = y + 1 *)

  subst x.
  (* ============================
     Nahradí x výrazom y vo všetkých výskytoch

     y : nat
     ============================
     y + 1 = y + 1 *)

  reflexivity.
Qed.

Príklad, kde sa nahrádza aj viac rovností naraz.

Lemma subst_example_2 :
  forall (a b c : nat),
    a = b -> b = c -> a + b = c + c.
Proof.
  intros a b c H1 H2.
  subst.  (* nahradí a aj b podľa dostupných rovností *)
  reflexivity.
Qed.

Nahradenie sa prejaví aj vo vnorených výrazoch:

Lemma subst_example_3 :
  forall (n m : nat),
    n = m ->
    S (n * n) = S (m * m).
Proof.
  intros n m H.
  subst.
  reflexivity.
Qed.

Príklad, kde subst ušetrí prácu oproti manuálnemu prepísaniu.

Lemma subst_example_4 :
  forall (x y z : nat),
    x = y + 1 ->
    y = z ->
    x = z + 1.
Proof.
  intros x y z Hxy Hyz.
  subst.  (* využije obe rovnosti na odstránenie premenných *)
  reflexivity.
Qed.

Porovnanie: manuálne nahradenie bez subst.

Lemma subst_example_4_manual :
  forall (x y z : nat),
    x = y + 1 ->
    y = z ->
    x = z + 1.
Proof.
  intros x y z Hxy Hyz.
  rewrite Hyz in Hxy.  (* manuálne nahradenie y za z *)
  rewrite Hxy.         (* manuálne nahradenie x *)
  reflexivity.
Qed.

Rozdiel medzi rewrite a subst

• subst eliminuje premenné pomocou vhodných rovností v kontexte a odstráni aj použité rovnosti.

• rewrite H prepíše výraz podľa rovnosti H vo zvolenom mieste, napríklad v cieli alebo pomocou in Hxy v hypotéze. Rovnosť H pritom ponechá v kontexte a dokáže prepisovať aj zložené výrazy, nielen premenné.

Taktika remember

Príkaz remember t as b eqn:Hb nahradí výskyty výrazu t v cieli novou premennou b a uloží rovnosť Hb : b = t. Nevytvára lokálnu definíciu b := t: premennú b môžeme rozobrať pomocou destruct a rovnosť Hb zachová spojenie s pôvodným výrazom.

Nasledujúca veta rozlišuje, či je n nula, podľa výsledku booleovského testu n =? 0. Ak test vráti true, dokazujeme n = 0; inak dokazujeme n <> 0. Samotná znalosť vetvy nestačí: potrebujeme vedieť, že práve test n =? 0 dal príslušný výsledok.

Lemma remember_example :
  forall (n : nat),
    if n =? 0 then n = 0 else n <> 0.
Proof.
  intros n.
  remember (n =? 0) as b eqn:Hb.
  (* n : nat
     b : bool
     Hb : b = (n =? 0)
     ============================
     if b then n = 0 else n <> 0 *)

  destruct b.
  - (* Hb : true = (n =? 0)
       ============================
       n = 0 *)
    symmetry in Hb.
    apply Nat.eqb_eq in Hb.
    (* Hb : n = 0 *)
    exact Hb.
  - (* Hb : false = (n =? 0)
       ============================
       n <> 0 *)
    symmetry in Hb.
    apply Nat.eqb_neq in Hb.
    (* Hb : n <> 0 *)
    exact Hb.
Qed.

Po destruct b sa podmienka if vyhodnotí v každej vetve. Rovnosť Hb však zostane a hovorí, aký výsledok mal pôvodný test. Obrátime ju pomocou symmetry in Hb, aby mala tvar očakávaný knižničnými lemami:

• Nat.eqb_eq vyjadruje (n =? m) = true <-> n = m.
• Nat.eqb_neq vyjadruje (n =? m) = false <-> n <> m.

Pomocou apply ... in Hb tak prejdeme od výsledku výpočtu v bool k tvrdeniu v Prop. Bez zachovanej rovnosti by rozbor pomenovanej hodnoty neposkytol informáciu potrebnú na tento prechod. Podobný výsledok možno dosiahnuť aj priamo príkazom destruct (n =? 0) eqn:Hb.

Taktika generalize dependent

Taktika generalize dependent l vráti premennú l aj hypotézy, ktoré od nej závisia, z kontextu do cieľa. Premenná bude v cieli opäť univerzálne kvantifikovaná. Pred indukciou tým môžeme zabezpečiť, aby indukčný predpoklad platil pre ľubovoľné l, nielen pre hodnotu zavedenú pred indukciou.

Uvažujme vetu firstn n l ++ skipn n l = l. Funkcia firstn n l vyberie prvých n prvkov zoznamu a skipn n l ich vynechá. Ak je zoznam kratší než n, dostaneme celý zoznam a prázdny zvyšok. Veta tvrdí, že spojením oboch častí získame pôvodný zoznam.

Prečo môže byť indukčný predpoklad príliš slabý?

Pri prirodzenom pokuse intros n l. a následnom induction n as [|n IH]. je už l zafixované. V indukčnom kroku preto dostaneme iba:

l : list nat
IH : firstn n l ++ skipn n l = l
============================
firstn (S n) l ++ skipn (S n) l = l

Po rozbore neprázdneho zoznamu l na x :: xs sa aj IH prepíše na tvrdenie o tomto celom zozname:

IH : firstn n (x :: xs) ++ skipn n (x :: xs) = x :: xs

Zjednodušenie cieľa v kroku pre S n však vyžaduje rovnosť pre chvost xs:

firstn n xs ++ skipn n xs = xs

Pôvodný IH nie je univerzálne kvantifikovaný podľa zoznamu, takže doň nemôžeme dosadiť xs. Pred indukciou preto vrátime l do cieľa.

Dôkaz so zovšeobecnením zoznamu

Lemma generalize_dependent_example :
  forall (n : nat) (l : list nat),
    firstn n l ++ skipn n l = l.
Proof.
  intros n l.
  generalize dependent l.
  (* n : nat
     ============================
     forall l : list nat, firstn n l ++ skipn n l = l *)

  induction n as [|n IH].
  - intros l.
    simpl. reflexivity.
  - (* n : nat
       IH : forall l : list nat, firstn n l ++ skipn n l = l
       ============================
       forall l : list nat, firstn (S n) l ++ skipn (S n) l = l *)
    intros l.
    destruct l as [|x xs].
    + simpl. reflexivity.
    + simpl.
      (* IH : forall l : list nat, firstn n l ++ skipn n l = l
         ============================
         x :: (firstn n xs ++ skipn n xs) = x :: xs *)
      f_equal.
      (* ============================
         firstn n xs ++ skipn n xs = xs *)
      apply IH.
Qed.

Pre n = 0 je prvá časť prázdna a zvyškom je celý zoznam. V kroku pre S n je prázdny zoznam opäť priamy prípad. Pri x :: xs sa hlava x zachová a zostáva rovnosť pre xs. Taktika f_equal, ktorú vysvetlíme nižšie, odstráni spoločný vonkajší konštruktor z cieľa. Tentoraz môžeme použiť IH, pretože platí pre každý zoznam, teda aj pre xs.

Rovnakú všeobecnosť by sme získali, keby sme na začiatku zaviedli iba n a l ponechali v cieli. Taktika generalize dependent je užitočná, keď sme už premennú zaviedli a potrebujeme ju pred indukciou zovšeobecniť. Ak od nej závisia hypotézy, vráti do cieľa aj tie. Príbuzný príkaz revert l vráti l do cieľa, ale závislé hypotézy treba v príkaze tiež uviesť.

Taktika f_equal

Taktika f_equal slúži na dokazovanie rovnosti výrazov, ktoré majú rovnaký vonkajší tvar (funkciu), ale líšia sa v argumentoch.

Pri cieli S x = S y prejde na rovnosť argumentov x = y. Ide o zachovanie rovnosti funkciou: ak sú argumenty rovnaké, rovnaké sú aj výsledky. Funkcia pritom nemusí byť injektívna. Na rozdiel od injection teda neodvodzujeme rovnosť argumentov z hypotézy o rovnosti výsledkov, ale volíme postačujúci podcieľ pre dôkaz rovnosti výsledkov.

Rozlišujeme príkazy f_equal. a apply f_equal.. Prvý vykonáva taktiku, ktorá rozkladá rovnosť funkčných výrazov a niektoré jednoduché podciele uzavrie automaticky. Druhý aplikuje rovnomennú globálnu lemu o zachovaní rovnosti. Jej typ môžeme skontrolovať príkazom:

Check @f_equal : forall (A B : Type) (f : A -> B) (x y : A),
  x = y -> f x = f y.

V nasledujúcom príklade použijeme samotnú taktiku:

Lemma f_equal_example :
  forall (x y : nat),
    x = y ->
    S x = S y.
Proof.
  intros x y H.
  (* H : x = y
     ============================
     S x = S y *)

  f_equal.
  (* ============================
     Prejdeme na dokazovanie rovnosti argumentov funkcie S.

     H : x = y
     ============================
     x = y *)

  exact H.
Qed.

Na tomto jednoduchom cieli možno namiesto f_equal. použiť aj apply f_equal. a následne exact H.. Oba postupy využívajú rovnaký matematický princíp, ale taktika a aplikácia lemy nie sú totožný mechanizmus.

Taktika admit

Počas vývoja dôkazu môžeme pomocou admit dočasne prijať aktuálny podcieľ bez dôkazu a pokračovať v ďalších vetvách. Podcieľ sa odstráni zo zoznamu otvorených cieľov, ale dôkaz tým nie je matematicky úplný.

• admit prijme aktuálny cieľ bez dôkazu.
• Admitted ukončí deklaráciu bez úplného dôkazu a prijme tvrdenie ako predpoklad.
• Qed uzavrie dokončený dôkaz overený jadrom Rocqu. Ak sme použili admit, nemožno ho takto uzavrieť.

Ani admit, ani Admitted nenahrádzajú matematický dôkaz. Nasledujúca deklarácia je zámernou ukážkou nedokončeného dôkazu; pri jej dokončení treba admit nahradiť dôkazom a Admitted príkazom Qed.

Príklad: rozdelenie prípadu pomocou destruct.

Lemma admit_example :
  forall (b : bool),
    if b then 1 + 1 = 2 else 2 + 2 = 4.
Proof.
  intros b.
  destruct b.
  - (* ============================
       Prvá vetva: b = true

       ============================
       1 + 1 = 2 *)

    admit.  (* túto časť dokážeme neskôr *)
  - (* ============================
       Druhá vetva: b = false

       ============================
       2 + 2 = 4 *)

    simpl. reflexivity.
Admitted.

Taktika assumption

Taktika assumption vyhľadá v kontexte hypotézu, ktorá priamo dokazuje cieľ. Pri cieli P a hypotéze HP : P má rovnaký výsledok ako exact HP, ale meno hypotézy nemusíme uviesť. Ak vhodnú hypotézu nenájde, zlyhá.

Lemma assumption_example :
  forall (P Q : Prop),
    P ->
    Q ->
    P.
Proof.
  intros P Q HP HQ.
  (* P, Q : Prop
     HP : P
     HQ : Q
     ============================
     P *)

  assumption.  (* použije hypotézu HP na vyriešenie cieľa *)
Qed.

Taktika try

Taktický operátor try T sa pokúsi vykonať taktiku T. Ak T zlyhá, obnoví pôvodný stav a uspeje bez jeho zmeny. Hodí sa, keď sa ten istý krok dá použiť iba na niektoré z podcieľov.

V príklade split rozdelí konjunkciu na ciele P a 2 = 2. Operátor ;, ktorému sa venujeme nižšie, vykoná try assumption v oboch podcieľoch.

Lemma try_assumption_example :
  forall P : Prop,
    P -> P /\ (2 = 2).
Proof.
  intros P HP.
  split; try assumption.
  (* P vyriešila hypotéza HP. Pre druhý cieľ vhodná hypotéza nie je:
     P : Prop
     HP : P
     ============================
     2 = 2 *)
  reflexivity.
Qed.

Bez try by príkaz split; assumption zlyhal pri cieli 2 = 2. S try tento podcieľ zostane otvorený a dokončíme ho pomocou reflexivity.

Taktika repeat

Taktický operátor repeat T opakuje T na vznikajúcich podcieľoch, kým taktika nezlyhá alebo neprestane meniť dôkazový stav. Samotné repeat pri takomto zastavení nezlyhá. Je užitočné napríklad pri opakovanom prepisovaní rovnakou lemou.

Bez repeat

Lemma repeat_example_manual :
  forall n, (((n + 0) + 0) + 0) = n.
Proof.
  intros n.
  rewrite PeanoNat.Nat.add_0_r.
  rewrite PeanoNat.Nat.add_0_r.
  rewrite PeanoNat.Nat.add_0_r.
  reflexivity.
Qed.

S repeat rewrite

Lemma repeat_example :
  forall n, (((n + 0) + 0) + 0) = n.
Proof.
  intros n.
  repeat rewrite PeanoNat.Nat.add_0_r.
  reflexivity.
Qed.

Po odstránení všetkých pripočítaní nuly už rewrite Nat.add_0_r nemožno použiť a opakovanie sa zastaví. Pri inej taktike treba zvoliť opakovanie uvážene: cyklické zmeny stavu, napríklad opakované obracanie rovnosti, môžu viesť k neukončeniu. Úspech bez zmeny stavu však repeat zastaví.

Taktický operátor bodkočiarka (;)

Taktický operátor T1; T2 aplikuje T2 na všetky podciele, ktoré vzniknú po vykonaní T1. Naproti tomu pri T1. T2. pracuje druhý príkaz iba s aktuálnym podcieľom.

V nasledujúcom dôkaze vytvorí destruct b vetvy pre true a false a reflexivity uzavrie obe.

Lemma semicolon_simple :
  forall b : bool, (if b then true else false) = b.
Proof.
  intros b.
  destruct b; reflexivity.
Qed.

Vo vetve pre true sa cieľ zredukuje na true = true, vo vetve pre false na false = false. Preto je v oboch prípadoch vhodná rovnaká taktika.

Ako si vybrať správnu taktiku?

Najprv rozlíšime tvar cieľa a dostupné hypotézy. Tabuľky uvádzajú vhodný ďalší krok; nové podciele potom treba dokázať.

Rovnosti a spor

Úprava dôkazového stavu a riadenie vetiev

Dokončený dôkaz uzavrieme príkazom Qed. Príkazy admit a Admitted prijímajú tvrdenia bez úplného dôkazu a slúžia iba ako dočasné pomôcky pri jeho tvorbe.

Zhrnutie

Pri výbere taktiky vychádzame z tvaru cieľa a dostupných hypotéz. Rovnosti môžeme prepisovať, rozkladať pomocou vlastností konštruktorov alebo použiť na úpravu kontextu. Pri indukcii potrebujeme dostatočne všeobecný indukčný predpoklad a pri rozbore výrazov môže byť dôležité zachovať rovnosť s pôvodným výrazom.

Operátory try, repeat a ; umožňujú kombinovať jednotlivé kroky. Dokončený dôkaz overíme príkazom Qed; ukážka s Admitted zostáva zámerne nedokončená. Práci s logickými spojkami sa venuje nasledujúca prednáška.