exercises_tactics.v

(** Exercise sheet for lecture 4: Tactics in Coq.

Written by Ralph Matthes (CNRS, IRIT, Univ. Toulouse, France).
 *)

(** * Exercise 1
Formalize the following types in UniMath and construct elements for them interactively - 
if they exist. Give a counter-example otherwise, i.e., give specific parameters and a
proof of the negation of the statement.

[[
1.    A × (B + C) → A × B + A × C, given types A, B, C
2.    (A → A) → (A → A), given type A (for extra credit, write down five elements of this type)
3.    Id_nat (0, succ 0)
4.    ∑ (A : Universe) (A → empty) → empty
5.    ∏ (n : nat), ∑ (m : nat), Id_nat n (2 * m) + Id_nat n (2 * m + 1),
      assuming you have got arithmetic
6.    (∑ (x : A) B × P x) → B × ∑ (x : A) P x, given types A, B, and P : A → Universe
7.    B → (B → A) → A, given types A and B
8.    B → ∏ (A : Universe) (B → A) → A, given type B
9.    (∏ (A : Universe) (B → A) → A) → B, given type B
]]

More precise instructions and hints:

1.  Use [⨿] in place of the + and pay attention to operator precedence.

2.  Write a function that provides different elements for any natural number argument, 
    not just five elements; for extra credits: state correctly that they are different - 
    for a good choice of [A]; for more extra credits: prove that they are different.

3.  An auxiliary function may be helpful (a well-known trick).

4.  The symbol for Sigma-types is [∑], not [Σ].

5.  Same as 1; and there is need for module [UniMath.Foundations.NaturalNumbers], e.g., 
    for Lemma [natpluscomm].

6.-9. no further particulars
*)

Require Import UniMath.Foundations.Preamble.
Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.NaturalNumbers.



(** * Exercise 2
Define two computable strict comparison operators for natural numbers based on the fact
that [m < n] iff [n - m <> 0] iff [(m+1) - n = 0]. Prove that the two operators are
equal (using function extensionality, i.e., [funextfunStatement] in the UniMath library).

It may be helpful to use the definitions of the exercises for lecture 2.
The following lemmas on substraction [sub] in the natural numbers may be
useful:

a) [sub n (S m) = pred (sub n m)]

b) [sub 0 n = 0]

c) [pred (sub 1 n) = 0]

d) [sub (S n) (S m) = sub n m]

*)


(** from exercises to Lecture 2: *)
Definition ifbool (A : UU) (x y : A) : bool -> A :=
  bool_rect (λ _ : bool, A) x y.

Definition negbool : bool -> bool := ifbool bool false true.

Definition nat_rec (A : UU) (a : A) (f : nat -> A -> A) : nat -> A :=
  nat_rect (λ _ : nat, A) a f.

Definition pred : nat -> nat := nat_rec nat 0 (fun x _ => x).

Definition is_zero : nat -> bool := nat_rec bool true (λ _ _, false).

Definition iter (A : UU) (a : A) (f : A → A) : nat → A :=
  nat_rec A a (λ _ y, f y).

Notation "f ̂ n" := (λ x, iter _ x f n) (at level 10).

Definition sub (m n : nat) : nat := pred ̂ n m.