exercises_1

Exercises sheet 1: Type Theory as a Mathematical Language

In this exercise sheet we will work over the fundamentals of functional programming and dependent types.
First, we declare our usual prelude:
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definition fixme {T} : T. Admitted.

Commands and syntax

  • Exercise: what is the type of the equality 3 + 4 = 9
Check fixme.
  • Exercise: complete the definition of these functions
Definition apply_two_parameters (f : nat → nat) (n : nat) : nat := fixme.
Definition apply_two_parameters_using_fun : (nat → nat) → nat → nat := fixme.
  • Exercise: use proof by computation to test the functions behave as intended, for a return value of 4
Definition check_ap : _ := erefl 4.
  • Exercise: write a function that takes two functions and returns their composition
Definition fun_comp (T U V : Type) (f : T → U) (g : U → V) : T → V := fixme.

Booleans:

  • Exercise: Complete the below function implementing negation, write a test for it
Definition notb (b : bool) : bool := fixme.
Fail Definition notb_test _ := fixme.
  • Exercise: Implement xor, write a test for it
Definition xorb (b1 b2 : bool) : bool := fixme.
Fail Definition xorg_test _ := fixme.

Propositions:

  • Exercise: write a function orC : or A B → or B A that flips or.
Definition orC (P Q : Prop) : or P Q → or Q P := fixme.
  • Exercise: complete proj2, which will return the proof of B from A ∧ B
As an example, we provide proj1 which returns the proof of A from A ∧ B
Definition proj1 (A B : Prop) (H : and A B) : A :=
  match H with
  | conj pA pB ⇒ pA
  end.

Definition proj2 (A B : Prop) (H : and A B) : B := fixme.
  • Exercise: complete the function ex_wit which extracts the witness from an existential
Print sig.
Definition ex_wit T (x : T) (P : T → Prop) : { x : T | P x } → T := fixme.
  • Exercise: complete the following function
Definition forall_dist T (P Q : T → Prop) :
  (∀ (x : T), P x ∧ Q x) →
  (∀ (x : T), P x) ∧ (∀ (x : T), Q x) := fixme.
  • Exercise: complete the following function
Print not.
Definition not_not_a (P : Prop) : P → ¬ (~ P) := fixme.

natural numbers

  • Exercise: Define multiplicaton of naturals.
Print nat.
Fixpoint nat_mul (m n : nat) : nat := fixme.
Compute (nat_mul 3 3).

  • Exercise: recall the weird_natural definition from the
lesson. Do you think it could work as a more efficient enconding than the usualy nat unary one? If so, how would that enconding be? Rename the constructors accordingly.
Inductive weird_natural : Type :=
  | zero' : weird_natural
  | succ' : weird_natural → weird_natural
  | weird : weird_natural → weird_natural → weird_natural.

  • Exercise: Complete the below function from weird_natural to nat
Definition to_nat (n : weird_natural) : nat := fixme.
  • Exercise: Complete the below function for addition of weird_natural
Fixpoint weird_add (n1 n2 : weird_natural) : weird_natural := fixme.
  • Exercise: Write a test ensuring that weird_add and to_nat commute
Fail Definition weird_add_test : _ := fixme.
  • Exercise: complete a division / remainder function
Fixpoint divn (n1 n2 : nat) : nat × nat := fixme.
  • Exercise: write a test for the above function using nat_mul
Fail Definition div_n_test : _ := fixme.

lists

Print list.
  • Exercise: complete the following function that transforms a list pointwise
Fixpoint map (A B : Type) (f : A → B) (l : seq A) : seq B := fixme.

  • Exercise: complete the following function that filters a list
Fixpoint filter (A : Type) (f : A → bool) (l : seq A) : seq A := fixme.
  • Exercise: filter a list of naturals to select the even numbers
Compute (filter _ [::1;2]).
  • Exercise: complete the following function that concatenates 2 lists
Fixpoint append (A : Type) (s1 s2 : seq A) : seq A := fixme.
  • Exercise: complete the following function that reverses a list
Fixpoint rev (A : Type) (s : seq A) : seq A := fixme.

Inductive types

  • Exercise: syntax for propositional logic. Complete the below inductive to add cases for and and or
Inductive form : Type :=
  | TT : form
  | FF : form
  | Not : form → form.
  • Exercise: eval. Complete the below evalution function for the extended syntax
Fixpoint eval_form (f : form) : bool :=
  match f with
  | TT ⇒ true
  | FF ⇒ true
  | Not f ⇒ eval_form f
  end.
Compute (eval_form (Not FF)).
  • Exercise: the above evalution function has some bugs; write a test that showcases it. What do you need to assume? Fix the evaluation function.

Fixpoint eval_form' (f : form) : bool :=
  match f with
  | TT ⇒ true
  | FF ⇒ true
  | Not f ⇒ eval_form f
  end.
Records
  • Exercise: write a record capturing the axioms of a group. Provide an instance for it.
Inductive group := .
State passing
  • Exercise: the definition of a function with state S from A to B is given below.
Complete the definition of function composition.
Definition fn_st S A B := A → S → B × S.

Definition fn_comp S A B C (f : fn_st S A B) (g: fn_st S B C) : fn_st S A C := fixme.