(* Adapted from Adam Chlipala's CPDT *)

Require Import List.

Require Import Cpdt.CpdtTactics Cpdt.MoreSpecif.

Set Implicit Arguments.
Set Asymmetric Patterns.

(** Proof by reflection. *)

(** * Proving Evenness *)

(** Can we prove evenness automatically with LTac? *)

Inductive isEven : nat -> Prop :=
| Even_O : isEven O
| Even_SS : forall n, isEven n -> isEven (S (S n)).

Ltac prove_even := repeat constructor.

Theorem even_256 : isEven 256.
  prove_even.
Qed.

Print even_256.

(* Yikes. This proof term is quite large... How big? 

Is it: 
(A) linear in the input value
(B) super-linear in the input value
(C) logarithmic in the input value?

 *)


















(* Print even_256. *)


(* The main construct we need to introduce is the notion of partially decidable propositions. *)

Module PartialPlayground.

  Inductive partial (P : Prop) : Set :=  
  | Proved : P -> partial P
  | Uncertain : partial P.

  (* 
  Notation "[ P ]" := (partial P).
  Notation "'Yes'" := (Proved _) : partial_scope.
  Notation "'No'" := (Uncertain _) : partial_scope.

  Notation "'Reduce' v" := 
    (if v then Yes else No) : partial_scope.
  Notation "x || y" := (if x then Yes else Reduce y) : partial_scope.
  Notation "x && y" := (if x then Reduce y else No) : partial_scope.
   *)
End PartialPlayground.

Print partial.

Local Open Scope partial_scope.

Definition check_even :
  forall n : nat, [isEven n].

  Local Hint Constructors isEven : core.

  refine (fix F (n : nat) : [isEven n] :=
    match n with
      | 0 => Proved _
      | 1 => No
      | S (S n') =>
        Reduce (F n')
    end); auto.
Defined.

Set Printing All.
Print check_even.

(** The function [check_even] may be viewed as a _verified decision
procedure_, because its type guarantees that it never returns Yes for
inputs that are not even. *)


(* How can we use this? Fancy dependent pattern matching! *)

Definition partialOut (P : Prop) (x : [P]) :=
  match x return (match x with
                    | Proved _ => P
                    | Uncertain => True
                  end) with
    | Proved pf => pf
    | Uncertain => I
  end.

(** It may seem strange to define a function like this.  However, it turns out to be very useful in writing a reflective version of our earlier [prove_even] tactic: *)

Ltac prove_even_reflective :=
  match goal with
  | [ |- isEven ?N] =>
    exact (partialOut (check_even N))
  end.


(** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call. *)

Theorem even_256' : isEven 256.
  prove_even_reflective.
Qed.

Print even_256'.

(** The size of proof term is now linear! *)

(*  What happens if we try the tactic with an odd number? *)

Theorem even_255 : isEven 255.
  (* prove_even_reflective. *)
Abort.

(** Our tactic [prove_even_reflective] is reflective because it performs a proof search process (a trivial one, in this case) wholly within Gallina, where the only use of Ltac is to translate a goal into an appropriate use of [check_even]. *)


(** * Reifying the Syntax of a Trivial Tautology Language *)

(** We might also like to have reflective proofs of trivial tautologies like this one: *)

Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
  tauto.
Qed.

Print true_galore.

(* Again, explicit applications, adds overhead.
   In large proofs, this can cause typechecking to be slow. VERY slow. *)

(* How can reflection help here? Well, we need to get 
to the actual reflection part: 
  * Get a [Prop]
  * Reify it into some type we _can_ case analyze.
  * Use the same technique as above. 
*)

Inductive taut : Set :=
| TautTrue : taut
| TautAnd : taut -> taut -> taut
| TautOr : taut -> taut -> taut
| TautImp : taut -> taut -> taut.

(* To reflect this syntax back to Prop, we need to write an _interpretation function_: *)

Fixpoint tautDenote (t : taut) : Prop :=
  match t with
    | TautTrue => True
    | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2
    | TautOr t1 t2 => tautDenote t1 \/ tautDenote t2
    | TautImp t1 t2 => tautDenote t1 -> tautDenote t2
  end.

(** It is easy to prove that every formula in the range of [tautDenote] is true. *)

Theorem tautTrue : forall t, tautDenote t.
  induction t; crush.
Qed.

(** To use [tautTrue] to prove particular formulas, we need to implement the syntax reification process.  A recursive Ltac function does the job. *)

Ltac tautReify P :=
  match P with
    | True => TautTrue
    | ?P1 /\ ?P2 =>
      let t1 := tautReify P1 in
      let t2 := tautReify P2 in
        constr:(TautAnd t1 t2)
    | ?P1 \/ ?P2 =>
      let t1 := tautReify P1 in
      let t2 := tautReify P2 in
        constr:(TautOr t1 t2)
    | ?P1 -> ?P2 =>
      let t1 := tautReify P1 in
      let t2 := tautReify P2 in
        constr:(TautImp t1 t2)
  end.

(** With [tautReify] available, it is easy to finish our reflective tactic.  We look at the goal formula, reify it, and apply [tautTrue] to the reified formula. *)

Ltac obvious :=
  match goal with
    | [ |- ?P ] =>
      let t := tautReify P in
        exact (tautTrue t)
  end.

(** We can verify that [obvious] solves our original example, with a proof term that does not mention details of the proof. *)

Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))).
  obvious.
