(** * Auto: More Automation *)

Set Warnings "-notation-overridden,-parsing".
Require Import Coq.omega.Omega.
From LF Require Import Maps.
From LF Require Import Imp.

(** Consider the proof below, showing that [ceval] is
    deterministic.  There's a lot of repetition and a lot of
    near-repetition... *)

Theorem ceval_deterministic: forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2;
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst.
  - (* E_Skip *) reflexivity.
  - (* E_Ass *) reflexivity.
  - (* E_Seq *)
    apply IHE1_1 in H1. subst.
    apply IHE1_2. assumption.
  (* E_IfTrue *)
  - (* b evaluates to true *)
    apply IHE1. assumption.
  - (* b evaluates to false (contradiction) *)
    rewrite H in H5. discriminate. 
  (* E_IfFalse *)
  - (* b evaluates to true (contradiction) *)
    rewrite H in H5. discriminate.
  - (* b evaluates to false *)
    apply IHE1. assumption.
  (* E_WhileFalse *)
  - (* b evaluates to false *)
    reflexivity.
  - (* b evaluates to true (contradiction) *)
    rewrite H in H2. discriminate.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rewrite H in H4. discriminate. 
  - (* b evaluates to true *)    
    apply IHE1_1 in H3. subst.
    apply IHE1_2. assumption.  Qed.

