doc: examples for Certora tutorial

doc/examples/Certora2022/ex1.lean

@@ -0,0 +1,22 @@
+/- "Hello world" -/
+
+#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/Certora2022/ex10.lean

@@ -0,0 +1,19 @@
+/- Dependent pattern matching -/
+
+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
+    ...
+-/

doc/examples/Certora2022/ex11.lean

@@ -0,0 +1,22 @@
+/- Structures -/
+
+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
+

doc/examples/Certora2022/ex12.lean

@@ -0,0 +1,28 @@
+/- Type classes -/
+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/Certora2022/ex13.lean

@@ -0,0 +1,44 @@
+/- Type classes are heavily used in Lean -/
+namespace Example
+
+class Mul (α : Type u) where
+  mul : α → α → α
+
+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 β
+
+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
+
+/-
+`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

doc/examples/Certora2022/ex14.lean

@@ -0,0 +1,31 @@
+/- Tactics -/
+
+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 hp; exact And.intro hq hp
+
+/- Structuring proofs -/
+
+example : p → q → p ∧ q ∧ p := by
+  intro hp hq
+  apply And.intro
+  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

doc/examples/Certora2022/ex15.lean

@@ -0,0 +1,19 @@
+/- intro tactic variants -/
+
+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 ⟨_, 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⟩

doc/examples/Certora2022/ex16.lean

@@ -0,0 +1,12 @@
+/- Inaccessible names -/
+
+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

doc/examples/Certora2022/ex17.lean

@@ -0,0 +1,19 @@
+/- More tactics -/
+
+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/Certora2022/ex18.lean

@@ -0,0 +1,20 @@
+/- Structuring proofs (cont.) -/
+
+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

doc/examples/Certora2022/ex19.lean

@@ -0,0 +1,10 @@
+/- Tactic combinators -/
+
+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/Certora2022/ex2.lean

@@ -0,0 +1,14 @@
+/- First-class functions -/
+
+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/Certora2022/ex20.lean

@@ -0,0 +1,22 @@
+/- 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
+
+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

doc/examples/Certora2022/ex21.lean

@@ -0,0 +1,21 @@
+/- Simplifier -/
+
+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 [*]

doc/examples/Certora2022/ex22.lean

@@ -0,0 +1,13 @@
+/- Simplifier -/
+
+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

doc/examples/Certora2022/ex23.lean

@@ -0,0 +1,26 @@
+/- split tactic -/
+
+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

doc/examples/Certora2022/ex24.lean

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

doc/examples/Certora2022/ex3.lean

@@ -0,0 +1,59 @@
+/- Enumerated types -/
+
+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
+
+/- Proving theorems using tactics -/
+
+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/Certora2022/ex4.lean

@@ -0,0 +1,20 @@
+/- What is the type of Nat? -/
+
+#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

doc/examples/Certora2022/ex5.lean

@@ -0,0 +1,21 @@
+/- Implicit arguments and universe polymorphism -/
+
+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/Certora2022/ex6.lean

@@ -0,0 +1,14 @@
+/- Inductive Types -/
+
+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)
+

doc/examples/Certora2022/ex7.lean

@@ -0,0 +1,25 @@
+/- Recursive functions -/
+
+#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/Certora2022/ex8.lean

@@ -0,0 +1,25 @@
+/- Well-founded recursion -/
+
+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
+        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/Certora2022/ex9.lean

@@ -0,0 +1,44 @@
+/- Mutual recursion -/
+
+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 recursion in theorems -/
+
+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