From 89e1bc72ed32695d763b38623623eda8895583a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Nov 2022 17:02:28 -0800 Subject: [PATCH] doc: examples for Certora tutorial --- doc/examples/Certora2022/ex1.lean | 22 +++++++++++ doc/examples/Certora2022/ex10.lean | 19 ++++++++++ doc/examples/Certora2022/ex11.lean | 22 +++++++++++ doc/examples/Certora2022/ex12.lean | 28 ++++++++++++++ doc/examples/Certora2022/ex13.lean | 44 ++++++++++++++++++++++ doc/examples/Certora2022/ex14.lean | 31 ++++++++++++++++ doc/examples/Certora2022/ex15.lean | 19 ++++++++++ doc/examples/Certora2022/ex16.lean | 12 ++++++ doc/examples/Certora2022/ex17.lean | 19 ++++++++++ doc/examples/Certora2022/ex18.lean | 20 ++++++++++ doc/examples/Certora2022/ex19.lean | 10 +++++ doc/examples/Certora2022/ex2.lean | 14 +++++++ doc/examples/Certora2022/ex20.lean | 22 +++++++++++ doc/examples/Certora2022/ex21.lean | 21 +++++++++++ doc/examples/Certora2022/ex22.lean | 13 +++++++ doc/examples/Certora2022/ex23.lean | 26 +++++++++++++ doc/examples/Certora2022/ex24.lean | 9 +++++ doc/examples/Certora2022/ex3.lean | 59 ++++++++++++++++++++++++++++++ doc/examples/Certora2022/ex4.lean | 20 ++++++++++ doc/examples/Certora2022/ex5.lean | 21 +++++++++++ doc/examples/Certora2022/ex6.lean | 14 +++++++ doc/examples/Certora2022/ex7.lean | 25 +++++++++++++ doc/examples/Certora2022/ex8.lean | 25 +++++++++++++ doc/examples/Certora2022/ex9.lean | 44 ++++++++++++++++++++++ 24 files changed, 559 insertions(+) create mode 100644 doc/examples/Certora2022/ex1.lean create mode 100644 doc/examples/Certora2022/ex10.lean create mode 100644 doc/examples/Certora2022/ex11.lean create mode 100644 doc/examples/Certora2022/ex12.lean create mode 100644 doc/examples/Certora2022/ex13.lean create mode 100644 doc/examples/Certora2022/ex14.lean create mode 100644 doc/examples/Certora2022/ex15.lean create mode 100644 doc/examples/Certora2022/ex16.lean create mode 100644 doc/examples/Certora2022/ex17.lean create mode 100644 doc/examples/Certora2022/ex18.lean create mode 100644 doc/examples/Certora2022/ex19.lean create mode 100644 doc/examples/Certora2022/ex2.lean create mode 100644 doc/examples/Certora2022/ex20.lean create mode 100644 doc/examples/Certora2022/ex21.lean create mode 100644 doc/examples/Certora2022/ex22.lean create mode 100644 doc/examples/Certora2022/ex23.lean create mode 100644 doc/examples/Certora2022/ex24.lean create mode 100644 doc/examples/Certora2022/ex3.lean create mode 100644 doc/examples/Certora2022/ex4.lean create mode 100644 doc/examples/Certora2022/ex5.lean create mode 100644 doc/examples/Certora2022/ex6.lean create mode 100644 doc/examples/Certora2022/ex7.lean create mode 100644 doc/examples/Certora2022/ex8.lean create mode 100644 doc/examples/Certora2022/ex9.lean diff --git a/doc/examples/Certora2022/ex1.lean b/doc/examples/Certora2022/ex1.lean new file mode 100644 index 0000000000..539de041e8 --- /dev/null +++ b/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 + + diff --git a/doc/examples/Certora2022/ex10.lean b/doc/examples/Certora2022/ex10.lean new file mode 100644 index 0000000000..6f1dba630f --- /dev/null +++ b/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 + ... +-/ diff --git a/doc/examples/Certora2022/ex11.lean b/doc/examples/Certora2022/ex11.lean new file mode 100644 index 0000000000..183588ff90 --- /dev/null +++ b/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 + diff --git a/doc/examples/Certora2022/ex12.lean b/doc/examples/Certora2022/ex12.lean new file mode 100644 index 0000000000..0dd359f0db --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex13.lean b/doc/examples/Certora2022/ex13.lean new file mode 100644 index 0000000000..a78cd872f9 --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex14.lean b/doc/examples/Certora2022/ex14.lean new file mode 100644 index 0000000000..79569fddf6 --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex15.lean b/doc/examples/Certora2022/ex15.lean new file mode 100644 index 0000000000..46e493c70d --- /dev/null +++ b/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⟩ diff --git a/doc/examples/Certora2022/ex16.lean b/doc/examples/Certora2022/ex16.lean new file mode 100644 index 0000000000..333b3f8456 --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex17.lean b/doc/examples/Certora2022/ex17.lean new file mode 100644 index 0000000000..c64cc9bb97 --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex18.lean b/doc/examples/Certora2022/ex18.lean new file mode 100644 index 0000000000..e74262d2af --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex19.lean b/doc/examples/Certora2022/ex19.lean new file mode 100644 index 0000000000..2246d43632 --- /dev/null +++ b/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)) diff --git a/doc/examples/Certora2022/ex2.lean b/doc/examples/Certora2022/ex2.lean new file mode 100644 index 0000000000..591ba9920f --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex20.lean b/doc/examples/Certora2022/ex20.lean new file mode 100644 index 0000000000..391b31cbb5 --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex21.lean b/doc/examples/Certora2022/ex21.lean new file mode 100644 index 0000000000..37f6c5e565 --- /dev/null +++ b/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 [*] diff --git a/doc/examples/Certora2022/ex22.lean b/doc/examples/Certora2022/ex22.lean new file mode 100644 index 0000000000..762c52b037 --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex23.lean b/doc/examples/Certora2022/ex23.lean new file mode 100644 index 0000000000..f51a1d255f --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex24.lean b/doc/examples/Certora2022/ex24.lean new file mode 100644 index 0000000000..bd832421fb --- /dev/null +++ b/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! [*] diff --git a/doc/examples/Certora2022/ex3.lean b/doc/examples/Certora2022/ex3.lean new file mode 100644 index 0000000000..3db2507777 --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex4.lean b/doc/examples/Certora2022/ex4.lean new file mode 100644 index 0000000000..79bb5a8226 --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex5.lean b/doc/examples/Certora2022/ex5.lean new file mode 100644 index 0000000000..4ee42805ca --- /dev/null +++ b/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 diff --git a/doc/examples/Certora2022/ex6.lean b/doc/examples/Certora2022/ex6.lean new file mode 100644 index 0000000000..dfeecbaacd --- /dev/null +++ b/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) + diff --git a/doc/examples/Certora2022/ex7.lean b/doc/examples/Certora2022/ex7.lean new file mode 100644 index 0000000000..10370fbf42 --- /dev/null +++ b/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 +-/ diff --git a/doc/examples/Certora2022/ex8.lean b/doc/examples/Certora2022/ex8.lean new file mode 100644 index 0000000000..0e30270ac4 --- /dev/null +++ b/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 +-/ diff --git a/doc/examples/Certora2022/ex9.lean b/doc/examples/Certora2022/ex9.lean new file mode 100644 index 0000000000..85a4886975 --- /dev/null +++ b/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