Joachim Breitner's Homepage

TL;DR: Some mildly tricky tricks allow you to select subgoals by name, like in Isabelle. This leads to more readable proofs, and proofs that are more robust against changes.

The need for case names

Consider the following Coq proof, right out of the respected Software Foundations book, Chapter “Inductively Defined Propositions” (and slightly simplified):

Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp T),
  s1 =~ Star re ->
  s2 =~ Star re ->
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
  remember (Star re) as re'.
   generalize dependent s2.
  induction H1.
  - (* MEmpty *) discriminate.
  - (* MChar *) discriminate.
  - (* MApp *) discriminate.
  - (* MUnionL *) discriminate.
  - (* MUnionR *) discriminate.
  - (* MStar0 *)
    injection Heqre' as Heqre''. intros s H. apply H.
  - (* MStarApp *)
    injection Heqre' as Heqre''.
    intros s3 H1. rewrite <- app_assoc.
    apply MStarApp.
    + apply H1_.
    + apply IHexp_match2.
      * rewrite Heqre''. reflexivity.
      * apply H1.
Qed.

This is a very typical example for a proof by induction over an inductively defined relation (in this case, the relations s =~ re which indicates that the string s matches the regular expression re): After some preparation, the invocation of a tactic like induction (could also be inversion or others) creates a number of new goals, one of for each rule of the relation. Then the modern(!) Coq user uses proof bullets to focus the goals, one after another, in order, to solve them.

We can see from this example that proof bullets (which were a big improvement) are not quite satisfactory, and the author of this proof felt the need to annotate each subproof with the case it corresponds to.

But these are mere comments! This is unsatisfactory, as there is nothing keeping them correct as my proof changes. And anyone who came to Coq from Isabelle is just flabbergasted that the state of art in Coq is still at that level…

So, wouldn’t it be great if

• I could focus goals by their name (e.g. MEmpty)
• Focus them in any order (so that refactoring of my data types do not break my proofs)
• This even worked when simultaneously inducting over or inverting multiple relations?

Simulating named goals in Coq

Well, with a few tricks we can! It just takes three simple steps:

1. I load a small file full of hacks (explained below):

   Require Import NamedCases.

2. This allows me to prefix the type of the constructors of the inductive relations (i.e. the rules of the relation) with case <name>, …, as follows:

   Reserved Notation "s =~ re" (at level 80).
   Inductive exp_match {T} : list T -> reg_exp T -> Prop :=
     | MEmpty:
       case empty,
       [] =~ EmptyStr
     | MChar:
       case char,
       forall x,
       [x] =~ (Char x)
     | MApp:
       case app,
       forall s1 re1 s2 re2
       (H1 : s1 =~ re1)
       (H2 : s2 =~ re2),
       (s1 ++ s2) =~ (App re1 re2)
     | MUnionL:
       case union_l,
       forall s1 re1 re2
       (H1 : s1 =~ re1),
       s1 =~ (Union re1 re2)
     | MUnionR:
       case union_r,
       forall re1 s2 re2
       (H2 : s2 =~ re2),
       s2 =~ (Union re1 re2)
     | MStar0:
       case star0,
       forall re,
       [] =~ (Star re)
     | MStarApp:
       case star_app,
       forall s1 s2 re
       (H1 : s1 =~ re)
       (H2 : s2 =~ (Star re)),
       (s1 ++ s2) =~ (Star re)
     where "s =~ re" := (exp_match s re).

   This is the definition from the Software Foundations book; only the case <name>, lines are added.

3. Now I can change the proof: After the induction tactic I use …; name_cases to name the cases, and then I can use the relatively new named goal focusing feature ([name]: { … }, which I suggested two years ago, and was implemented by Théo Zimmermann) to focus a specific case:

   Lemma star_app2: forall T (s1 s2 : list T) (re : reg_exp T),
     s1 =~ Star re ->
     s2 =~ Star re ->
     s1 ++ s2 =~ Star re.
   Proof.
     intros T s1 s2 re H1.
     remember (Star re) as re'.
      generalize dependent s2.
     induction H1; name_cases.
     [empty]: {
        discriminate.
     }
     [char]: {
        discriminate.
     }
     [app]: {
        discriminate.
     }
     [unionL]: {
        discriminate.
     }
     [unionR]: {
       discriminate.
     }
     [star0]: {
       injection Heqre' as Heqre''. intros s H. apply H.
     }
     [starApp]: {
       injection Heqre' as Heqre''.
       intros s3 H1. rewrite <- app_assoc.
       apply MStarApp; clear_names.
       + apply H1_.
       + apply IHexp_match2.
         * rewrite Heqre''. reflexivity.
         * apply H1.
      }
   Qed.

   The comments have turned into actual names!

Goal focusing is now just much more reliable. For example, let me try to discharge the boring cases by using …; try discriminate after the induction. This means there are suddenly only two goals left. With bullets, the first bullet would now suddenly focus a different goal, and my proof script would likely fail somewhere. With named goals, I get a helpful error message No such goal: empty and I can’t even enter the first subproof. So let me delete these goals and, just to show off, focus the remaining goals in the “wrong” order:

Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp T),
  s1 =~ Star re ->
  s2 =~ Star re ->
  s1 ++ s2 =~ Star re.
Proof.
  intros T s1 s2 re H1.
  remember (Star re) as re'.
   generalize dependent s2.
  induction H1; name_cases; try discriminate.
  [starApp]: {
    injection Heqre' as Heqre''.
    intros s3 H1. rewrite <- app_assoc.
    apply MStarApp; clear_names.
    + apply H1_.
    + apply IHexp_match2.
      * rewrite Heqre''. reflexivity.
      * apply H1.
   }
  [star0]: {
    injection Heqre' as Heqre''. intros s H. apply H.
  }
