Domácí úkoly 2:

From Coq Require Import Lists.List.
From Coq Require Import PeanoNat.
Import List.ListNotations.
Import PeanoNat.Nat.

Příklad A: 1 bod

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.

☐

Příklad B: 2 body

Vezměme si následující dva induktivně definované typy Arith_expr_1 a Arith_expr_2, které oba mohou být použity pro reprezentaci aritmetických výrazů tvořených konstantami typu nat a operacemi plus, mínus a krát.

Inductive Arith_expr_1 :=
    | AE1_Num : nat → Arith_expr_1
    | AE1_Plus : Arith_expr_1 → Arith_expr_1 → Arith_expr_1
    | AE1_Minus : Arith_expr_1 → Arith_expr_1 → Arith_expr_1
    | AE1_Times : Arith_expr_1 → Arith_expr_1 → Arith_expr_1.

Inductive arith_op := Plus | Minus | Times.

Inductive Arith_expr_2 :=
    | AE2_Num : nat → Arith_expr_2
    | AE2_BinOp : Arith_expr_2 → arith_op → Arith_expr_2 → Arith_expr_2.

Pro oba tyto datové typy navrhněte funkce, které provedou vyhodnocení daného výrazu, tj. vrátí jako výsledek hodnotu typu nat, která bude výsledkem vyhodnocení všech aritmetických operací tvořících daný výraz.

Fixpoint eval_ae_1 (e : Arith_expr_1) : nat
. Admitted.

Fixpoint eval_ae_2 (e : Arith_expr_2) : nat
. Admitted.

Otestujte vaše implementace těchto funkcí na několika jednoduchých příkladech:

Example eval_ae_1_ex1 : eval_ae_1 (AE1_Num 5) = 5.
Admitted.

Example eval_ae_1_ex2 : eval_ae_1 (AE1_Plus (AE1_Num 1) (AE1_Num 1)) = 2.
Admitted.

Example eval_ae_1_ex3 : eval_ae_1
(AE1_Minus (AE1_Times (AE1_Num 3) (AE1_Num 7)) (AE1_Num 4)) = 17.
Admitted.

Example eval_ae_2_ex1 : eval_ae_2 (AE2_Num 5) = 5.
Admitted.

Example eval_ae_2_ex2 : eval_ae_2 (AE2_BinOp (AE2_Num 1) Plus (AE2_Num 1)) = 2.
Admitted.

Example eval_ae_2_ex3 : eval_ae_2
(AE2_BinOp (AE2_BinOp (AE2_Num 3) Times (AE2_Num 7)) Minus (AE2_Num 4)) = 17.
Admitted.

Navrhněte funkci ae1_to_ae2, která transformuje aritmetický výraz z formátu reprezentovaného typem Arith_expr_1 do tvaru reprezentovaného typem Arith_expr_2, a podobnou funkci ae2_to_ae1, která bude provádět transformaci opačným směrem.

Fixpoint ae1_to_ae2 (e : Arith_expr_1) : Arith_expr_2
. Admitted.

Fixpoint ae2_to_ae1 (e : Arith_expr_2) : Arith_expr_1
. Admitted.

Ukažte, že tyto dvě funkce ae1_to_ae2 a ae2_to_ae1 jsou vzájemně inverzní (tj. že jejich složením v jednom či druhém směru dostaneme vždy původní aritmetický výraz).

Theorem ae1_ae2_inv : ∀ a : Arith_expr_1,
ae2_to_ae1 (ae1_to_ae2 a) = a.
Proof.
Admitted.

Theorem ae2_ae1_inv : ∀ a : Arith_expr_2,
ae1_to_ae2 (ae2_to_ae1 a) = a.
Proof.
Admitted.

☐

Příklad C: 1 bod

Mnoho běžných funkcí na seznamech je možno implementovat pomocí následující funkce fold:

Module Fold_exercises.

Fixpoint fold {X Y: Type} (f : X→Y→Y) (l : list X) (b : Y) : Y :=
  match l with
  | nil ⇒ b
  | h :: t ⇒ f h (fold f t b)
  end.

Například zde je alternativní definice funkce length počítající délku seznamu:

Definition fold_length {X : Type} (l : list X) : nat :=
fold (fun _ n ⇒ S n) l 0.

Example test_fold_length1 : fold_length [4;7;0] = 3.
Proof. reflexivity. Qed.

Dokažte korektnost funkce fold_length.

Theorem fold_length_correct : ∀ X (l : list X),
fold_length l = length l.
Proof.
Admitted.

Rovněž funkce map může být definována pomocí fold. Doplňte níže uvedenou definici funkce fold_map tak, aby volala pouze funkci fold a sama nepoužívala rekurzi.

Definition fold_map {X Y: Type} (f: X → Y) (l: list X) : list Y
. Admitted.

Napište v Coqu teorém fold_map_correct, který bude říkat, že funkce fold_map je korektní, tj. že funkce fold_map vrací stejné výsledky jako funkce map definovaná ve standardní knihovně (v Coq.Lists.List) a dokažte tento teorém.

End Fold_exercises.

☐

Příklad D: 1 bod

Dokažte následující tvrzení:

Theorem impl_th1 : ∀ P Q R : Prop,
    (P → Q) → (Q → R) → (P → R).
Proof.
Admitted.

Theorem impl_th2 : ∀ P Q R : Prop,
    (P → Q → R) → (Q → P → R).
Proof.
Admitted.

Theorem impl_th3 : ∀ P Q R : Prop,
    (P → Q → R) → (P → Q) → (P → R).
Proof.
Admitted.

Theorem contrapositive : ∀ P Q : Prop,
    (P → Q) → (~Q → ¬P).
Proof.
Admitted.

Theorem not_both_true_and_false : ∀ P : Prop,
    ~(P ∧ ¬P).
Proof.
Admitted.

Theorem neg_neg_neg_impl_neg : ∀ P : Prop,
    ~~~P → ¬P.
Proof.
Admitted.

Theorem de_morgan_not_or : ∀ (P Q : Prop),
    ¬ (P ∨ Q) → ¬P ∧ ¬Q.
Proof.
Admitted.

Theorem or_distributes_over_and : ∀ P Q R : Prop,
  P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R).
Proof.
Admitted.

Theorem dist_exists_or : ∀ (X:Type) (P Q : X → Prop),
  (∃ x, P x ∨ Q x) ↔ (∃ x, P x) ∨ (∃ x, Q x).
Proof.
Admitted.

☐

This page has been generated by coqdoc