From cb32681978e87b7212e3711eba6f0c79e376c8cd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 May 2022 18:20:37 -0700 Subject: [PATCH] doc: add slide headers to examples --- doc/examples/NFM2022/nfm1.lean | 2 ++ doc/examples/NFM2022/nfm10.lean | 2 ++ doc/examples/NFM2022/nfm11.lean | 2 ++ doc/examples/NFM2022/nfm12.lean | 1 + doc/examples/NFM2022/nfm13.lean | 16 ++++++++++++++++ doc/examples/NFM2022/nfm14.lean | 4 ++++ doc/examples/NFM2022/nfm15.lean | 1 + doc/examples/NFM2022/nfm16.lean | 2 ++ doc/examples/NFM2022/nfm17.lean | 2 ++ doc/examples/NFM2022/nfm18.lean | 2 ++ doc/examples/NFM2022/nfm19.lean | 2 ++ doc/examples/NFM2022/nfm2.lean | 2 ++ doc/examples/NFM2022/nfm20.lean | 2 ++ doc/examples/NFM2022/nfm21.lean | 2 ++ doc/examples/NFM2022/nfm22.lean | 6 ++++-- doc/examples/NFM2022/nfm23.lean | 2 ++ doc/examples/NFM2022/nfm24.lean | 2 +- doc/examples/NFM2022/nfm3.lean | 4 ++++ doc/examples/NFM2022/nfm4.lean | 1 + doc/examples/NFM2022/nfm5.lean | 2 ++ doc/examples/NFM2022/nfm6.lean | 1 + doc/examples/NFM2022/nfm7.lean | 2 ++ doc/examples/NFM2022/nfm8.lean | 2 ++ doc/examples/NFM2022/nfm9.lean | 5 +++++ 24 files changed, 66 insertions(+), 3 deletions(-) diff --git a/doc/examples/NFM2022/nfm1.lean b/doc/examples/NFM2022/nfm1.lean index 6126f09adc..539de041e8 100644 --- a/doc/examples/NFM2022/nfm1.lean +++ b/doc/examples/NFM2022/nfm1.lean @@ -1,3 +1,5 @@ +/- "Hello world" -/ + #eval "hello" ++ " " ++ "world" -- "hello world" diff --git a/doc/examples/NFM2022/nfm10.lean b/doc/examples/NFM2022/nfm10.lean index 1b54af6411..6f1dba630f 100644 --- a/doc/examples/NFM2022/nfm10.lean +++ b/doc/examples/NFM2022/nfm10.lean @@ -1,3 +1,5 @@ +/- Dependent pattern matching -/ + inductive Vector (α : Type u) : Nat → Type u | nil : Vector α 0 | cons : α → Vector α n → Vector α (n+1) diff --git a/doc/examples/NFM2022/nfm11.lean b/doc/examples/NFM2022/nfm11.lean index d513520b28..183588ff90 100644 --- a/doc/examples/NFM2022/nfm11.lean +++ b/doc/examples/NFM2022/nfm11.lean @@ -1,3 +1,5 @@ +/- Structures -/ + structure Point where x : Int := 0 y : Int := 0 diff --git a/doc/examples/NFM2022/nfm12.lean b/doc/examples/NFM2022/nfm12.lean index b20017aaf5..0dd359f0db 100644 --- a/doc/examples/NFM2022/nfm12.lean +++ b/doc/examples/NFM2022/nfm12.lean @@ -1,3 +1,4 @@ +/- Type classes -/ namespace Example class ToString (α : Type u) where diff --git a/doc/examples/NFM2022/nfm13.lean b/doc/examples/NFM2022/nfm13.lean index c9d6f816c0..a78cd872f9 100644 --- a/doc/examples/NFM2022/nfm13.lean +++ b/doc/examples/NFM2022/nfm13.lean @@ -1,3 +1,4 @@ +/- Type classes are heavily used in Lean -/ namespace Example class Mul (α : Type u) where @@ -26,3 +27,18 @@ class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where comp_map (g : α → β) (h : β → γ) (x : f α) :(h ∘ g) <$> x = h <$> g <$> x end Example + +/- +`Deriving instances automatically` + +We have seen `deriving Repr` in a few examples. +It is an instance generator. +Lean comes equipped with generators for the following classes. +`Repr`, `Inhabited`, `BEq`, `DecidableEq`, +`Hashable`, `Ord`, `FromToJson`, `SizeOf` +-/ + +inductive Tree (α : Type u) where + | leaf (val : α) + | node (left right : Tree α) + deriving DecidableEq, Ord, Inhabited, Repr diff --git a/doc/examples/NFM2022/nfm14.lean b/doc/examples/NFM2022/nfm14.lean index b9c268e598..79569fddf6 100644 --- a/doc/examples/NFM2022/nfm14.lean +++ b/doc/examples/NFM2022/nfm14.lean @@ -1,3 +1,5 @@ +/- Tactics -/ + example : p → q → p ∧ q ∧ p := by intro hp hq apply And.intro @@ -9,6 +11,8 @@ example : p → q → p ∧ q ∧ p := by example : p → q → p ∧ q ∧ p := by intro hp hq; apply And.intro hp; exact And.intro hq hp +/- Structuring proofs -/ + example : p → q → p ∧ q ∧ p := by intro hp hq apply And.intro diff --git a/doc/examples/NFM2022/nfm15.lean b/doc/examples/NFM2022/nfm15.lean index e2701a387b..46e493c70d 100644 --- a/doc/examples/NFM2022/nfm15.lean +++ b/doc/examples/NFM2022/nfm15.lean @@ -1,3 +1,4 @@ +/- intro tactic variants -/ example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by intro h diff --git a/doc/examples/NFM2022/nfm16.lean b/doc/examples/NFM2022/nfm16.lean index 7a551be6d6..333b3f8456 100644 --- a/doc/examples/NFM2022/nfm16.lean +++ b/doc/examples/NFM2022/nfm16.lean @@ -1,3 +1,5 @@ +/- Inaccessible names -/ + example : ∀ x y : Nat, x = y → y = x := by intros apply Eq.symm diff --git a/doc/examples/NFM2022/nfm17.lean b/doc/examples/NFM2022/nfm17.lean index 21591b45cd..c64cc9bb97 100644 --- a/doc/examples/NFM2022/nfm17.lean +++ b/doc/examples/NFM2022/nfm17.lean @@ -1,3 +1,5 @@ +/- More tactics -/ + example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by intro h cases h with diff --git a/doc/examples/NFM2022/nfm18.lean b/doc/examples/NFM2022/nfm18.lean index fac172ca16..e74262d2af 100644 --- a/doc/examples/NFM2022/nfm18.lean +++ b/doc/examples/NFM2022/nfm18.lean @@ -1,3 +1,5 @@ +/- Structuring proofs (cont.) -/ + example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by intro h have hp : p := h.left diff --git a/doc/examples/NFM2022/nfm19.lean b/doc/examples/NFM2022/nfm19.lean index a6e6ea6678..2246d43632 100644 --- a/doc/examples/NFM2022/nfm19.lean +++ b/doc/examples/NFM2022/nfm19.lean @@ -1,3 +1,5 @@ +/- Tactic combinators -/ + example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by intros repeat (any_goals constructor) diff --git a/doc/examples/NFM2022/nfm2.lean b/doc/examples/NFM2022/nfm2.lean index fa9f1df0c2..591ba9920f 100644 --- a/doc/examples/NFM2022/nfm2.lean +++ b/doc/examples/NFM2022/nfm2.lean @@ -1,3 +1,5 @@ +/- First-class functions -/ + def twice (f : Nat → Nat) (a : Nat) := f (f a) diff --git a/doc/examples/NFM2022/nfm20.lean b/doc/examples/NFM2022/nfm20.lean index e38bdecbcd..391b31cbb5 100644 --- a/doc/examples/NFM2022/nfm20.lean +++ b/doc/examples/NFM2022/nfm20.lean @@ -1,3 +1,5 @@ +/- Rewriting -/ + example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by rw [h₂] -- replace k with 0 rw [h₁] -- replace f 0 with 0 diff --git a/doc/examples/NFM2022/nfm21.lean b/doc/examples/NFM2022/nfm21.lean index da3b2e98b3..37f6c5e565 100644 --- a/doc/examples/NFM2022/nfm21.lean +++ b/doc/examples/NFM2022/nfm21.lean @@ -1,3 +1,5 @@ +/- Simplifier -/ + example (p : Nat → Prop) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by simp diff --git a/doc/examples/NFM2022/nfm22.lean b/doc/examples/NFM2022/nfm22.lean index 36f76ca12f..762c52b037 100644 --- a/doc/examples/NFM2022/nfm22.lean +++ b/doc/examples/NFM2022/nfm22.lean @@ -1,8 +1,10 @@ +/- Simplifier -/ + def mk_symm (xs : List α) := - xs ++ xs.reverse + xs ++ xs.reverse @[simp] theorem reverse_mk_symm : (mk_symm xs).reverse = mk_symm xs := by - simp [mk_symm] + simp [mk_symm] theorem tst : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by simp diff --git a/doc/examples/NFM2022/nfm23.lean b/doc/examples/NFM2022/nfm23.lean index 770b867fb1..f51a1d255f 100644 --- a/doc/examples/NFM2022/nfm23.lean +++ b/doc/examples/NFM2022/nfm23.lean @@ -1,3 +1,5 @@ +/- split tactic -/ + def f (x y z : Nat) : Nat := match x, y, z with | 5, _, _ => y diff --git a/doc/examples/NFM2022/nfm24.lean b/doc/examples/NFM2022/nfm24.lean index 2ff564d7cf..9b3d1687d4 100644 --- a/doc/examples/NFM2022/nfm24.lean +++ b/doc/examples/NFM2022/nfm24.lean @@ -1,4 +1,4 @@ - +/- induction tactic -/ example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by induction as with diff --git a/doc/examples/NFM2022/nfm3.lean b/doc/examples/NFM2022/nfm3.lean index 8b22076865..3db2507777 100644 --- a/doc/examples/NFM2022/nfm3.lean +++ b/doc/examples/NFM2022/nfm3.lean @@ -1,3 +1,5 @@ +/- Enumerated types -/ + inductive Weekday where | sunday | monday | tuesday | wednesday | thursday | friday | saturday @@ -37,6 +39,8 @@ def Weekday.previous : Weekday → Weekday | friday => thursday | saturday => friday +/- Proving theorems using tactics -/ + theorem Weekday.next_previous (d : Weekday) : d.next.previous = d := match d with | sunday => rfl diff --git a/doc/examples/NFM2022/nfm4.lean b/doc/examples/NFM2022/nfm4.lean index 1efbd87cdd..79bb5a8226 100644 --- a/doc/examples/NFM2022/nfm4.lean +++ b/doc/examples/NFM2022/nfm4.lean @@ -1,3 +1,4 @@ +/- What is the type of Nat? -/ #check 0 -- Nat diff --git a/doc/examples/NFM2022/nfm5.lean b/doc/examples/NFM2022/nfm5.lean index 676526371e..4ee42805ca 100644 --- a/doc/examples/NFM2022/nfm5.lean +++ b/doc/examples/NFM2022/nfm5.lean @@ -1,3 +1,5 @@ +/- Implicit arguments and universe polymorphism -/ + def f (α β : Sort u) (a : α) (b : β) : α := a #eval f Nat String 1 "hello" diff --git a/doc/examples/NFM2022/nfm6.lean b/doc/examples/NFM2022/nfm6.lean index f6e9132632..dfeecbaacd 100644 --- a/doc/examples/NFM2022/nfm6.lean +++ b/doc/examples/NFM2022/nfm6.lean @@ -1,3 +1,4 @@ +/- Inductive Types -/ inductive Tree (β : Type v) where | leaf diff --git a/doc/examples/NFM2022/nfm7.lean b/doc/examples/NFM2022/nfm7.lean index d37463c700..10370fbf42 100644 --- a/doc/examples/NFM2022/nfm7.lean +++ b/doc/examples/NFM2022/nfm7.lean @@ -1,3 +1,5 @@ +/- Recursive functions -/ + #print Nat -- Nat is an inductive datatype def fib (n : Nat) : Nat := diff --git a/doc/examples/NFM2022/nfm8.lean b/doc/examples/NFM2022/nfm8.lean index 3dc105340a..0e30270ac4 100644 --- a/doc/examples/NFM2022/nfm8.lean +++ b/doc/examples/NFM2022/nfm8.lean @@ -1,3 +1,5 @@ +/- Well-founded recursion -/ + def ack : Nat → Nat → Nat | 0, y => y+1 | x+1, 0 => ack x 1 diff --git a/doc/examples/NFM2022/nfm9.lean b/doc/examples/NFM2022/nfm9.lean index 8a5e2490cf..85a4886975 100644 --- a/doc/examples/NFM2022/nfm9.lean +++ b/doc/examples/NFM2022/nfm9.lean @@ -1,3 +1,5 @@ +/- Mutual recursion -/ + inductive Term where | const : String → Term | app : String → List Term → Term @@ -7,6 +9,7 @@ mutual def numConsts : Term → Nat | const _ => 1 | app _ cs => numConstsLst cs + def numConstsLst : List Term → Nat | [] => 0 | c :: cs => numConsts c + numConstsLst cs @@ -22,6 +25,8 @@ mutual | c :: cs => replaceConst a b c :: replaceConstLst a b cs end +/- Mutual recursion in theorems -/ + mutual theorem numConsts_replaceConst (a b : String) (e : Term) : numConsts (replaceConst a b e) = numConsts e := by