(** * BasicsLecture: Functional Programming in Rocq -- Lecture Notes *)

(** These notes accompany the [Basics] chapter of _Logical Foundations_.
    They are meant to be stepped through interactively during lecture. *)

From Stdlib Require Export String.

(* ################################################################# *)
(** * Inductive Types *)

(* ================================================================= *)
(** ** Days of the Week *)

(** The [Inductive] keyword defines a new type by listing its
    constructors. *)

Inductive day : Type :=
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday.

(** Functions over [day] use [match] for pattern matching. *)

Definition next_working_day (d : day) : day :=
  match d with
  | monday    => tuesday
  | tuesday   => wednesday
  | wednesday => thursday
  | thursday  => friday
  | friday    => monday
  | saturday  => monday
  | sunday    => monday
  end.

(** [Compute] evaluates an expression and prints the result. *)

Compute (next_working_day friday).
(* ==> monday : day *)

Compute (next_working_day (next_working_day saturday)).
(* ==> tuesday : day *)

(** [Example] states a property and lets us prove it. [Lemma], [Theorem] and
  [Corollary] do the same thing.  Choose the name that is most descriptive.
  other declarations do the same thing
  *)

Example test_next_working_day :
  next_working_day (next_working_day saturday) = tuesday.
Proof. simpl. reflexivity. Qed.

(* ================================================================= *)
(** ** Booleans *)

(** We define [bool] from scratch, just as Rocq builds everything
    from first principles. *)

Inductive bool : Type :=
  | true
  | false.

Definition negb (b : bool) : bool :=
  match b with
  | true  => false
  | false => true
  end.

Definition andb (b1 b2 : bool) : bool :=
  match b1 with
  | true  => b2
  | false => false
  end.

Definition orb (b1 b2 : bool) : bool :=
  match b1 with
  | true  => true
  | false => b2
  end.

(** A truth table as unit tests: *)

Example test_orb1 : orb true  false = true.  Proof. reflexivity. Qed.
Example test_orb2 : orb false false = false. Proof. reflexivity. Qed.
Example test_orb3 : orb false true  = true.  Proof. reflexivity. Qed.
Example test_orb4 : orb true  true  = true.  Proof. reflexivity. Qed.

(** Infix notation using [Notation]. *)

Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).

Example test_notation : false || false || true = true.
Proof. reflexivity. Qed.

(** An alternative style using [if]: Rocq's [if] works on any
    inductive type with exactly two constructors -- the first
    constructor is treated as [true]. *)

Definition negb' (b : bool) : bool :=
  if b then false else true.

(** **** In-class exercise: nandb
    Define [nandb] (NAND) -- returns [true] if either or both
    inputs are [false]. *)

Definition nandb (b1 b2 : bool) : bool :=
  negb (andb b1 b2).

Example test_nandb1 : nandb true  false = true.  (* FILL IN HERE *) Admitted.
Example test_nandb2 : nandb false false = true.  (* FILL IN HERE *) Admitted.
Example test_nandb3 : nandb false true  = true.  (* FILL IN HERE *) Admitted.
Example test_nandb4 : nandb true  true  = false. (* FILL IN HERE *) Admitted.

(* ================================================================= *)
(** ** Types *)

(** [Check] reports the type of an expression. *)

Check true.
(* ===> true : bool *)

Check negb.
(* ===> negb : bool -> bool *)

Check andb.
(* ===> andb : bool -> bool -> bool *)

(* ================================================================= *)
(** ** New Types from Old *)

(** Constructors can take arguments, building richer types. *)

Inductive rgb : Type :=
  | red
  | green
  | blue.

Inductive color : Type :=
  | black
  | white
  | primary (p : rgb).

Definition monochrome (c : color) : bool :=
  match c with
  | black     => true
  | white     => true
  | _ => false
  end.

Definition isred (c : color) : bool :=
  match c with
  | primary red => true
  | _           => false
  end.

(** The wildcard [_] matches any constructor. *)

