A new Coq tactic for inversion
- May 4, 2013
Boutillier, we have been working on a new Coq tactic lately, called
invert. From my point of view, it started as a quest to
build a replacement to the
inversion is a pain to use, as it generates sub-goals with
many (dependent) equalities that must be substituted, which force the
subst, which in turns also has its quirks, making
inversion H; clear H; subst quite fragile.
inversion has efficiency problems, being quite
slow and generating big proof terms. From Pierre’s point of view, this
work was a good way to implement a better
based on what he did during an internship (report
in French (PDF)).
In a nutshell, the idea behind a destruction and an inversion is
quite similar: it boils down to a case analysis over a given hypothesis.
And there are quite a few tactics that follow this scheme:
discriminate (it is true that
the last two tactics are quite specialized, but fit the bill
nevertheless). Why on Earth would we need to add a new element to this
Well, it turns out that building on ideas by Jean-Francois Monin to make so called “small inversions”, one can unify the inner-working of most of the aforementioned list: it suffices to build the right return clause for the case analysis.
Let’s take an example.
Variable A : Type. Inductive vector: nat -> Type :=0 | nil : vector | cons: forall n (h:A) (v: vector n), vector (S n). Inductive P : forall n, vector n -> Prop :=0 nil | Pnil : P | Pcons: forall n h v, P n v -> P (S n) (cons n h v). Lemma test n h v (H: P (S n) (cons n h v)) : P n v.Proof.
At this point, doing
inversion H generates 4 new
H2 : P n v0 H0 : n0 = n H1 : h0 = hfun n : nat => vector n) n v0 = H3 : existT (fun n : nat => vector n) n v existT ( ============================ P n v
H1 are just cruft.
Then, the goal isn’t very palatable, because the equality
v0 is defined in
terms of a dependent equality: in order to go further, one need to
assume axioms about dependent equality1,
equivalent to Streicher’s axiom K. (Just to keep tabs, note that running
Show Proof command in Coq outputs a partial proof term
that is already 73 lines long at this point.)
If we use
dependent destruction H instead of inversion,
we get the expected hypothesis
H: P n v (which is far
better from an usability point of view). Yet, there is no magic here:
dependent destruction simply used a dependent equality axiom internally
to get rid of the dependent equality, and generates a 64 lines long
proof term that is not very pretty.
At this point, one may wonder: what should the proof term look like? and, is it necessary to use the K axiom here?
A black belt Coq user versed in dependent types could write the following one.
let diag := fun n0 : nat => match n0 as n' return (forall v0 : vector n', P n' v0 -> Prop) with 0 => fun (v0 : vector 0) (_ : P 0 v0) => True | | S m =>fun v0 : vector (S m) => match v0 as v1 in (vector m0) return (P m0 v1 -> Prop) with fun _ : P 0 nil => True | nil => fun _ : P (S p) (cons p x v1) => P p v1 | cons p x v1 => end end in match H as H' in (P x y) return (diag x y H') with | Pnil => I | Pcons n0 h0 v0 Pv => Pvend.
Wow, 15 lines long. Let’s demystify it a bit.
First, recall that the return type of a match is dictated by its
return clause (the
as ... in ... return ... part). This is
basically a function that binds the arguments of the inductive
S n as x,
cons n h v as y in our case),
H' of type
P x y, and which body is the return
part. Usually, the return part is a constant (e.g., nat for the match in
the List.length), but it is not mandatory. Here, the
term packs some computations, such that
diag (S n) (cons n h v) H reduces to
P n v,
the conclusion of the goal. (In general, this kind of return clauses
make it possible to eliminate impossible branches in a match, as done
here by marking them with the trivial return type
direct the interested readers to the online CPDT book by Adam Chlipala
for more informations on this, especially this
Then, what is
diag? Well, it is a function that follows
the structure of the arguments of
P to single out
impossible cases, and to refine the context in the other ones using
dependent pattern matching, in order to reduce to the right type (the
type of the initial conclusion of the goal). The idea behind such
“small-scale inversions” was described by Monin in 2010 and is out of
the scope of this blog post. What is new here is that we have mechanized
the construction of the
diag functions as a Coq tactic,
making this whole approach practical.
All in all, using our new tactic, we can just use the following proof script:
invert H; tauto.
At this point,
Show Proof. outputs the following
complete proof term (where
invert_subgoal is the type of
the subgoal solved by
let diag := fun n0 : nat => match n0 as n1 return (forall v0 : vector n1, P n1 v0 -> Prop) with 0 => fun (v0 : vector 0) (_ : P 0 v0) => False -> True | | S x =>fun v0 : vector (S x) => match as v1 in (vector n1) v0 returnmatch n1 as n2 return (vector n2 -> Type) with (0 => fun _ : vector 0 => False -> True | fun v2 : vector (S x0) => P (S x0) v2 -> Prop | S x0 => end v1) with fun H0 : False => False_rect True H0 | nil => fun _ : P (S n1) (cons n1 h0 v1) => P n1 v1 | cons n1 h0 v1 => end end in fun ( invert_subgoal : forall (n0 : nat) (h0 : A) (v0 : vector n0) (H0 : P n0 v0), diag (S n0) (cons n0 h0 v0) (Pcons n0 h0 v0 H0) =>match H as p in (P n0 v0) return (diag n0 v0 p) with fun H0 : False => False_rect True H0 | Pnil => | Pcons x x0 x1 x2 => invert_subgoal x x0 x1 x2end) (fun (n0 : nat) (_ : A) (v0 : vector n0) (H0 : P n0 v0) => H0))
Some of the differences with the proof term above come from the fact that we generate it interactively, rather than writing it once at all.
A legitimate question: how do we compare to destruct and inversion
and dependent destruction? First, we aim at producing a “better”
destruct: that is, we might resolve the situation in which
destruct fails, in order to avoid producing ill-typed
terms. Then, the situation with respect to inversion and dependent
destruction is less clear. Right now, we would rather not
assume the K axiom (the right thing to do if homotopy is the future). In
that case, we would fail for inversion problems that require K, and
inversion and dependent destruction would be more powerful than our
tactic. For problems that do no require to use K,
would be equivalent to
dependent destruction with better
looking proof terms2.
We are still working on our prototype, but we are quite confident that we got the main thing right: mechanizing the construction of the return clause. We will come back to this blog when we need beta-testers!
See the following FAQ question (Can I prove that the second components of equal dependent pairs are equal?). You may also be interested in this other question (What is Streicher’s axiom K?). The EqdepFacts standard library module, that has the equivalence proofs between all those subtle notions. Finally, if you want to finish this proof using these axioms, you can use
Require Import Eqdep.then the
inj_pair2lemma. Once you’re done,
Print Assumptions test.will let you check that you relied on an additional axiom – or
Print Assumptions inj_pair2.↩︎
Moreover, since our proof terms are less cluttered, it seems less likely than recursive definitions made in “proof mode” with
invertwill fail to pass the termination check once Coq’s guard condition deals properly with such commutative cuts, another part of Pierre’s thesis work.↩︎