Qed.

I did not explain the clear_names tactic yet that I had to use after apply MStarApp. What I am showing here is a hack, and it shows… these case names are extra hypothesis (of a trivially true type CaseName), and this tactic gets rid of it.

Even better than Isabelle

The above even works when there are multiple inductions/inversions involved. To give an example, let’s introduce another inductive predicate, and begin proving a lemma that one can do by induction on one and inversion on the other predicate.

Inductive Palindrome {T} : list T -> Prop :=
| EmptyPalin:
  case emptyP,
  Palindrome []
| SingletonPalin:
  case singletonP,
  forall x,
  Palindrome [x]
| GrowPalin:
  case growP,
  forall l x,
  Palindrome l -> Palindrome ([x] ++ l ++ [x])
.

Lemma palindrome_star_of_two:
  forall T (s : list T) x y,
  Palindrome s -> s =~ Star (App (Char x) (Char y)) ->
  s = [] \/ x = y.
Proof.
  intros T s x y HPalin HRe.
  induction HPalin; inversion HRe; name_cases.

At this point we have four open goals. Can you tell why there are four, and which ones they are?

Luckily, Show Existentials will tell us their names (and Coq 8.13 will just show them in the proof state window). These names not only help us focus the goal in a reliable way; they even assist us in understanding what goal we have to deal with. For example, the last goal arose from the GrowP rule and the StarApp rule. Neat!

  [emptyP_star0]: {
    left. reflexivity.
  }
  [emptyP_starApp]: {
     left. reflexivity.
  }
  [singletonP_starApp]: {
    inversion HRe; clear HRe.
    inversion H5; clear H5.
    inversion H10; clear H10.
    inversion H11; clear H11.
    subst.
    inversion H3.
  }
 [growP_starApp]: {
    admit. (* I did not complete the proof *)
 }

Under the hood (the hack)

The above actually works, but it works with a hack, and I wish that Coq’s induction tactic would just do the right thing here. I hope eventually this will be the case, and this section will just be curiosity… but until, it may actually be helpful.

1. The trick¹ is to leave “markers” in the proof state. We use a dedicate type CaseName, and a hypothesis name : CaseName indicates that this goal arose from the that case.

   Inductive CaseName := CaseNameI.

   With this, we can write StarApp: forall (starApp : CaseName), … to name this case.

2. For a little bit of polish, we can introduce notation for that:

   Notation "'case' x , t" := (forall {x : CaseName}, t) (at level 200).

   This allows us to use the syntax you saw above.

3. To easily discharge these CaseName assumptions when using the introduction forms, I wrote these tactics:

   Ltac clear_names := try exact CaseNameI.
   Ltac named_constructor  := constructor; [ exact CaseNameI | idtac .. ].
   Ltac named_econstructor := econstructor; [ exact CaseNameI | idtac .. ].

4. Finally I wrote the tactic name_cases. What it does is relatively simple:

   For each subgoal: Take all hypotheses of type CaseName, concatenate their names, change the name of the current goal to that, and clear these hypotheses

   Unfortunately, my grasp of Coq tactic programming is rather rudimentary, and the only way I manged to solve this is a horrible monster of Ltac2, including hand-rolled imperative implementations of string concatenation and a little nested Ltac1 tactic within. You have been warned:

   From Ltac2 Require Import Ltac2.
   From Ltac2 Require Option.
   Set Default Proof Mode "Classic".
   Ltac name_cases := ltac2:(
     (* Horribly manual string manipulations. Does this mean I should
        go to the Ocaml level?
     *)
     let strcpy s1 s2 o :=
       let rec go := fun n =>
         match Int.lt n (String.length s2) with
         | true => String.set s1 (Int.add o n) (String.get s2 n); go (Int.add n 1)
         | false => ()
         end
       in go 0
     in
     let concat := fun s1 s2 =>
       let l := Int.add (Int.add (String.length s1) (String.length s2)) 1 in
       let s := String.make l (Char.of_int 95) in
       strcpy s s1 0;
       strcpy s s2 (Int.add (String.length s1) 1);
       s
     in
     Control.enter (let rec go () :=
       lazy_match! goal with
       | [ h1 : CaseName, h2 : CaseName |- _ ] =>
         (* Multiple case names? Combine them (and recurse) *)
         let h := concat (Ident.to_string h1) (Ident.to_string h2) in
         Std.clear [h1; h2];
         let h := Option.get (Ident.of_string h) in
         assert ($h := CaseNameI);
         go ()
       | [ _ : CaseName |- _ ] =>
         (* A single case name? Set current goal name accordingly. *)
         ltac1:(
           (* How to do this in ltac2? *)
           lazymatch goal with
           | [ H : CaseName |- _ ] => refine ?[H]; clear H
           end
         )
       | [ |- _ ] =>
         Control.backtrack_tactic_failure "Did not find any CaseName hypotheses"
       end
     in go)
   ).

   If someone feels like re-implementing this in a way that is more presentable, I’ll be happy to update this code (and learn something along the way

That’s all it takes!

Conclusion

With some mild hackery, we can get named cases in Coq, which I find indispensable in managing larger, evolving proofs. I wonder why this style is not more common, and available out of the box, but maybe it is just not known well enough? Maybe this blog post can help a bit here.