Proving Evenness

Proving that particular natural-number constants are even is certainly something we would rather have happen automatically. The Ltac-programming techniques that we learned previously make it easy to implement such a procedure.

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

Theorem even_256_repeat : Even 256.
Even 256
Proof.
Even 256
  repeat constructor.
Qed.

Theorem even_256_eauto : Even 256.
Even 256
Proof.
Even 256
  Hint Constructors Even : core.
Even 256
  eauto 129.
Qed.

Set Printing All.
Print even_256_repeat.
even_256_repeat =
Even_SS
  (S (S (S (S (S (S (S (S (S (S (S (S (...)))))))))))))
  (Even_SS
     (S (S (S (S (S (S (S (S (S (S (S (...))))))))))))
     (Even_SS
        (S (S (S (S (S (S (S (S (S (S (...)))))))))))
        (Even_SS
           (S (S (S (S (S (S (S (S (S (...))))))))))
           (Even_SS
              (S (S (S (S (S (S (S (S (...)))))))))
              (Even_SS
                 (S (S (S (S (S (S (S (...))))))))
                 (Even_SS
                    (S (S (S (S (S (S (...)))))))
                    (Even_SS (S (S (S (S (S (...))))))
                       (Even_SS (S (S (S (S (...)))))
                          (Even_SS (S (S (S (...))))
                             (Even_SS (S (S (...)))
                                (Even_SS (S (...))
                                   (Even_SS (...)
                                      (...)))))))))))))
     : Even
         (S
            (S
               (S
                  (S
                     (S
                        (S
                           (S
                              (S (S (S (S (S (...)))))))))))))
Print even_256_eauto.
even_256_eauto =
Even_SS
  (S (S (S (S (S (S (S (S (S (S (S (S (...)))))))))))))
  (Even_SS
     (S (S (S (S (S (S (S (S (S (S (S (...))))))))))))
     (Even_SS
        (S (S (S (S (S (S (S (S (S (S (...)))))))))))
        (Even_SS
           (S (S (S (S (S (S (S (S (S (...))))))))))
           (Even_SS
              (S (S (S (S (S (S (S (S (...)))))))))
              (Even_SS
                 (S (S (S (S (S (S (S (...))))))))
                 (Even_SS
                    (S (S (S (S (S (S (...)))))))
                    (Even_SS (S (S (S (S (S (...))))))
                       (Even_SS (S (S (S (S (...)))))
                          (Even_SS (S (S (S (...))))
                             (Even_SS (S (S (...)))
                                (Even_SS (S (...))
                                   (Even_SS (...)
                                      (...)))))))))))))
     : Even
         (S
            (S
               (S
                  (S
                     (S
                        (S
                           (S
                              (S (S (S (S (S (...)))))))))))))
Unset Printing All.

Here we see a term of Coq's core proof language, which we don't explain in detail, but roughly speaking such a term is a syntax tree recording which lemmas were used, and how their quantifiers were instantiated, to prove a theorem. This Ltac 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 superlinear in the input value, which we reveal with Set Printing All, to disable all syntactic niceties and show every node of the internal proof AST. The problem is that each Even_SS application needs a choice of n, and we wind up giving every even number from 0 to 254 in that position, at some point or another, for quadratic proof-term size.

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.

The techniques of proof by reflection address both complaints. We will be able to write proofs like in the example above with constant size overhead beyond the size of the input, and we will do it with verified decision procedures written in Gallina.

