**diff options**

Diffstat (limited to 'site')

-rw-r--r-- | site/index.html | 61 | ||||

-rw-r--r-- | site/posts/Ltac101.v | 304 | ||||

-rw-r--r-- | site/posts/RewritingInCoq.v | 347 | ||||

-rw-r--r-- | site/posts/StronglySpecifiedFunctions.v | 375 | ||||

-rw-r--r-- | site/posts/StronglySpecifiedFunctionsProgram.v | 533 | ||||

-rw-r--r-- | site/posts/extensible-type-safe-error-handling.org | 392 | ||||

-rw-r--r-- | site/posts/index.html | 22 | ||||

-rw-r--r-- | site/posts/lisp-journey-getting-started.org | 255 | ||||

-rw-r--r-- | site/posts/monad-transformers.org | 71 | ||||

-rw-r--r-- | site/style/main.css | 126 |

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 |