Logika v Rocq

Rozlišovať booleovské výpočty a tvrdenia v Prop .
Dokazovať tvrdenia s logickými spojkami a kvantifikátormi.
Rozlišovať konštruktívne a klasické dokazovanie.

Po prednáške o taktikách sa zameriame na logické tvrdenia v Prop. Pri spojkách a kvantifikátoroch rozlíšime, ako tvrdenie dokázať v cieli a ako využiť jeho dôkaz v kontexte. Tieto postupy spojíme v dôkazoch o príslušnosti do zoznamu a napokon objasníme rozdiel medzi konštruktívnym a klasickým dokazovaním.

Tvrdenia, dôkazy a rozdiel medzi bool a Prop
Logické spojky a kvantifikátory
Negácia, False a princíp ex falso
Rekurzívne predikáty nad zoznamami
Konštruktívna a klasická logika

Kódové bloky vykonávame postupne v poradí kapitoly.

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

Dosiaľ sme pracovali najmä s rovnosťami, implikáciami a univerzálne kvantifikovanými tvrdeniami. Teraz sa pozrieme na ďalšie logické spojky a existenčný kvantifikátor. Pri každej konštrukcii rozlíšime, ako ju dokázať v cieli a ako využiť jej dôkaz v hypotéze.

Booleovské výpočty a logické tvrdenia

bool je induktívny typ s konštruktormi true a false. Booleovské funkcie používame pri výpočtoch a v podmienkach if. Nasledujúce testy prirodzených čísel majú výsledok typu bool:

Výraz	Význam výsledku `true`
`n =? m`	`n` sa rovná `m`
`n <=? m`	`n` je menšie alebo rovné `m`
`n <? m`	`n` je menšie než `m`

Príklady:

Compute (3 <=? 5).  (* true *)
Compute (5 =? 3).   (* false *)
Compute (4 <? 4).   (* false *)

Booleovské hodnoty môžeme kombinovať funkciami negb (negácia), andb (konjunkcia), orb (disjunkcia) a xorb (výlučná disjunkcia).

Príklady:

Compute (andb true false).   (* false *)
Compute (orb true false).    (* true *)
Compute (negb true).         (* false *)
Compute (xorb true false).   (* true *)

Prop je sort logických tvrdení. Výrazy n = m a n <= m sú tvrdenia v Prop; ich zapísaním nezískame booleovskú hodnotu. Rozlišujeme dva úsudky:

P : Prop hovorí, že P je korektne utvorené tvrdenie.
p : P hovorí, že p je dôkazom tvrdenia P.

Napríklad (n =? m) = true je tvrdenie o výsledku booleovského výpočtu. Lema Nat.eqb_eq ho spája s tvrdením n = m, ako sme videli pri remember.

Základné logické konštrukcie v Prop sú:

Zápis	Význam
`P /\ Q`	konjunkcia: `P` a `Q`
`P \/ Q`	disjunkcia: `P` alebo `Q`
`P -> Q`	implikácia: ak `P`, potom `Q`
`~P`	negácia: `P -> False`
`P <-> Q`	ekvivalencia: oba smery implikácie
`forall x : A, P x`	vlastnosť platí pre každý prvok typu `A`
`exists x : A, P x`	existuje prvok typu `A` s vlastnosťou `P`

Tvrdenia a ich dôkazy

Príkaz Check kontroluje typovú správnosť výrazu. Oba výrazy 2 = 2 aj 3 = 2 majú typ Prop, hoci prvé tvrdenie vieme dokázať a druhé vyvrátiť. Úspešné Check teda nedokazuje pravdivosť tvrdenia.

Check 2 = 2 : Prop.
Check 3 = 2 : Prop.
Check (forall n : nat, n = 2) : Prop.

Tvrdenie v teoréme

Na rozdiel od kontroly typu teraz skonštruujeme dôkaz rovnosti:

Theorem plus_2_2_is_4 :
  2 + 2 = 4.
Proof. reflexivity. Qed.

Pomenované tvrdenia

Pomocou Definition môžeme tvrdenie pomenovať. Táto deklarácia pomenúva tvrdenie, neposkytuje jeho dôkaz:

