summaryrefslogtreecommitdiffstats
path: root/site
diff options
context:
space:
mode:
Diffstat (limited to 'site')
-rw-r--r--site/index.html61
-rw-r--r--site/posts/Ltac101.v304
-rw-r--r--site/posts/RewritingInCoq.v347
-rw-r--r--site/posts/StronglySpecifiedFunctions.v375
-rw-r--r--site/posts/StronglySpecifiedFunctionsProgram.v533
-rw-r--r--site/posts/extensible-type-safe-error-handling.org392
-rw-r--r--site/posts/index.html22
-rw-r--r--site/posts/lisp-journey-getting-started.org255
-rw-r--r--site/posts/monad-transformers.org71
-rw-r--r--site/style/main.css126
10 files changed, 2486 insertions, 0 deletions
diff --git a/site/index.html b/site/index.html
new file mode 100644
index 0000000..442f5a5
--- /dev/null
+++ b/site/index.html
@@ -0,0 +1,61 @@
+<!doctype html>
+<html lang="en">
+ <head>
+ <meta charset="utf-8">
+ <meta name="viewport" content="width=device-width, user-scalable=no">
+ <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/fork-awesome@1.1.7/css/fork-awesome.min.css" integrity="sha256-gsmEoJAws/Kd3CjuOQzLie5Q3yshhvmo7YNtBG7aaEY=" crossorigin="anonymous">
+ <link rel="stylesheet" href="https://cdn.jsdelivr.net/gh/tonsky/FiraCode@1.207/distr/fira_code.css">
+ <link rel="stylesheet" href="https://edwardtufte.github.io/et-book/et-book.css">
+ <link rel="stylesheet" href="/style/main.css">
+ <title></title>
+ </head>
+ <body id="vcard">
+ <article>
+ <img src="https://avatars0.githubusercontent.com/u/1141231?s=460&v=4">
+
+ <p>
+ Hi, awesome stranger.
+ </p>
+
+ <p>
+ I am <strong>lthms</strong>, and I welcome you in my little corner of
+ the Internet.
+ </p>
+
+ <nav>
+ <dl>
+ <dt><a href="/posts/">my blog</a></dt>
+ <dd>
+ You may find interesting my articles if you are into functional
+ programming languages.
+ </dd>
+ </dl>
+ <dl>
+ <dt><a href="https://code.soap.coffee"><i class="fa fa-code" aria-hidden="true"></i> code.soap.coffee</a></dt>
+ <dd>
+ A collection of personal git repositories, including a set of
+ dotfiles (emacs, sway…), a set of tools for story writers.
+ </dd>
+ </dl>
+ <dl>
+ <dt><a href="https://mastodon.social/@lthms"><i class="fa fa-mastodon" aria-hidden="true"></i> @lthms@mastodon.social</a></dt>
+ <dd>
+ My personal account on the fediverse. I mostly toot about functional
+ programming languages, formal methods, and my Emacs configuration.
+ </dd>
+ </dl>
+ <dl>
+ <dt><a href="https://dblp.org/pers/hd/l/Letan:Thomas">my academic publications</a></dt>
+ <dd>
+ I have a PhD in computer science, and I focus my research on
+ applying formal methods approaches to prove security properties.
+ </dd>
+ </dl>
+ </nav>
+
+ <p>
+ I wish you a wonderful day.
+ </p>
+ </article>
+ </body>
+</html>
diff --git a/site/posts/Ltac101.v b/site/posts/Ltac101.v
new file mode 100644
index 0000000..a9d4d68
--- /dev/null
+++ b/site/posts/Ltac101.v
@@ -0,0 +1,304 @@
+(** #
+<h1>Ltac 101</h1>
+<time datetime="2017-10-16">2017-10-16</time>
+ # *)
+
+(** In this article, I give an overview of my findings about the Ltac language,
+ more precisely how it can be used to automate the construction of proof
+ terms. If you never wrote a tactic in Coq and are curious about the subject,
+ it might be a good starting point. *)
+
+(** #<div id="generate-toc"></div># *)
+
+(** ** Tactics Aliases *)
+
+(** The first thing you will probably want to do with Ltac is define aliases for
+ recurring (sequences of) tactics.
+
+ To take a concrete example, the very first tactic I wrote was for a project
+ called SpecCert where _many_ lemmas are basically about proving a given
+ property [P] is a state invariant of a given transition system. As a
+ consequence, they have the very same “shape:”
+
+ \( \forall s\ l\ s', P(s) \wedge s \overset{l\ }{\mapsto} s' \rightarrow P(s') \),
+ that is, if [P] is satisfied for [s], and there exists a transition from [s]
+ to [s'], then [P] is satisfied for [s'].
+
+ Both states and labels are encoded in record, and the first thing I was
+ doing at the time with them was [destruct]ing them. Similarly, the predicate
+ [P] is an aggregation of sub-predicates (using \( \wedge \)). In practice,
+ most of my proofs started with something like [intros [x1 [y1 z1]] [a b] [x2
+ [y2 z2]] [HP1 [HP2 [HP3 HP4]]] [R1|R2]]. Nothing copy/past cannot solve at
+ first, of course, but as soon as the definitions change, you have to change
+ every single [intros] and it is quite boring, to say the least.
+
+ The solution is simple: define a new tactic to use in place of your “raw”
+ [intros]: *)
+
+Ltac my_intros_1 :=
+ intros [x1 [y1 z1]] [a b] [x2 [y2 z2]] [HP1 [HP2 [HP3 HP4]]] [R1|R2].
+
+(** As a more concrete example, we consider the following goal: *)
+
+Goal (forall (P Q : Prop), P /\ Q -> P).
+
+(** A typical way to move the premises of this statement from the goal to the
+ context is by means of [intro], and it is possible to destruct the term [p
+ /\ q] with a pattern. *)
+
+ intros P Q [p q].
+
+(** which leaves the following goal to prove:
+
+<<
+ P, Q : Prop
+ p : P
+ q : Q
+ ============================
+ P
+>>
+
+ Rather than having to remember the exact syntax of the intro-pattern, Coq
+ users can write a specialized tactic. *)
+
+(* begin hide *)
+Undo.
+(* end hide *)
+
+Ltac and_intro := intros [p q].
+
+(** [and_intro] is just another tactic, and therefore is straightforward to
+ use. *)
+
+ intros P Q.
+ and_intro.
+
+(** This leaves the goal to prove in the exact same state as in our previous
+ attempt, which is great because it was exactly the point. However, there is
+ an issue with the [and_intro] command. To demonstrate it, let us consider a
+ slightly different goal. *)
+
+(* begin hide *)
+Abort.
+(* end hide *)
+
+Goal (forall (P Q : Prop), P /\ Q -> Q /\ P -> P).
+
+(** The statement is not very interesting from a logical standpoint, but bear
+ with me while I try to prove it. *)
+
+Proof.
+ intros P Q.
+ and_intro.
+
+(** Again, the goal is as we expect it to be:
+
+<<
+ P, Q : Prop
+ p : P
+ q : Q
+ ============================
+ P /\ Q -> P
+>>
+
+ We still have a premise of the form [P /\ Q] in the current goal… but at the
+ same time, we also have hypotheses named [p] and [q] (the named used by
+ <<and_intro>>) in the context. If we try to use <<and_intro>> again, Coq
+ legitimely complains.
+
+<<
+p is already used.
+>> *)
+(* begin hide *)
+Reset and_intro.
+(* end hide *)
+
+(** To tackle this apparent issue, Ltac provides a mechanic to fetch “fresh”
+ (unused in the current context) names. *)
+
+Ltac and_intro :=
+ let p := fresh "p" in
+ let q := fresh "q" in
+ intros [p q].
+
+(** This time, using [and_intro] several time works fine. In our previous
+ example, the resulting goal is the following: *)
+
+(**
+<<
+ P, Q : Prop
+ p : P
+ q, p0 : Q
+ q0 : P
+ ============================
+ P
+>> *)
+
+(** Finally, tactics can take a set of arguments. They can be of various forms,
+ but the most common to my experience is hypothesis name. For instance, we
+ can write a tactic call <<destruct_and>> to… well, destruct an hypothesis of
+ type [P /\ Q]. *)
+
+Ltac destruct_and H :=
+ let p := fresh "p" in
+ let q := fresh "q" in
+ destruct H as [Hl Hr].
+
+(** With that, you can already write some very useful tactic aliases. It can
+ save you quite some time when refactoring your definitions, but Ltac is
+ capable of much more. *)
+
+(** ** Printing Messages *)
+
+(** One thing that can be useful while writing/debugging a tactic is the ability
+ to print a message. You have to strategies available in Ltac as far as I
+ know: [idtac] and [fail], where [idtac] does not stop the proof script on an
+ error whereas [fail] does. *)
+
+(** ** It Is Just Pattern Matching, Really *)
+
+(** If you need to remember one thing from this blogpost, it is probably this:
+ Ltac pattern matching features are amazing. That is, you will try to find in
+ your goal and hypotheses relevant terms and sub terms you can work with.
+
+ You can pattern match a value as you would do in Gallina, but in Ltac, the
+ pattern match is also capable of more. The first case scenario is when you
+ have a hypothesis name and you want to check its type: *)
+
+Ltac and_or_destruct H :=
+ let Hl := fresh "Hl" in
+ let Hr := fresh "Hr" in
+ match type of H with
+ | _ /\ _
+ => destruct H as [Hl Hr]
+ | _ \/ _
+ => destruct H as [Hl|Hr]
+ end.
+
+(** For the following incomplete proof script: *)
+
+Goal (forall P Q, P /\ Q -> Q \/ P -> True).
+ intros P Q H1 H2.
+ and_or_destruct H1.
+ and_or_destruct H2.
+
+(** We get two sub goals:
+
+<<
+2 subgoals, subgoal 1 (ID 20)
+
+ P, Q : Prop
+ Hl : P
+ Hr, Hl0 : Q
+ ============================
+ True
+
+subgoal 2 (ID 21) is:
+ True
+>>
+ *)
+
+Abort.
+
+(** We are not limited to constructors with the [type of] keyword, We can
+ also pattern match using our own definitions. For instance: *)
+
+Parameter (my_predicate: nat -> Prop).
+
+Ltac and_my_predicate_simpl H :=
+ match type of H with
+ | my_predicate _ /\ _
+ => destruct H as [Hmy_pred _]
+ | _ /\ my_predicate _
+ => destruct H as [_ Hmy_pred]
+ end.
+
+(** Last but not least, it is possible to introspect the current goal of your
+ proof development: *)
+
+Ltac rewrite_something :=
+ match goal with
+ | H: ?x = _ |- context[?x]
+ => rewrite H
+ end.
+
+(** So once again, as an example, the following proof script: *)
+
+Goal (forall (x :nat) (equ : x = 2), x + 2 = 4).
+ intros x equ.
+ rewrite_something.
+
+(** This leaves the following goal to prove:
+
+<<
+1 subgoal, subgoal 1 (ID 6)
+
+ x : nat
+ Heq : x = 2
+ ============================
+ 2 + 2 = 4
+>> *)
+(* begin hide *)
+Abort.
+(* end hide *)
+(** The [rewrite_something] tactic will search an equality relation to use to
+ modify your goal. How does it work?
+
+ - [match goal with] tells Coq we want to pattern match on the whole proof
+ state, not only a known named hypothesis
+ - [ H: ?x = _ |- _ ] is a pattern to tell coq we are looking for a
+ hypothesis [_ = _]
+ - [?x] is a way to bind the left operand of [=] to the name [x]
+ - The right side of [|-] is dedicated to the current goal
+ - [context[?x]] is a way to tell Coq we don’t really want to pattern-match
+ the goal as a whole, but rather we are looking for a subterm of the form
+ [?x]
+ - [rewrite H] will be used in case Coq is able to satisfy the constrains
+ specified by the pattern, with [H] being the hypothesis selected by Coq
+
+
+ Finally, there is one last thing you really need to know before writing a
+ tactic: the difference between [match] and [lazymatch]. Fortunately, it is
+ pretty simple. One the one hand, with [match], if one pattern matches, but
+ the branch body fails, Coq will backtrack and try the next branch. On the
+ other hand, [lazymatch] will stop on error.
+
+ So, for instance, the two following tactics will print two different
+ messages: *)
+
+Ltac match_failure :=
+ match goal with
+ | [ |- _ ]
+ => fail "fail in first branch"
+ | _
+ => fail "fail in second branch"
+ end.
+
+Ltac match_failure' :=
+ lazymatch goal with
+ | [ |- _ ]
+ => fail "fail in first branch"
+ | _
+ => fail "fail in second branch"
+ end.
+
+(** We can try that quite easily by starting a dumb goal (eg. [Goal (True).])
+ and call our tactic. For [match_failure], we get:
+
+<<
+Ltac call to "match_failure" failed.
+Error: Tactic failure: fail in second branch.
+>>
+
+ On the other hand, for [lazymatch_failure], we get:
+
+<<
+Ltac call to "match_failure'" failed.
+Error: Tactic failure: fail in first branch.
+>> *)
+
+(** ** Conclusion *)
+
+(** I were able to tackle my automation needs with these Ltac features. As
+ always with Coq, there is more to learn. For instance, I saw that there is a
+ third kind of pattern match ([multimatch]) I know nothing about. *)
diff --git a/site/posts/RewritingInCoq.v b/site/posts/RewritingInCoq.v
new file mode 100644
index 0000000..5ebf6c6
--- /dev/null
+++ b/site/posts/RewritingInCoq.v
@@ -0,0 +1,347 @@
+(** #
+<h1>Rewriting in Coq</h1>
+<time datetime="2017-05-13">2017-05-13</time>
+ # *)
+
+(** I have to confess something. In the published codebase of SpecCert lies a
+ shameful secret. It takes the form of a set of axioms which are not
+ required. I thought they were when I wrote them, but it was before I heard
+ about “generalized rewriting,” setoids and morphisms.
+
+ Now, I know the truth. I will have to update SpecCert eventually. But,
+ in the meantime, let me try to explain how it is possible to rewrite a
+ term in a proof using a ad-hoc equivalence relation and, when
+ necessary, a proper morphism. *)
+
+(** #<div id="generate-toc"></div># *)
+
+(** ** Gate: Our Case Study *)
+
+(** Now, why would anyone want such a thing as “generalized rewriting” when the
+ [rewrite] tactic works just fine.
+
+ The thing is: it does not in some cases. To illustrate my statement, we will
+ consider the following definition of a gate in Coq: *)
+
+Record Gate :=
+ { open: bool
+ ; lock: bool
+ ; lock_is_close: lock = true -> open = false
+ }.
+
+(** According to this definition, a gate can be either open or closed. It can
+ also be locked, but if it is, it cannot be open at the same time. To express
+ this constrain, we embed the appropriate proposition inside the Record. By
+ doing so, we _know_ for sure that we will never meet an ill-formed Gate
+ instance. The Coq engine will prevent it, because to construct a gate, one
+ will have to prove the [lock_is_close] predicate holds.
+
+ The [program] attribute makes it easy to work with embedded proofs. For
+ instance, defining the ”open gate” is as easy as: *)
+
+Require Import Coq.Program.Tactics.
+
+#[program]
+Definition open_gate :=
+ {| open := true