(** ** Some presentations *)
(** Who am I? Who are you? What are the goals here? *)

(** ** Coq 101 *)

Section Playground.

  Variable (P Q : Prop).

  (* Coq is a proof assistant *)

  Lemma and_comm : P /\ Q -> Q /\ P.
  Proof.
    intros [p q].
    split.
    - exact q.
    - exact p.
  Qed.

  (* But Coq is primarily a (dependently-typed) programming language! *)
  Print and_comm.

  Definition or_comm : P \/ Q -> Q \/ P :=
    fun h => match h with
      | or_introl p => or_intror p
      | or_intror q => or_introl q
    end.

  Lemma id : P -> P.
  Proof.
    intros HP.
    Show Proof.
    assumption.
  Qed.

  Print id.

  Definition id' : P -> P :=
    fun p => p.

End Playground.

(** As any functional programming language, we have datatypes. *)

Inductive my_bool : Type := 
  | my_true : my_bool
  | my_false : my_bool.

Definition my_andb (b b' : my_bool) : my_bool :=
  match b with
  | my_true => b'
  | my_false => my_false
  end.

(** computation is part of the logic *)
Lemma and_true_true :
  my_andb my_true my_true = my_true.
Proof.
  simpl.
  reflexivity.
Restart.
  reflexivity.
Qed.

Print and_true_true.

(** A prime case of dependent types *)
About eq_refl.

Definition and_true_true' :
  my_andb my_true my_true = my_true
:= eq_refl.

(* reflexivity is not always enough, though! *)
Lemma andb_true_right (b : my_bool) :
  my_andb b my_true = b.
Proof.
  simpl.
  Fail reflexivity.
  case b.
  - simpl.
    reflexivity.
  - reflexivity.
Qed.

(* How do we use an equality? *)

Lemma andb_true_eq (b b' : my_bool) :
  b' = my_true -> my_andb b b' = b.
Proof.
  intros H.
  rewrite H.
  rewrite andb_true_right.
  reflexivity.
Qed.

(* Everything is a term! *)
Definition andb_true_eq' (b b' : my_bool)
  (e : b' = my_true) :
  my_andb b b' = b :=
  match (eq_sym e) with
  | eq_refl =>
      match b with
      | my_true => eq_refl
      | my_false => eq_refl
      end
  end.

(** ** Real inductive types *)

Inductive my_nat : Type :=
  | O : my_nat
  | S : my_nat -> my_nat.

Fixpoint my_add (m n : my_nat) : my_nat :=
  match m with
  | O => n
  | S m' => S (my_add m' n)
  end.

Infix "+" := my_add.

Lemma my_add_0 (n : my_nat) : n + O = n.
Proof.
  induction n.
  - simpl.
    reflexivity.
  - simpl.
    rewrite IHn.
    reflexivity.
Qed.

Lemma my_add_S (m n : my_nat) : n + S m = S (n + m).
Proof.
  induction n ; simpl ; try reflexivity.
  now rewrite IHn.
Qed.

Lemma my_add_comm (m n : my_nat) : m + n = n + m.
Proof.
  induction m.
  - simpl.
    rewrite my_add_0.
    reflexivity.
  - simpl.
    rewrite my_add_S, IHm.
    reflexivity.
Qed.

(** ** Types are data, too *)

Definition id'' (T : Type) (t : T) : T := t.

Definition id''' : forall T : Type, T -> T :=
  fun T t => t.

Check Type.

(** *** The inductive type of lists *)

Inductive my_list (A : Type) : Type :=
| my_nil : my_list A
| my_cons (a : A) (l : my_list A) : my_list A.

(** Polymorphic functions are "just" functions taking a parameter of type [Type] *)
About my_list.
Check (my_list nat).

Fixpoint my_append {A : Type} (l l' : my_list A) : my_list A :=
  match l with
  | my_nil _ => l'
  | my_cons _ hd tl => my_cons A hd (my_append tl l')
  end.

Infix "++" := my_append.

Lemma my_append_assoc {A : Type} (l l' l'' : my_list A) :
l ++ l' ++ l'' = (l ++ l') ++ l''.
Proof.
  induction l.
  - reflexivity.
  - simpl.
    rewrite IHl.
    reflexivity.
Qed.