Definition plus_claim : Prop := 2 + 2 = 4.
Check plus_claim : Prop.

Dôkaz pomenovaného tvrdenia uvedieme samostatne:

Theorem plus_claim_is_true : plus_claim.
Proof. reflexivity. Qed.

Predikáty

Predikát je funkcia, ktorá pre každý argument vytvorí tvrdenie v Prop. Napríklad is_three n vyjadruje, že n je číslo tri:

Definition is_three (n : nat) : Prop := n = 3.
Check is_three : nat -> Prop.

Polymorfná vlastnosť

Injektívnosť môžeme vyjadriť pre funkcie medzi ľubovoľnými typmi A a B. Definícia injective pomenúva túto vlastnosť; lema succ_inj dokazuje, že ju má konštruktor S.

Definition injective {A B} (f : A -> B) : Prop :=
  forall x y : A, f x = f y -> x = y.
Lemma succ_inj : injective S.
Proof.
  unfold injective. (* nie je nutné rozbaliť injective *)
  intros x y H.
  injection H as H1.
  apply H1.
Qed.

Rovnosť

Rovnosť eq, zapisovaná ako =, je polymorfne definovaný logický vzťah. Pre ľubovoľný typ A vytvorí z dvoch prvkov typu A tvrdenie v Prop. Zápis @eq sprístupní aj implicitný argument určujúci typ:

Check @eq : forall A : Type, A -> A -> Prop.

Logické spojky v Rocq

Konjunkcia: `P /\ Q`

Konjunkcia tvrdí, že platí P aj Q. Pri cieli P /\ Q potrebujeme oba dôkazy. Taktika split vytvorí dva podciele, jeden pre každú zložku.

Ako dokázať konjunkciu (split):

Lemma and_example : forall P Q : Prop,
  P -> Q -> P /\ Q.
Proof.
  intros P Q HP HQ.
  split.
  - (* ============================
       Prvý podcieľ: dokázať P

       P, Q : Prop
       HP : P
       HQ : Q
       ============================
       P *)

    apply HP.

  - (* ============================
       Druhý podcieľ: dokázať Q

       P, Q : Prop
       HP : P
       HQ : Q
       ============================
       Q *)
    apply HQ.
Qed.

Ak máme konjunkciu v hypotéze, získame oba dôkazy pomocou destruct H as [HP HQ]:

Lemma and_elim_left : forall P Q : Prop,
  P /\ Q -> P.
Proof.
  intros P Q H.
  (* H : P /\ Q
     ============================
     P *)

  destruct H as [HP HQ].
  (* ============================
     Rozložíme konjunkciu na oba dôkazy.

     HP : P
     HQ : Q
     ============================
     P *)

  apply HP.                (* použijeme ľavú časť *)
Qed.

Rozbor konjunkcie nevytvára dve vetvy: poskytne HP aj HQ v jednom kontexte. Na dôkaz ľavej zložky potom použijeme HP.

Disjunkcia: `P \/ Q`

Na dôkaz disjunkcie stačí dokázať jednu zo strán. Taktika left zvolí cieľ P, taktika right cieľ Q:

Lemma or_example_left : forall P Q : Prop,
  P -> P \/ Q.
Proof.
  intros P Q HP.
  left.       (* zvolíme ľavú vetvu *)
  apply HP.
Qed.

Lemma or_example_right : forall P Q : Prop,
  Q -> P \/ Q.
Proof.
  intros P Q HQ.
  right.      (* zvolíme pravú vetvu *)
  apply HQ.
Qed.

Ak máme H : P \/ Q v kontexte, nevieme všeobecne zvoliť, ktorá strana platí. Príkaz destruct H as [HP | HQ] vytvorí dve vetvy a v každej musíme dokázať pôvodný cieľ. Disjunkcia pripúšťa aj platnosť oboch strán.

Príklad:

Lemma disj_in_context :
  forall P Q R : Prop, P \/ Q -> (P -> R) -> (Q -> R) -> R.