Fixpoint evenp (n : nat) : bool :=
  match n with
  | 0 => true
  | 1 => false
  | S (S n') => evenp n'
  end.

To prove evenp sound, we perform two IH strengthenings:

• Effectively switch to strong induction with an extra numeric variable, asserted to be less than the one we induct on.

• Express both cases for how a evenp test might turn out.

Lemma evenp_ok' : forall N n,
    n < N ->
    if evenp n then Even n else ~Even n.
forall N n : nat,
n < N -> if evenp n then Even n else ~ Even n
Proof.
forall N n : nat,
n < N -> if evenp n then Even n else ~ Even n
  induction N; simpl; intros;
    destruct n as [ | [ | ] ]; simpl; try lia.
N: nat
IHN: forall n : nat, n < N -> if evenp n then Even n else ~ Even n
H: 0 < S N
Even 0
N: nat
IHN: forall n : nat, n < N -> if evenp n then Even n else ~ Even n
H: 1 < S N
~ Even 1
N: nat
IHN: forall n : nat, n < N -> if evenp n then Even n else ~ Even n
n: nat
H: S (S n) < S N
if evenp n then Even (S (S n)) else ~ Even (S (S n))

  -
N: nat
IHN: forall n : nat, n < N -> if evenp n then Even n else ~ Even n
H: 0 < S N
Even 0 constructor.
  -
N: nat
IHN: forall n : nat, n < N -> if evenp n then Even n else ~ Even n
H: 1 < S N
~ Even 1 inversion 1.
  -
N: nat
IHN: forall n : nat, n < N -> if evenp n then Even n else ~ Even n
n: nat
H: S (S n) < S N
if evenp n then Even (S (S n)) else ~ Even (S (S n)) specialize (IHN n ltac:(lia)).
N, n: nat
IHN: if evenp n then Even n else ~ Even n
H: S (S n) < S N
if evenp n then Even (S (S n)) else ~ Even (S (S n))
    destruct evenp; (constructor || inversion 1); eauto.
Qed.

Fixpoint evenp_ok'' n :
  if evenp n then Even n else ~Even n.
evenp_ok'': forall n : nat,
if evenp n then Even n else ~ Even n
n: nat
if evenp n then Even n else ~ Even n
Proof.
evenp_ok'': forall n : nat,
if evenp n then Even n else ~ Even n
n: nat
if evenp n then Even n else ~ Even n
  destruct n as [ | [ | ] ]; simpl.
evenp_ok'': forall n : nat,
if evenp n then Even n else ~ Even n
Even 0
evenp_ok'': forall n : nat,
if evenp n then Even n else ~ Even n
~ Even 1
evenp_ok'': forall n : nat,
if evenp n then Even n else ~ Even n
n: nat
if evenp n then Even (S (S n)) else ~ Even (S (S n))
  -
evenp_ok'': forall n : nat,
if evenp n then Even n else ~ Even n
Even 0 constructor.
  -
evenp_ok'': forall n : nat,
if evenp n then Even n else ~ Even n
~ Even 1 inversion 1.
  -
evenp_ok'': forall n : nat,
if evenp n then Even n else ~ Even n
n: nat
if evenp n then Even (S (S n)) else ~ Even (S (S n)) specialize (evenp_ok'' n).
n: nat
evenp_ok'': if evenp n then Even n else ~ Even n
if evenp n then Even (S (S n)) else ~ Even (S (S n))
    destruct evenp.
n: nat
evenp_ok'': Even n
Even (S (S n))
n: nat
evenp_ok'': ~ Even n
~ Even (S (S n))
    +
n: nat
evenp_ok'': Even n
Even (S (S n)) constructor; eauto.
    +
n: nat
evenp_ok'': ~ Even n
~ Even (S (S n)) inversion 1; eauto.
Qed.

Theorem evenp_ok : forall n,
    evenp n = true -> Even n.
forall n : nat, evenp n = true -> Even n
Proof.
forall n : nat, evenp n = true -> Even n
  intros n H.
n: nat
H: evenp n = true
Even n
  pose proof (evenp_ok' (S n) n ltac:(lia)) as H0.
n: nat
H: evenp n = true
H0: if evenp n then Even n else ~ Even n
Even n
  rewrite H in H0.
n: nat
H: evenp n = true
H0: Even n
Even n
  assumption.
Qed.

As this theorem establishes, the function evenp may be viewed as a verified decision procedure. It is now trivial to write a tactic to prove evenness.

Ltac prove_even_reflective :=
  match goal with
    | [ |- Even _ ] => apply evenp_ok; reflexivity
  end.

Theorem even_256' : Even 256.
Even 256
Proof.
Even 256
  prove_even_reflective.
Qed.

Set Printing All.
Print even_256'.
even_256' =
evenp_ok
  (S (S (S (S (S (S (S (S (S (S (S (S (...)))))))))))))
  (@eq_refl bool true)
     : Even
         (S
            (S
               (S
                  (S
                     (S
                        (S
                           (S
                              (S (S (S (S (S (...)))))))))))))
Unset Printing All.

Notice that only one nat appears as an argument to an applied lemma, and that's the original number to test for evenness. Proof-term size scales linearly.

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

Theorem even_255 : Even 255.
Even 255
Proof.
Even 255
  Fail prove_even_reflective.
The command has indeed failed with message:
Unable to unify "true" with "evenp 255".
Even 255
Abort.

Coq reports that reflexivity can't prove false = true, which makes perfect sense!

Our tactic prove_even_reflective is reflective because it performs a proof-search process (a trivial one, in this case) wholly within Gallina.

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))).
True /\ True -> True \/ True /\ (True -> True)
Proof.
True /\ True -> True \/ True /\ (True -> True)
  tauto.
Qed.

