1 files changed, 38 insertions, 0 deletions
diff --git a/content/zettel/3b7.md b/content/zettel/3b7.md
new file mode 100644
index 0000000..9a6e659
--- /dev/null
+++ b/content/zettel/3b7.md
@@ -0,0 +1,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>