Proof.
  intros P Q R H HPtoR HQtoR.
  destruct H as [HP | HQ].   (* rozdelíme prípady *)
  - (* ============================
       Prvá vetva: predpokladáme P

       HP : P
       HPtoR : P -> R
       HQtoR : Q -> R
       ============================
       R *)

    apply HPtoR. exact HP.
  - (* ============================
       Druhá vetva: predpokladáme Q

       HQ : Q
       HPtoR : P -> R
       HQtoR : Q -> R
       ============================
       R *)

    apply HQtoR. exact HQ.
Qed.

Implikácia: `P -> Q`

Implikáciu dokážeme tak, že zavedieme predpoklad HP : P pomocou intros HP a dokážeme Q. Ak už máme hypotézu H : P -> Q, môžeme ju použiť spätne na cieľ Q pomocou apply H, alebo dopredne na hypotézu HP : P pomocou apply H in HP.

Ako dokázať implikáciu:

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

  apply H.
  (* ============================
     Na dôkaz Q pomocou H zostáva dokázať P.

     P, Q : Prop
     H : P -> Q
     HP : P
     ============================
     P *)

  apply HP.
Qed.

Negácia a `False`

Negácia ~P je definovaná ako P -> False. Pri cieli ~P preto príkaz intros HP zavedie predpoklad HP : P a zostane dokázať False z dostupných hypotéz. V nasledujúcom príklade tento krok zabezpečuje posledný argument príkazu intros P H HP.

Ako dokázať negáciu:

Lemma not_example : forall P : Prop,
  (P -> False) -> ~P.
Proof.
  intros P H HP.
  (* P : Prop
     H : P -> False
     HP : P
     ============================
     False *)

  apply H.
  (* ============================
     Na odvodenie False pomocou H zostáva dokázať P.

     P : Prop
     H : P -> False
     HP : P
     ============================
     P *)

  apply HP.
Qed.

Samotné destruct HP nie je všeobecný postup dokazovania negácie. Pomôže iba vtedy, keď štruktúra konkrétneho tvrdenia P umožňuje rozborom odvodiť spor. Pri ľubovoľnom P : Prop takýto postup nemáme.

Tvrdenie False nemá žiadny konštruktor. Ak máme jeho dôkaz v kontexte, destruct nevytvorí žiadnu vetvu a uzavrie ľubovoľný cieľ. Ide o princíp explózie:

Lemma absurd_example : forall P : Prop, False -> P.
Proof.
  intros P H.
  destruct H.   (* z False môžeme dokázať čokoľvek *)
Qed.

Alternatívne:

Lemma absurd_example' : forall P : Prop, False -> P.
Proof.
  intros P H.
  contradiction.
Qed.

Pravdivé tvrdenie `True`

True je induktívne tvrdenie v sorte Prop s konštruktorom I : True. Preto ho môžeme dokázať príkazom exact I, apply I alebo taktikou constructor.

Ako dokázať True:

Lemma true_example : True.
Proof.
  apply I.   (* I je dôkazom True *)
Qed.

Ekvivalencia: `P <-> Q`

Ekvivalencia vyjadruje platnosť oboch implikácií P -> Q a Q -> P. Taktika split vytvorí tieto dva podciele.

Ako dokázať ekvivalenciu:

Lemma iff_example : forall P Q : Prop,
  (P -> Q) -> (Q -> P) -> (P <-> Q).
Proof.
  intros P Q H1 H2.
  (* P, Q : Prop
     H1 : P -> Q
     H2 : Q -> P
     ============================
     P <-> Q *)

  split.
  - apply H1.   (* dokážeme P -> Q *)
  - apply H2.   (* dokážeme Q -> P *)
Qed.

Hypotézu H : P <-> Q môžeme rozložiť pomocou destruct H as [HPQ HQP]. Získame HPQ : P -> Q a HQP : Q -> P, ktoré používame ako bežné implikácie.

Existenčný kvantifikátor: `exists n, P n`

Na dôkaz existencie zvolíme svedka, teda prvok príslušného typu, a dokážeme, že má požadovanú vlastnosť. Príkaz exists 0 zmení cieľ exists n, P n na P 0:

Lemma exists_example : forall P : nat -> Prop,
  P 0 -> exists n, P n.
