Induktívne definované výroky

Definovať predikáty pomocou induktívnych pravidiel.
Analyzovať dôkazy pomocou destruct a inversion .
Dokazovať vlastnosti relácií a ich uzáverov.

Logické tvrdenia môžeme definovať aj induktívne pomocou pravidiel, ktoré určujú prípustné dôkazy. Na príkladoch usporiadania a párnosti ukážeme ich konštruovanie aj rozbor. Potom prejdeme k vlastnostiam binárnych relácií a k uzáverom. Tie pripravia pôdu pre nasledujúcu prednášku o formalizácii vyhodnocovania jazyka NBL.

Induktívne definície usporiadania a párnosti
Konštruovanie, rozbor a inverzia dôkazov
Taktiky auto, eauto a eapply
Binárne relácie a ich vlastnosti
Tranzitívny a reflexívno-tranzitívny uzáver

Kódové bloky vykonávame postupne v poradí prednášky. Vlastné definície usporiadania a párnosti uzavrieme do modulu inductively.

Module inductively.

Základné pojmy

V Rocq (a všeobecne v logike) induktívne definovaný výrok znamená, že daný predikát alebo množina je definovaná pomocou pravidiel konštrukcie, ktoré určujú:

kedy výrok platí (aké sú základné prípady - base cases),
pravidlá pre odvodenie ďalších prípadov (inductive step).

Induktívna definícia vzťahu menší alebo rovný

Dedukčné pravidlá:

$$ \frac{\ }{n\leq n}\,{\scriptstyle(\mathrm{le\_n})} $$ $$ \frac{n\leq m}{n\leq S\,m}\,{\scriptstyle(\mathrm{le\_S})} $$

Definícia v Rocq:

Inductive le : nat -> nat -> Prop :=
  | le_n (n : nat) : le n n
  | le_S (n m : nat) : le n m -> le n (S m).

(* Notácia pre konkrétnu syntax *)
Notation "n <= m" := (le n m) (at level 70).

Odvodenie:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{} \RightLabel{$\scriptstyle(\mathrm{le\_n})$} \UnaryInfC{$3\leq 3$} \RightLabel{$\scriptstyle(\mathrm{le\_S})$} \UnaryInfC{$3\leq 4$} \RightLabel{$\scriptstyle(\mathrm{le\_S})$} \UnaryInfC{$3\leq 5$} \end{prooftree} $$

Príklad dôkazu v Rocq: 3 <= 5

Example le_3_5 : 3 <= 5.
Proof.
  (* ============================
     3 <= 5 *)

  apply le_S.
  (* ============================
     3 <= 4 *)

  apply le_S.
  (* ============================
     3 <= 3 *)

  apply le_n.
Qed.

Príklad dôkazu v Rocq: 2+1 <= 5

Example le_2plus1_5 : 2+1 <= 5.
Proof.
  simpl.
  apply le_S.
  apply le_S.
  apply le_n.
Qed.

Induktívna definícia vzťahu párne čísla

Dedukčné pravidlá:

$$ \frac{\ }{\operatorname{even}\ 0}\,{\scriptstyle(\mathrm{even\_O})} $$ $$ \frac{\operatorname{even}\ n}{\operatorname{even}\ (S\,(S\,n))}\,{\scriptstyle(\mathrm{even\_SS})} $$

Definícia v Rocq: číslo je párne, ak je nula alebo má tvar S (S n), kde n je párne. Nestačí všeobecne požadovať párnosť n - 2, pretože odčítanie v nat je orezané na nule: aj 1 - 2 = 0.

Inductive even : nat -> Prop :=
  | even_O : even 0
  | even_SS : forall n, even n -> even (S (S n)).

Odvodenie:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{} \RightLabel{$\scriptstyle(\mathrm{even\_O})$} \UnaryInfC{$\operatorname{even}\ 0$} \RightLabel{$\scriptstyle(\mathrm{even\_SS}:n:=0)$} \UnaryInfC{$\operatorname{even}\ 2$} \RightLabel{$\scriptstyle(\mathrm{even\_SS}:n:=2)$} \UnaryInfC{$\operatorname{even}\ 4$} \end{prooftree} $$

