summaryrefslogtreecommitdiffstats log msg author committer range
blob: 2a4fe50eed2862ebc3644d646026c227619d5b8b (plain)
 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251  pre { line-height: 125%; } td.linenos .normal { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; } span.linenos { color: inherit; background-color: transparent; padding-left: 5px; padding-right: 5px; } td.linenos .special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; } span.linenos.special { color: #000000; background-color: #ffffc0; padding-left: 5px; padding-right: 5px; } .highlight .hll { background-color: #ffffcc } .highlight .c { color: #888888 } /* Comment */ .highlight .err { color: #a61717; background-color: #e3d2d2 } /* Error */ .highlight .k { color: #008800; font-weight: bold } /* Keyword */ .highlight .ch { color: #888888 } /* Comment.Hashbang */ .highlight .cm { color: #888888 } /* Comment.Multiline */ .highlight .cp { color: #cc0000; font-weight: bold } /* Comment.Preproc */ .highlight .cpf { color: #888888 } /* Comment.PreprocFile */ .highlight .c1 { color: #888888 } /* Comment.Single */ .highlight .cs { color: #cc0000; font-weight: bold; background-color: #fff0f0 } /* Comment.Special */ .highlight .gd { color: #000000; background-color: #ffdddd } /* Generic.Deleted */ .highlight .ge { font-style: italic } /* Generic.Emph */ .highlight .gr { color: #aa0000 } /* Generic.Error */ .highlight .gh { color: #333333 } /* Generic.Heading */ .highlight .gi { color: #000000; background-color: #ddffdd } /* Generic.Inserted */ .highlight .go { color: #888888 } /* Generic.Output */ .highlight .gp { color: #555555 } /* Generic.Prompt */ .highlight .gs { font-weight: bold } /* Generic.Strong */ .highlight .gu { color: #666666 } /* Generic.Subheading */ .highlight .gt { color: #aa0000 } /* Generic.Traceback */ .highlight .kc { color: #008800; font-weight: bold } /* Keyword.Constant */ .highlight .kd { color: #008800; font-weight: bold } /* Keyword.Declaration */ .highlight .kn { color: #008800; font-weight: bold } /* Keyword.Namespace */ .highlight .kp { color: #008800 } /* Keyword.Pseudo */ .highlight .kr { color: #008800; font-weight: bold } /* Keyword.Reserved */ .highlight .kt { color: #888888; font-weight: bold } /* Keyword.Type */ .highlight .m { color: #0000DD; font-weight: bold } /* Literal.Number */ .highlight .s { color: #dd2200; background-color: #fff0f0 } /* Literal.String */ .highlight .na { color: #336699 } /* Name.Attribute */ .highlight .nb { color: #003388 } /* Name.Builtin */ .highlight .nc { color: #bb0066; font-weight: bold } /* Name.Class */ .highlight .no { color: #003366; font-weight: bold } /* Name.Constant */ .highlight .nd { color: #555555 } /* Name.Decorator */ .highlight .ne { color: #bb0066; font-weight: bold } /* Name.Exception */ .highlight .nf { color: #0066bb; font-weight: bold } /* Name.Function */ .highlight .nl { color: #336699; font-style: italic } /* Name.Label */ .highlight .nn { color: #bb0066; font-weight: bold } /* Name.Namespace */ .highlight .py { color: #336699; font-weight: bold } /* Name.Property */ .highlight .nt { color: #bb0066; font-weight: bold } /* Name.Tag */ .highlight .nv { color: #336699 } /* Name.Variable */ .highlight .ow { color: #008800 } /* Operator.Word */ .highlight .w { color: #bbbbbb } /* Text.Whitespace */ .highlight .mb { color: #0000DD; font-weight: bold } /* Literal.Number.Bin */ .highlight .mf { color: #0000DD; font-weight: bold } /* Literal.Number.Float */ .highlight .mh { color: #0000DD; font-weight: bold } /* Literal.Number.Hex */ .highlight .mi { color: #0000DD; font-weight: bold } /* Literal.Number.Integer */ .highlight .mo { color: #0000DD; font-weight: bold } /* Literal.Number.Oct */ .highlight .sa { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Affix */ .highlight .sb { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Backtick */ .highlight .sc { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Char */ .highlight .dl { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Delimiter */ .highlight .sd { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Doc */ .highlight .s2 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Double */ .highlight .se { color: #0044dd; background-color: #fff0f0 } /* Literal.String.Escape */ .highlight .sh { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Heredoc */ .highlight .si { color: #3333bb; background-color: #fff0f0 } /* Literal.String.Interpol */ .highlight .sx { color: #22bb22; background-color: #f0fff0 } /* Literal.String.Other */ .highlight .sr { color: #008800; background-color: #fff0ff } /* Literal.String.Regex */ .highlight .s1 { color: #dd2200; background-color: #fff0f0 } /* Literal.String.Single */ .highlight .ss { color: #aa6600; background-color: #fff0f0 } /* Literal.String.Symbol */ .highlight .bp { color: #003388 } /* Name.Builtin.Pseudo */ .highlight .fm { color: #0066bb; font-weight: bold } /* Name.Function.Magic */ .highlight .vc { color: #336699 } /* Name.Variable.Class */ .highlight .vg { color: #dd7700 } /* Name.Variable.Global */ .highlight .vi { color: #3333bb } /* Name.Variable.Instance */ .highlight .vm { color: #336699 } /* Name.Variable.Magic */ .highlight .il { color: #0000DD; font-weight: bold } /* Literal.Number.Integer.Long */(** * Ltac is an Imperative Metaprogramming Language *) (** #
site/posts/LtacMetaprogramming.v
# *) (** Coq is often depicted as an _interactive_ proof assistant, thanks to its proof environment. Inside the proof environment, Coq presents the user a goal, and said user solves said goal by means of tactics which describes a logical reasoning. For instance, to reason by induction, one can use the <> tactic, while a simple case analysis can rely on the <> or <> tactics, etc. It is not uncommon for new Coq users to be introduced to Ltac, the Coq default tactic language, using this proof-centric approach. This is not surprising, since writing proofs remains the main use-case for Ltac. In practice though, this discourse remains an abstraction which hides away what actually happens under the hood when Coq executes a proof scripts. To really understand what Ltac is about, we need to recall ourselves that Coq kernel is mostly a typechecker. A theorem statement is expressed as a “type” (which lives in a dedicated sort called [Prop]), and a proof of this theorem is a term of this type, just like the term [S (S O)] (##2##) is of type [nat]. Proving a theorem in Coq requires to construct a term of the type encoding said theorem, and Ltac allows for incrementally constructing this term, one step at a time. Ltac generates terms, therefore it is a metaprogramming language. It does it incrementally, by using primitives to modifying an implicit state, therefore it is an imperative language. Henceforth, it is an imperative metaprogramming language. To summarize, a goal presented by Coq inside the environment proof is a hole within the term being constructed. It is presented to users as: - A list of “hypotheses,” which are nothing more than the variables in the scope of the hole - A type, which is the type of the term to construct to fill the hole We illustrate what happens under the hood of Coq executes a simple proof script. One can use the <> vernacular command to exhibit this. We illustrate how Ltac works with the following example. *) Theorem add_n_O : forall (n : nat), n + O = n. Proof. (** The <> vernacular command starts the proof environment. Since no tactic has been used, the term we are trying to construct consists solely in a hole, while Coq presents us a goal with no hypothesis, and with the exact type of our theorem, that is [forall (n : nat), n + O = n]. A typical Coq course will explain students the <> tactic allows for turning the premise of an implication into an hypothesis within the context. #
#C \vdash P \rightarrow Q#
# becomes #
#C,\ P \vdash Q#
# This is a fundamental rule of deductive reasoning, and <> encodes it. It achieves this by refining the current hole into an anymous function. When we use *) intro n. (** it refines the term << ?Goal1 >> into << fun (n : nat) => ?Goal2 >> The next step of this proof is to reason about induction on [n]. For [nat], it means that to be able to prove #
#\forall n, \mathrm{P}\ n#
# we need to prove that - #
#\mathrm{P}\ 0#
# - #
#\forall n, \mathrm{P}\ n \rightarrow \mathrm{P}\ (S n)#
# The <> tactic effectively turns our goal into two subgoals. But why is that? Because, under the hood, Ltac is refining the current goal using the [nat_ind] function automatically generated by Coq when [nat] was defined. The type of [nat_ind] is << forall (P : nat -> Prop), P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n >> Interestingly enough, [nat_ind] is not an axiom. It is a regular Coq function, whose definition is << fun (P : nat -> Prop) (f : P 0) (f0 : forall n : nat, P n -> P (S n)) => fix F (n : nat) : P n := match n as n0 return (P n0) with | 0 => f | S n0 => f0 n0 (F n0) end >> So, after executing *) induction n. (** The hidden term we are constructing becomes << (fun n : nat => nat_ind (fun n0 : nat => n0 + 0 = n0) ?Goal3 (fun (n0 : nat) (IHn : n0 + 0 = n0) => ?Goal4) n) >> And Coq presents us two goals. First, we need to prove ##\mathrm{P}\ 0##, i.e., ##0 + 0 = 0##. Similarly to Coq presenting a goal when what we are actually doing is constructing a term, the use of ##+## and ##+## (i.e., Coq notations mechanism) hide much here. We can ask Coq to be more explicit by using the vernacular command <> to learn that when Coq presents us a goal of the form [0 + 0 = 0], it is actually looking for a term of type [@eq nat (Nat.add O O) O]. [Nat.add] is a regular Coq (recursive) function. << fix add (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (add p m) end >> Similarly, [eq] is _not_ an axiom. It is a regular inductive type, defined as follows. << Inductive eq (A : Type) (x : A) : A -> Prop := | eq_refl : eq A x x >> Coming back to our current goal, proving [@eq nat (Nat.add 0 0) 0] (i.e., [0 + 0 = 0]) requires to construct a term of a type whose only constructor is [eq_refl]. [eq_refl] accepts one argument, and encodes the proof that said argument is equal to itself. In practice, Coq typechecker will accept the term [@eq_refl _ x] when it expects a term of type [@eq _ x y] _if_ it can reduce [x] and [y] to the same term. Is it the case for [0 + 0 = 0]? It is, since by definition of [Nat.add], [0 + x] is reduced to [x]. We can use the <> tactic to tell Coq to fill the current hole with [eq_refl]. *) + reflexivity. (** Suspicious readers may rely on <> to verify this assertion assert: << (fun n : nat => nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl (fun (n0 : nat) (IHn : n0 + 0 = n0) => ?Goal4) n) >> <> has indeed be replaced by [eq_refl]. One goal remains, as we need to prove that if [n + 0 = n], then [S n + 0 = S n]. Coq can reduce [S n + 0] to [S (n + 0)] by definition of [Nat.add], but it cannot reduce [S n] more than it already is. We can request it to do so using tactics such as [cbn]. *) + cbn. (** We cannot just use <> here (i.e., fill the hole with [eq_refl]), since [S (n + 0)] and [S n] cannot be reduced to the same term. However, at this point of the proof, we have the [IHn] hypothesis (i.e., the [IHn] argument of the anonymous function whose body we are trying to construct). The <> tactic allows for substituting in a type an occurence of [x] by [y] as long as we have a proof of [x = y]. *) rewrite IHn. (** Similarly to <> using a dedicated function , <> refines the current hole with the [eq_ind_r] function (not an axiom!). Replacing [n + 0] with [n] transforms the goal into [S n = S n]. Here, we can use <> (i.e., [eq_refl]) to conclude. *) reflexivity. (** After this last tactic, the work is done. There is no more goal to fill inside the proof term that we have carefully constructed. << (fun n : nat => nat_ind (fun n0 : nat => n0 + 0 = n0) eq_refl (fun (n0 : nat) (IHn : n0 + 0 = n0) => eq_ind_r (fun n1 : nat => S n1 = S n0) eq_refl IHn) n) >> We can finally use [Qed] or [Defined] to tell Coq to typecheck this term. That is, Coq does not trust Ltac, but rather typecheck the term to verify it is correct. This way, in case Ltac has a bug which makes it construct ill-formed type, at the very least Coq can reject it. *) Qed. (** In conclusion, tactics are used to incrementally refine hole inside a term until the latter is complete. They do it in a very specific manner, to encode certain reasoning rule. On the other hand, the <> tactic provides a generic, low-level way to do the same thing. Knowing how a given tactic works allows for mimicking its behavior using the <> tactic. If we take the previous theorem as an example, we can prove it using this alternative proof script. *) Theorem add_n_O' : forall (n : nat), n + O = n. Proof. refine (fun n => _). refine (nat_ind (fun n => n + 0 = n) _ _ n). + refine eq_refl. + refine (fun m IHm => _). refine (eq_ind_r (fun n => S n = S m) _ IHm). refine eq_refl. Qed. (** ** Conclusion *) (** This concludes our introduction to Ltac as an imperative metaprogramming language. In the ##next part of this series##, we present Ltac powerful pattern matching capabilities. *)