From bf5f107e74da9e25cd747275af3dcff5bea6d7bb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 23 May 2022 18:04:03 -0700
Subject: [PATCH] doc: missing NFM examples

---
 doc/examples/NFM2022/nfm10.lean | 17 +++++++++++++++++
 doc/examples/NFM2022/nfm11.lean | 20 ++++++++++++++++++++
 doc/examples/NFM2022/nfm12.lean |  2 +-
 doc/examples/NFM2022/nfm13.lean |  8 ++++++++
 doc/examples/NFM2022/nfm14.lean | 18 ++++++++++++++++--
 doc/examples/NFM2022/nfm15.lean |  9 +++++----
 doc/examples/NFM2022/nfm16.lean | 10 ++++++++++
 doc/examples/NFM2022/nfm18.lean | 18 ++++++++++++++++++
 doc/examples/NFM2022/nfm20.lean | 20 ++++++++++++++++++++
 doc/examples/NFM2022/nfm21.lean | 19 +++++++++++++++++++
 doc/examples/NFM2022/nfm22.lean | 11 +++++++++++
 doc/examples/NFM2022/nfm23.lean | 24 ++++++++++++++++++++++++
 doc/examples/NFM2022/nfm4.lean  | 19 +++++++++++++++++++
 doc/examples/NFM2022/nfm6.lean  | 13 +++++++++++++
 doc/examples/NFM2022/nfm8.lean  |  6 ++++++
 15 files changed, 207 insertions(+), 7 deletions(-)

diff --git a/doc/examples/NFM2022/nfm10.lean b/doc/examples/NFM2022/nfm10.lean
index e69de29bb2..1b54af6411 100644
--- a/doc/examples/NFM2022/nfm10.lean
+++ b/doc/examples/NFM2022/nfm10.lean
@@ -0,0 +1,17 @@
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+
+infix:67 "::" => Vector.cons
+
+def Vector.zip : Vector α n → Vector β n → Vector (α × β) n
+  | nil, nil => nil
+  | a::as, b::bs => (a, b) :: zip as bs
+
+#print Vector.zip
+/-
+def Vector.zip.{u_1, u_2} : {α : Type u_1} → {n : Nat} → {β : Type u_2} → Vector α n → Vector β n → Vector (α × β) n :=
+fun {α} {n} {β} x x_1 =>
+  Vector.brecOn (motive := fun {n} x => {β : Type u_2} → Vector β n → Vector (α × β) n) x
+    ...
+-/
diff --git a/doc/examples/NFM2022/nfm11.lean b/doc/examples/NFM2022/nfm11.lean
index e69de29bb2..d513520b28 100644
--- a/doc/examples/NFM2022/nfm11.lean
+++ b/doc/examples/NFM2022/nfm11.lean
@@ -0,0 +1,20 @@
+structure Point where
+  x : Int := 0
+  y : Int := 0
+  deriving Repr
+
+#eval Point.x (Point.mk 10 20)
+-- 10
+
+#eval { x := 10, y := 20 : Point }
+
+def p : Point := { y := 20 }
+
+#eval p.x
+#eval p.y
+#eval { p with x := 5 }
+-- { x := 5, y := 20 }
+
+structure Point3D extends Point where
+  z : Int
+
diff --git a/doc/examples/NFM2022/nfm12.lean b/doc/examples/NFM2022/nfm12.lean
index 4c6b325197..b20017aaf5 100644
--- a/doc/examples/NFM2022/nfm12.lean
+++ b/doc/examples/NFM2022/nfm12.lean
@@ -16,7 +16,7 @@ instance : ToString Bool where
 export ToString (toString)
 #eval toString true
 -- "true"
-#eval toString (true, "hello") -- Error
+-- #eval toString (true, "hello") -- Error
 
 instance [ToString α] [ToString β] : ToString (α × β) where
   toString p := "(" ++ toString p.1 ++ ", " ++ toString p.2 ++ ")"
diff --git a/doc/examples/NFM2022/nfm13.lean b/doc/examples/NFM2022/nfm13.lean
index 42eaad5f43..c9d6f816c0 100644
--- a/doc/examples/NFM2022/nfm13.lean
+++ b/doc/examples/NFM2022/nfm13.lean
@@ -5,9 +5,17 @@ class Mul (α : Type u) where
 
 infixl:70 " * " => Mul.mul
 
+def double [Mul α] (a : α) := a * a
+
 class Semigroup (α : Type u) extends Mul α where
   mul_assoc : ∀ a b c : α, (a * b) * c = a * (b * c)
 