Proof.
  intros P H.
  (* P : nat -> Prop
     H : P 0
     ============================
     exists n : nat, P n *)

  exists 0.
  (* ============================
     Určíme konkrétnu hodnotu

     H : P 0
     ============================
     P 0 *)

  apply H.
Qed.

Lemma exists_example2 : exists n : nat, n = 3.
Proof.
  exists 3.
  reflexivity.
Qed.

Ak máme existenciu v hypotéze H : exists x, P x, príkaz destruct H as [x Hx] poskytne svedka x a dôkaz Hx : P x. Nemusíme pritom poznať číselnú hodnotu svedka. Nasledujúci príklad využije aj ďalšiu informáciu o ňom: svedok spĺňa P a rovná sa číslu tri.

Lemma exists_simple_example :
  forall (P : nat -> Prop),
    (exists n, P n /\ n = 3) -> P 3.
Proof.
  intros P H.
  destruct H as [n Hn].
  (* n : nat
     Hn : P n /\ n = 3
     ============================
     P 3 *)

  destruct Hn as [HP Heq].
  (* HP : P n
     Heq : n = 3
     ============================
     P 3 *)

  rewrite <- Heq.
  (* ============================
     P n *)
  exact HP.
Qed.

Najprv eliminujeme existenčný kvantifikátor a potom rozložíme konjunkciu. Rovnosť Heq umožní nahradiť 3 v cieli svedkom n, takže použijeme získaný dôkaz HP. Oba rozbory možno zapísať aj jedným príkazom destruct H as [n [HP Heq]].

Negácia, `exfalso` a spor v kontexte

Nasledujúce príklady používajú knižničnú definíciu not P := P -> False; znova ju nedeklarujeme. Taktika unfold not ju explicitne rozbalí. Samotné rozbalenie definície ešte spor nedokazuje: potrebujeme aj dôkaz jej predpokladu.

Rozbalenie negácie v hypotéze

Lemma not_example1 : forall P : Prop, ~P -> P -> False.
Proof.
  intros P HnotP HP.
  (* P : Prop
     HnotP : ~P
     HP : P
     ============================
     False *)

  unfold not in HnotP.
  (* ============================
     Rozbalíme definíciu not: ~P je P -> False

     P : Prop
     HnotP : P -> False
     HP : P
     ============================
     False *)

  apply HnotP.
  exact HP.
Qed.

Negácia zloženého tvrdenia

Pri ~(P /\ Q) potrebujeme zostaviť dôkaz celej konjunkcie, aby sme odvodili False.

Lemma not_example2 :
  forall P Q : Prop, ~(P /\ Q) -> P -> Q -> False.
Proof.
  intros P Q HnotPQ HP HQ.
  unfold not in HnotPQ.
  (* rozbalíme ~(P /\ Q) na (P /\ Q) -> False *)
  apply HnotPQ.
  split; assumption.
Qed.

Taktika `exfalso`

Taktika exfalso nahradí aktuálny cieľ cieľom False. Ak dokážeme False z dostupných predpokladov, princíp ex falso poskytne dôkaz pôvodného cieľa. Nepredpokladáme pritom negáciu cieľa a nepoužívame klasický dôkaz sporom.

Lemma exfalso_example : forall P Q : Prop, P -> ~P -> Q.
Proof.
  intros P Q HP HnotP.
  unfold not in HnotP.
  exfalso.          (* meníme cieľ Q na cieľ False *)
  (* HP : P
     HnotP : P -> False
     ============================
     False *)
  apply HnotP.
  exact HP.
Qed.

`False` priamo v kontexte

Ak už máme Hfalse : False, môžeme použiť contradiction alebo prejsť pomocou exfalso na cieľ, ktorého dôkaz je priamo v kontexte:

Lemma false_in_context : forall P : Prop, False -> P.
Proof.
  intros P Hfalse.
  contradiction.     (* z False ide dokázať čokoľvek *)
Qed.

Alternatíva s exfalso.

Lemma false_in_context_alt : forall P : Prop, False -> P.
Proof.
  intros P Hfalse.
  exfalso. exact Hfalse.
Qed.

Negácia rovnosti: `a <> b`

