blob: af90b26ef9d9cf5dfbf5eff70570a5b2a0627682 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
+++
title = "Benefits of proofs by reflection"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b7"]
forwardlinks = []
zettelid = "3b7a"
+++
The two main benefits of proof by reflection are that:
- The size of the proof is small, because the statement of the
function is enough as a proof for it, meaning that it is often only
linear in the size of the number being proven, for example.
- Proofs by reflection also "just work", because the dependent type of
the function gives a good indication about what proofs it will
return. As it has been verified to be correct, one knows that the
decision procedure will also work correctly. This is much better
than defining a recursive `Ltac` function as that does not have any
guarantees at all.
|
