Domácí úkoly 1:

Příklad A: 1 bod

Příkaz Admitted slouží k označení nehotového důkazu. V následujících příkladech je použit v místech, která je třeba dodělat. Úkolem je tedy nahradit tento příkaz skutečným řešením.

Odstraňte příkaz "Admitted." a doplňte definice následující funkce nandb. Poté ověřte, že tvrzení uvedená v následujících Examples skutečně platí a mohou být ověřena Coqem. (Tj. odstraňte v nich "Admitted." a nahraďte je skutečnými důkazy ukončenými "Qed.".)

(Funkce nandb by měla vracet true právě tehdy, když alespoň jeden z jejích argumentů má hodnotu false.)

Definition nandb (b1:bool) (b2:bool) : bool
. Admitted.

Example test_nandb1: (nandb true true) = false.
Admitted.
Example test_nandb2: (nandb true false) = true.
Admitted.
Example test_nandb3: (nandb false true) = true.
Admitted.
Example test_nandb4: (nandb false false) = true.
Admitted.

Udělejte totéž pro následující funkci norb.

(Funkce norb by měla vracet true právě tehdy, jestliže oba argumenty mají hodnotu false.)

Definition norb (b1:bool) (b2:bool) : bool
. Admitted.

Example test_norb1: (norb true true) = false.
Admitted.
Example test_norb2: (norb true false) = false.
Admitted.
Example test_norb3: (norb false true) = false.
Admitted.
Example test_norb4: (norb false false) = true.
Admitted.

Udělejte totéž pro následující funkci andb3. Tato funkce by měla vracet true právě tehdy, když všechny tři argumenty mají hodnotu true.)

Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool
. Admitted.

Example test_andb31: (andb3 true true true) = true.
Admitted.
Example test_andb32: (andb3 false true true) = false.
Admitted.
Example test_andb33: (andb3 true false true) = false.
Admitted.
Example test_andb34: (andb3 true true false) = false.
Admitted.

☐

Příklad B: 2 body

Místo unární reprezentace přirozených čísel je možné definovat efektivnější binární reprezentaci, kde binárně zapsané číslo budeme reprezentovat jako sekvenci konstruktorů B0 a B1 (které reprezentují nuly a jedničky), která je ukončena konstruktorem Z. Ve srovnání s tím vypadá unární reprezentace jako sekvence konstruktorů S ukončená konstruktorem O.

Například:

       desítkově             binárně                         unárně
           0                       Z                              O
           1                    B1 Z                            S O
           2                B0 (B1 Z)                        S (S O)
           3                B1 (B1 Z)                     S (S (S O))
           4            B0 (B0 (B1 Z))                 S (S (S (S O)))
           5            B1 (B0 (B1 Z))              S (S (S (S (S O))))
           6            B0 (B1 (B1 Z))           S (S (S (S (S (S O)))))
           7            B1 (B1 (B1 Z))        S (S (S (S (S (S (S O))))))
           8        B0 (B0 (B0 (B1 Z)))    S (S (S (S (S (S (S (S O)))))))

Všimněte si, že nejméně významný bit je uveden vlevo a nejvýznamnější bit je vpravo --- binární čísla jsou obvykle zapisována v opačném pořadí. Zde zvolené pořadí umožňuje snadnější manipulaci s čísly při definování různých matematických operací.

Inductive bin : Type :=
  | Z
  | B0 (n : bin)
  | B1 (n : bin).

Doplňte definice níže uvedené funkce incr, která zvetší hodnotu čísla o jedna, a funkce bin_to_nat, která provede konverzi binárního čísla na unární.

Fixpoint incr (m:bin) : bin
. Admitted.

Fixpoint bin_to_nat (m:bin) : nat
. Admitted.

Pokud jste tyto funkce pro zvetšení binárního čísla o jedna a převod binárního čísla na unární definovali správně, následující "unit testy" by měly projít. Tyto unit testy samozřejmě plně neprokazují korektnost vaší implementace!

Example test_bin_incr1 : (incr (B1 Z)) = B0 (B1 Z).
Admitted.

Example test_bin_incr2 : (incr (B0 (B1 Z))) = B1 (B1 Z).
Admitted.

Example test_bin_incr3 : (incr (B1 (B1 Z))) = B0 (B0 (B1 Z)).
Admitted.

Example test_bin_incr4 : bin_to_nat (B0 (B1 Z)) = 2.
Admitted.

Example test_bin_incr5 :
bin_to_nat (incr (B1 Z)) = 1 + bin_to_nat (B1 Z).
Admitted.

Example test_bin_incr6 :
bin_to_nat (incr (incr (B1 Z))) = 2 + bin_to_nat (B1 Z).
Admitted.

Další bonusový bod (k výše uvedeným dvěma bodům) dostanete, pokud se vám podaří dokázat následující tvrzení:

Theorem bin_to_nat_pres_incr : ∀ b : bin,
bin_to_nat (incr b) = 1 + bin_to_nat b.
Proof.
Admitted.

☐

Příklad C: 2 body

Pomocí indukce dokažte následující čtyři tvrzení.

(V této posloupnosti čtyř tvrzení může být u některých z nich výhodné v důkazu využít některé z předchozích tvrzení z této čtveřice.)

Pokud budete potřebovat pro tyto důkazy nějaká pomocná tvrzení, tak je dokažte jako Lemma.

Theorem mul_0_r : ∀ n:nat,
  n × 0 = 0.
Proof.
Admitted.

Theorem plus_n_Sm : ∀ n m : nat,
  S (n + m) = n + (S m).
Proof.
Admitted.

Theorem add_comm : ∀ n m : nat,
  n + m = m + n.
Proof.
Admitted.

Theorem add_assoc : ∀ n m p : nat,
  n + (m + p) = (n + m) + p.
Proof.
Admitted.

☐

This page has been generated by coqdoc