(* ################################################################# *)
(** * The [auto] Tactic *)

(** Thus far, our proof scripts mostly apply relevant hypotheses or
    lemmas by name, and one at a time. *)

Example auto_example_1 : forall (P Q R: Prop),
  (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  intros P Q R H1 H2 H3.
  apply H2. apply H1. assumption.
Qed.

(** The [auto] tactic frees us from this drudgery by _searching_ for a
    sequence of applications that will prove the goal: *)

Example auto_example_1' : forall (P Q R: Prop),
  (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  auto.
Qed.

(** The [auto] tactic solves goals that are solvable by any combination of
     - [intros] and
     - [apply] (of hypotheses from the local context, by default). *)

(** Here is a more interesting example showing [auto]'s power: *)

Example auto_example_2 : forall P Q R S T U : Prop,
  (P -> Q) ->
  (P -> R) ->
  (T -> R) ->
  (S -> T -> U) ->
  ((P->Q) -> (P->S)) ->
  T ->
  P ->
  U.
Proof. auto. Qed.

(** Proof search could, in principle, take an arbitrarily long time,
    so there are limits to how far [auto] will search by default. *)

Example auto_example_3 : forall (P Q R S T U: Prop),
  (P -> Q) ->
  (Q -> R) ->
  (R -> S) ->
  (S -> T) ->
  (T -> U) ->
  P ->
  U.
Proof.
  (* When it cannot solve the goal, [auto] does nothing *)
  auto.
  (* Optional argument says how deep to search (default is 5) *)
  auto 6.
Qed.

(** [auto] considers the hypotheses in the current context
    together with a _hint database_ of other lemmas and constructors.
    Some common facts about equality and logical operators are
    installed in the hint database by default. *)

Example auto_example_4 : forall P Q R : Prop,
  Q ->
  (Q -> R) ->
  P \/ (Q /\ R).
Proof. auto. Qed.

(** We can extend the hint database just for the purposes of one
    application of [auto] by writing "[auto using ...]". *)

Lemma le_antisym : forall n m: nat, (n <= m /\ m <= n) -> n = m.
Proof. intros. omega. Qed.

Example auto_example_6 : forall n m p : nat,
  (n <= p -> (n <= m /\ m <= n)) ->
  n <= p ->
  n = m.
Proof.
  auto using le_antisym.
Qed.

(** We can also permanently extend the hint database:

      - [Hint Resolve T.]

          Add theorem or constructor [T] to the global DB

      - [Hint Constructors c.]

          Add _all_ constructors of [c] to the global DB

      - [Hint Unfold d.]

          Automatically expand defined symbol [d] during [auto]
*)

(** In general, we want to put our own tactics in their own
    databases, so they don't clutter up (and slow down) the default
    database. For this lecture, we'll use the example database
    [ex_db] which we invoke via [auto with ex_db] *)

Hint Resolve le_antisym : ex_db.

Example auto_example_6' : forall n m p : nat,
  (n<= p -> (n <= m /\ m <= n)) ->
  n <= p ->
  n = m.
Proof.
  intros.
  auto with ex_db. (* picks up hint from database *)
Qed.

Definition is_fortytwo x := (x = 42).

Example auto_example_7: forall x,
  (x <= 42 /\ 42 <= x) -> is_fortytwo x.
Proof.
  auto with ex_db.  (* does nothing *)
Abort.

Hint Unfold is_fortytwo : ex_db.

Example auto_example_7' : forall x,
  (x <= 42 /\ 42 <= x) -> is_fortytwo x.
Proof. auto with ex_db. Qed.

(** We can check which hints are in our database via the following
    command *)

Print HintDb ex_db.

(** Let's take a first pass over [ceval_deterministic] to simplify the
    proof script. *)

Theorem ceval_deterministic': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
       induction E1; intros st2 E2; inversion E2; subst; auto.
  - (* E_Seq *)
    apply IHE1_1 in H1. subst. auto.
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rewrite H in H5. inversion H5.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H5. inversion H5.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rewrite H in H2. inversion H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rewrite H in H4. inversion H4.
  - (* b evaluates to true *)
    apply IHE1_1 in H3. subst. auto.
Qed.

(* ################################################################# *)
(** * Searching For Hypotheses *)

(** The proof has become simpler, but there is still an annoying
    amount of repetition.

    Let's first tackle the contradiction cases.  Each occurs where we
    have hypothesis of the form

      H1: beval st b = false

    as well as:

      H2: beval st b = true


    First step: Abstracting out that piece of script in Coq's tactic 
    scripting language, Ltac.
*)

Ltac rwdisc H1 H2 := rewrite H1 in H2; discriminate.
(* NOTE: RNR: Also, inv isn't necessary *and* our students already
   know about the [discriminate] tactic! *)

(** Using [rwinv]... *)

Theorem ceval_deterministic'': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; auto.
  - (* E_Seq *)
    apply IHE1_1 in H1. subst. auto.
  - (* E_IfTrue *)
    + (* b evaluates to false (contradiction) *)
      rwdisc H H5.
  - (* E_IfFalse *)
    + (* b evaluates to true (contradiction) *)
      rwdisc H H5.
  - (* E_WhileFalse *)
    + (* b evaluates to true (contradiction) *)
      rwdisc H H2.
  (* E_WhileTrue *)
  - (* b evaluates to false (contradiction) *)
    rwdisc H H4.
  - (* b evaluates to true *)
    apply IHE1_1 in H3. subst. auto.
Qed.

(** That was a bit better, but we really want Coq to discover the
    relevant hypotheses for us.  We can do this by using the [match
    goal] facility of Ltac. *)

Ltac find_rwdisc :=
  match goal with
    H1: ?E = true, H2: ?E = false |- _ => rwdisc H1 H2
  end.

(** The [match goal] tactic looks for hypotheses matching the
    pattern specified. In this case, we're looking for two equalities
    [H1] and [H2] equating the same thing [?E] to [true] and [false]. *)

Theorem ceval_deterministic''': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; try find_rwdisc; auto.
  - (* E_Seq *)
    apply IHE1_1 in H1. subst. auto.
  - (* E_WhileTrue *)
    apply IHE1_1 in H3. subst. auto.
Qed.

(** Now for the remaining cases. Each applies a conditional
    hypothesis to extract an equality. Let's automate this task! *)

Ltac find_eqn :=
  match goal with
    H1: forall x, ?P x -> ?L = ?R,
    H2: ?P ?X
    |- _ => rewrite (H1 X H2) in *
  end.

(** Now we can make use of [find_eqn] to repeatedly rewrite
    with the appropriate hypothesis, wherever it may be found.

    In our example proof, we [repeat find_eqn], which will repeatedly
    rewrite until only trivial rewrites are available (since [rewrite]
    fails when given a trivial equation). *)

Theorem ceval_deterministic''''': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1; intros st2 E2; inversion E2; subst; try find_rwdisc;
    repeat find_eqn; auto.
Qed.

(** The big payoff in this approach is that our proof script should be
    more robust in the face of modest changes to our language.  To
    test whether it really is, let's try adding a [REPEAT] command to
    the language. *)

Module Repeat.

(* NOTE: RNR: CAsgn is CAss in Imp.v. Consistency would be nice. Also,
   what happened to our nice definition of ceval with notations??? 
   Actually, going to fix these in my version. *)
  
Inductive com : Type :=
  | CSkip
  | CAss (x : string) (a : aexp)
  | CSeq (c1 c2 : com)
  | CIf (b : bexp) (c1 c2 : com)
  | CWhile (b : bexp) (c : com)
  | CRepeat (c : com) (b : bexp).

(** [REPEAT] behaves like [WHILE], except that the loop guard is
    checked _after_ each execution of the body, with the loop
    repeating as long as the guard stays _false_.  Because of this,
    the body will always execute at least once. *)

Notation "'SKIP'" :=
  CSkip.
Notation "c1 ;; c2" :=
  (CSeq c1 c2) (at level 80, right associativity).
Notation "X '::=' a" :=
  (CAss X a) (at level 60).
Notation "'WHILE' b 'DO' c 'END'" :=
  (CWhile b c) (at level 80, right associativity).
Notation "'IFB' e1 'THEN' e2 'ELSE' e3 'FI'" :=
  (CIf e1 e2 e3) (at level 80, right associativity).
Notation "'REPEAT' e1 'UNTIL' b2 'END'" :=
  (CRepeat e1 b2) (at level 80, right associativity).

Reserved Notation "c1 '/' st '\\' st'"
                  (at level 40, st at level 39).

Inductive ceval : com -> state -> state -> Prop :=
  | E_Skip : forall st,
      SKIP / st \\ st
  | E_Ass  : forall st a1 n x,
      aeval st a1 = n ->
      (x ::= a1) / st \\ st & { x --> n }
  | E_Seq : forall c1 c2 st st' st'',
      c1 / st  \\ st' ->
      c2 / st' \\ st'' ->
      (c1 ;; c2) / st \\ st''
  | E_IfTrue : forall st st' b c1 c2,
      beval st b = true ->
      c1 / st \\ st' ->
      (IFB b THEN c1 ELSE c2 FI) / st \\ st'
  | E_IfFalse : forall st st' b c1 c2,
      beval st b = false ->
      c2 / st \\ st' ->
      (IFB b THEN c1 ELSE c2 FI) / st \\ st'
  | E_WhileFalse : forall b st c,
      beval st b = false ->
      (WHILE b DO c END) / st \\ st
  | E_WhileTrue : forall st st' st'' b c,
      beval st b = true ->
      c / st \\ st' ->
      (WHILE b DO c END) / st' \\ st'' ->
      (WHILE b DO c END) / st \\ st''
  | E_RepeatEnd : forall st st' b1 c1,
      c1 / st \\ st' ->
      beval st' b1 = true ->
      (CRepeat c1 b1) / st \\ st'
  | E_RepeatLoop : forall st st' st'' b1 c1,
      c1 / st \\ st' ->
      beval st' b1 = false ->
      (CRepeat c1 b1) / st' \\ st'' ->
      (CRepeat c1 b1) / st \\ st''

  where "c1 '/' st '\\' st'" := (ceval c1 st st').

(** Our first attempt at the determinacy proof does not quite succeed:
    the [E_RepeatEnd] and [E_RepeatLoop] cases are not handled by our
    previous automation. *)

Theorem ceval_deterministic: forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1;
    intros st2 E2; inversion E2; subst; try find_rwdisc; repeat find_eqn; auto.
  - (* E_RepeatEnd *)
    + (* b evaluates to false (contradiction) *)
       find_rwdisc.
       (* oops: why didn't [find_rwinv] solve this for us already?
          answer: we did things in the wrong order. *)
  - (* E_RepeatLoop *)
     + (* b evaluates to true (contradiction) *)
        find_rwdisc.
Qed.

(** Fortunately, to fix this, we just have to swap the invocations of
    [find_eqn] and [find_rwinv]. *)

Theorem ceval_deterministic': forall c st st1 st2,
     c / st \\ st1  ->
     c / st \\ st2 ->
     st1 = st2.
Proof.
  intros c st st1 st2 E1 E2.
  generalize dependent st2;
  induction E1;
    intros st2 E2; inversion E2; subst; repeat find_eqn; try find_rwdisc; auto.
Qed.

End Repeat.

(* ================================================================= *)
(** ** The [eapply] and [eauto] variants *)

(** Recall this example from the [Imp] chapter: *)

Example ceval_example1:
    (X ::= 2;;
     IFB X <= 1
       THEN Y ::= 3
       ELSE Z ::= 4
     FI)
   / { --> 0 }
   \\ { X --> 2 ; Z --> 4 }.
Proof.
  (* We supply the intermediate state [st']... *)
  apply E_Seq with { X --> 2 }.
  - apply E_Ass. reflexivity.
  - apply E_IfFalse. reflexivity. apply E_Ass. reflexivity.
Qed.

(** In the first step of the proof, we had to explicitly provide
    a longish expression, due to the "hidden" argument [st'] to the [E_Seq]
    constructor:

          E_Seq : forall c1 c2 st st' st'',
            c1 / st  \\ st' ->
            c2 / st' \\ st'' ->
            (c1 ;; c2) / st \\ st''
*)

(** If we leave out the [with], this step fails, because Coq cannot
    find an instance for the variable [st']. But this is silly! The appropriate
    value for [st'] will become obvious in the very next step. *)

(** With [eapply], we can eliminate this silliness: *)

Example ceval'_example1:
    (X ::= 2;;
     IFB X <= 1
       THEN Y ::= 3
       ELSE Z ::= 4
     FI)
   / { --> 0 }
   \\ { X --> 2 ; Z --> 4 }.
Proof.
  eapply E_Seq. (* 1 *)
  - apply E_Ass. (* 2 *)
    reflexivity. (* 3 *)
  - (* 4 *) apply E_IfFalse. reflexivity. apply E_Ass. reflexivity.
Qed.

(** Several of the tactics that we've seen so far, including [exists],
    [constructor], and [auto], have [e...] variants.  For example,
    here's a proof using [eauto]: *)

Hint Constructors ceval : ex_db.
Hint Transparent state : ex_db.
Hint Transparent total_map : ex_db.

Definition st12 := { X --> 1 ; Y --> 2 }.
Definition st21 := { X --> 2 ; Y --> 1 }.

Example eauto_example : exists s',
  (IFB X <= Y
    THEN Z ::= Y - X
    ELSE Y ::= X + Z
  FI) / st21 \\ s'.
Proof. eauto with ex_db. Qed.

(** The [eauto] tactic works just like [auto], except that it uses
    [eapply] instead of [apply].

    Pro tip: One might think that, since [eapply] and [eauto] are more
    powerful than [apply] and [auto], it would be a good idea to use
    them all the time.  Unfortunately, they are also significantly
    slower -- especially [eauto].  Coq experts tend to use [apply] and
    [auto] most of the time, only switching to the [e] variants when
    the ordinary variants don't do the job. *)

(* ================================================================= *)
(** ** Homework *)

(** No homework for this chapter - don't bother turning it in. But go
    back to earlier chapters and do some exercises using automation! *)