summaryrefslogtreecommitdiffstats log msg author committer range
blob: fb30186745e73e0b7856fb5a6f3b29b1809de8f2 (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 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330  .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 */(** * Mixing Ltac and Gallina for Fun and Benefits *) (** One of the most misleading introduction to Coq is to say that “Gallina is for programs, while tactics are for proofs.” Indeed, in Coq we construct terms of given types, always. Terms encodes both programs and proofs about these programs. Gallina is the preferred way to construct programs, and tactics are the preferred way to construct proofs. The key word here is “preferred.” We do not always need to use tactics to construct a proof term. Conversly, there are some occasions where constructing a program with tactics become handy. Furthermore, Coq allows for calling tactics from Gallina definitions. Compare to Gallina, Ltac provides two very interesting features: - With [match goal with] it can inspect its context - With [match type of _ with] it can pattern matches on types It turns out these features are more than handy when it comes to metaprogramming (that is, the generation of programs by programs). We proceed as follows. First, we try to demystify how Ltac actually works under the hood. Then, we detail which bridges exists between Gallian and Ltac. Finally, we quickly discuss the risk of using Ltac to generate terms that do not encode proofs. *) (** #
# #
site/posts/MixingLtacAndGallina.v
# *) (** ** What Do Tactics Do? *) (** The Coq proof environment is basically a State monad, where said state is an incomplete terms that is being gradually constructed. This term is hidden to the user, and Coq rather presents so-called “goals.” From this perspective, a goal in Coq in basically a hole within the term we are constructing. 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. *) Definition identity : forall (α : Type), α -> α. (** At this point, we have tell Coq that we want to construct a term of type [forall (α : Type), α -> α]. *) Proof. (** Coq presents us one goal of the form #
#\vdash \forall (\alpha : \mathrm{Type}),\ \alpha \rightarrow \alpha#
# As for the term that we want to construct and that Coq is hiding from us, it is just a hole. In a Coq course, you will learn than the <> allows for turning the premise of an implication into an hypothesis within the context, that is #
#C \vdash P \rightarrow Q#
# becomes #
#C,\ P \vdash Q#
# What <> actually does in refining the “hidden” terms, by inserting an anonymous function. So, when we use *) intro α. (** it refines the term << _1 >> into << fun (α : Type) => _2 >> Similarly, *) intros x. (** refines <<_2>> into << fun (x : α) => _3 >> which means the term constructed (and hidden) by Coq is now << fun (α : Type) (x : α) => _3 >> In the scope wherein <<_3>> lives, two variables are available: [α] and [x]. Therefore, the goal presented by Coq is #
#\alpha : \mathrm{Type},\ x : \alpha \vdash \alpha#
# The [assert] tactic is used to “add an hypothesis to the context, assuming you can prove the hypothesis is true from the context.” What [assert] does under the hood is refine the term we are constructed using [let _ in _]. More precisely, when we use *) assert (y : α). (** It refines the hole [_3] into << let y : α := _4 in _5 >> which means the term we are constructing becomes << fun (α : Type) (x : α) => let y : α := _4 in _5 >> On the one hand, there are two variables availabre inside the scope wherein <<_4>> lives, so the related goal is #
#α : \mathrm{Type},\ x : α \vdash \alpha#
# On the other hand, there are _three_ variables available for defining <<_5>> and the goal presented to the user is now #
#\alpha : \mathrm{Type},\ x : \alpha,\ y : \alpha \vdash \alpha#
# To conclude this first example, we can discuss the [exact] tactic. This tactic takes a term as its argument, and fills the current hole (solves the current goal) with this term. We solve the two subgoals generated by [assert] using [exact]. First, we fill <<_4>> with [x]. *) + exact x. (** Therefore, <<_4>> becomes [x], and the terms that we are gradually defining now is << fun (α : Type) (x : α) => let y : α := x in _5 >> Similarly, *) + exact y. (** fill the last hole with [y]. << fun (α : Type) (x : α) => let y : α := x in y >> The term that we are constructing does not have any hole we need to fill, and therefore Coq does not present us any more “goals to solve.” This is not the end of the story, though. Tactics in Coq are not trusted. It is assumed they can be buggy, which would mean that they can in theory generate incorrect terms. As a consequence, we need to tell Coq to check the term (or verify the proof) using [Qed] or [Defined]. *) Defined. (** Coq accepts the [Defined] command without complaining. It means that the term generated by the tactics typechecks. To some extend, the [refine] tactics is actually the most basic tool you may need. For instance, - [intro x] is equivalent to [refine (fun x => _)] - [assert (x : T)] is equivalent to [refine (let x : T := _ in _)] - [exact x] is equivalent to [refine x] And so on. As a consequence, we can rewrite the previous proof script using [refine]. *) Definition identity' : forall (α : Type), α -> α. Proof. refine (fun (α : Type) => _). refine (fun (x : α) => _). unshelve refine (let y : α := _ in _). + refine x. + refine y. Defined. (** ** A Tale of Two Worlds, and Some Bridges *) (** Constructing terms proofs directly in Gallina often happens when one is writing dependently-typed definition. For instance, we can write a type safe [from_option] function (inspired by ##this very nice write-up##) such that the option to unwrap shall be accompagnied by a proof that said option contains something. This extra argument is used in the [None] case to derive a proof of [False], from which we can derive anything. *) Definition is_some {α} (x : option α) : bool := match x with Some _ => true | None => false end. Lemma is_some_None {α} (x : option α) : x = None -> is_some x <> true. Proof. intros H. rewrite H. discriminate. Qed. Definition from_option {α} (x : option α) (some : is_some x = true) : α := match x as y return x = y -> α with | Some x => fun _ => x | None => fun equ => False_rect α (is_some_None x equ some) end eq_refl. (** In [from_option], we construct two proofs without using tactics: - [False_rect α (is_some_None x equ some)] to exclude the absurd case - [eq_refl] in conjunction with a dependent pattern matching (if you are not familiar with this trick: the main idea is to allow Coq to “remember” that [x = None] in the second branch) We can use another approach. We can decide to implement [from_option] with a proof script. *) Definition from_option' {α} (x : option α) (some : is_some x = true) : α. Proof. case_eq x. + intros y _. exact y. + intros equ. rewrite equ in some. now apply is_some_None in some. Defined. (** There is a third approach we can consider: mixing Gallina terms, and tactics. This is possible thanks to the [ltac:()] feature. *) Definition from_option'' {α} (x : option α) (some : is_some x = true) : α := match x as y return x = y -> α with | Some x => fun _ => x | None => fun equ => ltac:(rewrite equ in some; now apply is_some_None in some) end eq_refl. (** When Coq encounters [ltac:()], it treats it as a hole. It sets up a corresponding goal, and tries to solve it with the supplied tactic. Conversly, there exists ways to construct terms in Gallina when writing a proof script. Certains tactics takes such terms as arguments. Besides, Ltac provides [constr:()] and [uconstr:()] which work similarly to [ltac:()]. The difference between [constr:()] and [uconstr:()] is that Coq will try to assign a type to the argument of [constr:()], but will leave the argument of [uconstr:()] untyped. For instance, consider the following tactic definition. *) Tactic Notation "wrap_id" uconstr(x) := let f := uconstr:(fun x => x) in exact (f x). (** Both [x] the argument of [wrap_id] and [f] the anonymous identity function are not typed. It is only when they are composed together as an argument of [exact] (which expects a typed argument, more precisely of the type of the goal) that Coq actually tries to typecheck it. As a consequence, [wrap_id] generates a specialized identity function for each specific context. *) Definition zero : nat := ltac:(wrap_id 0). (** The generated anonymous identity function is [fun x : nat => x]. *) Definition empty_list α : list α := ltac:(wrap_id nil). (** The generated anonymous identity function is [fun x : list α => x]. Besides, we do not need to give more type information about [nil]. If [wrap_id] were to be expecting a typed term, we would have to replace [nil] by [(@nil α)]. *) (** ** Beware the Automation Elephant in the Room *) (** Proofs and computational programs are encoded in Coq as terms, but there is a fundamental difference between them, and it is highlighted by one of the axiom provided by the Coq standard library: proof irrelevance. Proof irrelevance states that two proofs of the same theorem (i.e., two proof terms which share the same type) are essentially equivalent, and can be substituted without threatening the trustworthiness of the system. From a formal methods point of view, it makes sense. Even if we value “beautiful proofs,” we mostly want correct proofs. The same reasoning does _not_ apply to computational programs. Two functions of type [nat -> nat -> nat] are unlikely to be equivalent. For instance, [add], [mul] or [sub] share the same type, but computes totally different results. Using tactics such as [auto] to generate terms which do not live inside [Prop] is risky, to say the least. For instance, *) Definition add (x y : nat) : nat := ltac:(auto). (** This works, but it is certainly not what you would expect: << add = fun _ y : nat => y : nat -> nat -> nat >> That being said, if we keep that in mind, and assert the correctness of the generated programs (either by providing a proof, or by extensively testing it), there is no particular reason not to use Ltac to generate terms when it makes sens. Dependently-typed programming can help here. If we decorate the return type of a function with the expected properties of the result wrt. the function’s arguments, we can ensure the function is correct, and conversly prevent tactics such as [auto] to generate “incorrect” terms. Interested readers may refer to ##the dedicated series on this very website#. *)