Príklad dôkazu v Rocq: 4 je párne

Lemma four_is_even : even 4.
Proof.
  (* 4 = S (S 2), 2 = S (S 0) *)

  (* ============================
     even 4 *)

  apply even_SS.
  (* ============================
     even 2 *)

  apply even_SS.
  (* ============================
     even 0 *)

  apply even_O.
Qed.

Okrem konštruovania dôkazov, že nejaké číslo je párne, môžeme tieto dôkazy aj rozkladať – teda uvažovať o tom, ako mohli byť vytvorené.

Definícia predikátu even pomocou príkazu Inductive hovorí nielen to, že konštruktory even_O a even_SS sú platné spôsoby, ako vytvoriť dôkaz o tom, že číslo je párne, ale aj to, že sú to jediné dva možné spôsoby, ako taký dôkaz zostrojiť.

Inými slovami, pre každý dôkaz E tvrdenia even n, nutne platí jedno z nasledovného:

E = even_O a teda n = 0,
alebo E = even_SS n' E', kde n = S (S n') a E' je dôkaz pre even n'.

To znamená, že je možné analyzovať hypotézu tvaru even n podobne, ako iné induktívne definované dátové štruktúry.

Teda existuje spôsob, ako vykonať analýzu podľa prípadov (case analysis) alebo indukciu priamo nad štruktúrou dôkazu.

Majme tvrdenie o čísle n za predpokladu even n.

Analýza podľa prípadov môže byť vykonaná nielen na čísle n pomocou destruct alebo induction, ale aj priamo na dôkaze even n.

Týmto spôsobom sa skúma štruktúra samotného dôkazu, nie hodnota čísla.

Theorem even_inversion :
  forall (n : nat),
  even n ->
    (n = 0) \/ (exists n', n = S (S n') /\ even n').
Proof.
  intros n E.
  destruct E as [| k Ek].
  - (* ============================
       Podcieľ 1/2: konštruktor even_O : even 0

       ============================
       0 = 0 \/ (exists n' : nat, 0 = S (S n') /\ even n') *)

    left. reflexivity.
  - (* ============================
       Podcieľ 2/2: konštruktor even_SS k Ek

       k : nat
       Ek : even k
       ============================
       S (S k) = 0 \/
         (exists n' : nat, S (S k) = S (S n') /\ even n') *)

    right. exists k. split.
    + reflexivity.
    + apply Ek.
Qed.

Tento druh viet sa často nazýva inverzné vety (inversion lemmas), pretože umožňujú "obrátiť" dôkaz – získať informáciu o tom, ako mohol byť vytvorený.

Pre predikát even existujú dve možnosti, ako zostrojiť dôkaz even n, a inverzná veta ich explicitne rozlíši.

Použitie inverznej vety v dôkaze

Theorem evSS_ev :
  forall n, even (S (S n)) -> even n.
Proof.
  intros n E.
  apply even_inversion in E.
  (* E : S (S n) = 0 \/
         (exists n', S (S n) = S (S n') /\ even n')
     ============================
     even n *)

  destruct E as [H0 | [n' [Heq Heven]]].
  - (* ============================
       Podcieľ 1/2: nemožná rovnosť

       H0 : S (S n) = 0
       ============================
       even n *)

    discriminate H0.
  - (* ============================
       Podcieľ 2/2: prípad konštruktora even_SS

       n' : nat
       Heq : S (S n) = S (S n')
       Heven : even n'
       ============================
       even n *)

    injection Heq as Hn.
    (* Hn : n = n'
       ============================
       even n *)

    rewrite Hn. apply Heven.
Qed.

Aplikácia inverznej vety zmení hypotézu E na disjunkciu. Až jej rozbor pomocou destruct vytvorí dva podciele:

jeden je kontradikcia (S (S n) = 0),
druhý využíva injection a rewrite.

Rocq poskytuje aj užitočnú taktiku inversion, ktorá vlastnosť inverzie spracuje automaticky – netreba ručne dokazovať inverzné vety pre každú induktívnu definíciu.

Theorem evSS_ev' :
  forall n, even (S (S n)) -> even n.
Proof.
  intros n E.
  (* E : even (S (S n))
     ============================
     even n *)

  inversion E as [| n' Heven]; subst.
  (* inversion vylúči even_O a v prípade even_SS získa
     rovnosť indexov n' = n aj dôkaz Heven : even n'.
     Taktika subst použije rovnosť na dosadenie.

     Po týchto krokoch sú relevantné predpoklady a cieľ:
     n : nat
     E : even (S (S n))
     Heven : even n
     ============================
     even n *)

  apply Heven.
Qed.

Taktika inversion analyzuje možné konštruktory dôkazu, vylúči nemožné prípady a zo zhody indexov odvodí príslušné rovnosti aj predpoklady. Poskytne tak informácie potrebné na dokončenie dôkazu; v tomto príklade po subst použijeme Heven.

Taktika discriminate využíva odlišnosť rôznych konštruktorov, injection injektívnosť rovnakého konštruktora. Inverzia tieto vlastnosti využíva pri analýze indexov induktívneho predikátu, napríklad pri vylúčení dôkazu even 1.

Porovnanie: dôkaz s `inversion` a s našou vetou

Theorem one_not_even :
  ~ even 1.
Proof.
  intros H.
  apply even_inversion in H.
  destruct H as [H0 | [n [Heq Heven]]].
  - (* H0 : 1 = 0; cieľ: False *)
    discriminate H0.
  - (* Heq : 1 = S (S n), Heven : even n; cieľ: False *)
    discriminate Heq.
Qed.

Theorem one_not_even' :
  ~ even 1.
Proof.
  intros H.
  inversion H.
  (* Automaticky rozpozná, že even 1 je nemožné,
     pretože 1 ≠ 0 a 1 ≠ S (S n) *)
Qed.

Zhrnutie: Inverzia

Každá induktívna definícia v Rocq-u implicitne určuje všetky možné spôsoby, ako mohol vzniknúť dôkaz.
Pomocou destruct alebo inversion je možné tieto dôkazy analyzovať.
Taktika inversion eliminuje nemožné prípady a priamo rozdeľuje hypotézy podľa tvaru dôkazu.
Je to kľúčový nástroj pri práci s dôkazmi o vlastnostiach induktívnych údajových typov.

End inductively.

Taktika `auto`

Automatické dokazovanie. Taktika auto sa pokúsi vyriešiť cieľ pomocou dostupných hypotéz a základných logických pravidiel.

Využíva hypotézy v kontexte a databázu pomocných viet (hintov, predvolene core). Zavádza predpoklady, skúša aplikovať vety a uzatvárať ciele hypotézami; možnosti prehľadáva predvolene do hĺbky 5. Databázu možno rozšíriť príkazmi Hint Resolve pre pomocné vety a Hint Constructors pre konštruktory.

Lemma auto_example :
  forall (P Q R : Prop),
    P -> Q -> R -> P /\ Q /\ R.
Proof.
  intros P Q R HP HQ HR.
  auto.
  (* Použije konštruktor konjunkcie a hypotézy HP, HQ, HR. *)
Qed.

Príklad použitia:

auto.     (* pokúsi sa vyriešiť cieľ automaticky *)
auto n.   (* s určenou hĺbkou n *)

Taktika `eauto`

Rozšírené automatické dokazovanie. Taktika eauto používa rovnaké databázy hintov ako auto, navyše však môže pri aplikovaní viet ponechať niektoré argumenty zatiaľ neurčené ako existenčné metavariabilné premenné, napríklad ?x. Ich hodnoty potom doplní unifikáciou pri riešení ďalších podcieľov.

Metavariabilná premenná je dočasne neurčený term v rozpracovanom dôkaze, nie nový logický predpoklad ani samotný kvantifikátor exists. Pri vhodných hintoch tak eauto dokáže odložiť aj voľbu svedka existenčného tvrdenia.

Použitie:

eauto.          (* vyhľadávanie aj s neurčenými argumentmi *)
eauto 6.        (* určuje hĺbku vyhľadávania *)

Predpoklady hovoria, že každý prvok s vlastnosťou P má aj vlastnosť Q a že P n platí. Dokážeme existenciu prvku s vlastnosťou Q.

Example eauto_example :
  forall (P Q : nat -> Prop) (n : nat),
    (forall x, P x -> Q x) -> P n -> exists x, Q x.
Proof.
  intros P Q n H HP.
  Fail solve [auto].
  (* auto s predvolenými hintmi tento cieľ neuzavrie. *)
  eauto.
Qed.

Pri použití konštruktora existencie zostáva svedok ako ?x a cieľ má tvar Q ?x. Hypotéza H ho prevedie na P ?x; použitie HP : P n určí ?x := n. Dôkaz tak využije oba predpoklady.

Príkaz Fail solve [auto] overuje, že samotné auto tento konkrétny cieľ neuzavrie. Netvrdí, že auto nikdy nedokáže tvrdenie s exists: napríklad môže použiť jeho hotový dôkaz z kontextu. Uvedený príklad funguje v Rocq 9.1.1 s predvolenou databázou core, bez pridania hintov.

Taktika `eapply`

Taktika apply už využíva unifikáciu záveru aplikovanej vety s aktuálnym cieľom na určenie jej argumentov. Nie všetky argumenty však možno takto odvodiť.

Taktika eapply môže navyše ponechať niektoré argumenty neurčené ako existenčné metavariabilné premenné. Tie sa môžu určiť až unifikáciou pri riešení nasledujúcich podcieľov.

Použijeme štandardnú vetu eq_trans, ktorú znova nedefinujeme:

Check @eq_trans : forall (A : Type) (x y z : A),
  x = y -> y = z -> x = z.

Pri cieli n = m sa určia krajné prvky x := n a z := m, ale prostredný prvok y zo samotného cieľa nevyplýva. Pri apply ho tu zadáme explicitne:

Lemma ex_eq_trans_apply :
  forall p n m : nat, n = p -> p = m -> n = m.
Proof.
  intros p n m Hnp Hpm.
  apply eq_trans with (y := p).
  - apply Hnp.
  - apply Hpm.
Qed.

Pri eapply vzniknú podciele n = ?y a ?y = m. Použitie Hnp : n = p na prvý podcieľ určí ?y := p, takže druhý podcieľ má už tvar p = m:

Lemma ex_eq_trans_eapply :
  forall p n m : nat, n = p -> p = m -> n = m.
Proof.
  intros p n m Hnp Hpm.
  eapply eq_trans.
  - apply Hnp.
  - apply Hpm.
Qed.

Definícia

Binárna relácia na množine X v Rocq má typ: X -> X -> Prop.

Ide o množinu tvrdení parameterizovanú dvoma prvkami množiny X, teda tvrdenie o dvojiciach prvkov X.

(* Definícia binárnej relácie *)
Definition relation (X: Type) := X -> X -> Prop.

Po End inductively je naša relácia dostupná pod kvalifikovaným názvom inductively.le. Modul tvorí menný priestor, takže v rôznych moduloch môžu existovať definície s rovnakým základným názvom le. Keďže obsah modulu neimportujeme, nekvalifikované le a notácia <= teraz opäť označujú štandardnú reláciu Corelib.Init.Peano.le.

Obe relácie vyjadrujú tú istú matematickú vlastnosť „menší alebo rovný“, ale v Rocq ide o dve odlišné induktívne definície. Naša definícia má oba indexy za dvojbodkou; štandardná má prvý argument ako parameter. Dôkaz jednej relácie preto nie je automaticky dôkazom druhej. Nasledujúce dôkazy o usporiadaní používajú štandardnú reláciu.

Check inductively.le : relation nat.
Print inductively.le.
Check Corelib.Init.Peano.le : relation nat.
Print Corelib.Init.Peano.le.
(* Inductive le (n : nat) : nat -> Prop :=
      le_n : n <= n
    | le_S : forall m : nat, n <= m -> n <= S m *)

Check le : nat -> nat -> Prop.
Check le : relation nat.

Vlastnosti binárnych relácií

1. Reflexívna relácia

Definition reflexive {X: Type} (R: relation X) :=
  forall a : X, R a a.

2. Transitívna relácia

Definition transitive {X: Type} (R: relation X) :=
  forall a b c : X, R a b -> R b c -> R a c.

3. Symetrická relácia

Definition symmetric {X: Type} (R: relation X) :=
  forall a b : X, R a b -> R b a.

4. Antisymetrická relácia

Definition antisymmetric {X: Type} (R: relation X) :=
  forall a b : X, R a b -> R b a -> a = b.

5. Ekvivalencia

Definition equivalence {X:Type} (R: relation X) :=
  reflexive R /\ symmetric R /\ transitive R.

6. Čiastočné usporiadanie

Definition partialorder {X:Type} (R: relation X) :=
  reflexive R /\ antisymmetric R /\ transitive R.

7. Kváziusporiadanie

Definition preorder {X:Type} (R: relation X) :=
  reflexive R /\ transitive R.

Reflexívnosť:

Theorem le_reflexive : reflexive le.
Proof.
  unfold reflexive.
  intro n.
  apply le_n.
Qed.

Tranzitívnosť:

Theorem le_trans : transitive le.
Proof.
  unfold transitive.
  intros n m o Hnm Hmo.
  induction Hmo.
  - (* Prípad: o = m *)
    apply Hnm.
  - (* Prípad: o = S m0, kde m <= m0 *)
    apply le_S.
    apply IHHmo.
Qed.

Pomocná veta pre antisymetriu:

Lemma Sn_le_Sm__n_le_m :
  forall n m, le (S n) (S m) -> le n m.
Proof.
  intros.
  inversion H.
  (* Prípad 1: S n = S m *)
  - apply le_n.
  (* Prípad 2: S n <= m0 a m = S m0 *)
  - subst.
    eapply le_trans.
    + apply le_S. apply le_n.
    + apply H1.
Qed.

Antisymetria:

Theorem le_antisymmetric : antisymmetric le.
Proof.
  unfold antisymmetric.
  induction a.
  - intros.
    inversion H0.
    reflexivity.
  - intros.
    destruct b.
    + inversion H.
    + apply Sn_le_Sm__n_le_m in H.
      apply Sn_le_Sm__n_le_m in H0.
      f_equal.
      apply IHa in H; assumption.
Qed.

Čiastočné usporiadanie:

Theorem le_partialorder : partialorder le.
Proof.
  unfold partialorder.
  split.
  - apply le_reflexive.
  - split.
    + apply le_antisymmetric.
    + apply le_trans.
Qed.

Tranzitívny uzáver

Tranzitívny uzáver spája prvky cestou zloženou z jedného alebo viacerých krokov relácie R. Sám osebe nezaručuje reflexívnosť; dvojica (x, x) doň môže patriť, ak v R existuje neprázdna cesta z x späť do x.

Dedukčné pravidlá:

$$ \frac{R\ x\ y}{\operatorname{clos\_trans}\ R\ x\ y} \,{\scriptstyle(\mathrm{t\_step})} $$ $$ \frac{\operatorname{clos\_trans}\ R\ x\ y\qquad\operatorname{clos\_trans}\ R\ y\ z}{\operatorname{clos\_trans}\ R\ x\ z} \,{\scriptstyle(\mathrm{t\_trans})} $$

Induktívna definícia tranzitívneho uzáveru:

Inductive clos_trans
    {X: Type} (R: X -> X -> Prop) : X -> X -> Prop :=
  | t_step (x y : X) :
      R x y ->
      clos_trans R x y
  | t_trans (x y z : X) :
      clos_trans R x y ->
      clos_trans R y z ->
      clos_trans R x z.

Induktívny vzťah "parent_of" a jeho tranzitívny uzáver "ancestor_of".

(* Definícia slovanských bohov *)
Inductive God : Type :=
  | Svarog
  | Perun
  | Dažbog
  | Lada.

(* Induktívna definícia vzťahu rodič *)
Inductive parent_of : God -> God -> Prop :=
  | po_SP : parent_of Svarog Perun
  | po_SD : parent_of Svarog Dažbog
  | po_PL : parent_of Perun Lada.
(*
- Svarog je rodičom Peruna a Dažboga,
- Perun je rodičom Lady
*)

(* Definícia vzťahu "ancestor_of" ako tranzitívne uzavretie parent_of *)
Definition ancestor_of : God -> God -> Prop :=
  clos_trans parent_of.

Dôkaz, že Svarog je predkom Lada:

Odvodenie:

-----------------------(po_SP)  -----------------------(po_PL)
 parent_of Svarog Perun           parent_of Perun Lada
-----------------------(t_step) -----------------------(t_step)
ancestor_of Svarog Perun         ancestor_of Perun Lada
-------------------------------------------------------(t_trans)
                ancestor_of Svarog Lada

Dôkaz v Rocq:

Example ancestor_of_ex : ancestor_of Svarog Lada.
Proof.
  unfold ancestor_of.
  apply t_trans with Perun.
  - apply t_step. apply po_SP.
  - apply t_step. apply po_PL.
Qed.

Reflexívny a tranzitívny uzáver

Reflexívno-tranzitívny uzáver pripúšťa aj cestu s nulovým počtom krokov, preto obsahuje dvojicu (x, x) pre každý prvok nosného typu X.

Dedukčné pravidlá:

$$ \frac{R\ x\ y}{\operatorname{clos\_refl\_trans}\ R\ x\ y} \,{\scriptstyle(\mathrm{rt\_step})} $$ $$ \frac{\ }{\operatorname{clos\_refl\_trans}\ R\ x\ x} \,{\scriptstyle(\mathrm{rt\_refl})} $$ $$ \frac{\operatorname{clos\_refl\_trans}\ R\ x\ y\qquad\operatorname{clos\_refl\_trans}\ R\ y\ z}{\operatorname{clos\_refl\_trans}\ R\ x\ z} \,{\scriptstyle(\mathrm{rt\_trans})} $$

Pravidlo rt_refl je bezpremisové: x : X je parameter určujúci prvok, nie premisa, ktorú treba dokazovať.

Induktívna definícia: reflexívny a tranzitívny uzáver:

Inductive clos_refl_trans
  {X: Type} (R: X -> X -> Prop) : X -> X -> Prop :=
  | rt_step (x y : X) :
      R x y ->
      clos_refl_trans R x y
  | rt_refl (x : X) :
      clos_refl_trans R x x
  | rt_trans (x y z : X) :
      clos_refl_trans R x y ->
      clos_refl_trans R y z ->
      clos_refl_trans R x z.

Reláciu R definujeme na celom type nat. Jej jediné dvojice sú $(1,2)$ a $(2,3)$; následne odlíšime uzáver na nat od jeho obmedzenia na $A=\{1,2,3\}$.

Definícia relácie R.

Definition R (x y : nat) : Prop :=
  (x = 1 /\ y = 2) \/ (x = 2 /\ y = 3).

Relácia R medzi prirodzenými číslami x a y. Relácia R x y je pravdivá, ak platí buď:

x = 1 a y = 2, alebo
x = 2 a y = 3.

Množina hodnôt, pre ktoré R je pravdivá: {(1,2), (2,3)}

Example R_example1 : R 1 2.
Proof.
  unfold R.
  left. split; reflexivity.
Qed.

Example R_example2 : R 2 3.
Proof.
  right. split; reflexivity.
Qed.

Example R_example3 : ~ R 1 3.
Proof.
  unfold not. intros H.
  destruct H as [[H1 H2] | [H1 H2]]; discriminate.
Qed.

Reflexívny a tranzitívny uzáver relacie R:

Definition R_refl_trans := clos_refl_trans R.

Ak označíme tento uzáver ako $R^*$, na celom type nat obsahuje presne

$$R^*=\{(n,n)\mid n\in\mathbb{N}\}\cup\{(1,2),(2,3),(1,3)\}.$$

Najmä obsahuje aj $(0,0)$, $(4,4)$ a všetky ostatné reflexívne dvojice. Pre každé prirodzené číslo platí

$$\forall n:\mathsf{nat},\quad R^*(n,n).$$

Lemma R_refl_trans_reflexive :
  forall n : nat, R_refl_trans n n.
Proof.
  intro n.
  apply rt_refl.
Qed.

Až po obmedzení oboch argumentov na $A=\{1,2,3\}$ dostaneme uvedených šesť dvojíc:

$$R^*\cap(A\times A)=\{(1,1),(2,2),(3,3),(1,2),(2,3),(1,3)\}.$$

V tomto konkrétnom príklade je to aj reflexívno-tranzitívny uzáver obmedzenia $R$ na $A$, pretože žiadny krok $R$ nevedie mimo $A$. Samotné označenie množiny $A$ v texte však nemení nosný typ nat v definícii Rocq.

Reflexívne prípady: každý prvok je v uzávere v relácii sám so sebou.

Example refl_1 : R_refl_trans 1 1.
Proof.
  apply rt_refl.
Qed.

Example refl_2 : R_refl_trans 2 2.
Proof.
  apply rt_refl.
Qed.

Example refl_3 : R_refl_trans 3 3.
Proof.
  apply rt_refl.
Qed.

Jeden krok a skladanie ciest: použijeme pravidlá rt_step a rt_trans toho istého reflexívno-tranzitívneho uzáveru.

Example trans_1_2 : R_refl_trans 1 2.
Proof.
  apply rt_step. left. split; reflexivity.
Qed.

Example trans_2_3 : R_refl_trans 2 3.
Proof.
  apply rt_step. right. split; reflexivity.
Qed.

Example trans_1_3 : R_refl_trans 1 3.
Proof.
  apply rt_trans with 2.
  - apply rt_step. left. split; reflexivity.
  - apply rt_step. right. split; reflexivity.
Qed.

Reflexívno-tranzitívny uzáver umožňuje formalizovať vykonanie ľubovoľného konečného počtu krokov. Jeden krok vyhodnotenia budeme reprezentovať binárnou reláciou medzi termami; jej tranzitívny uzáver opíše jeden alebo viac krokov a reflexívno-tranzitívny uzáver nula alebo viac krokov výpočtu.

Túto súvislosť využíva druhá časť referenčného súboru prednaska5_nova_notacia.v pri formalizácii jazyka NBL: relácia smallstep opisuje jeden krok a multistep nula alebo viac krokov. Jej konštruktory skladajú cestu po jednom kroku; vyjadruje rovnakú reláciu ako clos_refl_trans smallstep. Syntax, pravidlá a dôkazy vlastností NBL rozoberá nasledujúca prednáška.

Induktívne pravidlá určujú, ako možno zostrojiť dôkaz tvrdenia. Pomocou destruct a inversion skúmame jeho štruktúru a odvodzujeme dôsledky. Binárne relácie a ich tranzitívne či reflexívno-tranzitívne uzávery poskytujú základ na opis viacerých krokov vyhodnotenia programov.

Induktívne definované výroky

Ciele

Obsah