commit ecee7a8a87f1eae644750ed8b0cd57550995ce2c
parent 76a15ac585e2db32e57cfe25f8e5166706d809a4
Author: Alex Balgavy <alex@balgavy.eu>
Date: Mon, 16 Nov 2020 15:18:28 +0100
Updated logical verification notes
Diffstat:
3 files changed, 139 insertions(+), 0 deletions(-)
diff --git a/content/logical-verification/Metaprogramming.md b/content/logical-verification/Metaprogramming.md
@@ -0,0 +1,70 @@
++++
+title = 'Metaprogramming'
++++
+# Metaprogramming
+You can extend Lean with custom tactics/tools; this is metaprogramming.
+
+## Tactics, tactic combinators
+Combinators help if you have to do the same thing multiple times, or recover from failures.
+
+- `repeat`: applies argument repeatedly on all goals until it can't be applied any further
+- `iterate`: applies argument repeatedly on first goal until it fails, and then stops
+- `<|>` ('orelse'): tries first argument, and if it fails, applies second argument
+- `all_goals`: applies argument once to each goal, succeeds only if succeeds on all goals
+- `any_goals`: applies argument once to each goal, succeeds if succeeds on any goal
+- `try`: transforms argument into tactic that never fails (i.e. try it and if you fail it's ok)
+- `solve1`: if argument doesn't prove the goal, fail
+
+## The metaprogramming monad
+`meta` lets a function call other metafunctions.
+Tactics have access to:
+- list of goals as metavariables (`tactic.target`, `tactic.get_goals`)
+- the elaborator to elaborate expressions and find their type
+- the environment with all declarations and inductive types (`tactic.local_context`, `tactic.get_local ``hypothesis`)
+- the attributes (e.g. the list of `@[simp]` rules)
+
+You can print stuff with `tactic.trace`.
+`run_cmd` can run a tactic.
+
+For example, we can rewrite `assumption` which looks through all hypotheses in the context and succeeds if it finds one that works with the goal.
+
+```lean
+meta def exact_list : list expr → tactic unit
+| [] := tactic.fail "no matching hypothesis in environment"
+| (h :: hs) :=
+ do { tactic.trace "trying",
+ tactic.trace h,
+ tactic.exact h }
+ <|> exact_list hs
+
+meta def my_assumption : tactic unit :=
+do
+ hs ← tactic.local_context,
+ exact_list hs
+```
+
+The framework revolves around five main types:
+- `tactic`: manages proof state, global context, etc
+- `name`: represents structured name
+- `expr`: represents expression (term) as abstract syntax tree
+ - `expr.var` gets variables based on De Bruijn indices
+ - `expr.lam` is a lambda expression
+ - `expr.sort` are 'universes' (`Sort 0` is `Prop`, `Sort 1` is `Type`, etc)
+ - `expr.local_const` is hypothesis
+ - `expr.pi` is used for pi binders (e.g. ∀)
+- `declaration`: represents constant declaration, definition, axiom, or lemma
+- `environment`: stores all declarations and notations that make up global context
+
+Unelaborated expressions (pre-expressions) omit some information, elaborated expressions have everything.
+
+We can create literal expressions:
+- expressions with single backtick must be fully elaborated
+- expressions with two backticks are pre-expressions
+- expressions with three backticks are pre-expressions without name checking
+
+Similar for names:
+- names with single backtick are not checked for existence
+- names with two backticks are resolved and checked
+
+Antiquotation lets you embed existing expression into larger expression, using prefix `%%` and name from current context.
+You can also use them in pattern matching, like `(%%a + %%b = %%c) ← tactic.target`
diff --git a/content/logical-verification/Monads.md b/content/logical-verification/Monads.md
@@ -0,0 +1,67 @@
++++
+title = 'Monads'
++++
+# Monads
+## Two operations, three laws
+Monad: type constructor `m` that depends on type parameter `α`.
+Has two operations:
+- `pure {α : Type} : α → m α`: takes a type and wraps it in the monad
+- `bind {α β : Type} : m α → (α → m β) → m β`: takes a type wrapped in monad, modifies it using a function, and returns it wrapped again
+ - `bind ma f` can also be written `ma >>= f`
+
+In english, a monad is a box. `pure` puts stuff in the box, `bind` lets you use and modify stuff in the box.
+
+The `←` operator inside `do` can extract stuff from the monad (take it out of the box).
+
+First law:
+
+```lean
+do
+ a' ← pure a,
+ f a'
+=
+ f a
+```
+
+Second law:
+
+```lean
+do
+ a ← ma,
+ pure a
+=
+ ma
+```
+
+## Mutable state
+The state monad is based on an 'action':
+
+```lean
+def action (σ α : Type) :=
+σ → α × σ
+```
+
+`σ` is the state here, or the 'context'.
+
+Then you can have several operations on the state:
+
+```lean
+def action.read {σ : Type} : action σ σ
+| s := (s, s)
+
+def action.write {σ : Type} (s : σ) : action σ unit
+| _ := ((), s)
+
+def action.pure {σ α : Type} (a : α) : action σ α
+| s := (a, s)
+
+def action.bind {σ : Type} {α β : Type} (ma : action σ α) (f : α → action σ β) : action σ β
+| s :=
+ match ma s with
+ | (a, s') := f a s'
+ end
+```
+
+## Nondeterminism
+When a program can return one of many possible values.
+This can be modelled with sets -- i.e. it returns something from a set of values.
diff --git a/content/logical-verification/_index.md b/content/logical-verification/_index.md
@@ -12,3 +12,5 @@ There is a [Git repository](https://github.com/blanchette/logical_verification_2
- [Forward proofs](forward-proofs/)
- [Functional programming](functional-programming/)
- [Inductive predicates](inductive-predicates/)
+- [Monads](monads/)
+- [Metaprogramming](metaprogramming/)