(* ================================================================= *)
(** ** Modules *)

(** [Module] / [End] limits scope so we can reuse names. *)

Module Playground.
  Definition foo : rgb := blue.
End Playground.

Definition foo : bool := true.

Check Playground.foo : rgb.
Check foo            : bool.

(* ================================================================= *)
(** ** Tuples *)

Module TuplePlayground.

Inductive bit : Type :=
  | B1
  | B0.

(** A single constructor with multiple arguments acts as a tuple. *)

Inductive nybble : Type :=
  | bits (b0 b1 b2 b3 : bit).

Check (bits B1 B0 B1 B0) : nybble.

Definition all_zero (nb : nybble) : bool :=
  match nb with
  | bits B0 B0 B0 B0 => true
  | bits _ _ _ _     => false
  end.

Compute (all_zero (bits B1 B0 B1 B0)).  (* ==> false *)
Compute (all_zero (bits B0 B0 B0 B0)).  (* ==> true  *)

End TuplePlayground.

(* ################################################################# *)
(** * Natural Numbers *)

(* ================================================================= *)
(** ** Unary Representation *)

Module NatPlayground.

(** Natural numbers as a recursive inductive type -- unary representation. *)

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

(** [O] is zero; [S n] is the successor of [n] (i.e., [n+1]).
    So 1 = [S O], 2 = [S (S O)], 3 = [S (S (S O))], ... *)

(** Pattern matching and the predecessor function: *)

Definition pred (n : nat) : nat :=
  match n with
  | O    => O
  | S n' => n'
  end.

End NatPlayground.

(** Outside the module, [nat] is the standard-library type.
    Rocq prints decimal numerals for it: *)

Check (S (S (S (S O)))).
(* ===> 4 : nat *)

Definition minustwo (n : nat) : nat :=
  match n with
  | O      => O
  | S O    => O
  | S (S n') => n'
  end.

Compute (minustwo 4). (* ==> 2 *)

(* ================================================================= *)
(** ** Fixpoint: Recursive Functions *)

(** For recursion we use [Fixpoint] instead of [Definition]. *)

Fixpoint even (n : nat) : bool :=
  match n with
  | O        => true
  | S O      => false
  | S (S n') => even n'
  end.

Definition odd (n : nat) : bool := negb (even n).

Example test_odd1 : odd 1 = true.  Proof. reflexivity. Qed.
Example test_odd2 : odd 4 = false. Proof. reflexivity. Qed.

Module NatPlayground2.

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

(** Step-by-step evaluation of [plus 3 2]:
<<
      plus (S (S (S O))) (S (S O))
  ==> S (plus (S (S O)) (S (S O)))
  ==> S (S (plus (S O) (S (S O))))
  ==> S (S (S (plus O (S (S O)))))
  ==> S (S (S (S (S O))))   (* i.e. 5 *)
>>
*)

Compute (plus 3 2). (* ==> 5 *)

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

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

End NatPlayground2.

Fixpoint exp (base power : nat) : nat :=
  match power with
  | O   => S O
  | S p => mult base (exp base p)
  end.

(** Arithmetic notation: *)

Notation "x + y" := (plus x y)  (at level 50, left associativity) : nat_scope.
Notation "x - y" := (minus x y) (at level 50, left associativity) : nat_scope.
Notation "x * y" := (mult x y)  (at level 40, left associativity) : nat_scope.

Check ((0 + 1) + 1) : nat.

(** **** In-class exercise: factorial *)

Fixpoint factorial (n : nat) : nat
  (* FILL IN HERE *). Admitted.

Example test_factorial1 : factorial 3 = 6.          (* FILL IN HERE *) Admitted.
Example test_factorial2 : factorial 5 = mult 10 12. (* FILL IN HERE *) Admitted.

(* ================================================================= *)
(** ** Equality and Comparison on Nat *)

(** [eqb] tests equality, returning a [bool]. *)

Fixpoint eqb (n m : nat) : bool :=
  match n with
  | O => match m with
         | O    => true
         | S m' => false
         end
  | S n' => match m with
            | O    => false
            | S m' => eqb n' m'
            end
  end.

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O    => true
  | S n' =>
    match m with
    | O    => false
    | S m' => leb n' m'
    end
  end.

Notation "x =? y" := (eqb x y) (at level 70) : nat_scope.
Notation "x <=? y" := (leb x y) (at level 70) : nat_scope.

Example test_leb1 : (2 <=? 4) = true.  Proof. reflexivity. Qed.
Example test_leb2 : (4 <=? 2) = false. Proof. reflexivity. Qed.

Print test_leb1.

Definition ltb (n m : nat) : bool := (S n) <=? m.

Notation "x <? y" := (ltb x y) (at level 70) : nat_scope.

Example test_ltb1 : (2 <? 2) = false. Proof. reflexivity. Qed.
Example test_ltb2 : (2 <? 4) = true.  Proof. reflexivity. Qed.

(** Key distinction: [x = y] is a logical _proposition_ (something
    to prove); [x =? y] is a boolean _expression_ (something to
    compute). *)

(* ################################################################# *)
(** * Proof Tactics *)

(* ================================================================= *)
(** ** Proof by Simplification *)

(** [simpl] reduces both sides of an equation; [reflexivity]
    checks that they are identical. *)

Theorem plus_O_n : forall n : nat, 0 + n = n.
Proof.
  intros n. simpl. reflexivity. Qed.

(** [reflexivity] can often handle the simplification itself: *)

Theorem plus_O_n' : forall n : nat, 0 + n = n.
Proof.
  intros n. reflexivity. Qed.

Theorem plus_1_l : forall n : nat, 1 + n = S n.
Proof.
  intros n. reflexivity. Qed.

Theorem mult_0_l : forall n : nat, 0 * n = 0.
Proof.
  intros n. reflexivity. Qed.

(* ================================================================= *)
(** ** Proof by Rewriting *)

(** When we have a hypothesis [H : n = m], [rewrite -> H] replaces
    [n] with [m] in the goal. *)

Theorem plus_id_example : forall n m : nat,
  n = m -> n + n = m + m.
Proof.
  intros n m.   (* introduce variables *)
  intros H.     (* introduce hypothesis *)
  rewrite -> H. (* replace n with m everywhere in goal *)
  reflexivity.
Qed.

(** **** In-class exercise *)
Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
  (* FILL IN HERE *) Admitted.

(** We can also [rewrite] using a previously proved theorem. *)

Check mult_n_O.
(* ===> forall n : nat, 0 = n * 0 *)

Check mult_n_Sm.
(* ===> forall n m : nat, n * m + n = n * S m *)

Theorem mult_n_0_m_0 : forall p q : nat,
  (p * 0) + (q * 0) = 0.
Proof.
  intros p q.
  rewrite <- mult_n_O.
  rewrite <- mult_n_O.
  reflexivity.
Qed.

(** **** In-class exercise: use [mult_n_Sm] and [mult_n_O] *)
Theorem mult_n_1 : forall p : nat, p * 1 = p.
Proof.
  (* FILL IN HERE *) Admitted.

(* ================================================================= *)
(** ** Proof by Case Analysis *)

(** When [simpl] gets stuck on an unknown variable, use [destruct]
    to split into cases. *)

Theorem plus_1_neq_0_firsttry : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n.
  simpl. (* stuck: [n] is unknown, can't reduce [n + 1] *)
Abort.

Theorem plus_1_neq_0 : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros n. destruct n as [| n'] eqn:E.
  - (* n = O   *) reflexivity.
  - (* n = S n'*) reflexivity.
Qed.

(** [destruct] also works on [bool]: *)

Theorem negb_involutive : forall b : bool,
  negb (negb b) = b.
Proof.
  intros b. destruct b eqn:E.
  - reflexivity.
  - reflexivity.
Qed.

(** Nested [destruct] for two booleans.  Use different bullet styles
    for nested levels: [-] then [+]. *)

Theorem andb_commutative : forall b c, andb b c = andb c b.
Proof.
  intros b c. destruct b eqn:Eb.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
  - destruct c eqn:Ec.
    + reflexivity.
    + reflexivity.
Qed.

(** **** In-class exercise *)
Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  (* FILL IN HERE *) Admitted.

(** Shorthand: [intros [|n]] combines [intros n] and [destruct n]. *)

Theorem plus_1_neq_0' : forall n : nat,
  (n + 1) =? 0 = false.
Proof.
  intros [|n].
  - reflexivity.
  - reflexivity.
Qed.

(** **** In-class exercise *)
Theorem zero_nbeq_plus_1 : forall n : nat,
  0 =? (n + 1) = false.
Proof.
  (* FILL IN HERE *) Admitted.

(* ################################################################# *)
(** * Application: Late-Days Grading Policy *)

Module LateDays.

(** A running application example that ties together inductive
    types, pattern matching, and proofs. *)

Inductive letter : Type :=
  | A | B | C | D | F.

Inductive modifier : Type :=
  | Plus | Natural | Minus.

Inductive grade : Type :=
  Grade (l : letter) (m : modifier).

Inductive comparison : Type :=
  | Eq
  | Lt
  | Gt.

(** Comparing letters.  Simultaneous matching on two values with [,];
    multi-case patterns with [|]. *)

Definition letter_comparison (l1 l2 : letter) : comparison :=
  match l1, l2 with
  | A, A => Eq  | A, _ => Gt
  | B, A => Lt  | B, B => Eq  | B, _ => Gt
  | C, (A | B) => Lt  | C, C => Eq  | C, _ => Gt
  | D, (A | B | C) => Lt  | D, D => Eq  | D, _ => Gt
  | F, (A | B | C | D) => Lt  | F, F => Eq
  end.

Compute letter_comparison B A.  (* ==> Lt *)
Compute letter_comparison D D.  (* ==> Eq *)
Compute letter_comparison B F.  (* ==> Gt *)

(** **** In-class exercise: prove letter_comparison is reflexive *)
Theorem letter_comparison_Eq : forall l, letter_comparison l l = Eq.
Proof.
  (* FILL IN HERE *) Admitted.

Definition modifier_comparison (m1 m2 : modifier) : comparison :=
  match m1, m2 with
  | Plus,    Plus    => Eq  | Plus,    _       => Gt
  | Natural, Plus    => Lt  | Natural, Natural => Eq  | Natural, _ => Gt
  | Minus,   (Plus | Natural) => Lt  | Minus,   Minus   => Eq
  end.

(** **** In-class exercise: grade comparison (lexicographic) *)
Definition grade_comparison (g1 g2 : grade) : comparison
  (* FILL IN HERE *). Admitted.

Example test_grade_comparison1 :
  grade_comparison (Grade A Minus) (Grade B Plus) = Gt.
(* FILL IN HERE *) Admitted.

Example test_grade_comparison2 :
  grade_comparison (Grade A Minus) (Grade A Plus) = Lt.
(* FILL IN HERE *) Admitted.

(** Lower a letter by one step. *)

Definition lower_letter (l : letter) : letter :=
  match l with
  | A => B  | B => C  | C => D  | D => F  | F => F
  end.

(** Notice: the theorem below is NOT provable -- can you see why? *)

Theorem lower_letter_lowers_broken : forall (l : letter),
  letter_comparison (lower_letter l) l = Lt.
Proof.
  intros l. destruct l.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. reflexivity.
  - simpl. (* stuck on F: lower_letter F = F *)
Abort.

Theorem lower_letter_F_is_F : lower_letter F = F.
Proof. simpl. reflexivity. Qed.

(** A corrected theorem that excludes the F edge case: *)

Theorem lower_letter_lowers : forall (l : letter),
  letter_comparison F l = Lt ->
  letter_comparison (lower_letter l) l = Lt.
Proof.
  (* FILL IN HERE *) Admitted.

(** Lower a full grade by one step. *)

Definition lower_grade (g : grade) : grade :=
  match g with
  | Grade l Plus    => Grade l Natural
  | Grade l Natural => Grade l Minus
  | Grade F Minus   => Grade F Minus
  | Grade l Minus   => Grade (lower_letter l) Plus
  end.

Example lower_grade_A_Plus :
  lower_grade (Grade A Plus) = Grade A Natural.
Proof. simpl. reflexivity. Qed.

Example lower_grade_A_Minus :
  lower_grade (Grade A Minus) = Grade B Plus.
Proof. simpl. reflexivity. Qed.

Example lower_grade_F_Minus :
  lower_grade (Grade F Minus) = Grade F Minus.
Proof. simpl. reflexivity. Qed.

(** The late-days penalty policy:
<<
    0--8  late days: no penalty
    9--16: lower by 1
   17--20: lower by 2
      21+: lower by 3
>>
*)

Definition apply_late_policy (late_days : nat) (g : grade) : grade :=
  if late_days <? 9  then g
  else if late_days <? 17 then lower_grade g
  else if late_days <? 21 then lower_grade (lower_grade g)
  else lower_grade (lower_grade (lower_grade g)).

(** Unfolding lemma -- useful for rewriting in proofs. *)

Theorem apply_late_policy_unfold :
  forall (late_days : nat) (g : grade),
    apply_late_policy late_days g
    =
    (if late_days <? 9  then g
     else if late_days <? 17 then lower_grade g
     else if late_days <? 21 then lower_grade (lower_grade g)
     else lower_grade (lower_grade (lower_grade g))).
Proof.
  intros. reflexivity.
Qed.

(** **** In-class exercise *)
Theorem no_penalty_for_mostly_on_time :
  forall (late_days : nat) (g : grade),
    (late_days <? 9 = true) ->
    apply_late_policy late_days g = g.
Proof.
  (* FILL IN HERE *) Admitted.

(** **** In-class exercise *)
Theorem grade_lowered_once :
  forall (late_days : nat) (g : grade),
    (late_days <? 9  = false) ->
    (late_days <? 17 = true)  ->
    apply_late_policy late_days g = lower_grade g.
Proof.
  (* FILL IN HERE *) Admitted.

End LateDays.

(* ################################################################# *)
(** * Binary Numbers *)

(** A richer inductive type: binary numerals.
    Low-order bit on the left; high-order bit on the right.

<<
    decimal   binary          unary
       0      Z               O
       1      B1 Z            S O
       2      B0 (B1 Z)       S (S O)
       3      B1 (B1 Z)       S (S (S O))
       4      B0 (B0 (B1 Z))  S (S (S (S O)))
>>
*)

Inductive bin : Type :=
  | Z
  | B0 (n : bin)
  | B1 (n : bin).

(** **** In-class exercise: increment and conversion *)

Fixpoint incr (m : bin) : bin
  (* FILL IN HERE *). Admitted.

Fixpoint bin_to_nat (m : bin) : nat
  (* FILL IN HERE *). Admitted.

Example test_bin_incr1 : incr (B1 Z) = B0 (B1 Z).
(* FILL IN HERE *) Admitted.

Example test_bin_incr2 : incr (B0 (B1 Z)) = B1 (B1 Z).
(* FILL IN HERE *) Admitted.

Example test_bin_incr3 : incr (B1 (B1 Z)) = B0 (B0 (B1 Z)).
(* FILL IN HERE *) Admitted.

Example test_bin_incr4 : bin_to_nat (B0 (B1 Z)) = 2.
(* FILL IN HERE *) Admitted.

Example test_bin_incr5 :
  bin_to_nat (incr (B1 Z)) = 1 + bin_to_nat (B1 Z).
(* FILL IN HERE *) Admitted.

(* 2026-01-07 13:17 *)