doc: NFM'22 examples

doc/examples/NFM2022/nfm1.lean

@@ -0,0 +1,20 @@
+#eval "hello" ++ " " ++ "world"
+-- "hello world"
+
+#check true
+-- Bool
+
+def x := 10
+
+#eval x + 2
+-- 12
+
+def double (x : Int) := 2*x
+
+#eval double 3
+-- 6
+#check double
+-- Int → Int
+example : double 4 = 8 := rfl
+
+

doc/examples/NFM2022/nfm12.lean

@@ -0,0 +1,27 @@
+namespace Example
+
+class ToString (α : Type u) where
+  toString : α → String
+
+#check @ToString.toString
+-- {α : Type u_1} → [self : ToString α] → α → String
+
+instance : ToString String where
+  toString s := s
+
+instance : ToString Bool where
+  toString b := if b then "true" else "false"
+
+#eval ToString.toString "hello"
+export ToString (toString)
+#eval toString true
+-- "true"
+#eval toString (true, "hello") -- Error
+
+instance [ToString α] [ToString β] : ToString (α × β) where
+  toString p := "(" ++ toString p.1 ++ ", " ++ toString p.2 ++ ")"
+
+#eval toString (true, "hello")
+-- "(true, hello)"
+
+end Example

doc/examples/NFM2022/nfm13.lean

@@ -0,0 +1,20 @@
+namespace Example
+
+class Mul (α : Type u) where
+  mul : α → α → α
+
+infixl:70 " * " => Mul.mul
+
+class Semigroup (α : Type u) extends Mul α where
+  mul_assoc : ∀ a b c : α, (a * b) * c = a * (b * c)
+
+class Functor (f : Type u → Type v) : Type (max (u+1) v) where
+  map : (α → β) → f α → f β
+
+infixr:100 " <$> " => Functor.map
+
+class LawfulFunctor (f : Type u → Type v) [Functor f] : Prop where
+  id_map   (x : f α) : id <$> x = x
+  comp_map (g : α → β) (h : β → γ) (x : f α) :(h ∘ g) <$> x = h <$> g <$> x
+
+end Example

doc/examples/NFM2022/nfm14.lean

@@ -0,0 +1,13 @@
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq
+  apply And.intro
+  exact hp
+  apply And.intro
+  exact hq
+  exact hp
+
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq
+  apply And.intro
+  exact hp
+  exact And.intro hq hp

doc/examples/NFM2022/nfm15.lean

@@ -0,0 +1,17 @@
+
+example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro h
+  match h with
+  | Exists.intro w (And.intro hp hq) => exact Exists.intro w (And.intro hq hp)
+
+example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro (Exists.intro _ (And.intro hp hq))
+  exact Exists.intro _ (And.intro hq hp)
+
+example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro (.intro _ (.intro hp hq))
+  exact .intro _ (.intro hq hp)
+
+example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro ⟨_, hp, hq⟩
+  exact ⟨_, hq, hp⟩

doc/examples/NFM2022/nfm17.lean

@@ -0,0 +1,17 @@
+example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := by
+  intro h
+  cases h with
+  | intro x hpq =>
+    cases hpq with
+    | intro hp hq =>
+      exists x
+
+example : p ∧ q → q ∧ p := by
+  intro p
+  cases p
+  constructor <;> assumption
+
+example : p ∧ ¬ p → q := by
+  intro h
+  cases h
+  contradiction

doc/examples/NFM2022/nfm19.lean

@@ -0,0 +1,8 @@
+example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
+  intros
+  repeat (any_goals constructor)
+  all_goals assumption
+
+example : p → q → r → p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := by
+  intros
+  repeat (any_goals (first | assumption | constructor))

doc/examples/NFM2022/nfm2.lean

@@ -0,0 +1,12 @@
+def twice (f : Nat → Nat) (a : Nat) :=
+  f (f a)
+
+#check twice
+-- (Nat → Nat) → Nat → Nat
+
+#eval twice (fun x => x + 2) 10
+
+theorem twice_add_2 (a : Nat) : twice (fun x => x + 2) a = a + 4 := rfl
+
+-- `(· + 2)` is syntax sugar for `(fun x => x + 2)`.
+#eval twice (· + 2) 10

doc/examples/NFM2022/nfm24.lean

@@ -0,0 +1,9 @@
+
+
+example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
+  induction as with
+  | nil => rfl
+  | cons x xs ih => simp [List.concat, ih]
+
+example (as : List α) (a : α) : (as.concat a).length = as.length + 1 := by
+  induction as <;> simp! [*]

doc/examples/NFM2022/nfm3.lean

