Joachim Breitner: Coinduction in Coq and Isabelle
The DeepSpec Summer School is almost over, and I have had a few good discussions. One revolved around coinduction: What is it, how does it differ from induction, and how do you actually prove something. In the course of the discussion, I came up with a very simple coinductive exercise, and solved it both in Coq and Isabelle
The task
Define the extended natural numbers coinductively. Define the min function and the relation. Show that min(n, m) n holds.
Coq
The definitions are straight forward. Note that in Coq, we use the same command to define a coinductive data type and a coinductively defined relation:
CoInductive ENat :=
N : ENat
S : ENat -> ENat.
CoFixpoint min (n : ENat) (m : ENat)
:=match n, m with S n', S m' => S (min n' m')
_, _ => N end.
CoInductive le : ENat -> ENat -> Prop :=
leN : forall m, le N m
leS : forall n m, le n m -> le (S n) (S m).
The lemma is specified as
Lemma min_le: forall n m, le (min n m) n.
and the proof method of choice to show that some coinductive relation holds, is cofix. One would wish that the following proof would work:
Lemma min_le: forall n m, le (min n m) n.
Proof.
cofix.
destruct n, m.
* apply leN.
* apply leN.
* apply leN.
* apply leS.
apply min_le.
Qed.
but we get the error message
Error:
In environment
min_le : forall n m : ENat, le (min n m) n
Unable to unify "le N ?M170" with "le (min N N) N
Effectively, as Coq is trying to figure out whether our proof is correct, i.e. type-checks, it stumbled on the equation min N N = N, and like a kid scared of coinduction, it did not dare to run the min function. The reason it does not just run a CoFixpoint is that doing so too daringly might simply not terminate. So, as Adam explains in a chapter of his book, Coq reduces a cofixpoint only when it is the scrutinee of a match statement.
So we need to get a match statement in place. We can do so with a helper function:
Definition evalN (n : ENat) :=
match n with N => N
S n => S n end.
Lemma evalN_eq : forall n, evalN n = n.
Proof. intros. destruct n; reflexivity. Qed.
This function does not really do anything besides nudging Coq to actually evaluate its argument to a constructor (N or S _). We can use it in the proof to guide Coq, and the following goes through:
Lemma min_le: forall n m, le (min n m) n.
Proof.
cofix.
destruct n, m; rewrite <- evalN_eq with (n := min _ _).
* apply leN.
* apply leN.
* apply leN.
* apply leS.
apply min_le.
Qed.
Isabelle
In Isabelle, definitions and types are very different things, so we use different commands to define ENat and le:
theory ENat imports Main begin
codatatype ENat = N S ENat
primcorec min where
"min n m = (case n of
N N
S n' (case m of
N N
S m' S (min n' m')))"
coinductive le where
leN: "le N m"
leS: "le n m le (S n) (S m)"
There are actually many ways of defining min; I chose the one most similar to the one above. For more details, see the corec tutorial.
Now to the proof:
lemma min_le: "le (min n m) n"
proof (coinduction arbitrary: n m)
case le
show ?case
proof(cases n)
case N then show ?thesis by simp
next
case (S n') then show ?thesis
proof(cases m)
case N then show ?thesis by simp
next
case (S m') with n = _ show ?thesis
unfolding min.code[where n = n and m = m]
by auto
qed
qed
qed
The coinduction proof methods produces this goal:
proof (state)
goal (1 subgoal):
1. n m. ( m'. min n m = N n = m')
( n' m'.
min n m = S n'
n = S m'
(( n m. n' = min n m m' = n) le n' m'))
I chose to spell the proof out in the Isar proof language, where the outermost proof structure is done relatively explicity, and I proceed by case analysis mimiking the min function definition.
In the cases where one argument of min is N, Isabelle s simplifier (a term rewriting tactic, so to say), can solve the goal automatically. This is because the primcorec command produces a bunch of lemmas, one of which states n = N m = N min n m = N.
In the other case, we need to help Isabelle a bit to reduce the call to min (S n) (S m) using the unfolding methods, where min.code contains exactly the equation that we used to specify min. Using just unfolding min.code would send this method into a loop, so we restrict it to the concrete arguments n and m. Then auto can solve the remaining goal (despite all the existential quantifiers).
Summary
Both theorem provers are able to prove the desired result. To me it seems that it is slightly more convenient in Isabelle because a lot of Coq infrastructure relies on the type checker being able to effectively evaluate expressions, which is tricky with cofixpoints, wheras evaluation plays a much less central role in Isabelle, where rewriting is the crucial technique, and while one still cannot simply throw min.code into the simpset, so working with objects that do not evaluate easily or completely is less strange.
Agda
I was challenged to do it in Agda. Here it is:
module ENat where
open import Coinduction
data ENat : Set where
N : ENat
S : ENat ENat
min : ENat ENat ENat
min (S n') (S m') = S ( (min ( n') ( m')))
min _ _ = N
data le : ENat ENat Set where
leN : m le N m
leS : n m (le ( n) ( m)) le (S n) (S m)
min_le : n m le (min n m) n
min_le S n' S m' = leS ( min_le)
min_le N S m' = leN
min_le S n' N = leN
min_le N N = leN
I will refrain from commenting it, because I do not really know what I have been doing here, but it typechecks, and refer you to the official documentation on coinduction in Agda. But let me note that I wrote this using plain inductive types and recursion, and added , and until it worked.
CoInductive ENat :=
N : ENat
S : ENat -> ENat.
CoFixpoint min (n : ENat) (m : ENat)
:=match n, m with S n', S m' => S (min n' m')
_, _ => N end.
CoInductive le : ENat -> ENat -> Prop :=
leN : forall m, le N m
leS : forall n m, le n m -> le (S n) (S m).Lemma min_le: forall n m, le (min n m) n.cofix. One would wish that the following proof would work:
Lemma min_le: forall n m, le (min n m) n.
Proof.
cofix.
destruct n, m.
* apply leN.
* apply leN.
* apply leN.
* apply leS.
apply min_le.
Qed.Error:
In environment
min_le : forall n m : ENat, le (min n m) n
Unable to unify "le N ?M170" with "le (min N N) Nmin N N = N, and like a kid scared of coinduction, it did not dare to run the min function. The reason it does not just run a CoFixpoint is that doing so too daringly might simply not terminate. So, as Adam explains in a chapter of his book, Coq reduces a cofixpoint only when it is the scrutinee of a match statement.
So we need to get a match statement in place. We can do so with a helper function:
Definition evalN (n : ENat) :=
match n with N => N
S n => S n end.
Lemma evalN_eq : forall n, evalN n = n.
Proof. intros. destruct n; reflexivity. Qed.N or S _). We can use it in the proof to guide Coq, and the following goes through:
Lemma min_le: forall n m, le (min n m) n.
Proof.
cofix.
destruct n, m; rewrite <- evalN_eq with (n := min _ _).
* apply leN.
* apply leN.
* apply leN.
* apply leS.
apply min_le.
Qed.Isabelle
In Isabelle, definitions and types are very different things, so we use different commands to define ENat and le:
theory ENat imports Main begin
codatatype ENat = N S ENat
primcorec min where
"min n m = (case n of
N N
S n' (case m of
N N
S m' S (min n' m')))"
coinductive le where
leN: "le N m"
leS: "le n m le (S n) (S m)"
There are actually many ways of defining min; I chose the one most similar to the one above. For more details, see the corec tutorial.
Now to the proof:
lemma min_le: "le (min n m) n"
proof (coinduction arbitrary: n m)
case le
show ?case
proof(cases n)
case N then show ?thesis by simp
next
case (S n') then show ?thesis
proof(cases m)
case N then show ?thesis by simp
next
case (S m') with n = _ show ?thesis
unfolding min.code[where n = n and m = m]
by auto
qed
qed
qed
The coinduction proof methods produces this goal:
proof (state)
goal (1 subgoal):
1. n m. ( m'. min n m = N n = m')
( n' m'.
min n m = S n'
n = S m'
(( n m. n' = min n m m' = n) le n' m'))
I chose to spell the proof out in the Isar proof language, where the outermost proof structure is done relatively explicity, and I proceed by case analysis mimiking the min function definition.
In the cases where one argument of min is N, Isabelle s simplifier (a term rewriting tactic, so to say), can solve the goal automatically. This is because the primcorec command produces a bunch of lemmas, one of which states n = N m = N min n m = N.
In the other case, we need to help Isabelle a bit to reduce the call to min (S n) (S m) using the unfolding methods, where min.code contains exactly the equation that we used to specify min. Using just unfolding min.code would send this method into a loop, so we restrict it to the concrete arguments n and m. Then auto can solve the remaining goal (despite all the existential quantifiers).
Summary
Both theorem provers are able to prove the desired result. To me it seems that it is slightly more convenient in Isabelle because a lot of Coq infrastructure relies on the type checker being able to effectively evaluate expressions, which is tricky with cofixpoints, wheras evaluation plays a much less central role in Isabelle, where rewriting is the crucial technique, and while one still cannot simply throw min.code into the simpset, so working with objects that do not evaluate easily or completely is less strange.
Agda
I was challenged to do it in Agda. Here it is:
module ENat where
open import Coinduction
data ENat : Set where
N : ENat
S : ENat ENat
min : ENat ENat ENat
min (S n') (S m') = S ( (min ( n') ( m')))
min _ _ = N
data le : ENat ENat Set where
leN : m le N m
leS : n m (le ( n) ( m)) le (S n) (S m)
min_le : n m le (min n m) n
min_le S n' S m' = leS ( min_le)
min_le N S m' = leN
min_le S n' N = leN
min_le N N = leN
I will refrain from commenting it, because I do not really know what I have been doing here, but it typechecks, and refer you to the official documentation on coinduction in Agda. But let me note that I wrote this using plain inductive types and recursion, and added , and until it worked.
theory ENat imports Main begin
codatatype ENat = N S ENat
primcorec min where
"min n m = (case n of
N N
S n' (case m of
N N
S m' S (min n' m')))"
coinductive le where
leN: "le N m"
leS: "le n m le (S n) (S m)"lemma min_le: "le (min n m) n"
proof (coinduction arbitrary: n m)
case le
show ?case
proof(cases n)
case N then show ?thesis by simp
next
case (S n') then show ?thesis
proof(cases m)
case N then show ?thesis by simp
next
case (S m') with n = _ show ?thesis
unfolding min.code[where n = n and m = m]
by auto
qed
qed
qedproof (state)
goal (1 subgoal):
1. n m. ( m'. min n m = N n = m')
( n' m'.
min n m = S n'
n = S m'
(( n m. n' = min n m m' = n) le n' m'))min.code into the simpset, so working with objects that do not evaluate easily or completely is less strange.
Agda
I was challenged to do it in Agda. Here it is:
module ENat where
open import Coinduction
data ENat : Set where
N : ENat
S : ENat ENat
min : ENat ENat ENat
min (S n') (S m') = S ( (min ( n') ( m')))
min _ _ = N
data le : ENat ENat Set where
leN : m le N m
leS : n m (le ( n) ( m)) le (S n) (S m)
min_le : n m le (min n m) n
min_le S n' S m' = leS ( min_le)
min_le N S m' = leN
min_le S n' N = leN
min_le N N = leN
I will refrain from commenting it, because I do not really know what I have been doing here, but it typechecks, and refer you to the official documentation on coinduction in Agda. But let me note that I wrote this using plain inductive types and recursion, and added , and until it worked.
module ENat where
open import Coinduction
data ENat : Set where
N : ENat
S : ENat ENat
min : ENat ENat ENat
min (S n') (S m') = S ( (min ( n') ( m')))
min _ _ = N
data le : ENat ENat Set where
leN : m le N m
leS : n m (le ( n) ( m)) le (S n) (S m)
min_le : n m le (min n m) n
min_le S n' S m' = leS ( min_le)
min_le N S m' = leN
min_le S n' N = leN
min_le N N = leN
Is it possible to do software development, mathematical or not, as mathematician in academics? This is a question I was asking myself recently a lot, seeing my own development from logician at a state university getting rid of foreigners to software developer. And then, a friend pointed me to this very depressing document: 
.. because you will never wake up the next day, since the alarm was deleted due to an unattended (so-called) sync operation. Happened to me, several times, worst was when I was with clients working as guide.
So the problem is well known, see 
A new version of 
In measured boot, each component of the boot process is "measured" (ie, hashed and that hash recorded) in a register in the Trusted Platform Module (TPM) build into the system. The TPM has several different registers (Platform Configuration Registers, or PCRs) which are typically used for different purposes - for instance, PCR0 contains measurements of various system firmware components, PCR2 contains any option ROMs, PCR4 contains information about the partition table and the bootloader. The allocation of these is defined by the 
Rar support is necessary in the case that the eBook uses rar as compression, which happens quite often in comic books (cbr extension). Calibre 3 has split out rar support into a dynamically loaded module, so what needs to be done is packaging it. I have prepared a package for the Python library unrardll which allows Calibre to read rar-compressed ebooks, but it depends on the unrar shared library, which unfortunately is not built in Debian. I have sent a patch to fix this to the maintainer, see bug 
Lumicall 1.13.0 is released! 
Through Lumicall, you can make encrypted calls and send messages using open standards. It uses the SIP protocol to inter-operate with other apps and corporate telephone systems.
During the Outreachy Internship period I worked on the following issues :-
You can try the new version of 
As 
Dear all, This would be a biggish one so please have a chai/coffee or something stronger as it would take a while.
I would start with attempt at some alcohol humor. While some people know that I have had a 
It included couple of co-organizers with most people being newbies so while I had thought of showing how to contribute via reporting bugs or putting up patches, had to set that aside and explain how things work in free software and open-source world. We didn t get into the debate of free vs open-source or free/open-source/open-core as that would have been counter-productive and probably confusing for newbies.
We did however share the debian tree structure
I was stumped by /var and /proc . I hadn t taken my lappy as it is expensive (a lenovo thinkpad I love very dearly) and I was unsure if I would be able to take care of it (weight wise). Dhanesh had told me that he had Debian on his lappy + zsh both of which are my favourites.
While back at home I realized /var has been relegated to having apache/server logs and stuff like that, I do recall (vaguely) a thread on debian-devel about removing /var although that discussion went nowhere.
One of the bugs that we hit early on is that nobody had enough space on their hdd to have Debian comfortably. It took a while to get an external hdd and push some of the content from somebody s lappy to the external drive to have space for the installation.
I did share the /. /home, optional swap while Dhanesh helped by sharing about having a separate /boot partition as well which I had forgotten. I can t even begin to remember the number of times having a separate /boot partition has helped me in all of my systems.
That done, we did try to install/show Debian 9 without network but were hit with 
Dhanesh is on the left while I m on the right.
We did have a cute 3-4 year old boy as our guest as well bud didn t get good pictures of him.
Lastly, the Debian cake itself
We also talked about the kernel and subsystem maintainers and how Linus is the overlord.
Look forward to comments. I am hoping Dhanesh might recollect some points that I might have missed/forgotten.
Update 07/07/17 All programming languages stats. can be seen 
My monthly report covers a large part of what I have been doing in the free software world. I write it for 
To be able to get in sync with Kali, I introduced an hashcat-meta source package (in contrib) providing hashcat-nvidia to make it easy to install hashcat for owners of NVidia hardware.
Misc stuff
Distro Tracker. I merged a small CSS fix from Aur lien Couderc (
I was assigned 15 hours of work by Freexian's Debian LTS initiative
and carried over 5 hours. I worked all 20 hours.
I spent most of my time working - together with other Linux kernel
developers - on backporting and testing several versions of the fix for
CVE-2017-1000364, part of the
Two scenarios are tested:
