-
Notifications
You must be signed in to change notification settings - Fork 2
/
agda.txt
142 lines (87 loc) · 3.48 KB
/
agda.txt
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
=== Ideen für Agda-Aufgaben
* https://www.cs.bham.ac.uk/~mhe/TypeTopology/Various.RootsOfBooleanFunctions.html#1925
* Euklidische Geometrie
* Primzahlen, siehe etwa
https://hrmacbeth.github.io/math2001/07_Number_Theory.html
* Graham
* Nelson
- Sein PA-Buch formalisieren
- Seinen Beweisassistenten in Agda implementieren
* Deep/shallow embedding
* φ ⇒ ¬¬φ beweisen, sowie ¬¬¬φ ⇒ ¬φ, sowie erklären, wie man den Beweis des
zweiten Resultats mit dem ersten vereinfachen kann.
Außerdem Dinge wie ¬∃ ↔ ∀¬.
Und ganz banal: Gegeben f : A → B und g : B → C, dann habe A → C.
Sowie Drinker.
* Todd Ambridge, https://www.cs.bham.ac.uk/~txw467/mgs24/
* Wenn A und B entscheidbar, dann auch A + B, A x B, A → B.
* Rätsel zum Auswahlaxiom
* Kalupen
* Qx. Qy. x = 2y
* Calkin–Wilf-Baum
cf : [Bool] → ℕ × ℕ
cf-reduced : (α : [Bool]) → IsReduced (cf α)
cf-surjective : (p q : ℕ) → NonZero p → NonZero q → IsReduced (p , q) → ∃[ α ] cf α ≡ (p , q)
* SL₂(ℕ): https://www.codewars.com/kata/5c930224c4661143a6666add
* Blaue-Augen-Rätsel
* uniq
* Reguläre Sprachen etc.? Pumping Lemma!
http://conal.net/talks/language-derivatives.pdf
* Imperative Programmierung (State Monad), Hoare-Tripel
https://github.com/piotr-lewandowski/hoare-triples/blob/master/HoareTriples.agda
* https://github.com/martinescardo/HoTTEST-Summer-School
* https://mathworld.wolfram.com/CosmologicalTheorem.html?
=== Philosophie
* Terence Tao: Formales Beweisen erschließt neue Möglichkeiten der
Kollaboration.
https://www.quantamagazine.org/what-makes-for-good-mathematics-20240201/
* Terminierungsaufgaben von
https://github.com/coq-community/almost-full/blob/master/theories/Default/AFExamples.v
* Mit decision procedures können wir manche Beweise konzeptuell vereinfachen.
Nicht mehr Symmetrieargumente vornehmen, um die Anzahl Fälle auf ein
menschengenießbares Maß zu reduzieren. Sondern einfach automatisiert alle
prüfen. https://arxiv.org/pdf/2405.04699
=== Besonderheiten von Agda
* https://proofassistants.stackexchange.com/questions/1981/what-are-the-complex-induction-patterns-supported-by-agda/2002#2002
* https://proofassistants.stackexchange.com/questions/1981/what-are-the-complex-induction-patterns-supported-by-agda
=== Braucht Berechenbarkeitstheorie computergeprüfte Beweise?
https://yforster.de/files/talk-chocola-synthetic-computability.pdf#page=26
=== Formalisierungsideen Graphentheorie
Graph
- Edge-Relation könnte entscheidbar sein (und überhaupt erst mal eine Prop)
- Vertex-Typ könnte endlich sein
- locally finite
Walk
- ++
- ∈
Acyclic
Sink
Tree
Forest (höchstens ein irredudanter Pfad)
Star
Isomorphism
Ramsey?
Minor
some specific graphs:
- ring
- complete
Reachability
Spanning tree
Menger's theorem?
https://types22.inria.fr/files/2022/06/TYPES_2022_paper_70.pdf
https://cstheory.stackexchange.com/questions/44198/representations-of-planar-graphs-in-coq
https://hal.science/hal-02127698/document
https://dominicpm.github.io/publications/markhert-dijkstra-2016.pdf
https://github.com/pnguyen4/agda-shortest-path
https://publications.lib.chalmers.se/records/fulltext/117330.pdf
=== 2024, Sitzung 1
grande-teorema : 2 + 2 ≡ 4
grande-teorema = refl
favorite-number : ℕ
favorite-number = 42
ℕ : Set
ℕ = ?
- Beispiele für Anwendungen von Agda, u.a. mein Paper mit Peter
- Bool, ℕ, id, neg, and, pred, twice, Empty, Weird
- Dependent-Type-Notation für Funktionstypen
- LessThan2, IsZero, Even, Odd