+instance : Semigroup Nat where
+  mul := Nat.mul
+  mul_assoc := Nat.mul_assoc
+
+#eval double 5
+
 class Functor (f : Type u → Type v) : Type (max (u+1) v) where
   map : (α → β) → f α → f β
 
diff --git a/doc/examples/NFM2022/nfm14.lean b/doc/examples/NFM2022/nfm14.lean
index c47488695a..b9c268e598 100644
--- a/doc/examples/NFM2022/nfm14.lean
+++ b/doc/examples/NFM2022/nfm14.lean
@@ -6,8 +6,22 @@ example : p → q → p ∧ q ∧ p := by
   exact hq
   exact hp
 
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq; apply And.intro hp; exact And.intro hq hp
+
 example : p → q → p ∧ q ∧ p := by
   intro hp hq
   apply And.intro
-  exact hp
-  exact And.intro hq hp
+  case left => exact hp
+  case right =>
+    apply And.intro
+    case left => exact hq
+    case right => exact hp
+
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq
+  apply And.intro
+  . exact hp
+  . apply And.intro
+    . exact hq
+    . exact hp
diff --git a/doc/examples/NFM2022/nfm15.lean b/doc/examples/NFM2022/nfm15.lean
index d8fdb54ad6..e2701a387b 100644
--- a/doc/examples/NFM2022/nfm15.lean
+++ b/doc/examples/NFM2022/nfm15.lean
@@ -8,10 +8,11 @@ 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⟩
+
+example (α : Type) (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := by
+  intro
+    | ⟨_, .inl h⟩ => exact ⟨_, .inr h⟩
+    | ⟨_, .inr h⟩ => exact ⟨_, .inl h⟩
diff --git a/doc/examples/NFM2022/nfm16.lean b/doc/examples/NFM2022/nfm16.lean
index e69de29bb2..7a551be6d6 100644
--- a/doc/examples/NFM2022/nfm16.lean
+++ b/doc/examples/NFM2022/nfm16.lean
@@ -0,0 +1,10 @@
+example : ∀ x y : Nat, x = y → y = x := by
+  intros
+  apply Eq.symm
+  assumption
+
+example : ∀ x y : Nat, x = y → y = x := by
+  intros
+  apply Eq.symm
+  rename_i a b hab
+  exact hab
diff --git a/doc/examples/NFM2022/nfm18.lean b/doc/examples/NFM2022/nfm18.lean
index e69de29bb2..fac172ca16 100644
--- a/doc/examples/NFM2022/nfm18.lean
+++ b/doc/examples/NFM2022/nfm18.lean
@@ -0,0 +1,18 @@
+example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
+  intro h
+  have hp : p := h.left
+  have hqr : q ∨ r := h.right
+  show (p ∧ q) ∨ (p ∧ r)
+  cases hqr with
+  | inl hq => exact Or.inl ⟨hp, hq⟩
+  | inr hr => exact Or.inr ⟨hp, hr⟩
+
+example : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := by
+  intro ⟨hp, hqr⟩
+  cases hqr with
+  | inl hq =>
+    have := And.intro hp hq
+    apply Or.inl; exact this
+  | inr hr =>
+    have := And.intro hp hr
+    apply Or.inr; exact this
diff --git a/doc/examples/NFM2022/nfm20.lean b/doc/examples/NFM2022/nfm20.lean
index e69de29bb2..e38bdecbcd 100644
--- a/doc/examples/NFM2022/nfm20.lean
+++ b/doc/examples/NFM2022/nfm20.lean
@@ -0,0 +1,20 @@
+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
+
+example (f : Nat → Nat) (k : Nat) (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := by
+  rw [h₂, h₁]
+
+example (f : Nat → Nat) (a b : Nat) (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := by
+  rw [← h₁, h₂]
+
+example (f : Nat → Nat) (a : Nat) (h : 0 + a = 0) : f a = f 0 := by
+  rw [Nat.zero_add] at h
+  rw [h]
+
+def Tuple (α : Type) (n : Nat) :=
+  { as : List α // as.length = n }
+
+example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := by
+  rw [h] at t
+  exact t
diff --git a/doc/examples/NFM2022/nfm21.lean b/doc/examples/NFM2022/nfm21.lean
index e69de29bb2..da3b2e98b3 100644
--- a/doc/examples/NFM2022/nfm21.lean
+++ b/doc/examples/NFM2022/nfm21.lean
@@ -0,0 +1,19 @@
+example (p : Nat → Prop) : (x + 0) * (0 + y * 1 + z * 0) = x * y := by
+  simp
+
+example (p : Nat → Prop) (h : p (x * y)) : p ((x + 0) * (0 + y * 1 + z * 0)) := by
+  simp; assumption
+
+example (p : Nat → Prop) (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := by
+  simp at h; assumption
+
+def f (m n : Nat) : Nat :=
+  m + n + m
+
+example (h : n = 1) (h' : 0 = m) : (f m n) = n := by
+  simp [h, ←h', f]
+
+example (p : Nat → Prop) (h₁ : x + 0 = x') (h₂ : y + 0 = y')
+        : x + y + 0 = x' + y' := by
+  simp at *
+  simp [*]
diff --git a/doc/examples/NFM2022/nfm22.lean b/doc/examples/NFM2022/nfm22.lean
index e69de29bb2..36f76ca12f 100644
--- a/doc/examples/NFM2022/nfm22.lean
+++ b/doc/examples/NFM2022/nfm22.lean
@@ -0,0 +1,11 @@
+def mk_symm (xs : List α) :=
+ xs ++ xs.reverse
+
+@[simp] theorem reverse_mk_symm : (mk_symm xs).reverse = mk_symm xs := by
+ simp [mk_symm]
+
+theorem tst : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := by
+  simp
+
+#print tst
+-- Lean reverse_mk_symm, and List.reverse_append
diff --git a/doc/examples/NFM2022/nfm23.lean b/doc/examples/NFM2022/nfm23.lean
index e69de29bb2..770b867fb1 100644
--- a/doc/examples/NFM2022/nfm23.lean
+++ b/doc/examples/NFM2022/nfm23.lean
@@ -0,0 +1,24 @@
+def f (x y z : Nat) : Nat :=
+  match x, y, z with
+  | 5, _, _ => y
+  | _, 5, _ => y
+  | _, _, 5 => y
+  | _, _, _ => 1
+
+example : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := by
+  intros
+  simp [f]
+  split
+  . contradiction
+  . contradiction
+  . contradiction
+  . rfl
+
+def g (xs ys : List Nat) : Nat :=
+  match xs, ys with
+  | [a, b], _ => a+b+1
+  | _, [b, c] => b+1
+  | _, _      => 1
+
+example (xs ys : List Nat) (h : g xs ys = 0) : False := by
+  unfold g at h; split at h <;> simp_arith at h
diff --git a/doc/examples/NFM2022/nfm4.lean b/doc/examples/NFM2022/nfm4.lean
index e69de29bb2..1efbd87cdd 100644
--- a/doc/examples/NFM2022/nfm4.lean
+++ b/doc/examples/NFM2022/nfm4.lean
@@ -0,0 +1,19 @@
+
+#check 0
+-- Nat
+#check Nat
+-- Type
+#check Type
+-- Type 1
+#check Type 1
+-- Type 2
+#check Eq.refl 2
+-- 2 = 2
+#check 2 = 2
+-- Prop
+#check Prop
+-- Type
+
+example : Prop = Sort 0   := rfl
+example : Type = Sort 1   := rfl
+example : Type 1 = Sort 2 := rfl
diff --git a/doc/examples/NFM2022/nfm6.lean b/doc/examples/NFM2022/nfm6.lean
index e69de29bb2..f6e9132632 100644
--- a/doc/examples/NFM2022/nfm6.lean
+++ b/doc/examples/NFM2022/nfm6.lean
@@ -0,0 +1,13 @@
+
+inductive Tree (β : Type v) where
+  | leaf
+  | node (left : Tree β) (key : Nat) (value : β) (right : Tree β)
+  deriving Repr
+
+#eval Tree.node .leaf 10 true .leaf
+-- Tree.node Tree.leaf 10 true Tree.leaf
+
+inductive Vector (α : Type u) : Nat → Type u
+  | nil : Vector α 0
+  | cons : α → Vector α n → Vector α (n+1)
+
diff --git a/doc/examples/NFM2022/nfm8.lean b/doc/examples/NFM2022/nfm8.lean
index 78ecadc640..3dc105340a 100644
--- a/doc/examples/NFM2022/nfm8.lean
+++ b/doc/examples/NFM2022/nfm8.lean
@@ -1,3 +1,9 @@
+def ack : Nat → Nat → Nat
+  | 0,   y   => y+1
+  | x+1, 0   => ack x 1
+  | x+1, y+1 => ack x (ack (x+1) y)
+termination_by ack x y => (x, y)
+
 def sum (a : Array Int) : Int :=
   let rec go (i : Nat) :=
      if i < a.size then