V Rocq je a <> b len skratka za ~(a = b), čo je teda (a = b) -> False. Preto aj tu môžeme použiť unfold not.

Lemma neq_unfold_example : forall (A : Type) (a b : A),
  a <> b -> a = b -> False.
Proof.
  intros A a b Hneq Heq.
  unfold not in Hneq.
  (* rozbalíme a <> b na (a = b) -> False *)
  apply Hneq.
  exact Heq.
Qed.

Použitie negácie rovnosti v dôkaze

Lemma neq_contradiction_example : forall (n m : nat),
  n <> m -> n = m -> 2 + 2 = 5.
Proof.
  intros n m Hneq Heq.
  unfold not in Hneq.
  exfalso.           (* cieľ 2 + 2 = 5 nahradíme cieľom False *)
  apply Hneq.
  exact Heq.
Qed.

Programovanie s tvrdeniami

Rekurzívny predikát príslušnosti do zoznamu

Funkcia môže rekurzívne zostavovať aj tvrdenie v Prop. Predikát my_In x l vyjadruje, že prvok x patrí do zoznamu l. Názov my_In odlišuje našu výučbovú definíciu od knižničného In.

Do prázdneho zoznamu nepatrí žiadny prvok, preto táto vetva vracia False. Pri x' :: l' požadujeme, aby sa x rovnal hlave alebo patril do chvosta. Rekurzia postupuje podľa štruktúry zoznamu a výsledkom je tvrdenie, nie booleovský test.

Fixpoint my_In {A : Type} (x : A) (l : list A) : Prop :=
  match l with
  | [] => False
  | x' :: l' => x' = x \/ my_In x l'
  end.

Example In_example_1 : my_In 4 [1;2;3;4;5].
Proof.
  simpl.
  (* ============================
     1 = 4 \/ 2 = 4 \/ 3 = 4 \/ 4 = 4 \/ 5 = 4 \/ False *)

  right.
  (* ============================
     2 = 4 \/ 3 = 4 \/ 4 = 4 \/ 5 = 4 \/ False *)

  right. right. left.
  (* ============================
     4 = 4 *)

  reflexivity.
Qed.

Example In_example_2 :
  forall n, my_In n [2;4] -> exists n', n = 2 * n'.