@@ -0,0 +1,55 @@
+inductive Weekday where
+  | sunday | monday | tuesday | wednesday
+  | thursday | friday | saturday
+
+#check Weekday.sunday
+-- Weekday
+
+open Weekday
+#check sunday
+
+def natOfWeekday (d : Weekday) : Nat :=
+  match d with
+  | sunday    => 1
+  | monday    => 2
+  | tuesday   => 3
+  | wednesday => 4
+  | thursday  => 5
+  | friday    => 6
+  | saturday  => 7
+
+def Weekday.next (d : Weekday) : Weekday :=
+  match d with
+  | sunday    => monday
+  | monday    => tuesday
+  | tuesday   => wednesday
+  | wednesday => thursday
+  | thursday  => friday
+  | friday    => saturday
+  | saturday  => sunday
+
+def Weekday.previous : Weekday → Weekday
+  | sunday    => saturday
+  | monday    => sunday
+  | tuesday   => monday
+  | wednesday => tuesday
+  | thursday  => wednesday
+  | friday    => thursday
+  | saturday  => friday
+
+theorem Weekday.next_previous (d : Weekday) : d.next.previous = d :=
+  match d with
+  | sunday    => rfl
+  | monday    => rfl
+  | tuesday   => rfl
+  | wednesday => rfl
+  | thursday  => rfl
+  | friday    => rfl
+  | saturday  => rfl
+
+theorem Weekday.next_previous' (d : Weekday) : d.next.previous = d := by -- switch to tactic mode
+  cases d -- Creates 7 goals
+  rfl; rfl; rfl; rfl; rfl; rfl; rfl
+
+theorem Weekday.next_previous'' (d : Weekday) : d.next.previous = d := by
+  cases d <;> rfl

doc/examples/NFM2022/nfm5.lean

@@ -0,0 +1,19 @@
+def f (α β : Sort u) (a : α) (b : β) : α := a
+
+#eval f Nat String 1 "hello"
+-- 1
+
+def g {α β : Sort u} (a : α) (b : β) : α := a
+
+#eval g 1 "hello"
+
+def h (a : α) (b : β) : α := a
+
+#check g
+-- ?m.1 → ?m.2 → ?m.1
+#check @g
+-- {α β : Sort u} → α → β → α
+#check @h
+-- {α : Sort u_1} → {β : Sort u_2} → α → β → α
+#check g (α := Nat) (β := String)
+-- Nat → String → Nat

doc/examples/NFM2022/nfm7.lean

@@ -0,0 +1,23 @@
+#print Nat -- Nat is an inductive datatype
+
+def fib (n : Nat) : Nat :=
+  match n with
+  | 0 => 1
+  | 1 => 1
+  | n+2 => fib (n+1) + fib n
+
+example : fib 5 = 8 := rfl
+
+example : fib (n+2) = fib (n+1) + fib n := rfl
+
+#print fib
+/-
+def fib : Nat → Nat :=
+fun n =>
+  Nat.brecOn n fun n f =>
+    (match (motive := (n : Nat) → Nat.below n → Nat) n with
+      | 0 => fun x => 1
+      | 1 => fun x => 1
+      | Nat.succ (Nat.succ n) => fun x => x.fst.fst + x.fst.snd.fst.fst)
+      f
+-/

doc/examples/NFM2022/nfm8.lean

@@ -0,0 +1,17 @@
+def sum (a : Array Int) : Int :=
+  let rec go (i : Nat) :=
+     if i < a.size then
+        a[i] + go (i+1)
+     else
+        0
+  go 0
+termination_by go i => a.size - i
+
+set_option pp.proofs true
+#print sum.go
+/-
+def sum.go : Array Int → Nat → Int :=
+fun a =>
+  WellFounded.fix (sum.go.proof_1 a) fun i a_1 =>
+    if h : i < Array.size a then Array.getOp a i + a_1 (i + 1) (sum.go.proof_2 a i h) else 0
+-/

doc/examples/NFM2022/nfm9.lean

@@ -0,0 +1,39 @@
+inductive Term where
+ | const : String → Term
+ | app   : String → List Term → Term
+
+namespace Term
+mutual
+ def numConsts : Term → Nat
+   | const _ => 1
+   | app _ cs => numConstsLst cs
+ def numConstsLst : List Term → Nat
+   | [] => 0
+   | c :: cs => numConsts c + numConstsLst cs
+end
+
+mutual
+  def replaceConst (a b : String) : Term → Term
+   | const c => if a = c then const b else const c
+   | app f cs => app f (replaceConstLst a b cs)
+
+  def replaceConstLst (a b : String) : List Term → List Term
+   | [] => []
+   | c :: cs => replaceConst a b c :: replaceConstLst a b cs
+end
+
+mutual
+  theorem numConsts_replaceConst (a b : String) (e : Term)
+            : numConsts (replaceConst a b e) = numConsts e := by
+    match e with
+    | const c => simp [replaceConst]; split <;> simp [numConsts]
+    | app f cs => simp [replaceConst, numConsts, numConsts_replaceConstLst a b cs]
+
+  theorem numConsts_replaceConstLst (a b : String) (es : List Term)
+            : numConstsLst (replaceConstLst a b es) = numConstsLst es := by
+    match es with
+    | [] => simp [replaceConstLst, numConstsLst]
+    | c :: cs =>
+      simp [replaceConstLst, numConstsLst, numConsts_replaceConst a b c,
+            numConsts_replaceConstLst a b cs]
+end