Domácí úkoly 2:

Příklad A: 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.

☐

Příklad B: 2 body

Uvažujme následují dvě funkce sum_rec a sum_iter, které obě spočítají jako výsledek součet všech čísel v seznamu typu natlist. (Přičemž funkce sum_iter používá při výpočtu pomocnou funkci sum_iter_loop.)

Module natlist_sum.

Inductive natlist :=
    | nil : natlist
    | cons : nat → natlist → natlist.

Notation "x :: l" := (cons x l) (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).

Fixpoint sum_rec (l : natlist) : nat :=
    match l with
    | [ ] ⇒ 0
    | x :: l' ⇒ x + sum_rec l'
    end.

Fixpoint sum_iter_loop (l : natlist) (acc : nat) : nat :=
    match l with
    | [ ] ⇒ acc
    | x :: l' ⇒ sum_iter_loop l' (acc + x)
    end.

Definition sum_iter (l : natlist) := sum_iter_loop l 0.

Dokažte, že obě funkce vrací pro jakýkoli vstup vždy stejný výsledek.

Theorem sum_rec_sum_item_eq : ∀ l : natlist,
sum_rec l = sum_iter l.
Proof.
Admitted.

End natlist_sum.

☐

This page has been generated by coqdoc