Proof.
  simpl. intros n [H | [H | []]].
  (* Rozbor disjunkcie: 2 = n, 4 = n alebo False.
     Prípad False sa uzavrie prázdnym vzorom []; zostanú dve vetvy. *)
  - (* ============================
       Prvá vetva: n = 2

       H : 2 = n
       ============================
       exists n' : nat, n = n' + (n' + 0) *)

    exists 1. rewrite <- H. reflexivity.
  - (* ============================
       Druhá vetva: n = 4

       H : 4 = n
       ============================
       exists n' : nat, n = n' + (n' + 0) *)

    exists 2. rewrite <- H. reflexivity.
Qed.

Zachovanie príslušnosti pri mapovaní

Ak x patrí do l, potom f x patrí do map f l. Dôkaz spája indukciu podľa zoznamu s rozborom logického tvrdenia o príslušnosti. Pri neprázdnom zozname rozlišujeme, či je prvok v hlave alebo v chvoste; v druhom prípade využijeme indukčný predpoklad.

Theorem In_map :
  forall (A B : Type) (f : A -> B) (l : list A) (x : A),
    my_In x l -> my_In (f x) (map f l).
Proof.
  intros A B f l x.
  induction l as [|x' l' IH].
  - (* ============================
       Základný prípad: prázdny zoznam

       f : A -> B
       x : A
       ============================
       my_In x [] -> my_In (f x) (map f []) *)

    simpl. intros [].
  - (* ============================
       Indukčný krok: neprázdny zoznam

       f : A -> B
       x' : A
       l' : list A
       x : A
       IH : my_In x l' -> my_In (f x) (map f l')
       ============================
       my_In x (x' :: l') -> my_In (f x) (map f (x' :: l')) *)

    simpl. intros [H | H].
    + (* ============================
         Prvok sa rovná hlave zoznamu.

         ...
         H : x' = x
         ============================
         f x' = f x \/ my_In (f x) (map f l') *)

      left. rewrite H. reflexivity.
    + (* ============================
         Prvok patrí do chvosta zoznamu.

         ...
         H : my_In x l'
         ============================
         f x' = f x \/ my_In (f x) (map f l') *)

      right. apply IH. apply H.
Qed.

Konštruktívna a klasická logika

V základnej konštruktívnej logike Rocqu nie je všeobecný zákon vylúčeného tretieho forall Q : Prop, Q \/ ~Q dokázateľný bez dodatočných axióm. To neznamená, že je nepravdivý. Znamená to, že pre ľubovoľné tvrdenie nemáme všeobecný konštruktívny dôkaz jednej z týchto možností.

Pre rozhodnuteľné tvrdenia môžeme Q \/ ~Q dokázať konštruktívne. Napríklad pri rovnosti prirodzených čísel rozoberieme výsledok testu n =? m a pomocou Nat.eqb_eq alebo Nat.eqb_neq získame rovnosť alebo jej negáciu. Tento prechod od výpočtu k tvrdeniu sme už použili v príklade s remember.

Aj pre konkrétne tvrdenie, ktoré už vieme dokázať, môžeme zvoliť ľavú stranu disjunkcie. Nasledujúca definícia pomenúva takéto tvrdenie; samotné Check ho však nedokazuje:

Definition P := forall n : nat, n = n.
Check P : Prop.

Použitie klasického princípu

Knižnica Classical poskytuje princíp classic. Načítame ju mimo modulu a jej krátke názvy importujeme iba v module ClassicalExamples. Tým klasický príklad prehľadne oddelíme. Modul však neodstraňuje závislosť dôkazu od klasickej axiómy.

From Stdlib Require Logic.Classical.

Module ClassicalExamples.
Import Classical.

Check classic : forall P : Prop, P \/ ~P.

Lemma excluded_middle_example : forall Q : Prop, Q \/ ~Q.
Proof.
  intros Q.
  apply classic.
Qed.

End ClassicalExamples.

Lema ClassicalExamples.excluded_middle_example používa klasický princíp, nejde teda o konštruktívny dôkaz všeobecného zákona vylúčeného tretieho. Príkaz Qed overí dôkaz vzhľadom na použité predpoklady; nezaručuje, že dôkaz nevyužíva axiómy. Závislosti môžeme zobraziť:

Print Assumptions ClassicalExamples.excluded_middle_example.

Záverečný príklad: kombinovanie implikácií

Z predpokladu A získame pomocou G dôkaz B. Hypotéza F potom z dôkazov A a B poskytne dôkaz C. Dôkaz postupuje od cieľa: aplikácia F najprv vytvorí podciele A a B.

Lemma example6 :
  forall A B C : Prop, (A -> B -> C) -> (A -> B) -> (A -> C).
Proof.
  intros A B C F G H.
  (* F : A -> B -> C
     G : A -> B
     H : A
     ============================
     C *)
  apply F.
  - assumption.
  - apply G. assumption.
Qed.

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

Logické konštrukcie v cieli a v hypotéze

Tvar	Ak je v cieli	Ak je v hypotéze `H`
`P -> Q`	`intros HP` zavedie `HP : P`; zostane `Q`.	`apply H` na cieľ `Q` vytvorí cieľ `P`; `apply H in HP` získa `Q` z `HP : P`.
`forall x : A, P x`	`intros x` zavedie ľubovoľné `x : A`.	`specialize H with (x := t)` dosadí `t : A`.
`P /\ Q`	`split` vytvorí podciele `P` a `Q`.	`destruct H as [HP HQ]` poskytne oba dôkazy.
`P \/ Q`	`left` zvolí `P`, `right` zvolí `Q`.	`destruct H as [HP \| HQ]` vytvorí dve vetvy.
`~P`, teda `P -> False`	`intros HP` zavedie `P`; potom treba odvodiť `False`.	Spolu s `HP : P` poskytne dôkaz `False`, napríklad pomocou `apply H in HP`.
`True`	`exact I` použije konštruktor.	Jeho rozbor nepridá žiadnu podstatnú informáciu.
`P <-> Q`	`split` vytvorí ciele `P -> Q` a `Q -> P`.	`destruct H as [HPQ HQP]` poskytne oba smery.
`exists x, P x`	`exists t` zvolí svedka; zostane `P t`.	`destruct H as [x Hx]` poskytne svedka a dôkaz `Hx : P x`.

Pri práci s logickými spojkami rozlišujeme konštrukciu dôkazu v cieli a využitie dôkazu v hypotéze. Konjunkcia poskytuje oba dôkazy, disjunkcia vedie k rozboru prípadov a existenčné tvrdenie k získaniu svedka a jeho vlastnosti. Tieto postupy sme spojili s indukciou v dôkaze zachovania príslušnosti pri mapovaní zoznamu.

Tvrdenia v Prop a výpočty v bool majú odlišné úlohy; knižničné lemy umožňujú prechádzať od výsledku testu k logickému tvrdeniu. Konštruktívne dôkazy sme odlíšili od klasického príkladu, ktorý výslovne používa dodatočnú axiómu.

Podrobnosti k jednotlivým príkazom nájdete v oficiálnej dokumentácii Rocq 9.1.1: taktiky a práca s rovnosťami.

Logika v Rocq

Ciele

Obsah

Potrebné knižnice

Logika v Rocq

Booleovské výpočty a logické tvrdenia

Tvrdenia a ich dôkazy

Tvrdenie v teoréme

Pomenované tvrdenia

Predikáty

Polymorfná vlastnosť

Rovnosť

Logické spojky v Rocq

Konjunkcia: `P /\ Q`

Disjunkcia: `P \/ Q`

Implikácia: `P -> Q`

Negácia a `False`

Pravdivé tvrdenie `True`

Ekvivalencia: `P <-> Q`

Existenčný kvantifikátor: `exists n, P n`

Negácia, `exfalso` a spor v kontexte

Rozbalenie negácie v hypotéze

Negácia zloženého tvrdenia

Taktika `exfalso`

`False` priamo v kontexte

Negácia rovnosti: `a <> b`

Použitie negácie rovnosti v dôkaze

Programovanie s tvrdeniami

Rekurzívny predikát príslušnosti do zoznamu

Zachovanie príslušnosti pri mapovaní

Konštruktívna a klasická logika

Použitie klasického princípu

Záverečný príklad: kombinovanie implikácií

Ako si vybrať správnu taktiku?

Logické konštrukcie v cieli a v hypotéze

Zhrnutie

Logika v Rocq

Ciele

Obsah

Potrebné knižnice

Logika v Rocq

Booleovské výpočty a logické tvrdenia

Tvrdenia a ich dôkazy

Tvrdenie v teoréme

Pomenované tvrdenia

Predikáty

Polymorfná vlastnosť

Rovnosť

Logické spojky v Rocq

Konjunkcia: P /\ Q

Disjunkcia: P \/ Q

Implikácia: P -> Q

Negácia a False

Pravdivé tvrdenie True

Ekvivalencia: P <-> Q

Existenčný kvantifikátor: exists n, P n

Negácia, exfalso a spor v kontexte

Rozbalenie negácie v hypotéze

Negácia zloženého tvrdenia

Taktika exfalso

False priamo v kontexte

Negácia rovnosti: a <> b

Použitie negácie rovnosti v dôkaze

Programovanie s tvrdeniami

Rekurzívny predikát príslušnosti do zoznamu

Zachovanie príslušnosti pri mapovaní

Konštruktívna a klasická logika

Použitie klasického princípu

Záverečný príklad: kombinovanie implikácií

Ako si vybrať správnu taktiku?

Logické konštrukcie v cieli a v hypotéze

Zhrnutie

Konjunkcia: `P /\ Q`

Disjunkcia: `P \/ Q`

Implikácia: `P -> Q`

Negácia a `False`

Pravdivé tvrdenie `True`

Ekvivalencia: `P <-> Q`

Existenčný kvantifikátor: `exists n, P n`

Negácia, `exfalso` a spor v kontexte

Taktika `exfalso`

`False` priamo v kontexte

Negácia rovnosti: `a <> b`