Print true_galore.
true_galore =
fun H : True /\ True =>
and_ind (fun _ _ : True => or_introl I) H
     : True /\ True -> True \/ True /\ (True -> True)

As we might expect, the proof that tauto builds contains explicit applications of deduction rules. For large formulas, this can add a linear amount of proof-size overhead, beyond the size of the input.

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 reify Prop into some type that we can analyze. This inductive type is a good candidate:

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

We write a recursive function to reflect this syntax back to Prop. Such functions are also called interpretation functions, and we have used them in previous examples to give semantics to small programming languages.

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.
forall t : taut, tautDenote t
Proof.
forall t : taut, tautDenote t
  induction t; simpl; intuition.
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. Recall that the change tactic replaces a conclusion formula with another that is equal to it, as shown by partial execution of terms.

Ltac obvious :=
  match goal with
    | [ |- ?P ] =>
      let t := tautReify P in
      change (tautDenote t); apply tautTrue
  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))).
True /\ True -> True \/ True /\ (True -> True)
Proof.
True /\ True -> True \/ True /\ (True -> True)
  obvious.
Qed.

Set Printing All.
Print true_galore'.
true_galore' =
tautTrue
  (TautImp (TautAnd TautTrue TautTrue)
     (TautOr TautTrue
        (TautAnd TautTrue (TautImp TautTrue TautTrue))))
     : forall _ : and True True,
       or True (and True (forall _ : True, True))
Unset Printing All.

It is worth considering how the reflective tactic improves on a pure-Ltac implementation. The formula-reification 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 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 benefit is in addition to the proof-size improvement that we have already seen.

It may also be worth pointing out that our previous example of evenness testing used a test evenp that could sometimes fail, while here we avoid the extra Boolean test by identifying a syntactic class of formulas that are always true by construction. Of course, many interesting proof steps don't have that structure, so let's look at an example that still requires extra proving after the reflective step.

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 => []
    | Var x => [x]
    | 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 ++ ml2) = mldenote ml1 + mldenote ml2.
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
forall ml2 ml1 : list A,
mldenote (ml1 ++ ml2) = mldenote ml1 + mldenote ml2
  Proof.
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
forall ml2 ml1 : list A,
mldenote (ml1 ++ ml2) = mldenote ml1 + mldenote ml2
    induction ml1; simpl; congruence.
  Qed.

  Hint Rewrite flatten_correct'.

  Theorem flatten_correct :
    forall me, mdenote me = mldenote (flatten me).
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
forall me : mexp, mdenote me = mldenote (flatten me)
  Proof.
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
forall me : mexp, mdenote me = mldenote (flatten me)
    induction me; simpl; autorewrite with core; intuition congruence.
  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.
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
forall me1 me2 : mexp,
mldenote (flatten me1) = mldenote (flatten me2) ->
mdenote me1 = mdenote me2
  Proof.
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
forall me1 me2 : mexp,
mldenote (flatten me1) = mldenote (flatten me2) ->
mdenote me1 = mdenote me2
    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.

  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 + e + d = a + (b + c) + d.
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
forall a b c d : A,
a + b + c + e + d = a + (b + c) + d
  Proof.
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
forall a b c d : A,
a + b + c + e + d = a + (b + c) + d
    intros; monoid.
A: Set
e: A
f: A -> A -> A
assoc: forall a b c : A, a + b + c = a + (b + c)
identl: forall a : A, e + a = a
identr: forall a : A, a + e = a
a, b, c, d: A
a + (b + (c + (d + e))) = a + (b + (c + (d + e)))

Our tactic has canonicalized both sides of the equality, such that we can finish the proof by reflexivity.

    reflexivity.
  Qed.

It is interesting to look at the form of the proof.

  Set Printing All.
  Print t1.
t1 =
fun a b c d : A =>
monoid_reflect
  (Op (Op (Op (Op (Var a) (Var b)) (Var c)) Ident)
     (Var d))
  (Op (Op (Var a) (Op (Var b) (Var c))) (Var d))
  (@eq_refl A (f a (f b (f c (f d e))))
   :
   @eq A
     (mldenote
        (flatten
           (Op
              (Op (Op (Op (Var a) (Var b)) (Var c))
                 Ident) (Var d))))
     (mldenote
        (flatten
           (Op (Op (Var a) (Op (Var b) (Var c)))
              (Var d)))))
     : forall a b c d : A,
       @eq A (f (f (f (f a b) c) e) d)
         (f (f a (f b c)) d)

Arguments t1 a b c d
t1 uses section variables A e f assoc identl identr.
  Unset Printing All.

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.

