exercises_1_solved

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.

Commands and syntax

Exercise: what is the type of the equality 3 + 4 = 9

Check (3+4=9).

Exercise: complete the definition of these functions

Definition apply_two_parameters (f : nat → nat) (n : nat) : nat := f n.
Definition apply_two_parameters_using_fun : (nat → nat) → nat → nat := fun f n ⇒ f n.

Exercise: use proof by computation to test the functions behave as intended, for a return value of 4

Definition check_ap :
apply_two_parameters_using_fun (fun x ⇒ x + x) 2 = 4 := 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 := fun x ⇒ g (f x).

Booleans:

Exercise: Complete the below function implementing negation, write a test for it

Definition notb (b : bool) : bool := match b with | true ⇒ false | false ⇒ true end.
Definition notb_test1 : notb true = false := erefl.
Definition notb_test2 : notb false = true := erefl.

Exercise: Implement xor, write a test for it

Definition xorb (b1 b2 : bool) : bool :=
  match b1, b2 with
  | true, true ⇒ false
  | false, false ⇒ false
  | _, _ ⇒ true
  end.
Definition xorg_test : xorb true false = true := erefl.

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 := fun op ⇒
  match op with
  | or_introl p ⇒ or_intror p
  | or_intror p ⇒ or_introl p
  end.

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 :=
  match H with
  | conj pA pB ⇒ pB
  end.

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 :=
fun e ⇒ match e with exist x _ ⇒ x end.

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) :=
    fun aPQ ⇒ conj (fun x ⇒ (aPQ x).1) (fun x ⇒ (aPQ x).2).

Exercise: complete the following function

Definition not_not_a (P : Prop) : P → ¬ (~ P) := fun p np ⇒ np p.

natural numbers

Exercise: Define multiplicaton of naturals.

Print nat.
Fixpoint nat_mul (m n : nat) : nat :=
  match m with
  | 0 ⇒ 0
  | m.+1 ⇒ n + nat_mul m n
  end.
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
  | add' : weird_natural → weird_natural → weird_natural.

Best here would be double : weird_natural -> weird_natural

Exercise: Complete the below function from weird_natural to nat

Fixpoint to_nat (n : weird_natural) : nat :=
  match n with
  | zero' ⇒ 0
  | succ' n ⇒ (to_nat n).+1
  | add' n m ⇒ to_nat n + to_nat m
  end.

Exercise: Complete the below function for addition of weird_natural

Fixpoint weird_add (n1 n2 : weird_natural) : weird_natural :=
  match n1 with
  | zero' ⇒ n2
  | succ' n ⇒ succ' (weird_add n n2)
  | add' n m ⇒ weird_add n (weird_add m n2)
  end.

Exercise: Write a test ensuring that weird_add and to_nat commute

Definition weird_add_test :
  to_nat (weird_add
            (add' (succ' (succ' zero')) (succ' (succ' zero')))
            (add' (succ' (succ' zero')) (succ' (succ' zero')))) = 8 := erefl.

Exercise: complete a division / remainder function

Fixpoint divn (n1 n2 : nat) : nat × nat := (0, 0).

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 :=
  match l with
  | [::] ⇒ [::]
  | [:: x & l] ⇒ [:: f x & map f l]
  end.

Exercise: complete the following function that filters a list

Fixpoint filter (A : Type) (p : A → bool) (l : seq A) : seq A :=
  match l with
  | [::] ⇒ [::]
  | [:: x & l] ⇒
      if p x then
        [:: x & filter p l]
      else filter p l
  end.

Exercise: filter a list of naturals to select the even numbers

Compute (filter (fun x ⇒ ~~ odd x) [::1;2]).

Exercise: complete the following function that concatenates 2 lists

Fixpoint append (A : Type) (s1 s2 : seq A) : seq A :=
  match s1 with
  | [::] ⇒ s2
  | [:: x & l] ⇒ [:: x & append l s2]
  end.

Exercise: complete the following function that reverses a list

Fixpoint rev (A : Type) (s : seq A) : seq A :=
  match s with
  | [::] ⇒ [::]
  | [:: x & l] ⇒ append (rev l) [:: x]
  end.

Inductive types

Exercise: syntax for propositional logic. Complete the below inductive to add cases for and and or

Exercise: eval. Complete the below evalution function for the extended syntax

Exercise: the above evalution function has some bugs; write a test that showcases it. What do you need to assume? Fix the evaluation function.

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 :=
  fun xa st ⇒
    match f xa st with
    | (xb, st') ⇒ g xb st'
    end.