adamc@221: (* Copyright (c) 2008-2009, Adam Chlipala
adamc@142: *
adamc@142: * This work is licensed under a
adamc@142: * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@142: * Unported License.
adamc@142: * The license text is available at:
adamc@142: * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@142: *)
adamc@142:
adamc@142: (* begin hide *)
adamc@142: Require Import List.
adamc@142:
adamc@142: Require Import Tactics MoreSpecif.
adamc@142:
adamc@142: Set Implicit Arguments.
adamc@142: (* end hide *)
adamc@142:
adamc@142:
adamc@142: (** %\chapter{Proof by Reflection}% *)
adamc@142:
adamc@142: (** The last chapter highlighted a very heuristic approach to proving. In this chapter, we will study an alternative technique, %\textit{%##proof by reflection##%}%. We will write, in Gallina, decision procedures with proofs of correctness, and we will appeal to these procedures in writing very short proofs. Such a proof is checked by running the decision procedure. The term %\textit{%##reflection##%}% applies because we will need to translate Gallina propositions into values of inductive types representing syntax, so that Gallina programs may analyze them. *)
adamc@142:
adamc@142:
adamc@142: (** * Proving Evenness *)
adamc@142:
adamc@142: (** Proving that particular natural number constants are even is certainly something we would rather have happen automatically. The Ltac-programming techniques that we learned in the last chapter make it easy to implement such a procedure. *)
adamc@142:
adamc@142: Inductive isEven : nat -> Prop :=
adamc@144: | Even_O : isEven O
adamc@144: | Even_SS : forall n, isEven n -> isEven (S (S n)).
adamc@142:
adamc@148: (* begin thide *)
adamc@142: Ltac prove_even := repeat constructor.
adamc@148: (* end thide *)
adamc@142:
adamc@142: Theorem even_256 : isEven 256.
adamc@142: prove_even.
adamc@142: Qed.
adamc@142:
adamc@142: Print even_256.
adamc@221: (** %\vspace{-.15in}% [[
adamc@142: even_256 =
adamc@142: Even_SS
adamc@142: (Even_SS
adamc@142: (Even_SS
adamc@142: (Even_SS
adamc@221:
adamc@142: ]]
adamc@142:
adamc@221: %\noindent%...and so on. This procedure always works (at least on machines with infinite resources), but it has a serious drawback, which we see when we print the proof it generates that 256 is even. The final proof term has length linear in the input value. This seems like a shame, since we could write a trivial and trustworthy program to verify evenness of constants. The proof checker could simply call our program where needed.
adamc@142:
adamc@142: It is also unfortunate not to have static typing guarantees that our tactic always behaves appropriately. Other invocations of similar tactics might fail with dynamic type errors, and we would not know about the bugs behind these errors until we happened to attempt to prove complex enough goals.
adamc@142:
adamc@142: The techniques of proof by reflection address both complaints. We will be able to write proofs like this with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.
adamc@142:
adamc@221: For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *)
adamc@142:
adamc@142: Print partial.
adamc@221: (** %\vspace{-.15in}% [[
adamc@221: Inductive partial (P : Prop) : Set := Proved : P -> [P] | Uncertain : [P]
adamc@221:
adamc@221: ]]
adamc@142:
adamc@221: A [partial P] value is an optional proof of [P]. The notation [[P]] stands for [partial P]. *)
adamc@142:
adamc@221: Local Open Scope partial_scope.
adamc@142:
adamc@142: (** We bring into scope some notations for the [partial] type. These overlap with some of the notations we have seen previously for specification types, so they were placed in a separate scope that needs separate opening. *)
adamc@142:
adamc@148: (* begin thide *)
adamc@142: Definition check_even (n : nat) : [isEven n].
adamc@142: Hint Constructors isEven.
adamc@142:
adamc@142: refine (fix F (n : nat) : [isEven n] :=
adamc@221: match n with
adamc@142: | 0 => Yes
adamc@142: | 1 => No
adamc@142: | S (S n') => Reduce (F n')
adamc@142: end); auto.
adamc@142: Defined.
adamc@142:
adamc@142: (** We can use dependent pattern-matching to write a function that performs a surprising feat. When given a [partial P], this function [partialOut] returns a proof of [P] if the [partial] value contains a proof, and it returns a (useless) proof of [True] otherwise. From the standpoint of ML and Haskell programming, it seems impossible to write such a type, but it is trivial with a [return] annotation. *)
adamc@142:
adamc@142: Definition partialOut (P : Prop) (x : [P]) :=
adamc@142: match x return (match x with
adamc@142: | Proved _ => P
adamc@142: | Uncertain => True
adamc@142: end) with
adamc@142: | Proved pf => pf
adamc@142: | Uncertain => I
adamc@142: end.
adamc@142:
adamc@142: (** It may seem strange to define a function like this. However, it turns out to be very useful in writing a reflective verison of our earlier [prove_even] tactic: *)
adamc@142:
adamc@142: Ltac prove_even_reflective :=
adamc@142: match goal with
adamc@142: | [ |- isEven ?N] => exact (partialOut (check_even N))
adamc@142: end.
adamc@148: (* end thide *)
adamc@142:
adamc@142: (** We identify which natural number we are considering, and we "prove" its evenness by pulling the proof out of the appropriate [check_even] call. *)
adamc@142:
adamc@142: Theorem even_256' : isEven 256.
adamc@142: prove_even_reflective.
adamc@142: Qed.
adamc@142:
adamc@142: Print even_256'.
adamc@221: (** %\vspace{-.15in}% [[
adamc@142: even_256' = partialOut (check_even 256)
adamc@142: : isEven 256
adamc@221:
adamc@142: ]]
adamc@142:
adamc@142: We can see a constant wrapper around the object of the proof. For any even number, this form of proof will suffice. What happens if we try the tactic with an odd number? *)
adamc@142:
adamc@142: Theorem even_255 : isEven 255.
adamc@142: (** [[
adamc@142: prove_even_reflective.
adamc@142:
adamc@142: User error: No matching clauses for match goal
adamc@221:
adamc@142: ]]
adamc@142:
adamc@142: Thankfully, the tactic fails. To see more precisely what goes wrong, we can run manually the body of the [match].
adamc@142:
adamc@142: [[
adamc@142: exact (partialOut (check_even 255)).
adamc@142:
adamc@142: Error: The term "partialOut (check_even 255)" has type
adamc@142: "match check_even 255 with
adamc@142: | Yes => isEven 255
adamc@142: | No => True
adamc@142: end" while it is expected to have type "isEven 255"
adamc@221:
adamc@142: ]]
adamc@142:
adamc@142: As usual, the type-checker performs no reductions to simplify error messages. If we reduced the first term ourselves, we would see that [check_even 255] reduces to a [No], so that the first term is equivalent to [True], which certainly does not unify with [isEven 255]. *)
adamc@221:
adamc@142: Abort.
adamc@143:
adamc@143:
adamc@143: (** * Reflecting the Syntax of a Trivial Tautology Language *)
adamc@143:
adamc@143: (** We might also like to have reflective proofs of trivial tautologies like this one: *)
adamc@143:
adamc@143: Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
adamc@143: tauto.
adamc@143: Qed.
adamc@143:
adamc@143: Print true_galore.
adamc@221: (** %\vspace{-.15in}% [[
adamc@143: true_galore =
adamc@143: fun H : True /\ True =>
adamc@143: and_ind (fun _ _ : True => or_introl (True /\ (True -> True)) I) H
adamc@143: : True /\ True -> True \/ True /\ (True -> True)
adamc@221:
adamc@143: ]]
adamc@143:
adamc@143: As we might expect, the proof that [tauto] builds contains explicit applications of natural deduction rules. For large formulas, this can add a linear amount of proof size overhead, beyond the size of the input.
adamc@143:
adamc@143: To write a reflective procedure for this class of goals, we will need to get into the actual "reflection" part of "proof by reflection." It is impossible to case-analyze a [Prop] in any way in Gallina. We must %\textit{%##reflect##%}% [Prop] into some type that we %\textit{%##can##%}% analyze. This inductive type is a good candidate: *)
adamc@143:
adamc@148: (* begin thide *)
adamc@143: Inductive taut : Set :=
adamc@143: | TautTrue : taut
adamc@143: | TautAnd : taut -> taut -> taut
adamc@143: | TautOr : taut -> taut -> taut
adamc@143: | TautImp : taut -> taut -> taut.
adamc@143:
adamc@143: (** We write a recursive function to "unreflect" this syntax back to [Prop]. *)
adamc@143:
adamc@143: Fixpoint tautDenote (t : taut) : Prop :=
adamc@143: match t with
adamc@143: | TautTrue => True
adamc@143: | TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2
adamc@143: | TautOr t1 t2 => tautDenote t1 \/ tautDenote t2
adamc@143: | TautImp t1 t2 => tautDenote t1 -> tautDenote t2
adamc@143: end.
adamc@143:
adamc@143: (** It is easy to prove that every formula in the range of [tautDenote] is true. *)
adamc@143:
adamc@143: Theorem tautTrue : forall t, tautDenote t.
adamc@143: induction t; crush.
adamc@143: Qed.
adamc@143:
adamc@143: (** To use [tautTrue] to prove particular formulas, we need to implement the syntax reflection process. A recursive Ltac function does the job. *)
adamc@143:
adamc@143: Ltac tautReflect P :=
adamc@143: match P with
adamc@143: | True => TautTrue
adamc@143: | ?P1 /\ ?P2 =>
adamc@143: let t1 := tautReflect P1 in
adamc@143: let t2 := tautReflect P2 in
adamc@143: constr:(TautAnd t1 t2)
adamc@143: | ?P1 \/ ?P2 =>
adamc@143: let t1 := tautReflect P1 in
adamc@143: let t2 := tautReflect P2 in
adamc@143: constr:(TautOr t1 t2)
adamc@143: | ?P1 -> ?P2 =>
adamc@143: let t1 := tautReflect P1 in
adamc@143: let t2 := tautReflect P2 in
adamc@143: constr:(TautImp t1 t2)
adamc@143: end.
adamc@143:
adamc@143: (** With [tautReflect] available, it is easy to finish our reflective tactic. We look at the goal formula, reflect it, and apply [tautTrue] to the reflected formula. *)
adamc@143:
adamc@143: Ltac obvious :=
adamc@143: match goal with
adamc@143: | [ |- ?P ] =>
adamc@143: let t := tautReflect P in
adamc@143: exact (tautTrue t)
adamc@143: end.
adamc@143:
adamc@143: (** We can verify that [obvious] solves our original example, with a proof term that does not mention details of the proof. *)
adamc@148: (* end thide *)
adamc@143:
adamc@143: Theorem true_galore' : (True /\ True) -> (True \/ (True /\ (True -> True))).
adamc@143: obvious.
adamc@143: Qed.
adamc@143:
adamc@143: Print true_galore'.
adamc@143:
adamc@221: (** %\vspace{-.15in}% [[
adamc@143: true_galore' =
adamc@143: tautTrue
adamc@143: (TautImp (TautAnd TautTrue TautTrue)
adamc@143: (TautOr TautTrue (TautAnd TautTrue (TautImp TautTrue TautTrue))))
adamc@143: : True /\ True -> True \/ True /\ (True -> True)
adamc@221:
adamc@143: ]]
adamc@143:
adamc@143: It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula reflection process is just as ad-hoc as before, so we gain little there. In general, proofs will be more complicated than formula translation, and the "generic proof rule" that we apply here %\textit{%##is##%}% on much better formal footing than a recursive Ltac function. The dependent type of the proof guarantees that it "works" on any input formula. This is all in addition to the proof-size improvement that we have already seen. *)
adamc@144:
adamc@144:
adamc@145: (** * A Monoid Expression Simplifier *)
adamc@145:
adamc@146: (** 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. *)
adamc@146:
adamc@145: Section monoid.
adamc@145: Variable A : Set.
adamc@145: Variable e : A.
adamc@145: Variable f : A -> A -> A.
adamc@145:
adamc@145: Infix "+" := f.
adamc@145:
adamc@145: Hypothesis assoc : forall a b c, (a + b) + c = a + (b + c).
adamc@145: Hypothesis identl : forall a, e + a = a.
adamc@145: Hypothesis identr : forall a, a + e = a.
adamc@145:
adamc@146: (** 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.
adamc@146:
adamc@146: 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. *)
adamc@146:
adamc@148: (* begin thide *)
adamc@145: Inductive mexp : Set :=
adamc@145: | Ident : mexp
adamc@145: | Var : A -> mexp
adamc@145: | Op : mexp -> mexp -> mexp.
adamc@145:
adamc@146: (** Next, we write an "un-reflect" function. *)
adamc@146:
adamc@145: Fixpoint mdenote (me : mexp) : A :=
adamc@145: match me with
adamc@145: | Ident => e
adamc@145: | Var v => v
adamc@145: | Op me1 me2 => mdenote me1 + mdenote me2
adamc@145: end.
adamc@145:
adamc@146: (** 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. *)
adamc@146:
adamc@145: Fixpoint mldenote (ls : list A) : A :=
adamc@145: match ls with
adamc@145: | nil => e
adamc@145: | x :: ls' => x + mldenote ls'
adamc@145: end.
adamc@145:
adamc@146: (** The flattening function itself is easy to implement. *)
adamc@146:
adamc@145: Fixpoint flatten (me : mexp) : list A :=
adamc@145: match me with
adamc@145: | Ident => nil
adamc@145: | Var x => x :: nil
adamc@145: | Op me1 me2 => flatten me1 ++ flatten me2
adamc@145: end.
adamc@145:
adamc@146: (** [flatten] has a straightforward correctness proof in terms of our [denote] functions. *)
adamc@146:
adamc@146: Lemma flatten_correct' : forall ml2 ml1,
adamc@146: mldenote ml1 + mldenote ml2 = mldenote (ml1 ++ ml2).
adamc@145: induction ml1; crush.
adamc@145: Qed.
adamc@145:
adamc@145: Theorem flatten_correct : forall me, mdenote me = mldenote (flatten me).
adamc@145: Hint Resolve flatten_correct'.
adamc@145:
adamc@145: induction me; crush.
adamc@145: Qed.
adamc@145:
adamc@146: (** Now it is easy to prove a theorem that will be the main tool behind our simplification tactic. *)
adamc@146:
adamc@146: Theorem monoid_reflect : forall me1 me2,
adamc@146: mldenote (flatten me1) = mldenote (flatten me2)
adamc@146: -> mdenote me1 = mdenote me2.
adamc@145: intros; repeat rewrite flatten_correct; assumption.
adamc@145: Qed.
adamc@145:
adamc@146: (** We implement reflection into the [mexp] type. *)
adamc@146:
adamc@146: Ltac reflect me :=
adamc@146: match me with
adamc@145: | e => Ident
adamc@146: | ?me1 + ?me2 =>
adamc@146: let r1 := reflect me1 in
adamc@146: let r2 := reflect me2 in
adamc@145: constr:(Op r1 r2)
adamc@146: | _ => constr:(Var me)
adamc@145: end.
adamc@145:
adamc@146: (** The final [monoid] tactic works on goals that equate two monoid terms. We reflect each and change the goal to refer to the reflected versions, finishing off by applying [monoid_reflect] and simplifying uses of [mldenote]. *)
adamc@146:
adamc@145: Ltac monoid :=
adamc@145: match goal with
adamc@146: | [ |- ?me1 = ?me2 ] =>
adamc@146: let r1 := reflect me1 in
adamc@146: let r2 := reflect me2 in
adamc@145: change (mdenote r1 = mdenote r2);
adamc@145: apply monoid_reflect; simpl mldenote
adamc@145: end.
adamc@145:
adamc@146: (** We can make short work of theorems like this one: *)
adamc@146:
adamc@148: (* end thide *)
adamc@148:
adamc@145: Theorem t1 : forall a b c d, a + b + c + d = a + (b + c) + d.
adamc@146: intros; monoid.
adamc@146: (** [[
adamc@146: ============================
adamc@146: a + (b + (c + (d + e))) = a + (b + (c + (d + e)))
adamc@221:
adamc@146: ]]
adamc@146:
adamc@146: [monoid] has canonicalized both sides of the equality, such that we can finish the proof by reflexivity. *)
adamc@146:
adamc@145: reflexivity.
adamc@145: Qed.
adamc@146:
adamc@146: (** It is interesting to look at the form of the proof. *)
adamc@146:
adamc@146: Print t1.
adamc@221: (** %\vspace{-.15in}% [[
adamc@146: t1 =
adamc@146: fun a b c d : A =>
adamc@146: monoid_reflect (Op (Op (Op (Var a) (Var b)) (Var c)) (Var d))
adamc@146: (Op (Op (Var a) (Op (Var b) (Var c))) (Var d))
adamc@146: (refl_equal (a + (b + (c + (d + e)))))
adamc@146: : forall a b c d : A, a + b + c + d = a + (b + c) + d
adamc@221:
adamc@146: ]]
adamc@146:
adamc@146: The proof term contains only restatements of the equality operands in reflected form, followed by a use of reflexivity on the shared canonical form. *)
adamc@221:
adamc@145: End monoid.
adamc@145:
adamc@146: (** Extensions of this basic approach are used in the implementations of the [ring] and [field] tactics that come packaged with Coq. *)
adamc@146:
adamc@145:
adamc@144: (** * A Smarter Tautology Solver *)
adamc@144:
adamc@221: (** Now we are ready to revisit our earlier tautology solver example. We want to broaden the scope of the tactic to include formulas whose truth is not syntactically apparent. We will want to allow injection of arbitrary formulas, like we allowed arbitrary monoid expressions in the last example. Since we are working in a richer theory, it is important to be able to use equalities between different injected formulas. For instance, we cannot prove [P -> P] by translating the formula into a value like [Imp (Var P) (Var P)], because a Gallina function has no way of comparing the two [P]s for equality.
adamc@147:
adamc@147: To arrive at a nice implementation satisfying these criteria, we introduce the [quote] tactic and its associated library. *)
adamc@147:
adamc@144: Require Import Quote.
adamc@144:
adamc@148: (* begin thide *)
adamc@144: Inductive formula : Set :=
adamc@144: | Atomic : index -> formula
adamc@144: | Truth : formula
adamc@144: | Falsehood : formula
adamc@144: | And : formula -> formula -> formula
adamc@144: | Or : formula -> formula -> formula
adamc@144: | Imp : formula -> formula -> formula.
adamc@144:
adamc@147: (** The type [index] comes from the [Quote] library and represents a countable variable type. The rest of [formula]'s definition should be old hat by now.
adamc@147:
adamc@147: The [quote] tactic will implement injection from [Prop] into [formula] for us, but it is not quite as smart as we might like. In particular, it interprets implications incorrectly, so we will need to declare a wrapper definition for implication, as we did in the last chapter. *)
adamc@144:
adamc@144: Definition imp (P1 P2 : Prop) := P1 -> P2.
adamc@144: Infix "-->" := imp (no associativity, at level 95).
adamc@144:
adamc@147: (** Now we can define our denotation function. *)
adamc@147:
adamc@147: Definition asgn := varmap Prop.
adamc@147:
adamc@144: Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
adamc@144: match f with
adamc@144: | Atomic v => varmap_find False v atomics
adamc@144: | Truth => True
adamc@144: | Falsehood => False
adamc@144: | And f1 f2 => formulaDenote atomics f1 /\ formulaDenote atomics f2
adamc@144: | Or f1 f2 => formulaDenote atomics f1 \/ formulaDenote atomics f2
adamc@144: | Imp f1 f2 => formulaDenote atomics f1 --> formulaDenote atomics f2
adamc@144: end.
adamc@144:
adamc@147: (** The [varmap] type family implements maps from [index] values. In this case, we define an assignment as a map from variables to [Prop]s. [formulaDenote] works with an assignment, and we use the [varmap_find] function to consult the assignment in the [Atomic] case. The first argument to [varmap_find] is a default value, in case the variable is not found. *)
adamc@147:
adamc@144: Section my_tauto.
adamc@144: Variable atomics : asgn.
adamc@144:
adamc@144: Definition holds (v : index) := varmap_find False v atomics.
adamc@144:
adamc@147: (** We define some shorthand for a particular variable being true, and now we are ready to define some helpful functions based on the [ListSet] module of the standard library, which (unsurprisingly) presents a view of lists as sets. *)
adamc@147:
adamc@144: Require Import ListSet.
adamc@144:
adamc@144: Definition index_eq : forall x y : index, {x = y} + {x <> y}.
adamc@144: decide equality.
adamc@144: Defined.
adamc@144:
adamc@144: Definition add (s : set index) (v : index) := set_add index_eq v s.
adamc@147:
adamc@221: Definition In_dec : forall v (s : set index), {In v s} + {~ In v s}.
adamc@221: Local Open Scope specif_scope.
adamc@144:
adamc@221: intro; refine (fix F (s : set index) : {In v s} + {~ In v s} :=
adamc@221: match s with
adamc@144: | nil => No
adamc@144: | v' :: s' => index_eq v' v || F s'
adamc@144: end); crush.
adamc@144: Defined.
adamc@144:
adamc@147: (** We define what it means for all members of an index set to represent true propositions, and we prove some lemmas about this notion. *)
adamc@147:
adamc@144: Fixpoint allTrue (s : set index) : Prop :=
adamc@144: match s with
adamc@144: | nil => True
adamc@144: | v :: s' => holds v /\ allTrue s'
adamc@144: end.
adamc@144:
adamc@144: Theorem allTrue_add : forall v s,
adamc@144: allTrue s
adamc@144: -> holds v
adamc@144: -> allTrue (add s v).
adamc@144: induction s; crush;
adamc@144: match goal with
adamc@144: | [ |- context[if ?E then _ else _] ] => destruct E
adamc@144: end; crush.
adamc@144: Qed.
adamc@144:
adamc@144: Theorem allTrue_In : forall v s,
adamc@144: allTrue s
adamc@144: -> set_In v s
adamc@144: -> varmap_find False v atomics.
adamc@144: induction s; crush.
adamc@144: Qed.
adamc@144:
adamc@144: Hint Resolve allTrue_add allTrue_In.
adamc@144:
adamc@221: Local Open Scope partial_scope.
adamc@144:
adamc@147: (** Now we can write a function [forward] which implements deconstruction of hypotheses. It has a dependent type, in the style of Chapter 6, 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]. *)
adamc@147:
adamc@144: Definition forward (f : formula) (known : set index) (hyp : formula)
adamc@144: (cont : forall known', [allTrue known' -> formulaDenote atomics f])
adamc@144: : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f].
adamc@144: refine (fix F (f : formula) (known : set index) (hyp : formula)
adamc@221: (cont : forall known', [allTrue known' -> formulaDenote atomics f])
adamc@144: : [allTrue known -> formulaDenote atomics hyp -> formulaDenote atomics f] :=
adamc@221: match hyp with
adamc@144: | Atomic v => Reduce (cont (add known v))
adamc@144: | Truth => Reduce (cont known)
adamc@144: | Falsehood => Yes
adamc@144: | And h1 h2 =>
adamc@144: Reduce (F (Imp h2 f) known h1 (fun known' =>
adamc@144: Reduce (F f known' h2 cont)))
adamc@144: | Or h1 h2 => F f known h1 cont && F f known h2 cont
adamc@144: | Imp _ _ => Reduce (cont known)
adamc@144: end); crush.
adamc@144: Defined.
adamc@144:
adamc@147: (** A [backward] function implements analysis of the final goal. It calls [forward] to handle implications. *)
adamc@147:
adamc@221: Definition backward (known : set index) (f : formula)
adamc@221: : [allTrue known -> formulaDenote atomics f].
adamc@221: refine (fix F (known : set index) (f : formula)
adamc@221: : [allTrue known -> formulaDenote atomics f] :=
adamc@221: match f with
adamc@144: | Atomic v => Reduce (In_dec v known)
adamc@144: | Truth => Yes
adamc@144: | Falsehood => No
adamc@144: | And f1 f2 => F known f1 && F known f2
adamc@144: | Or f1 f2 => F known f1 || F known f2
adamc@144: | Imp f1 f2 => forward f2 known f1 (fun known' => F known' f2)
adamc@144: end); crush; eauto.
adamc@144: Defined.
adamc@144:
adamc@147: (** A simple wrapper around [backward] gives us the usual type of a partial decision procedure. *)
adamc@147:
adamc@144: Definition my_tauto (f : formula) : [formulaDenote atomics f].
adamc@144: intro; refine (Reduce (backward nil f)); crush.
adamc@144: Defined.
adamc@144: End my_tauto.
adamc@144:
adamc@147: (** Our final tactic implementation is now fairly straightforward. First, we [intro] all quantifiers that do not bind [Prop]s. Then we call the [quote] tactic, which implements the reflection for us. Finally, we are able to construct an exact proof via [partialOut] and the [my_tauto] Gallina function. *)
adamc@147:
adamc@144: Ltac my_tauto :=
adamc@144: repeat match goal with
adamc@144: | [ |- forall x : ?P, _ ] =>
adamc@144: match type of P with
adamc@144: | Prop => fail 1
adamc@144: | _ => intro
adamc@144: end
adamc@144: end;
adamc@144: quote formulaDenote;
adamc@144: match goal with
adamc@144: | [ |- formulaDenote ?m ?f ] => exact (partialOut (my_tauto m f))
adamc@144: end.
adamc@148: (* end thide *)
adamc@144:
adamc@147: (** A few examples demonstrate how the tactic works. *)
adamc@147:
adamc@144: Theorem mt1 : True.
adamc@144: my_tauto.
adamc@144: Qed.
adamc@144:
adamc@144: Print mt1.
adamc@221: (** %\vspace{-.15in}% [[
adamc@147: mt1 = partialOut (my_tauto (Empty_vm Prop) Truth)
adamc@147: : True
adamc@221:
adamc@147: ]]
adamc@147:
adamc@147: We see [my_tauto] applied with an empty [varmap], since every subformula is handled by [formulaDenote]. *)
adamc@144:
adamc@144: Theorem mt2 : forall x y : nat, x = y --> x = y.
adamc@144: my_tauto.
adamc@144: Qed.
adamc@144:
adamc@144: Print mt2.
adamc@221: (** %\vspace{-.15in}% [[
adamc@147: mt2 =
adamc@147: fun x y : nat =>
adamc@147: partialOut
adamc@147: (my_tauto (Node_vm (x = y) (Empty_vm Prop) (Empty_vm Prop))
adamc@147: (Imp (Atomic End_idx) (Atomic End_idx)))
adamc@147: : forall x y : nat, x = y --> x = y
adamc@221:
adamc@147: ]]
adamc@147:
adamc@147: Crucially, both instances of [x = y] are represented with the same index, [End_idx]. The value of this index only needs to appear once in the [varmap], whose form reveals that [varmap]s are represented as binary trees, where [index] values denote paths from tree roots to leaves. *)
adamc@144:
adamc@144: Theorem mt3 : forall x y z,
adamc@144: (x < y /\ y > z) \/ (y > z /\ x < S y)
adamc@144: --> y > z /\ (x < y \/ x < S y).
adamc@144: my_tauto.
adamc@144: Qed.
adamc@144:
adamc@144: Print mt3.
adamc@221: (** %\vspace{-.15in}% [[
adamc@147: fun x y z : nat =>
adamc@147: partialOut
adamc@147: (my_tauto
adamc@147: (Node_vm (x < S y) (Node_vm (x < y) (Empty_vm Prop) (Empty_vm Prop))
adamc@147: (Node_vm (y > z) (Empty_vm Prop) (Empty_vm Prop)))
adamc@147: (Imp
adamc@147: (Or (And (Atomic (Left_idx End_idx)) (Atomic (Right_idx End_idx)))
adamc@147: (And (Atomic (Right_idx End_idx)) (Atomic End_idx)))
adamc@147: (And (Atomic (Right_idx End_idx))
adamc@147: (Or (Atomic (Left_idx End_idx)) (Atomic End_idx)))))
adamc@147: : forall x y z : nat,
adamc@147: x < y /\ y > z \/ y > z /\ x < S y --> y > z /\ (x < y \/ x < S y)
adamc@221:
adamc@147: ]]
adamc@147:
adamc@147: Our goal contained three distinct atomic formulas, and we see that a three-element [varmap] is generated.
adamc@147:
adamc@147: It can be interesting to observe differences between the level of repetition in proof terms generated by [my_tauto] and [tauto] for especially trivial theorems. *)
adamc@144:
adamc@144: Theorem mt4 : True /\ True /\ True /\ True /\ True /\ True /\ False --> False.
adamc@144: my_tauto.
adamc@144: Qed.
adamc@144:
adamc@144: Print mt4.
adamc@221: (** %\vspace{-.15in}% [[
adamc@147: mt4 =
adamc@147: partialOut
adamc@147: (my_tauto (Empty_vm Prop)
adamc@147: (Imp
adamc@147: (And Truth
adamc@147: (And Truth
adamc@147: (And Truth (And Truth (And Truth (And Truth Falsehood))))))
adamc@147: Falsehood))
adamc@147: : True /\ True /\ True /\ True /\ True /\ True /\ False --> False
adamc@147: ]] *)
adamc@144:
adamc@144: Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
adamc@144: tauto.
adamc@144: Qed.
adamc@144:
adamc@144: Print mt4'.
adamc@221: (** %\vspace{-.15in}% [[
adamc@147: mt4' =
adamc@147: fun H : True /\ True /\ True /\ True /\ True /\ True /\ False =>
adamc@147: and_ind
adamc@147: (fun (_ : True) (H1 : True /\ True /\ True /\ True /\ True /\ False) =>
adamc@147: and_ind
adamc@147: (fun (_ : True) (H3 : True /\ True /\ True /\ True /\ False) =>
adamc@147: and_ind
adamc@147: (fun (_ : True) (H5 : True /\ True /\ True /\ False) =>
adamc@147: and_ind
adamc@147: (fun (_ : True) (H7 : True /\ True /\ False) =>
adamc@147: and_ind
adamc@147: (fun (_ : True) (H9 : True /\ False) =>
adamc@147: and_ind (fun (_ : True) (H11 : False) => False_ind False H11)
adamc@147: H9) H7) H5) H3) H1) H
adamc@147: : True /\ True /\ True /\ True /\ True /\ True /\ False -> False
adamc@147: ]] *)
adamc@147:
adamc@149:
adamc@149: (** * Exercises *)
adamc@149:
adamc@221: (** remove printing * *)
adamc@221:
adamc@149: (** %\begin{enumerate}%##
adamc@149:
adamc@149: %\item%#- # Implement a reflective procedure for normalizing systems of linear equations over rational numbers. In particular, the tactic should identify all hypotheses that are linear equations over rationals where the equation righthand sides are constants. It should normalize each hypothesis to have a lefthand side that is a sum of products of constants and variables, with no variable appearing multiple times. Then, your tactic should add together all of these equations to form a single new equation, possibly clearing the original equations. Some coefficients may cancel in the addition, reducing the number of variables that appear.
adamc@149:
adamc@221: To work with rational numbers, import module [QArith] and use [Local Open Scope Q_scope]. All of the usual arithmetic operator notations will then work with rationals, and there are shorthands for constants 0 and 1. Other rationals must be written as [num # den] for numerator [num] and denominator [den]. Use the infix operator [==] in place of [=], to deal with different ways of expressing the same number as a fraction. For instance, a theorem and proof like this one should work with your tactic:
adamc@149:
adamc@149: [[
adamc@149: Theorem t2 : forall x y z, (2 # 1) * (x - (3 # 2) * y) == 15 # 1
adamc@149: -> z + (8 # 1) * x == 20 # 1
adamc@149: -> (-6 # 2) * y + (10 # 1) * x + z == 35 # 1.
adamc@149: intros; reflectContext; assumption.
adamc@149: Qed.
adamc@221:
adamc@205: ]]
adamc@205:
adamc@149: Your solution can work in any way that involves reflecting syntax and doing most calculation with a Gallina function. These hints outline a particular possible solution. Throughout, the [ring] tactic will be helpful for proving many simple facts about rationals, and tactics like [rewrite] are correctly overloaded to work with rational equality [==].
adamc@149:
adamc@149: %\begin{enumerate}%#
#
adamc@221: %\item%#- # Define an inductive type [exp] of expressions over rationals (which inhabit the Coq type [Q]). Include variables (represented as natural numbers), constants, addition, subtraction, and multiplication.#
#
adamc@149: %\item%#- # Define a function [lookup] for reading an element out of a list of rationals, by its position in the list.#
#
adamc@149: %\item%#- # Define a function [expDenote] that translates [exp]s, along with lists of rationals representing variable values, to [Q].#
#
adamc@149: %\item%#- # Define a recursive function [eqsDenote] over [list (exp * Q)], characterizing when all of the equations are true.#
#
adamc@149: %\item%#- # Fix a representation [lhs] of flattened expressions. Where [len] is the number of variables, represent a flattened equation as [ilist Q len]. Each position of the list gives the coefficient of the corresponding variable.#
#
adamc@151: %\item%#- # Write a recursive function [linearize] that takes a constant [k] and an expression [e] and optionally returns an [lhs] equivalent to [k * e]. This function returns [None] when it discovers that the input expression is not linear. The parameter [len] of [lhs] should be a parameter of [linearize], too. The functions [singleton], [everywhere], and [map2] from [DepList] will probably be helpful. It is also helpful to know that [Qplus] is the identifier for rational addition.#
#
adamc@149: %\item%#- # Write a recursive function [linearizeEqs : list (exp * Q) -> option (lhs * Q)]. This function linearizes all of the equations in the list in turn, building up the sum of the equations. It returns [None] if the linearization of any constituent equation fails.#
#
adamc@149: %\item%#- # Define a denotation function for [lhs].#
#
adamc@149: %\item%#- # Prove that, when [exp] linearization succeeds on constant [k] and expression [e], the linearized version has the same meaning as [k * e].#
#
adamc@149: %\item%#- # Prove that, when [linearizeEqs] succeeds on an equation list [eqs], then the final summed-up equation is true whenever the original equation list is true.#
#
adamc@149: %\item%#- # Write a tactic [findVarsHyps] to search through all equalities on rationals in the context, recursing through addition, subtraction, and multiplication to find the list of expressions that should be treated as variables. This list should be suitable as an argument to [expDenote] and [eqsDenote], associating a [Q] value to each natural number that stands for a variable.#
#
adamc@149: %\item%#- # Write a tactic [reflect] to reflect a [Q] expression into [exp], with respect to a given list of variable values.#
#
adamc@149: %\item%#- # Write a tactic [reflectEqs] to reflect a formula that begins with a sequence of implications from linear equalities whose lefthand sides are expressed with [expDenote]. This tactic should build a [list (exp * Q)] representing the equations. Remember to give an explicit type annotation when returning a nil list, as in [constr:(@nil (exp * Q))].#
#
adamc@149: %\item%#- # Now this final tactic should do the job:
adamc@221:
adamc@149: [[
adamc@149: Ltac reflectContext :=
adamc@149: let ls := findVarsHyps in
adamc@149: repeat match goal with
adamc@149: | [ H : ?e == ?num # ?den |- _ ] =>
adamc@149: let r := reflect ls e in
adamc@149: change (expDenote ls r == num # den) in H;
adamc@149: generalize H
adamc@149: end;
adamc@149: match goal with
adamc@149: | [ |- ?g ] => let re := reflectEqs g in
adamc@149: intros;
adamc@149: let H := fresh "H" in
adamc@149: assert (H : eqsDenote ls re); [ simpl in *; tauto
adamc@149: | repeat match goal with
adamc@149: | [ H : expDenote _ _ == _ |- _ ] => clear H
adamc@149: end;
adamc@149: generalize (linearizeEqsCorrect ls re H); clear H; simpl;
adamc@149: match goal with
adamc@149: | [ |- ?X == ?Y -> _ ] =>
adamc@149: ring_simplify X Y; intro
adamc@149: end ]
adamc@149: end.
adamc@149:
adamc@205: ]]
adamc@205:
adamc@149: #
#%\end{enumerate}%
adamc@149: # #
adamc@149:
adamc@149: #
#%\end{enumerate}% *)