Exercise sheet 1: Coq Core Topics and Tactics

In this exercise sheet we will work over the fundamentals of functional programming, dependent types, and tactics.
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.

Tactics

Exercise: prove the below using 'move:', 'move=>' and a final apply
Definition goal_reorder A B C (H : B → A → C) : A → B → C.
Proof. Admitted.

Exercise: prove that orC (orC P) = P
Lemma orC_inv A B (p : A ∨ B) : orC (orC p) = p.
Proof. Admitted.
Exercise: prove
Lemma orbC p q : p || q = q || p.
Proof. Admitted.

Exercise:
  • look up the definition of iter
  • prove this statement by induction
Lemma iterSr A n (f : A → A) x : iter n.+1 f x = iter n f (f x).
Proof. Admitted.

Exercise:
  • look up the definition of iter (note there is an accumulator varying during recursion)
  • prove the following statement by induction
Lemma iter_predn m n : iter n predn m = m - n.
Proof. Admitted.

Exercise:
  • prove this statement using only rewrite and by
  • use Search to find the relevant lemmas (all are good but for ltn_neqAle) or browse the online doc
    • proof sketch: 
              m < n = ~~ (n <= m)
              = ~~ (n == m || n < m)
              = n != m && ~~ (n < m)
              = ...
Lemma ltn_neqAle m n : (m < n) = (m != n) && (m ≤ n).
Proof. Admitted.

Exercise: use rewrite {pos}H to prove the following lemma:
Lemma rewrite_pos (P : nat → Prop) (H : 0 = 1) : P 0 → P 1.
Proof.
Admitted.

Exercise: rewrite !H will rewrite with H until the goal doesn't change. This can easily lead to infinite loops, for example when doing rewrite addnC. Use a rewrite pattern rewrite ![X in pat]addnC to avoid that and prove the below lemma:
Lemma rewrite_pat n m p q : n + m + p + q = q + (n + m + p).
Proof.
Admitted.

Exercise:
  • which is the size of an empty sequence?
  • Use lemmas about size and filter to prove the below
Lemma has_filter (T : eqType) a (s : seq T) : has a s = (filter a s != [::]).
Proof.
Admitted.

Exercise: prove filter_all using induction
Lemma filter_all T a (s : seq T) : all a (filter a s).
Proof.
Admitted.