Extensions of this basic approach are used in the implementations of the ring, field, and lia tactics that come packaged with Coq:

Require Import ZArith.
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
Module LiaExample.
  Open Scope Z_scope.

  Theorem arith_example x y z:
    x < 3 ->
    y < 7 ->
    z < 5 ->
    2*x + 3*y + z < 50.
x, y, z: Z
x < 3 -> y < 7 -> z < 5 -> 2 * x + 3 * y + z < 50
  Proof.
x, y, z: Z
x < 3 -> y < 7 -> z < 5 -> 2 * x + 3 * y + z < 50
    lia.
  Defined.

  Open Scope positive_scope.
  Arguments arith_example /.
  Eval simpl in arith_example.
= fun (x y z : Z) (H : (x < 3)%Z)
    (H0 : (y < 7)%Z) (H1 : (z < 5)%Z) =>
  ZMicromega.ZTautoChecker_sound
    (Tauto.IMPL
       (Tauto.A Tauto.isProp
          {|
            RingMicromega.Flhs := EnvRing.PEX 3;
            RingMicromega.Fop :=
              RingMicromega.OpLt;
            RingMicromega.Frhs := EnvRing.PEc 5%Z
          |} tt) None
       (Tauto.IMPL
          (Tauto.A Tauto.isProp
             {|
               RingMicromega.Flhs :=
                 EnvRing.PEX 2;
               RingMicromega.Fop :=
                 RingMicromega.OpLt;
               RingMicromega.Frhs :=
                 EnvRing.PEc 7%Z
             |} tt) None
          (Tauto.IMPL
             (Tauto.A Tauto.isProp
                {|
                  RingMicromega.Flhs :=
                    EnvRing.PEX 1;
                  RingMicromega.Fop :=
                    RingMicromega.OpLt;
                  RingMicromega.Frhs :=
                    EnvRing.PEc 3%Z
                |} tt) None
             (Tauto.A Tauto.isProp
                {|
                  RingMicromega.Flhs :=
                    EnvRing.PEadd
                      (EnvRing.PEadd
                         (EnvRing.PEmul
                            (EnvRing.PEc 2%Z)
                            (EnvRing.PEX 1))
                         (EnvRing.PEmul
                            (EnvRing.PEc 3%Z)
                            (EnvRing.PEX 2)))
                      (EnvRing.PEX 3);
                  RingMicromega.Fop :=
                    RingMicromega.OpLt;
                  RingMicromega.Frhs :=
                    EnvRing.PEc 50%Z
                |} tt))))
    [ZMicromega.RatProof
       (RingMicromega.PsatzAdd
          (RingMicromega.PsatzIn Z 3)
          (RingMicromega.PsatzAdd
             (RingMicromega.PsatzMulE
                (RingMicromega.PsatzC 3%Z)
                (RingMicromega.PsatzIn Z 2))
             (RingMicromega.PsatzAdd
                (RingMicromega.PsatzMulE
                   (RingMicromega.PsatzC 2%Z)
                   (RingMicromega.PsatzIn Z 1))
                (RingMicromega.PsatzIn Z 0))))
       ZMicromega.DoneProof] eq_refl
    (fun p : positive =>
     match p with
     | _~1 => z
     | _~0 => y
     | 1 => x
     end) H1 H0 H
: forall x y z : Z,
  (x < 3)%Z ->
  (y < 7)%Z ->
  (z < 5)%Z -> (2 * x + 3 * y + z < 50)%Z
End LiaExample.

Note the call to ZMicromega.ZTautoChecker_sound and the argument eq_refl to satisfy the hypothesis relating to the boolean check ZMicromega.ZTautoChecker:

Check ZMicromega.ZTautoChecker_sound.
ZMicromega.ZTautoChecker_sound
     : forall
         (f : Tauto.BFormula (RingMicromega.Formula Z)
                Tauto.isProp)
         (w : list ZMicromega.ZArithProof),
       ZMicromega.ZTautoChecker f w = true ->
       forall env : RingMicromega.PolEnv Z,
       Tauto.eval_bf (ZMicromega.Zeval_formula env) f

A Smarter Tautology Solver

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 Ps for equality.

We introduce a synonym for how we name variables: natural numbers.

Definition propvar := nat.

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

Now we can define our denotation function. First, a type of truth-value assignments to propositional variables:

Definition asgn := nat -> Prop.

Fixpoint formulaDenote (atomics : asgn) (f : formula) : Prop :=
  match f with
    | Atomic v => atomics v
    | 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.

Require Import ListSet.

Section my_tauto.
  Variable atomics : asgn.

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.