Qed.

Print true_galore'.

(* So how is this better than doing the whole thing in Ltac? 

* Proof size? Sure
* Reification? Just as ad-hoc as before, we don't gain much there. 
* Usually, the proofs are going to be more complicated
than the translation process, and writing that proof
is on much better formal footing than recursive Ltac.
* Plus: it "works" on any input formula.

*)


(** * A Monoid Expression Simplifier *)

(** Proof by reflection does not require encoding of all of the syntax
in a goal.  We can insert "variables" in our syntax types to allow
injection of arbitrary pieces, even if we cannot apply specialized
reasoning to them.  In this section, we explore that possibility by
writing a tactic for normalizing monoid equations. *)

Section monoid.
  Variable A : Set.
  Variable e : A.
  Variable f : A -> A -> A.

  Infix "+" := f.

  Hypothesis assoc : forall a b c, (a + b) + c = a + (b + c).
  Hypothesis identl : forall a, e + a = a.
  Hypothesis identr : forall a, a + e = a.

  (** We add variables and hypotheses characterizing an arbitrary instance of the algebraic structure of monoids.  We have an associative binary operator and an identity element for it.

     It is easy to define an expression tree type for monoid expressions.  A [Var] constructor is a "catch-all" case for subexpressions that we cannot model.  These subexpressions could be actual Gallina variables, or they could just use functions that our tactic is unable to understand. *)

  Inductive mexp : Set :=
  | Ident : mexp
  | Var : A -> mexp
  | Op : mexp -> mexp -> mexp.

  (** Next, we write an interpretation function. *)

  Fixpoint mdenote (me : mexp) : A :=
    match me with
      | Ident => e
      | Var v => v
      | Op me1 me2 => mdenote me1 + mdenote me2
    end.

  (** We will normalize expressions by flattening them into lists, via associativity, so it is helpful to have a denotation function for lists of monoid values. *)

  Fixpoint mldenote (ls : list A) : A :=
    match ls with
      | nil => e
      | x :: ls' => x + mldenote ls'
    end.

  (** The flattening function itself is easy to implement. *)

  Fixpoint flatten (me : mexp) : list A :=
    match me with
      | Ident => nil
      | Var x => x :: nil
      | Op me1 me2 => flatten me1 ++ flatten me2
    end.

  (** This function has a straightforward correctness proof in terms of our [denote] functions. *)

  Lemma flatten_correct' : forall ml2 ml1,
    mldenote ml1 + mldenote ml2 = mldenote (ml1 ++ ml2).
    induction ml1; crush.
  Qed.

  Theorem flatten_correct : forall me, mdenote me = mldenote (flatten me).

    Local Hint Resolve flatten_correct' : core.

    induction me; crush.
  Qed.

  (** Now it is easy to prove a theorem that will be the main tool behind our simplification tactic. *)

  Theorem monoid_reflect : forall me1 me2,
    mldenote (flatten me1) = mldenote (flatten me2)
    -> mdenote me1 = mdenote me2.
  Proof.
    intros;
    repeat rewrite flatten_correct; assumption.
  Qed.

  (** We implement reification into the [mexp] type. *)

  Ltac reify me :=
    match me with
      | e => Ident
      | ?me1 + ?me2 =>
        let r1 := reify me1 in
        let r2 := reify me2 in
          constr:(Op r1 r2)
      | _ => constr:(Var me)
    end.

  (** The final [monoid] tactic works on goals that equate two monoid terms.  We reify each and change the goal to refer to the reified versions, finishing off by applying [monoid_reflect] and simplifying uses of [mldenote].  Recall that the %\index{tactics!change}%[change] tactic replaces a conclusion formula with another that is definitionally equal to it. *)

  Ltac monoid :=
    match goal with
      | [ |- ?me1 = ?me2 ] =>
        let r1 := reify me1 in
        let r2 := reify me2 in
          change (mdenote r1 = mdenote r2);
            apply monoid_reflect; simpl
    end.

  (** We can make short work of theorems like this one: *)

  Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d.
    intros.
    let r1 := reify (f (f (f a b) c) d) in
    let r2 := reify (f (f a (f b c)) d) in
    change (mdenote r1 = mdenote r2).
    apply monoid_reflect.
    simpl.
    reflexivity.
  Qed.

  (** It is interesting to look at the form of the proof. *)

  Print t1.

  (*
      The proof term contains only restatements of the equality operands in reified form, followed by a use of reflexivity on the shared canonical form. *)

