From 020fb82888457062d70ecb5b232d8a60cc3ed951 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sun, 3 Apr 2022 11:17:39 +0200 Subject: [PATCH] doc: clean up examples markup --- doc/examples/bintree.lean | 16 +++++++--------- doc/examples/deBruijn.lean | 4 +--- doc/examples/interp.lean | 6 ++---- doc/examples/palindromes.lean | 12 +++++------- doc/examples/phoas.lean | 4 +--- doc/examples/tc.lean | 4 +--- 6 files changed, 17 insertions(+), 29 deletions(-) diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean index 016ffa59fa..180ec07e33 100644 --- a/doc/examples/bintree.lean +++ b/doc/examples/bintree.lean @@ -1,7 +1,5 @@ /-| -========================================== -Binary Search Trees -========================================== +# Binary Search Trees If the type of keys can be totally ordered -- that is, it supports a well-behaved `≤` comparison -- then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time @@ -101,17 +99,17 @@ We now prove that `t.toList` and `t.toListTR` return the same list. The proof is on induction, and as we used the auxiliary function `go` to define `Tree.toListTR`, we use the auxiliary theorem `go` to prove the theorem. -The proof of the auxiliary theorem is by induction on `t`\ . -The `generalizing acc` modifier instructs Lean to revert `acc`\ , apply the -induction theorem for `Tree`\ s, and then reintroduce `acc` in each case. -By using `generalizing`\ , we obtain the more general induction hypotheses +The proof of the auxiliary theorem is by induction on `t`. +The `generalizing acc` modifier instructs Lean to revert `acc`, apply the +induction theorem for `Tree`s, and then reintroduce `acc` in each case. +By using `generalizing`, we obtain the more general induction hypotheses - `left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc` - `right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc` Recall that the combinator `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, -concatenating all goals produced by `tac'`\ . In this theorem, we use it to apply +concatenating all goals produced by `tac'`. In this theorem, we use it to apply `simp` and close each subgoal produced by the `induction` tactic. The `simp` parameters `toListTR.go` and `toList` instruct the simplifier to try to reduce @@ -237,7 +235,7 @@ theorem Tree.bst_insert_of_bst exact .node h₁ h₂ b₁ b₂ /-| -Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`\ s. +Now, we define the type `BinTree` using a `Subtype` that states that only trees satisfying the BST invariant are `BinTree`s. -/ def BinTree (β : Type u) := { t : Tree β // BST t } diff --git a/doc/examples/deBruijn.lean b/doc/examples/deBruijn.lean index a155cbf00d..5ba4994a16 100644 --- a/doc/examples/deBruijn.lean +++ b/doc/examples/deBruijn.lean @@ -1,7 +1,5 @@ /-| -========================================== -Dependent de Bruijn Indices -========================================== +# Dependent de Bruijn Indices In this example, we represent program syntax terms in a type family parameterized by a list of types, representing the typing context, or information on which free variables are in scope and what diff --git a/doc/examples/interp.lean b/doc/examples/interp.lean index bf99e4a1d0..b89e134da8 100644 --- a/doc/examples/interp.lean +++ b/doc/examples/interp.lean @@ -1,7 +1,5 @@ /-| -========================================== -The Well-Typed Interpreter -========================================== +# The Well-Typed Interpreter In this example, we build an interpreter for a simple functional programming language, with variables, function application, binary operators and an `if...then...else` construct. @@ -22,7 +20,7 @@ inductive Vector (α : Type u) : Nat → Type u | cons : α → Vector α n → Vector α (n+1) /-| -We can overload the `List.cons` notation `::` and use it to create `Vector`\ s. +We can overload the `List.cons` notation `::` and use it to create `Vector`s. -/ infix:67 " :: " => Vector.cons diff --git a/doc/examples/palindromes.lean b/doc/examples/palindromes.lean index 02f06c3b2c..90a5b4169e 100644 --- a/doc/examples/palindromes.lean +++ b/doc/examples/palindromes.lean @@ -1,14 +1,12 @@ /-| -========================================== -Palindromes -========================================== +# Palindromes Palindromes are lists that read the same from left to right and from right to left. For example, `[a, b, b, a]` and `[a, h, a]` are palindromes. We use an inductive predicate to specify whether a list is a palindrome or not. Recall that inductive predicates, or inductively defined propositions, are a convenient -way to specify functions of type `... → Prop`\ . +way to specify functions of type `... → Prop`. This example is a based on an example from the book "The Hitchhiker's Guide to Logical Verification". -/ @@ -25,7 +23,7 @@ The definition distinguishes three cases: (1) `[]` is a palindrome; (2) for any -/ /-| -We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate `h : Palindrome as`\ . +We now prove that the reverse of a palindrome is a palindrome using induction on the inductive predicate `h : Palindrome as`. -/ theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse := by induction h with @@ -66,8 +64,8 @@ We use the attribute `@[simp]` to instruct the `simp` tactic to use this theorem exact dropLast_append_last (as := a₂ :: as) (by simp) /-| -We now define the following auxiliary induction principle for lists using well-founded recursion on `as.length`\ . -We can read it as follows, to prove `motive as`, it suffices to show that: (1) `motive []`\ ; (2) `motive [a]` for any `a`; +We now define the following auxiliary induction principle for lists using well-founded recursion on `as.length`. +We can read it as follows, to prove `motive as`, it suffices to show that: (1) `motive []`; (2) `motive [a]` for any `a`; (3) if `motive as` holds, then `motive ([a] ++ as ++ [b])` also holds for any `a`, `b`, and `as`. Note that the structure of this induction principle is very similar to the `Palindrome` inductive predicate. -/ diff --git a/doc/examples/phoas.lean b/doc/examples/phoas.lean index 6b2e879123..5f8413646e 100644 --- a/doc/examples/phoas.lean +++ b/doc/examples/phoas.lean @@ -1,7 +1,5 @@ /-| -========================================== -Parametric Higher-Order Abstract Syntax -========================================== +# Parametric Higher-Order Abstract Syntax In contrast to first-order encodings, higher-order encodings avoid explicit modeling of variable identity. Instead, the binding constructs of an object language (the language being diff --git a/doc/examples/tc.lean b/doc/examples/tc.lean index 766a020ca2..9ed3843bbf 100644 --- a/doc/examples/tc.lean +++ b/doc/examples/tc.lean @@ -1,7 +1,5 @@ /-| -========================================== -A Certified Type Checker -========================================== +# A Certified Type Checker In this example, we build a certified type checker for a simple expression language.