The eq_nat_dec below is a richly typed equality test on nats. See SubsetTypes.v for a review.

  Definition add (s : set propvar) (v : propvar) :=
    set_add eq_nat_dec v s.

We define what it means for all members of a variable set to represent true propositions, and we prove some lemmas about this notion.

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

  Theorem allTrue_add : forall v s,
    allTrue s
    -> atomics v
    -> allTrue (add s v).
atomics: asgn
forall (v : nat) (s : set propvar),
allTrue s -> atomics v -> allTrue (add s v)
  Proof.
atomics: asgn
forall (v : nat) (s : set propvar),
allTrue s -> atomics v -> allTrue (add s v)
    induction s; simpl; intuition;
      match goal with
        | [ |- context[if ?E then _ else _] ] => destruct E
      end; simpl; intuition.
  Qed.

  Theorem allTrue_In : forall v s,
    allTrue s
    -> set_In v s
    -> atomics v.
atomics: asgn
forall (v : propvar) (s : set propvar),
allTrue s -> set_In v s -> atomics v
  Proof.
atomics: asgn
forall (v : propvar) (s : set propvar),
allTrue s -> set_In v s -> atomics v
    induction s; simpl; intros; intuition congruence.
  Qed.

Now we can write a function forward that implements deconstruction of 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 (advanced functional-programming feature that often puzzles novices, so don't worry if it takes a while to digest!), which will be called once for each case.

  Fixpoint forward (known : set propvar) (hyp : formula)
           (cont : set propvar -> bool) : bool :=
    match hyp with
    | Atomic v => cont (add known v)
    | Truth => cont known
    | Falsehood => true
    | And h1 h2 => forward known h1 (fun known' =>
                     forward known' h2 cont)
    | Or h1 h2 => forward known h1 cont && forward known h2 cont
    | Imp _ _ => cont known
    end.

Some examples might help get the idea across.

  Compute fun cont =>
            forward [] (Atomic 0) cont.
= fun cont : set propvar -> bool => cont [0]
: (set propvar -> bool) -> bool
  Compute fun cont =>
            forward [] (Or (Atomic 0) (Atomic 1)) cont.
= fun cont : set propvar -> bool =>
  if cont [0] then cont [1] else false
: (set propvar -> bool) -> bool
  Compute fun cont =>
            forward [] (Or (Atomic 0) (And (Atomic 1) (Atomic 2))) cont.
= fun cont : set propvar -> bool =>
  if cont [0] then cont [1; 2] else false
: (set propvar -> bool) -> bool

A backward function implements analysis of the final goal. It calls forward to handle implications.

  Fixpoint backward (known : set propvar) (f : formula) : bool :=
    match f with
    | Atomic v => if In_dec eq_nat_dec v known then true else false
    | Truth => true
    | Falsehood => false
    | And f1 f2 => backward known f1 && backward known f2
    | Or f1 f2 => backward known f1 || backward known f2
    | Imp f1 f2 => forward known f1 (fun known' => backward known' f2)
    end.

Examples:

  Compute backward []
            (Atomic 0).
= false
: bool
  Compute backward [0]
            (Atomic 0).
= true
: bool
  Compute backward [0; 2]
            (Or (Atomic 0) (Atomic 1)).
= true
: bool
  Compute backward [2]
            (Or (Atomic 0) (Atomic 1)).
= false
: bool
  Compute backward [2]
            (Imp (Atomic 0) (Or (Atomic 0) (Atomic 1))).
= true
: bool
  Compute backward [2]
            (Imp (Or (Atomic 0) (Atomic 3)) (Or (Atomic 0) (Atomic 1))).
= false
: bool
  Compute backward [2]
            (Imp (Or (Atomic 1) (Atomic 0)) (Or (Atomic 0) (Atomic 1))).
= true
: bool
End my_tauto.

Hint Resolve allTrue_add : core.

Lemma forward_ok : forall atomics hyp f known cont,
    forward known hyp cont = true
    -> (forall known', allTrue atomics known'
                       -> cont known' = true
                       -> formulaDenote atomics f)
    -> allTrue atomics known
    -> formulaDenote atomics hyp
    -> formulaDenote atomics f.
forall (atomics : asgn) (hyp f : formula)
  (known : set propvar) (cont : set propvar -> bool),
forward known hyp cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true -> formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp -> formulaDenote atomics f
Proof.
forall (atomics : asgn) (hyp f : formula)
  (known : set propvar) (cont : set propvar -> bool),
forward known hyp cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true -> formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp -> formulaDenote atomics f
  induction hyp; simpl in *; intros.
atomics: asgn
p: propvar
f: formula
known: set propvar
cont: set propvar -> bool
H: cont (add known p) = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: atomics p
formulaDenote atomics f
atomics: asgn
f: formula
known: set propvar
cont: set propvar -> bool
H: cont known = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: True
formulaDenote atomics f
atomics: asgn
f: formula
known: set propvar
cont: set propvar -> bool
H: true = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: False
formulaDenote atomics f
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: forward known hyp1
  (fun known' : set propvar =>
   forward known' hyp2 cont) = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: formulaDenote atomics hyp1 /\
formulaDenote atomics hyp2
formulaDenote atomics f
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: forward known hyp1 cont && forward known hyp2 cont =
true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: formulaDenote atomics hyp1 \/
formulaDenote atomics hyp2
formulaDenote atomics f
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: cont known = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: formulaDenote atomics hyp1 ->
formulaDenote atomics hyp2
formulaDenote atomics f

  all: repeat match goal with
              | [ H: _ && _ = true |- _ ] =>
                  apply Bool.andb_true_iff in H; destruct H
         end.
atomics: asgn
p: propvar
f: formula
known: set propvar
cont: set propvar -> bool
H: cont (add known p) = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: atomics p
formulaDenote atomics f
atomics: asgn
f: formula
known: set propvar
cont: set propvar -> bool
H: cont known = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: True
formulaDenote atomics f
atomics: asgn
f: formula
known: set propvar
cont: set propvar -> bool
H: true = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: False
formulaDenote atomics f
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: forward known hyp1
  (fun known' : set propvar =>
   forward known' hyp2 cont) = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: formulaDenote atomics hyp1 /\
formulaDenote atomics hyp2
formulaDenote atomics f
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: forward known hyp1 cont = true
H3: forward known hyp2 cont = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: formulaDenote atomics hyp1 \/
formulaDenote atomics hyp2
formulaDenote atomics f
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: cont known = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H2: formulaDenote atomics hyp1 ->
formulaDenote atomics hyp2
formulaDenote atomics f

  all: intuition eauto 4.
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: forward known hyp1
  (fun known' : set propvar =>
   forward known' hyp2 cont) = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H3: formulaDenote atomics hyp1
H4: formulaDenote atomics hyp2
formulaDenote atomics f

  {
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: forward known hyp1
  (fun known' : set propvar =>
   forward known' hyp2 cont) = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H3: formulaDenote atomics hyp1
H4: formulaDenote atomics hyp2
formulaDenote atomics f eapply IHhyp1; eauto 3.
atomics: asgn
hyp1, hyp2: formula
IHhyp1: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp1 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp1 ->
formulaDenote atomics f
IHhyp2: forall (f : formula) (known : set propvar)
  (cont : set propvar -> bool),
forward known hyp2 cont = true ->
(forall known' : set propvar,
 allTrue atomics known' ->
 cont known' = true ->
 formulaDenote atomics f) ->
allTrue atomics known ->
formulaDenote atomics hyp2 ->
formulaDenote atomics f
f: formula
known: set propvar
cont: set propvar -> bool
H: forward known hyp1
  (fun known' : set propvar =>
   forward known' hyp2 cont) = true
H0: forall known' : set propvar,
allTrue atomics known' ->
cont known' = true -> formulaDenote atomics f
H1: allTrue atomics known
H3: formulaDenote atomics hyp1
H4: formulaDenote atomics hyp2
forall known' : set propvar,
allTrue atomics known' ->
(fun known'0 : set propvar =>
 forward known'0 hyp2 cont) known' = true ->
formulaDenote atomics f
    intros; eapply IHhyp2; eauto; eauto. }
Qed.

Lemma backward_ok' : forall atomics f known,
    backward known f = true
    -> allTrue atomics known
    -> formulaDenote atomics f.
forall (atomics : asgn) (f : formula)
  (known : set propvar),
backward known f = true ->
allTrue atomics known -> formulaDenote atomics f
Proof.
forall (atomics : asgn) (f : formula)
  (known : set propvar),
backward known f = true ->
allTrue atomics known -> formulaDenote atomics f
  induction f; simpl; intuition idtac.
atomics: asgn
p: propvar
known: set propvar
H: (if in_dec Nat.eq_dec p known then true else false) =
true
H0: allTrue atomics known
atomics p
atomics: asgn
known: set propvar
H: false = true
H0: allTrue atomics known
False
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: backward known f1 && backward known f2 = true
H0: allTrue atomics known
formulaDenote atomics f1
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: backward known f1 && backward known f2 = true
H0: allTrue atomics known
formulaDenote atomics f2
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: backward known f1 || backward known f2 = true
H0: allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: forward known f1
  (fun known' : set propvar => backward known' f2) =
true
H0: allTrue atomics known
H1: formulaDenote atomics f1
formulaDenote atomics f2

  all: repeat match goal with
         | _ => progress destruct in_dec
         | [ H: false = true |- _ ] => discriminate
              | [ H: _ && _ = true |- _ ] =>
                  apply Bool.andb_true_iff in H; destruct H
              | [ H: _ || _ = true |- _ ] =>
                  apply Bool.orb_true_iff in H; destruct H
         end.
atomics: asgn
p: propvar
known: set propvar
i: In p known
H: true = true
H0: allTrue atomics known
atomics p
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: backward known f1 = true
H1: backward known f2 = true
H0: allTrue atomics known
formulaDenote atomics f1
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: backward known f1 = true
H1: backward known f2 = true
H0: allTrue atomics known
formulaDenote atomics f2
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: backward known f1 = true
H0: allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: backward known f2 = true
H0: allTrue atomics known
formulaDenote atomics f1 \/ formulaDenote atomics f2
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: forward known f1
  (fun known' : set propvar => backward known' f2) =
true
H0: allTrue atomics known
H1: formulaDenote atomics f1
formulaDenote atomics f2

  all: intuition eauto.
atomics: asgn
p: propvar
known: set propvar
i: In p known
H: true = true
H0: allTrue atomics known
atomics p
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: forward known f1
  (fun known' : set propvar => backward known' f2) =
true
H0: allTrue atomics known
H1: formulaDenote atomics f1
formulaDenote atomics f2

  +
atomics: asgn
p: propvar
known: set propvar
i: In p known
H: true = true
H0: allTrue atomics known
atomics p eapply allTrue_In; unfold set_In; eauto.
  +
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: forward known f1
  (fun known' : set propvar => backward known' f2) =
true
H0: allTrue atomics known
H1: formulaDenote atomics f1
formulaDenote atomics f2 eapply forward_ok; eauto.
atomics: asgn
f1, f2: formula
IHf1: forall known : set propvar,
backward known f1 = true ->
allTrue atomics known ->
formulaDenote atomics f1
IHf2: forall known : set propvar,
backward known f2 = true ->
allTrue atomics known ->
formulaDenote atomics f2
known: set propvar
H: forward known f1
  (fun known' : set propvar => backward known' f2) =
true
H0: allTrue atomics known
H1: formulaDenote atomics f1
forall known' : set propvar,
allTrue atomics known' ->
(fun known'0 : set propvar => backward known'0 f2)
  known' = true -> formulaDenote atomics f2
    intros; eapply IHf2; eauto; eauto.
Qed.

Theorem backward_ok : forall f,
    backward [] f = true
    -> forall atomics, formulaDenote atomics f.
forall f : formula,
backward [] f = true ->
forall atomics : asgn, formulaDenote atomics f
Proof.
forall f : formula,
backward [] f = true ->
forall atomics : asgn, formulaDenote atomics f
  intros.
f: formula
H: backward [] f = true
atomics: asgn
formulaDenote atomics f
  apply backward_ok' with (known := []); simpl; eauto.
Qed.

Find the position of an element in a list.

Ltac position x ls :=
  match ls with
  | [] => constr:(@None nat)
  | x :: _ => constr:(Some 0)
  | _ :: ?ls' =>
    let p := position x ls' in
    match p with
    | None => p
    | Some ?n => constr:(Some (S n))
    end
  end.

Compute a duplicate-free list of all variables in P, combining it with acc.

Ltac vars_in P acc :=
  match P with
  | True => acc
  | False => acc
  | ?Q1 /\ ?Q2 =>
    let acc' := vars_in Q1 acc in
    vars_in Q2 acc'
  | ?Q1 \/ ?Q2 =>
    let acc' := vars_in Q1 acc in
    vars_in Q2 acc'
  | ?Q1 -> ?Q2 =>
    let acc' := vars_in Q1 acc in
    vars_in Q2 acc'
  | _ =>
    let pos := position P acc in
    match pos with
    | Some _ => acc
    | None => constr:(P :: acc)
    end
  end.

Reification of formula P, with a pregenerated list vars of variables it may mention

Ltac reify_tauto' P vars :=
  match P with
  | True => Truth
  | False => Falsehood
  | ?Q1 /\ ?Q2 =>
    let q1 := reify_tauto' Q1 vars in
    let q2 := reify_tauto' Q2 vars in
    constr:(And q1 q2)
  | ?Q1 \/ ?Q2 =>
    let q1 := reify_tauto' Q1 vars in
    let q2 := reify_tauto' Q2 vars in
    constr:(Or q1 q2)
  | ?Q1 -> ?Q2 =>
    let q1 := reify_tauto' Q1 vars in
    let q2 := reify_tauto' Q2 vars in
    constr:(Imp q1 q2)
  | _ =>
    let pos := position P vars in
    match pos with
    | Some ?pos' => constr:(Atomic pos')
    end
  end.

Our final tactic implementation is now fairly straightforward. First, we intro all quantifiers that do not bind Props. Then we reify. Finally, we call the verified procedure through a lemma.

Ltac my_tauto :=
  repeat match goal with
           | [ |- forall x : ?P, _ ] =>
             match type of P with
               | Prop => fail 1
               | _ => intro
             end
         end;
  match goal with
    | [ |- ?P ] =>
      let vars := vars_in P (@nil Prop) in
      let p := reify_tauto' P vars in
      change (formulaDenote (nth_default False vars) p)
  end;
  apply backward_ok; reflexivity.

A few examples demonstrate how the tactic works:

Theorem mt1 : True.
True
Proof.
True
  my_tauto.
Qed.

Print mt1.
mt1 =
backward_ok Truth eq_refl (nth_default False [])
     : True

Theorem mt2 : forall x y : nat, x = y -> x = y.
forall x y : nat, x = y -> x = y
Proof.
forall x y : nat, x = y -> x = y
  my_tauto.
Qed.

Print mt2.
mt2 =
fun x y : nat =>
backward_ok (Imp (Atomic 0) (Atomic 0)) eq_refl
  (nth_default False [x = y])
     : forall x y : nat, x = y -> x = y

Arguments mt2 (x y)%nat_scope _

Crucially, both instances of x = y are represented with the same variable 0.

Theorem mt3 : forall x y z,
  (x < y /\ y > z) \/ (y > z /\ x < S y)
  -> y > z /\ (x < y \/ x < S y).
forall x y z : nat,
x < y /\ y > z \/ y > z /\ x < S y ->
y > z /\ (x < y \/ x < S y)
Proof.
forall x y z : nat,
x < y /\ y > z \/ y > z /\ x < S y ->
y > z /\ (x < y \/ x < S y)
  my_tauto.
Qed.

Print mt3.
mt3 =
fun x y z : nat =>
backward_ok
  (Imp
     (Or (And (Atomic 2) (Atomic 1))
        (And (Atomic 1) (Atomic 0)))
     (And (Atomic 1) (Or (Atomic 2) (Atomic 0))))
  eq_refl (nth_default False [x < S y; y > z; x < y])
     : forall x y z : nat,
       x < y /\ y > z \/ y > z /\ x < S y ->
       y > z /\ (x < y \/ x < S y)

Arguments mt3 (x y z)%nat_scope _

Our goal contained three distinct atomic formulas, and we see that a three-element environment is generated.

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.

Theorem mt4 :
  True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
True /\ True /\ True /\ True /\ True /\ True /\ False ->
False
Proof.
True /\ True /\ True /\ True /\ True /\ True /\ False ->
False
  my_tauto.
Qed.

Print mt4.
mt4 =
backward_ok
  (Imp
     (And Truth
        (And Truth
           (And Truth
              (And Truth
                 (And Truth (And Truth Falsehood))))))
     Falsehood) eq_refl (nth_default False [])
     : True /\
       True /\ True /\ True /\ True /\ True /\ False ->
       False

Theorem mt4' :
  True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
True /\ True /\ True /\ True /\ True /\ True /\ False ->
False
Proof.
True /\ True /\ True /\ True /\ True /\ True /\ False ->
False
  tauto.
Qed.

Print mt4'.
mt4' =
fun
  H : True /\
      True /\ True /\ True /\ True /\ True /\ False =>
and_ind
  (fun (_ : True)
     (H1 : True /\
           True /\ True /\ True /\ True /\ False) =>
   and_ind
     (fun (_ : True)
        (H2 : True /\ True /\ True /\ True /\ False)
      =>
      and_ind
        (fun (_ : True)
           (H3 : True /\ True /\ True /\ False) =>
         and_ind
           (fun (_ : True)
              (H4 : True /\ True /\ False) =>
            and_ind
              (fun (_ : True) (H5 : True /\ False) =>
               and_ind
                 (fun (_ : True) (H6 : False) =>
                  False_ind False H6) H5) H4) H3) H2)
     H1) H
     : True /\
       True /\ True /\ True /\ True /\ True /\ False ->
       False

The traditional tauto tactic introduces a quadratic blow-up in the size of the proof term, whereas proofs produced by my_tauto always have linear size.