End monoid.

(** This is actually used in the ring and field tactics that are in the standard library! *)

(** * A Smarter Tautology Solver *)

(* Let's revisit the tautology example and broaden its scope: 
  * Their truth should not be syntactically apparent.
  * We can inject arbitrary formulas.
  * We can use equalities between formulas.

 *)

(** ** Manual Reification of Terms with Variables *)

(* Step one of the process is to crawl over a term, building a
duplicate-free list of all values that appear in positions we will
encode as variables.  A useful helper function adds an element to a
list, preventing duplicates.  Note how we use Ltac pattern matching to
implement an equality test on Gallina terms; this is simple syntactic
equality, not even the richer definitional equality.  We also
represent lists as nested tuples, to allow different list elements to
have different Gallina types. *)

Ltac inList x xs :=
  match xs with
    | tt => false
    | (x, _) => true
    | (_, ?xs') => inList x xs'
  end.

Ltac addToList x xs :=
  let b := inList x xs in
    match b with
      | true => xs
      | false => constr:((x, xs))
    end.

(** Now we can write our recursive function to calculate the list of variable values we will want to use to represent a term. *)

Ltac allVars xs e :=
  match e with
    | True => xs
    | False => xs
    | ?e1 /\ ?e2 =>
      let xs := allVars xs e1 in
        allVars xs e2
    | ?e1 \/ ?e2 =>
      let xs := allVars xs e1 in
        allVars xs e2
    | ?e1 -> ?e2 =>
      let xs := allVars xs e1 in
        allVars xs e2
    | _ => addToList e xs
  end.

(** We will also need a way to map a value to its position in a list. *)

Ltac lookup x xs :=
  match xs with
    | (x, _) => O
    | (_, ?xs') =>
      let n := lookup x xs' in
        constr:(S n)
  end.

(** The next building block is a procedure for reifying a term, given a list of all allowed variable values.  We are free to make this procedure partial, where tactic failure may be triggered upon attempting to reify a term containing subterms not included in the list of variables.  The type of the output term is a copy of [formula] where [index] is replaced by [nat], in the type of the constructor for atomic formulas. *)

Inductive formula : Set :=
| Atomic : nat -> formula
| Truth : formula
| Falsehood : formula
| And : formula -> formula -> formula
| Or : formula -> formula -> formula
| Imp : formula -> formula -> formula.

Ltac reifyTerm xs e :=
  match e with
    | True => Truth
    | False => Falsehood
    | ?e1 /\ ?e2 =>
      let p1 := reifyTerm xs e1 in
      let p2 := reifyTerm xs e2 in
        constr:(And p1 p2)
    | ?e1 \/ ?e2 =>
      let p1 := reifyTerm xs e1 in
      let p2 := reifyTerm xs e2 in
        constr:(Or p1 p2)
    | ?e1 -> ?e2 =>
      let p1 := reifyTerm xs e1 in
      let p2 := reifyTerm xs e2 in
        constr:(Imp p1 p2)
    | _ =>
      let n := lookup e xs in
        constr:(Atomic n)
  end.

(** Finally, we bring all the pieces together. *)

Ltac reify :=
  match goal with
  | [ |- ?G ] =>
    let xs := allVars tt G in
      let p := reifyTerm xs G in
        pose p
  end.

(** A quick test verifies that we are doing reification correctly. *)

Theorem mt3' : forall x y z,
  (x < y /\ y > z) \/ (y > z /\ x < S y)
  -> y > z /\ (x < y \/ x < S y).
  do 3 intro; reify.

(** Our simple tactic adds the translated term as a new variable. *)
Abort.

(** More work would be needed to complete the reflective tactic, as we must connect our new syntax type with the real meanings of formulas, but the details are the same as in our prior implementation with [quote]. *)

Fixpoint formulaDenote (atomics : list Prop) (f : formula) : Prop :=
  match f with
    | Atomic v => nth v atomics False
    | Truth => True
    | Falsehood => False
    | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2
    | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2
    | Imp f1 f2 => formulaDenote atomics f1 -> formulaDenote atomics f2
  end.

Section my_tauto.
  Variable atomics : list Prop.

  (* Shorthand for a variable being true. *)
  Definition holds (v : nat) := nth v atomics False.

  Require Import ListSet.

  Definition index_eq : forall x y : nat, {x = y} + {x <> y}.
    decide equality.
  Defined.

  Definition add (s : set nat) (v : nat) := set_add index_eq v s.

  Definition In_dec : forall v (s : set nat), {In v s} + {~ In v s}.
    Local Open Scope specif_scope.

    intro; refine (fix F (s : set nat) : {In v s} + {~ In v s} :=
      match s with
        | nil => No
        | v' :: s' => index_eq v' v || F s'
      end); crush.
  Defined.

  (** We define what it means for all members of an index set to represent true propositions, and we prove some lemmas about this notion. *)

  Fixpoint allTrue (s : set nat) : Prop :=
    match s with
      | nil => True
      | v :: s' => holds v /\ allTrue s'
    end.

  Theorem allTrue_add : forall v s,
    allTrue s
    -> holds v
    -> allTrue (add s v).
    induction s; crush;
      match goal with
        | [ |- context[if ?E then _ else _] ] => destruct E
      end; crush.
  Qed.

  Theorem allTrue_In : forall v s,
    allTrue s
    -> set_In v s
    -> nth v atomics False.
    induction s; crush.
  Qed.

  Local Hint Resolve allTrue_add allTrue_In : core.

  Local Open Scope partial_scope.

  (** The meat: the forward function.

   Deconstructs hypotheses, expanding a compound formula into a set of
   sets of atomic formulas covering all possible cases introduced with
   use of [Or].  To handle consideration of multiple cases, the
   function takes in a continuation argument, which will be called
   once for each case.

     The [forward] function has a dependent type guaranteeing
     correctness.  The arguments to [forward] are a goal formula [f],
     a set [known] of atomic formulas that we may assume are true, a
     hypothesis formula [hyp], and a success continuation [cont] that
     we call when we have extended [known] to hold new truths implied
     by [hyp]. *)

  Definition forward : forall (f : formula) (known : set nat) (hyp : formula)
    (cont : forall known', [allTrue known' -> formulaDenote atomics f]),
    [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f].
    refine (fix F (f : formula) (known : set nat) (hyp : formula)
      (cont : forall known', [allTrue known' -> formulaDenote atomics f])
      : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] :=
      match hyp with
        | Atomic v => Reduce (cont (add known v))
        | Truth => Reduce (cont known)
        | Falsehood => Yes
        | And h1 h2 =>
          Reduce (F (Imp h2 f) known h1 (fun known' =>
            Reduce (F f known' h2 cont)))
        | Or h1 h2 => F f known h1 cont && F f known h2 cont
        | Imp _ _ => Reduce (cont known)
      end); crush.
  Defined.

  (** A [backward] function implements analysis of the final goal.  It calls [forward] to handle implications. *)

  Definition backward : forall (known : set nat) (f : formula),
    [allTrue known -> formulaDenote atomics f].
    refine (fix F (known : set nat) (f : formula)
      : [allTrue known -> formulaDenote atomics f] :=
      match f with
        | Atomic v => Reduce (In_dec v known)
        | Truth => Yes
        | Falsehood => No
        | And f1 f2 => F known f1 && F known f2
        | Or f1 f2 => F known f1 || F known f2
        | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2)
      end); crush; eauto.
  Defined.

  (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *)

  Definition my_tauto : forall f : formula, [formulaDenote atomics f].
    intro; refine (Reduce (backward nil f)); crush.
  Defined.
End my_tauto.