(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
  * Chapter 2: Basic Program Syntax
  * Author: Adam Chlipala
  * License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)

Require Import Frap.
(* This [Import] command is for including a library of code, theorems, tactics, etc.
 * Here we just include the standard library of the book.
 * We won't distinguish carefully between built-in Coq features and those provided by that library. *)

(* As a first example, let's look at the syntax of simple arithmetic expressions.
 * We use the Coq feature of modules, which let us group related definitions together.
 * A key benefit is that names can be reused across modules,
 * which is helpful to define several variants of a suite of functionality,
 * within a single source file. *)
Module ArithWithConstants.

  (* The following definition closely mirrors a standard BNF grammar for expressions.
   * It defines abstract syntax trees of arithmetic expressions. *)
  Inductive arith : Set :=
  | Const (n : nat)
  | Plus (e1 e2 : arith)
  | Times (e1 e2 : arith).

  (* Here are a few examples of specific expressions. *)
  Example ex1 := Const 42.
  Example ex2 := Plus (Const 1) (Times (Const 2) (Const 3)).

  (* How many nodes appear in the tree for an expression?
   * Unlike in many programming languages, in Coq,
   * recursive functions must be marked as recursive explicitly.
   * That marking comes with the [Fixpoint] command, as opposed to [Definition].
   * Note also that Coq checks termination of each recursive definition.
   * Intuitively, recursive calls must be on subterms of the original argument. *)
  Fixpoint size (e : arith) : nat :=
    match e with
    | Const _ => 1
    | Plus e1 e2 => 1 + size e1 + size e2
    | Times e1 e2 => 1 + size e1 + size e2
    end.

  (* Here's how to run a program (evaluate a term) in Coq. *)
  Compute size ex1.
  Compute size ex2.

  (* What's the longest path from the root of a syntax tree to a leaf? *)
  Fixpoint depth (e : arith) : nat :=
    match e with
    | Const _ => 1
    | Plus e1 e2 => 1 + max (depth e1) (depth e2)
    | Times e1 e2 => 1 + max (depth e1) (depth e2)
    end.

  Compute depth ex1.
  Compute depth ex2.

  (* Our first proof!
   * Size is an upper bound on depth. *)
  Theorem depth_le_size : forall e, depth e <= size e.
  Proof.
    (* Within a proof, we apply commands called *tactics*.
     * Here's our first one.
     * Throughout the book's Coq code, we give a brief note documenting each tactic,
     * after its first use.
     * Keep in mind that the best way to understand what's going on
     * is to run the proof script for yourself, inspecting intermediate states! *)
    induct e.
    (* [induct x]: where [x] is a variable in the theorem statement,
     *   structure the proof by induction on the structure of [x].
     *   You will get one generated subgoal per constructor in the
     *   inductive definition of [x].  (Indeed, it is required that 
     *   [x]'s type was introduced with [Inductive].) *)

    simplify.
    (* [simplify]: simplify throughout the goal, applying the definitions of
     *   recursive functions directly.  That is, when a subterm
     *   matches one of the [match] cases in a defining [Fixpoint],
     *   replace with the body of that case, then repeat. *)
    linear_arithmetic.
    (* [linear_arithmetic]: a complete decision procedure for linear arithmetic.
     *   Relevant formulas are essentially those built up from
     *   variables and constant natural numbers and integers
     *   using only addition, with equality and inequality
     *   comparisons on top.  (Multiplication by constants
     *   is supported, as a shorthand for repeated addition.) *)

    simplify.
    linear_arithmetic.
    (* [linear_arithmetic] is quite clever in how it rewrites induction hypotheses.
       Try using [rewrite] tactic here. *)

    simplify.
    linear_arithmetic.
  Qed.

  Theorem depth_le_size_snazzy : forall e, depth e <= size e.
  Proof.
    induct e; simplify; linear_arithmetic.
    (* Oo, look at that!  Chaining tactics with semicolon, as in [t1; t2],
     * asks to run [t1] on the goal, then run [t2] on *every*
     * generated subgoal.  This is an essential ingredient for automation. *)
  Qed.

  (* A silly recursive function: swap the operand orders of all binary operators. *)
  Fixpoint commuter (e : arith) : arith :=
    match e with
    | Const _ => e
    | Plus e1 e2 => Plus (commuter e2) (commuter e1)
    | Times e1 e2 => Times (commuter e2) (commuter e1)
    end.

  Compute commuter ex1.
  Compute commuter ex2.

  (* [commuter] has all the appropriate interactions with other functions (and itself). *)

  Theorem size_commuter : forall e, size (commuter e) = size e.
  Proof.
    induct e; simplify; linear_arithmetic.
  Qed.

  Theorem depth_commuter : forall e, depth (commuter e) = depth e.
  Proof.
    induct e; simplify; linear_arithmetic.
  Qed.

  Theorem commuter_inverse : forall e, commuter (commuter e) = e.
  Proof.
    induct e; simplify; equality.
    (* [equality]: a complete decision procedure for the theory of equality
     *   and uninterpreted functions.  That is, the goal must follow
     *   from only reflexivity, symmetry, transitivity, and congruence
     *   of equality, including that functions really do behave as functions. *)
  Qed.

End ArithWithConstants.

(* Let's shake things up a bit by adding variables to expressions.
 * Note that all of the automated proof scripts from before will keep working
 * with no changes!  That sort of "free" proof evolution is invaluable for
 * theorems about real-world compilers, say. *)
Module ArithWithVariables.

  Inductive arith : Set :=
  | Const (n : nat)
  | Var (x : var) (* <-- this is the new constructor! *)
  | Plus (e1 e2 : arith)
  | Times (e1 e2 : arith).

  Example ex1 := Const 42.
  Example ex2 := Plus (Const 1) (Times (Var "x") (Const 3)).

  Fixpoint size (e : arith) : nat :=
    match e with
    | Const _ => 1
    | Var _ => 1
    | Plus e1 e2 => 1 + size e1 + size e2
    | Times e1 e2 => 1 + size e1 + size e2
    end.

  Compute size ex1.
  Compute size ex2.

  Fixpoint depth (e : arith) : nat :=
    match e with
    | Const _ => 1
    | Var _ => 1
    | Plus e1 e2 => 1 + max (depth e1) (depth e2)
    | Times e1 e2 => 1 + max (depth e1) (depth e2)
    end.

  Compute depth ex1.
  Compute depth ex2.

  Theorem depth_le_size : forall e, depth e <= size e.
  Proof.
    induct e; simplify; linear_arithmetic.
  Qed.

  Fixpoint commuter (e : arith) : arith :=
    match e with
    | Const _ => e
    | Var _ => e
    | Plus e1 e2 => Plus (commuter e2) (commuter e1)
    | Times e1 e2 => Times (commuter e2) (commuter e1)
    end.

  Compute commuter ex1.
  Compute commuter ex2.

  Theorem size_commuter : forall e, size (commuter e) = size e.
  Proof.
    induct e; simplify; linear_arithmetic.
  Qed.

  Theorem depth_commuter : forall e, depth (commuter e) = depth e.
  Proof.
    induct e; simplify; linear_arithmetic.
  Qed.

  Theorem commuter_inverse : forall e, commuter (commuter e) = e.
  Proof.
    induct e; simplify; equality.
  Qed.

  (* Now that we have variables, we can consider new operations,
   * like substituting an expression for a variable.
   * We use an infix operator [==v] for equality tests on strings.
   * It has a somewhat funny and very expressive type,
   * whose details we will try to gloss over.
   * (To dig into it more on your own, the appropriate keyword is "dependent types.") *)
  Fixpoint substitute (inThis : arith) (replaceThis : var) (withThis : arith) : arith :=
    match inThis with
    | Const _ => inThis
    | Var x => if x ==v replaceThis then withThis else inThis
    | Plus e1 e2 => Plus (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
    | Times e1 e2 => Times (substitute e1 replaceThis withThis) (substitute e2 replaceThis withThis)
    end.

  (* An intuitive property about how much [substitute] might increase depth. *)
  Theorem substitute_depth : forall replaceThis withThis inThis,
    depth (substitute inThis replaceThis withThis) <= depth inThis + depth withThis.
  Proof.
    induct inThis.

    simplify.
    linear_arithmetic.

    simplify.
    cases (x ==v replaceThis).
    (* [cases e]: break the proof into one case for each constructor that might have
     *   been used to build the value of expression [e].  In the special case where
     *   [e] essentially has a Boolean type, we consider whether [e] is true or false. *)
    linear_arithmetic.
    simplify.
    linear_arithmetic.

    simplify.
    linear_arithmetic.

    simplify.
    linear_arithmetic.
  Qed.
  
  (* A stronger property about substitution. [<=] replaced by [<] *)
  Theorem substitute_depth' : forall replaceThis withThis inThis,
    depth (substitute inThis replaceThis withThis) < depth inThis + depth withThis.
  Proof.
    induct inThis.

    simplify.
    destruct withThis; simplify; try linear_arithmetic.

    simplify.
    cases (x ==v replaceThis).
    (* [cases e]: break the proof into one case for each constructor that might have
     *   been used to build the value of expression [e].  In the special case where
     *   [e] essentially has a Boolean type, we consider whether [e] is true or false. *)
    linear_arithmetic.
    simplify.
    destruct withThis; simplify; try linear_arithmetic.

    simplify.
    linear_arithmetic.

    simplify.
    linear_arithmetic.
  Qed.

  (* Let's get fancier about automation, using [match goal] to pattern-match the goal
   * and decide what to do next!
   * The [|-] syntax separates hypotheses and conclusion in a goal.
   * The [context] syntax is for matching against *any subterm* of a term.
   * The construct [try] is also useful, for attempting a tactic and rolling back
   * the effect if any error is encountered. *)
  Theorem substitute_depth_snazzy : forall replaceThis withThis inThis,
    depth (substitute inThis replaceThis withThis) <= depth inThis + depth withThis.
  Proof.
    induct inThis; simplify;
    try match goal with
        | [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
        end; linear_arithmetic.
  Qed.

  (* A silly self-substitution has no effect. *)
  Theorem substitute_self : forall replaceThis inThis,
    substitute inThis replaceThis (Var replaceThis) = inThis.
  Proof.
    induct inThis; simplify;
    try match goal with
        | [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
        end; equality.
  Qed.

  (* We can do substitution and commuting in either order. *)
  Theorem substitute_commuter : forall replaceThis withThis inThis,
    commuter (substitute inThis replaceThis withThis)
    = substitute (commuter inThis) replaceThis (commuter withThis).
  Proof.
    induct inThis; simplify;
    try match goal with
        | [ |- context[if ?a ==v ?b then _ else _] ] => cases (a ==v b); simplify
        end; equality.
  Qed.

  (* *Constant folding* is one of the classic compiler optimizations.
   * We repeatedly find opportunities to replace fancier expressions
   * with known constant values. *)
  Fixpoint constantFold (e : arith) : arith :=
    match e with
    | Const _ => e
    | Var _ => e
    | Plus e1 e2 =>
      let e1' := constantFold e1 in
      let e2' := constantFold e2 in
      match e1', e2' with
      | Const n1, Const n2 => Const (n1 + n2)
      | Const 0, _ => e2'
      | _, Const 0 => e1'
      | _, _ => Plus e1' e2'
      end
    | Times e1 e2 =>
      let e1' := constantFold e1 in
      let e2' := constantFold e2 in
      match e1', e2' with
      | Const n1, Const n2 => Const (n1 * n2)
      | Const 1, _ => e2'
      | _, Const 1 => e1'
      | Const 0, _ => Const 0
      | _, Const 0 => Const 0
      | _, _ => Times e1' e2'
      end
    end.

  (* This is supposed to be an *optimization*, so it had better not *increase*
   * the size of an expression!
   * There are enough cases to consider here that we skip straight to
   * the automation.
   * A new scripting construct is [match] patterns with dummy bodies.
   * Such a pattern matches *any* [match] in a goal, over any type! *)
  Theorem size_constantFold : forall e, size (constantFold e) <= size e.
  Proof.
    induct e; simplify;
    repeat match goal with
           | [ |- context[match ?E with _ => _ end] ] => cases E; simplify
           end; linear_arithmetic.
  Qed.

  (* Business as usual, with another commuting law *)
  Theorem commuter_constantFold : forall e, commuter (constantFold e) = constantFold (commuter e).
  Proof.
    induct e; simplify;
    repeat match goal with
           | [ |- context[match ?E with _ => _ end] ] => cases E; simplify
           | [ H : ?f _ = ?f _ |- _ ] => invert H
           | [ |- ?f _ = ?f _ ] => f_equal
           end; equality || linear_arithmetic || ring.
    (* [f_equal]: when the goal is an equality between two applications of
     *   the same function, switch to proving that the function arguments are
     *   pairwise equal.
     * [invert H]: replace hypothesis [H] with other facts that can be deduced
     *   from the structure of [H]'s statement.  This is admittedly a fuzzy
     *   description for now; we'll learn much more about the logic shortly!
     *   Here, what matters is that, when the hypothesis is an equality between
     *   two applications of a constructor of an inductive type, we learn that
     *   the arguments to the constructor must be pairwise equal.
     * [ring]: prove goals that are equalities over some registered ring or
     *   semiring, in the sense of algebra, where the goal follows solely from
     *   the axioms of that algebraic structure. *)
  Qed.

  (* To define a further transformation, we first write a roundabout way of
   * testing whether an expression is a constant.
   * This detour happens to be useful to avoid overhead in concert with
   * pattern matching, since Coq internally elaborates wildcard [_] patterns
   * into separate cases for all constructors not considered beforehand.
   * That expansion can create serious code blow-ups, leading to serious
   * proof blow-ups! *)
  Definition isConst (e : arith) : option nat :=
    match e with
    | Const n => Some n
    | _ => None
    end.

  (* Our next target is a function that finds multiplications by constants
   * and pushes the multiplications to the leaves of syntax trees,
   * ideally finding constants, which can be replaced by larger constants,
   * not affecting the meanings of expressions.
   * This helper function takes a coefficient [multiplyBy] that should be
   * applied to an expression. *)
  Fixpoint pushMultiplicationInside' (multiplyBy : nat) (e : arith) : arith :=
    match e with
    | Const n => Const (multiplyBy * n)
    | Var _ => Times (Const multiplyBy) e
    | Plus e1 e2 => Plus (pushMultiplicationInside' multiplyBy e1)
                         (pushMultiplicationInside' multiplyBy e2)
    | Times e1 e2 =>
      match isConst e1 with
      | Some k => pushMultiplicationInside' (k * multiplyBy) e2
      | None => Times (pushMultiplicationInside' multiplyBy e1) e2
      end
    end.

  (* The overall transformation just fixes the initial coefficient as [1]. *)
  Definition pushMultiplicationInside (e : arith) : arith :=
    pushMultiplicationInside' 1 e.

  (* Let's prove this boring arithmetic property, so that we may use it below. *)
  Lemma n_times_0 : forall n, n * 0 = 0.
  Proof.
    linear_arithmetic.
  Qed.

  (* A fun fact about pushing multiplication inside:
   * the coefficient has no effect on depth!
   * Let's start by showing any coefficient is equivalent to coefficient 0. *)
  Lemma depth_pushMultiplicationInside'_irrelevance0 : forall e multiplyBy,
    depth (pushMultiplicationInside' multiplyBy e)
    = depth (pushMultiplicationInside' 0 e).
  Proof.
    induct e; simplify.

    linear_arithmetic.

    linear_arithmetic.

    rewrite IHe1.
    (* [rewrite H]: where [H] is a hypothesis or previously proved theorem,
     *  establishing [forall x1 .. xN, e1 = e2], find a subterm of the goal
     *  that equals [e1], given the right choices of [xi] values, and replace
     *  that subterm with [e2]. *)
    rewrite IHe2.
    linear_arithmetic.

    cases (isConst e1); simplify.

    rewrite IHe2.
    rewrite n_times_0.
    linear_arithmetic.

    rewrite IHe1.
    linear_arithmetic.
  Qed.

  (* It can be remarkably hard to get Coq's automation to be dumb enough to
   * help us demonstrate all of the primitive tactics. ;-)
   * In particular, we can redo the proof in an automated way, without the
   * explicit rewrites. *)
  Lemma depth_pushMultiplicationInside'_irrelevance0_snazzy : forall e multiplyBy,
    depth (pushMultiplicationInside' multiplyBy e)
    = depth (pushMultiplicationInside' 0 e).
  Proof.
    induct e; simplify;
    try match goal with
        | [ |- context[match ?E with _ => _ end] ] => cases E; simplify
        end; equality.
  Qed.

  (* Now the general corollary about irrelevance of coefficients for depth. *)
  Lemma depth_pushMultiplicationInside'_irrelevance : forall e multiplyBy1 multiplyBy2,
    depth (pushMultiplicationInside' multiplyBy1 e)
    = depth (pushMultiplicationInside' multiplyBy2 e).
  Proof.
    simplify.
    transitivity (depth (pushMultiplicationInside' 0 e)).
    (* [transitivity X]: when proving [Y = Z], switch to proving [Y = X]
     * and [X = Z]. *)
    apply depth_pushMultiplicationInside'_irrelevance0.
    (* [apply H]: for [H] a hypothesis or previously proved theorem,
     *   establishing some fact that matches the structure of the current
     *   conclusion, switch to proving [H]'s own hypotheses.
     *   This is *backwards reasoning* via a known fact. *)
    symmetry.
    (* [symmetry]: when proving [X = Y], switch to proving [Y = X]. *)
    apply depth_pushMultiplicationInside'_irrelevance0.
  Qed.

  (* Let's prove that pushing-inside has only a small effect on depth,
   * considering for now only coefficient 0. *)
  Lemma depth_pushMultiplicationInside' : forall e,
    depth (pushMultiplicationInside' 0 e) <= S (depth e).
  Proof.
    induct e; simplify.

    linear_arithmetic.

    linear_arithmetic.

    linear_arithmetic.

    cases (isConst e1); simplify.

    rewrite n_times_0.
    linear_arithmetic.

    linear_arithmetic.
  Qed.

  Hint Rewrite n_times_0.
  (* Registering rewrite hints will get [simplify] to apply them for us
   * automatically! *)

  Lemma depth_pushMultiplicationInside'_snazzy : forall e,
    depth (pushMultiplicationInside' 0 e) <= S (depth e).
  Proof.
    induct e; simplify;
    try match goal with
        | [ |- context[match ?E with _ => _ end] ] => cases E; simplify
        end; linear_arithmetic.
  Qed.

  Theorem depth_pushMultiplicationInside : forall e,
    depth (pushMultiplicationInside e) <= S (depth e).
  Proof.
    simplify.
    unfold pushMultiplicationInside.
    (* [unfold X]: replace [X] by its definition. *)
    rewrite depth_pushMultiplicationInside'_irrelevance0.
    apply depth_pushMultiplicationInside'.
  Qed.

End ArithWithVariables.