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

  prepared using material by Ralph Matthes
 *)

(** * 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
10.   x = y → y = x, for elements x and y of some type A
11.   x = y → y = z → x = z, for elements x, y, and z of some type A
]]

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.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.Foundations.Preamble.
Require Import UniMath.Foundations.PartA.
Require Import UniMath.Foundations.NaturalNumbers.

(* 1.    A × (B + C) → A × B + A × C, given types A, B, C *)
Goal ∏ (A B C : UU), A × (B ⨿ C) -> (A × B) ⨿ (A × C).
Proof.
  intros.
  induction X.
  induction pr2.
  - apply ii1. apply tpair. apply pr1. apply a. 
  - apply ii2. apply tpair. apply pr1. apply b. 
Defined.
  
(* 2.    (A → A) → (A → A), given type A (for extra credit, write down five elements of this type) *)
Goal ∏ (A : UU), (A -> A) -> (A -> A).
Proof.
  intros.
  apply X0.
Defined.

(* 3.    Id_nat (0, succ 0) *)
Goal (O = S O) -> empty.
Proof.
  intros.
  exact (transportf (fun c => match c with O => unit | S _ => empty end) X tt).
Defined.

Locate "∑".
Print total2.

(* 4.    ∑ (A : Universe) (A → empty) → empty *)
Goal ∑ (A : UU), (A -> empty) -> empty.
Proof.
  use tpair.
  - exact unit.
  - simpl. intros. apply X. exact tt.
Defined.

(* 5.    ∏ (n : nat), ∑ (m : nat), Id_nat n (2 * m) + Id_nat n (2 * m + 1), *)
      (* assuming you have got arithmetic *)
Goal ∏ (n : nat), ∑ (m : nat), (paths n (2 * m)) ⨿ (paths n (1 + (2 * m))).
Proof.
  intros.
  induction n.
  - use tpair.
    + exact 0.
    + simpl. apply inl. reflexivity.
  - induction IHn. induction pr2.
    * use tpair. exact pr1. simpl. apply inr. rewrite a. reflexivity.
    * use tpair. exact (S pr1). simpl. apply inl. rewrite b. simpl.
      assert (S (pr1 + pr1) = S pr1 + pr1).
      + reflexivity.
      + rewrite X. rewrite natpluscomm. reflexivity.
Defined.

(* 6.    (∑ (x : A) B × P x) → B × ∑ (x : A) P x, given types A, B, and P : A → Universe *)
Goal ∏ (A B : UU) (P : A -> UU), (∑ (x : A), B × P x) -> B × ∑ (x : A), P x.
Proof.
  intros.
  induction X. induction pr2.
  use tpair.
  * exact pr0. 
  * simpl. use tpair.
    + exact pr1.
    + simpl. exact pr2.
Defined.  

(* 7.    B → (B → A) → A, given types A and B *)
Goal ∏ (A B : UU), B -> (B -> A) -> A.
Proof.
  intros.
  apply X0. exact X.
Defined.

(* 8.    B → ∏ (A : Universe) (B → A) → A, given type B *)
Goal ∏ (B : UU), B -> ∏ (A : UU), (B -> A) -> A.
Proof.
  intros.
  apply X0. exact X.
Defined.

(* 9.    (∏ (A : Universe) (B → A) → A) → B, given type B *)
Goal ∏ (B : UU), (∏ (A : UU), (B -> A) -> A) -> B.
Proof.
  intros.
  exact (X B (fun x => x)).
Defined.

(* 10.   x = y → y = x, for elements x and y of some type A *)
Goal ∏ (A : UU) (x y : A), x = y -> y = x.
Proof.
  intros.
  induction X.
  apply idpath.
Defined.

(* 11.   x = y → y = z → x = z, for elements x, y, and z of some type A *)
Goal ∏ (A : UU) (x y z : A), x = y -> y = z -> x = z.
Proof.
  intros.
  induction X. induction X0.
  apply idpath.
Defined.

(** * 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.

Definition lt1 (m n : nat) : bool := negb (is_zero (sub m n)).

Definition lt2 (m n : nat) : bool := is_zero (sub (S m) n).

Definition lt1_eq_lt2 : lt1 = lt2.
Proof.
  rewrite (funextfun lt1 lt2).
  - apply idpath.
  - intro x. rewrite (funextfun (lt1 x) (lt2 x)).
    + apply idpath.
    + intro y. unfold lt1. unfold lt2.
      induction x.
      induction y.
      { auto. }
      { 
        assert (∏ (y : nat), sub 0 y = 0) as Sub0.
        { intros. induction y0. { auto. } { simpl. unfold pred. rewrite IHy0. auto. } }
        rewrite Sub0. cbn.
      }