Joachim Breitner: Named goals in Coq
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:
- I load a small file full of hacks (explained below):
Require Import NamedCases.
- 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.
- 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.
- The trick1 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.
- 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.
- 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 .. ].
- 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.
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.MEmpty)- I load a small file full of hacks (explained below):
Require Import NamedCases. - 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:
This is the definition from the Software Foundations book; only theReserved 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).case <name>,lines are added. - Now I can change the proof: After the induction tactic I use
; name_casesto 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:
The comments have turned into actual names!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.
; 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.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.
- The trick1 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.
- 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.
- 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 .. ].
- 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.
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. [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 *)
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.
- The trick1 is to leave markers in the proof state. We use a dedicate type
CaseName, and a hypothesisname : CaseNameindicates that this goal arose from the that case.
With this, we can writeInductive CaseName := CaseNameI.StarApp: forall (starApp : CaseName),to name this case. - For a little bit of polish, we can introduce notation for that:
This allows us to use the syntax you saw above.Notation "'case' x , t" := (forall x : CaseName , t) (at level 200). - To easily discharge these
CaseNameassumptions 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 .. ]. - Finally I wrote the tactic
name_cases. What it does is relatively simple:For each subgoal: Take all hypotheses of type
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:CaseName, concatenate their names, change the name of the current goal to that, and clear these hypotheses
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 wayFrom 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) ).
The Linux Foundation has published its 
The PDF producer meta data for the annual report PDF has been set to "Linux kernel 0.12.1 for Workgroups" and the PDF creator meta data element to "Sharp Zaurus XR-5000 (Maemo5) Edition". Somebody thought to better hide the real data and had some tongue-in-cheek ideas. Kudos.
But nicer would have been to use Open Source software to produce the report, not?
Running 
A new 
Currently, the Government procures rice in vast quantities and the farmers are assured at least some basic income, in the states of Punjab and Haryana
PTI News, Nov 27, 2020 
Once a year folks interested in Netfilter technologies gather together to discuss past, ongoing and
future works. The Netfilter Workshop is an opportunity to share and discuss new ideas, the state of
the project, bring people together to work & hack and to put faces to people who otherwise are just
email names. This is an event that 
Stefano Bravio commented on several open topics for nftables that he is interested on working on.
One of them, issues related to concatenations + vmap issues. He also addressed concerns with
people s expectations when migrating from ipset to nftables. There are several corner features in
ipset that aren t currently supported in nftables, and we should document them. Stefano is also
wondering about some tools to help in the migration. A translation layer like there is in place
for iptables. Eric Gaver commented there are a couple of semantics that will not be suitable for
translation, such as global sets, or sets of sets. But ipset is way simpler than iptables, so a
translation mechanism should probably be created. In any case, there was agreement that anything
that helps people migrate is more than welcome, even if it doesn t support 100% of the use cases.
Stefano is planning to write documentation in the 
Welcome to gambaru.de. Here is my monthly report (+ the first week in November) that covers what I have been doing for Debian. If you re interested in Java, Games and LTS topics, this might be interesting for you.
Debian Games
Justice Chandrachud If you don t like a channel then don t watch it. 11th November 2020 . 
Information and Broadcasting Ministry bringing OTT services as well as news within its ambit. 
Unfortunately, in Debian in particular, libgit2 is undergoing a 
Like 
This month, the Reproducible Builds project restarted our IRC meetings, managing to convene twice: the first time on October 12th (
