Lecture 3: Coq
==============

Goal of this lecture
  Review Coq
  Go over the homework assignments (Basics.v and Induction.v)

Questions about homeworks so far?

Concepts:
  Inductive types
    Inductive bool :=
    | true
    | false.

    Inductive item :=
    | rock
    | paper
    | scissors.

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

  Records
    special case of inductive type
    defines a struct with several fields
    field names are accessors for those fields

    Record nbpair := mkpair {
      first : nat;
      second : bool;
    }.

  Vernacular commands
    Check first.
    Check second.
    Print nbpair.
    Print first.
    Search nbpair.

  Definition
    gives a name to a term

    Definition p := mkpair 1 true.
    Print p.
    Eval compute in first p.

  Fixpoints for recursive definitions
    e.g., plus

  Theorems
    logical statements that refer to inductives, definitions, fixpoints, ..
    theorem statement is the same kind of a term that appears in a definition

    Theorem t1 : forall x y b, x = y -> mkpair x b = mkpair y b.
    Theorem t2 : forall x b, mkpair (x+x-x) b = mkpair x (negb (negb b)).

  Proofs
    written in a language called Ltac
    hypotheses: known facts (or available variables) in the current context
    subgoals: proof steps can create multiple proof obligations
      Global Set Default Goal Selector "!".
    tactics
      [intros]
      [reflexivity]
      simplification: [simpl]
      rewriting: [rewrite], [replace]
      [f_equal]
      case analysis: [case_eq], [destruct]
      induction: [induction]
      arithmetic: [lia]
      some automation: [eauto]
      [apply]

      https://coq.inria.fr/refman/coq-tacindex.html

  Notation
    1024
    [+] and [*] are notation for [plus] and [mult]

Walk through [simpl] of some expressions
  (S n) * (S m)
  (S m) + n * (S m)
  S (n + n * (S m))

Why is termination important?
  Let's say we can write:
    Fixpoint loop (x:nat) : ? := loop x
    [Coq will reject this]
  What is the return type?
    Every function must have a return type
  Nat? Bool? False?
    Fixpoint loop (x:nat) : False := loop x.
  What is loop 0?
    False
    Oops, we can proof False without hypothesis

Prop vs bool

Examples:
  mult_plus_distr_r
  mult_assoc