blob: 9a6e6598ab64fc2fa2f58bae78ae9eec9a07ba6c (
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
|
+++
title = "Proof by reflection"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b6"]
forwardlinks = ["3b8", "3b7a"]
zettelid = "3b7"
+++
Proofs by reflection \[1\] are extremely interesting, as the allow one
to write decision procedures in Gallina itself, which is the typed
language of Coq. The idea is that one can define inductive types which
represent the inputs to the decision procedure, and can then prove
statements about this structure using the decision procedure. Then, to
prove theorems about actual Coq terms, one can use reification to
convert Coq propositions and statements into the defined inductive type,
and then perform the proof by reflection on the type. This then results
in a proof for the original statement, as the decision procedure is
verified to be correct.
One then also has to define a function that evaluates (denotes) a Coq
value from the data-structure. This then has to be proven to be correct
according to the assigned semantics to the inductive structure. This
evaluation provides the reflection for the procedure.
<div id="refs" class="references csl-bib-body" markdown="1">
<div id="ref-chlipala13_certif" class="csl-entry" markdown="1">
<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">A. Chlipala, *Certified
programming with dependent types: A pragmatic introduction to the coq
proof assistant*. MIT Press, 2013.</span>
</div>
</div>
|
