blob: eae8eb98eeb7583677b6e6188fa55991909e6fe1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
+++
title = "Informal Mathematics"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["4e"]
forwardlinks = []
zettelid = "4f"
+++
Often when I write the mathematics seem to be informal. For example, the
following is meant to describe a **well-founded** relation:
> some metric stored in the $\sim$ relation is decreasing
Then, in many definitions I also do not seem to define things precisely.
I think this is mostly because there is so much content in the Coq proof
that cannot all be translated into words, and needs to be reduced
instead.
Another example is when describing hashed expressions, I think I can be
a bit more precise about what these are semantically, instead of
syntactically in the formalisation.
|
