commit 0c9993eb9c5e3a62245d405d5f0ec78c0eff23cb
parent e4d1a5f6d708c34f2fd24b0bd6efc7a93a0c6e8b
Author: Alex Balgavy <alex@balgavy.eu>
Date: Sat, 12 Dec 2020 18:19:01 +0100
Finalize logical verification notes
Diffstat:
6 files changed, 69 insertions(+), 21 deletions(-)
diff --git a/content/logical-verification/Backward proofs/index.md b/content/logical-verification/Backward proofs/index.md
@@ -1,7 +1,6 @@
+++
title = 'Backward proofs'
+++
-
# Backward proofs
This is like going up the proof tree.
diff --git a/content/logical-verification/Basics.md b/content/logical-verification/Basics.md
@@ -2,7 +2,6 @@
title = 'Basics'
template = 'page-math.html'
+++
-
# Basics
## Type checking
diff --git a/content/logical-verification/Forward proofs.md b/content/logical-verification/Forward proofs.md
@@ -90,4 +90,4 @@ lemma reverse_append {α : Type} :
∀xs ys : list α, reverse (xs ++ ys) = reverse ys ++ reverse xs
| [] ys := by simp [reverse]
| (x :: xs) ys := by simp [reverse, reverse_append xs ys]
-```-
\ No newline at end of file
+```
diff --git a/content/logical-verification/Functional programming.md b/content/logical-verification/Functional programming.md
@@ -112,4 +112,4 @@ Have nodes with max two children.
inductive btree (α : Type) : Type
| empty {} : btree
| node : α → btree → btree → btree
-```-
\ No newline at end of file
+```
diff --git a/content/logical-verification/Inductive predicates.md b/content/logical-verification/Inductive predicates.md
@@ -1,9 +1,7 @@
+++
title = 'Inductive predicates'
+++
-
# Inductive predicates
-
This is basically "logic programming."
Inductive predicates: inductively defined propositions, way to specify functions of type `... → Prop`.
diff --git a/content/logical-verification/_index.md b/content/logical-verification/_index.md
@@ -8,16 +8,70 @@ title = "Logical Verification"
There is a [Git repository](https://github.com/blanchette/logical_verification_2020) and a [book](https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide.pdf) (also [formatted for tablets](https://github.com/blanchette/logical_verification_2020/raw/master/hitchhikers_guide_tablet.pdf)).
- [Basics](basics)
-- [Backward proofs](backward-proofs/)
-- [Forward proofs](forward-proofs/)
-- [Functional programming](functional-programming/)
-- [Inductive predicates](inductive-predicates/)
-- [Monads](monads/)
-- [Metaprogramming](metaprogramming/)
-- [Operational semantics](operational-semantics/)
-- [Hoare logic](hoare-logic/)
-- [Denotational semantics](denotational-semantics/)
-- [Logical foundations of mathematics](logical-foundations-of-mathematics/)
-- [Basic mathematical structures](basic-mathematical-structures/)
-- [Rational and real numbers](rational-and-real-numbers/)
-- [Formalizing the p-adic numbers](formalizing-the-p-adic-numbers/)
+ - [Type checking](basics#type-checking)
+ - [Lean diagnosis commands](basics#lean-diagnosis-commands)
+ - [Inductive type definitions](basics#inductive-type-definitions)
+ - [Function definitions](basics#function-definitions)
+- [Backward proofs](backward-proofs)
+ - [Rewrite rules](backward-proofs#rewrite-rules)
+- [Forward proofs](forward-proofs)
+ - [Structured constructs](forward-proofs#structured-constructs)
+ - [Calculational proofs](forward-proofs#calculational-proofs)
+ - [Dependent types](forward-proofs#dependent-types)
+ - [Curry-Howard Correspondence](forward-proofs#curry-howard-correspondence)
+ - [Induction by pattern matching](forward-proofs#induction-by-pattern-matching)
+- [Functional programming](functional-programming)
+ - [Inductive types](functional-programming#inductive-types)
+ - [Structural induction](functional-programming#structural-induction)
+ - [Structural recursion](functional-programming#structural-recursion)
+ - [Pattern matching](functional-programming#pattern-matching)
+ - [Structures](functional-programming#structures)
+ - [Type classes](functional-programming#type-classes)
+ - [Lists](functional-programming#lists)
+ - [Binary trees](functional-programming#binary-trees)
+- [Inductive predicates](inductive-predicates)
+- [Monads](monads)
+ - [Two operations, three laws](monads#two-operations-three-laws)
+ - [Mutable state](monads#mutable-state)
+ - [Nondeterminism](monads#nondeterminism)
+- [Metaprogramming](metaprogramming)
+ - [Tactics, tactic combinators](metaprogramming#tactics-tactic-combinators)
+ - [The metaprogramming monad](metaprogramming#the-metaprogramming-monad)
+- [Operational semantics](operational-semantics)
+ - [Creating a small imperative language: WHILE](operational-semantics#creating-a-small-imperative-language-while)
+ - [Big-step (natural) semantics](operational-semantics#big-step-natural-semantics)
+ - [Properties of big-step semantics](operational-semantics#properties-of-big-step-semantics)
+ - [Small-step semantics](operational-semantics#small-step-semantics)
+ - [Properties of small-step semantics](operational-semantics#properties-of-small-step-semantics)
+- [Hoare logic](hoare-logic)
+ - [Hoare triples](hoare-logic#hoare-triples)
+ - [Hoare rules](hoare-logic#hoare-rules)
+ - [Semantic approach to Hoare Logic](hoare-logic#semantic-approach-to-hoare-logic)
+ - [Verification condition generator](hoare-logic#verification-condition-generator)
+ - [Hoare triples for total correctness](hoare-logic#hoare-triples-for-total-correctness)
+- [Denotational semantics](denotational-semantics)
+ - [Compositionality](denotational-semantics#compositionality)
+ - [Relational denotational semantics](denotational-semantics#relational-denotational-semantics)
+ - [Fixpoints](denotational-semantics#fixpoints)
+ - [Monotone functions](denotational-semantics#monotone-functions)
+ - [Complete lattices](denotational-semantics#complete-lattices)
+ - [Least fixpoint](denotational-semantics#least-fixpoint)
+ - [Application to program equivalence](denotational-semantics#application-to-program-equivalence)
+- [Logical foundations of mathematics](logical-foundations-of-mathematics)
+ - [Universes](logical-foundations-of-mathematics#universes)
+ - [The Prop universe](logical-foundations-of-mathematics#the-prop-universe)
+ - [Universe of α → β (impredicativity)](logical-foundations-of-mathematics#universe-of-a-b-impredicativity)
+ - [Proof irrelevance](logical-foundations-of-mathematics#proof-irrelevance)
+ - [No large elimination](logical-foundations-of-mathematics#no-large-elimination)
+ - [Axiom of choice](logical-foundations-of-mathematics#axiom-of-choice)
+ - [Subtypes](logical-foundations-of-mathematics#subtypes)
+ - [Quotient types](logical-foundations-of-mathematics#quotient-types)
+- [Basic mathematical structures](basic-mathematical-structures)
+ - [Type classes](basic-mathematical-structures#type-classes)
+ - [Lists, multisets, finite sets](basic-mathematical-structures#lists-multisets-finite-sets)
+ - [Order type classes](basic-mathematical-structures#order-type-classes)
+- [Rational and real numbers](rational-and-real-numbers)
+ - [Rational numbers](rational-and-real-numbers#rational-numbers)
+ - [Real numbers](rational-and-real-numbers#real-numbers)
+- [Formalizing the p-adic numbers](formalizing-the-p-adic-numbers)
+ - [The p-adic norm](formalizing-the-p-adic-numbers#the-p-adic-norm)
