(* Dependent Types lecture transcript *)
(* Charles Averill *)
(* https://charles.systems/ *)

Section RocqIntroduction.

Inductive primary :=
  | Red
  | Blue
  | Green.

Check Red. (* Red : primary *)

Inductive color :=
  | Plain (p : primary)
  | Dark  (c : color)
  | Light (c : color).

Check Dark (Plain Red). (* Dark (Plain Red) : color *)
Check Dark (Dark (Plain Red)). (* Dark (Dark (Plain Red)) : color *)

Definition darken (c : color) : color :=
  match c with
  | Light c => c
  | _ => Dark c
  end.

Compute darken (Plain Red). (* Dark (Plain Red) *)
Compute darken (Light (Plain Red)). (* Plain Red *)

Definition lighten (c : color) : color :=
  match c with
  | Dark c => c
  | _ => Light c
  end.

Compute darken (lighten (Plain Red)). (* Plain Red *)

End RocqIntroduction.

Section Vectors.

From Stdlib Require Import Vector.
Require Import Stdlib.Program.Equality.

Print Vector.t.

(*

Inductive t (A : Type) : nat -> Type :=
    nil : t A 0 | cons : A -> forall n : nat, t A n -> t A (S n).

Arguments t A%_type_scope _%_nat_scope
Arguments nil A%_type_scope
Arguments cons A%_type_scope h n%_nat_scope _

*)

Compute nil nat. (* t nat 0 *)
Compute cons nat 5 0 (nil nat). (* t nat 1 *)

Notation "[]" := (nil _).
Notation "h :: t" := (cons _ h _ t).

Check [] : t nat 0.
Check (5 :: []) : t nat 1.

Definition hd {T : Type} {n : nat} (vec : t T (S n)) : T :=
  match vec with
  | cons _ h _ _ => h
  end.

Definition tl {T : Type} {n : nat} (vec : t T (S n)) : t T n :=
  match vec with
  | cons _ _ _ t => t
  end.

Fixpoint vappend {A : Type} {n m : nat}
  (xs : t A n) (ys : t A m) : t A (n + m) :=
  match xs with
  | nil _ => ys
  | cons _ x n' xs' =>
      cons A x (n' + m) (vappend xs' ys)
  end.

Compute vappend (5 :: []) (6 :: []).

Check Vector.nth.
(* nth
     : t ?A ?n -> Fin.t ?n -> ?A
where
?A : [ |- Type]
?n : [ |- nat]
 *)

Check Fin.F1.
Check Fin.FS.
Check Vector.nth.
Check @Fin.of_nat_lt.
From Stdlib Require Import Lia.

Compute Vector.nth (5 :: 6 :: []) Fin.F1.
Compute Vector.nth (5 :: 6 :: []) (Fin.FS Fin.F1).
Compute Vector.nth (5 :: 6 :: []) (@Fin.of_nat_lt 0 2 ltac:(lia)).
Compute Vector.nth (5 :: 6 :: []) (@Fin.of_nat_lt 1 2 ltac:(lia)).

Print sigT.
Check existT.

End Vectors.

Section Proofs.

Theorem modus_ponens :
  forall (P Q : Prop),
    P -> (P -> Q) -> Q.
Proof.
  intros P Q HP HPQ.
  apply HPQ.
  apply HP.
Qed.

Print modus_ponens.

Inductive nat :=
| O
| S (n' : nat).

Inductive nat' :=
| O' : nat'
| S' : nat' -> nat'.

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

Notation "0" := O.
Notation "n + m" := (add n m).

Theorem add_0_r :
  forall (n : nat), n + 0 = n.
Proof.
  intros n. induction n.
  - simpl. reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.

Print add_0_r.

Check (fun n : nat => nat_ind (fun n' => n' + 0 = n') (eq_refl)
        (fun n' IHn' =>
          eq_ind_r (fun n1 : nat => S n1 = S n') eq_refl IHn') n)
      : forall (n : nat), n + 0 = n.

Print nat_ind.

Theorem plus_n_Sm :
  forall (n m : nat), S (n + m) = n + S m.
Proof.
  intros n m. induction n.
  - simpl. reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.

Theorem add_comm :
  forall (n m : nat), n + m = m + n.
Proof.
  intros n m. induction n.
  - simpl. rewrite add_0_r. reflexivity.
  - simpl. rewrite IHn. apply plus_n_Sm.
Qed.

Print and.
Print or.
Locate "->".
Print not.
Print True.
Print False.

Definition and_comm : forall (P Q : Prop), P /\ Q -> Q /\ P :=
  fun (P Q : Prop) (HPQ : P /\ Q) =>
    match HPQ with
    | conj HP HQ => conj HQ HP
    end.

Definition or_comm : forall (P Q : Prop), P \/ Q -> Q \/ P :=
  fun (P Q : Prop) (HPQ : P \/ Q) =>
    match HPQ with
    | or_introl HP => or_intror HP
    | or_intror HQ => or_introl HQ
    end.

End Proofs.

Section TypedExpressions.

From Stdlib Require Import PeanoNat.

Inductive ty :=
  | TNat
  | TBool.

Definition denote (t : ty) : Type :=
  match t with
  | TNat => Datatypes.nat
  | TBool => bool
  end.

Inductive expr : ty -> Type :=
  | ENat  : Datatypes.nat -> expr TNat
  | EBool : bool -> expr TBool
  | EAdd  : expr TNat -> expr TNat -> expr TNat
  | EEq   : expr TNat -> expr TNat -> expr TBool
  | EIf   : forall (t : ty),
      expr TBool -> expr t -> expr t -> expr t.

Fixpoint eval {t : ty} (e : expr t) : denote t :=
  match e with
  | ENat n => n
  | EBool b => b
  | EAdd x y => Nat.add (eval x) (eval y)
  | EEq x y => Nat.eqb (eval x) (eval y)
  | EIf t c e1 e2 =>
      if eval c then eval e1 else eval e2
  end.

Compute eval
  (EIf TNat
    (EEq (EAdd (ENat 2) (ENat 3)) (ENat 5))
    (ENat 10)
    (ENat 0)).

Fail Check (EAdd (ENat 2) (EBool true)).

End TypedExpressions.