Logical Foundations

10. Automation: More Automation🔗

Up to now, we've used the manual part of Lean's tactic facilities. In this chapter, we'll learn more about some of Lean's powerful automation features, including tactic combinators like try and repeat, decision procedures like lia, and automatic simplification using simp. Using these features together with Lean's metaprogramming facilities will enable us to make some of our proofs startlingly short! Used properly, they can also make proofs more maintainable and robust to changes in underlying definitions.

Our motivating example will be the following proof, repeated with just a few small changes from the IndProp chapter. We will simplify this proof in several stages.

theorem Perm3_In_old (α : Type) (x : α) (l₁ l₂ : List α) (hPerm : Perm3 l₁ l₂) (hIn : x ∈ l₁) : x ∈ l₂ := α:Typex:αl₁:List αl₂:List αhPerm:Perm3 l₁ l₂hIn:x ∈ l₁⊢ x ∈ l₂ induction hPerm with α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x ∈ []⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = x✝ ∨ x = z✝ ∨ x ∈ []; α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = x✝; All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = y✝; All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = x✝ ∨ x = z✝ ∨ x ∈ []; α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = z✝ ∨ x ∈ []; α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = z✝; All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x ∈ []⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = x✝; All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = z✝ ∨ x = y✝ ∨ x ∈ []; α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = y✝ ∨ x ∈ []; α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = y✝; All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = z✝ ∨ x = y✝ ∨ x ∈ []; α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = z✝; All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝ih₁₂:x ∈ l₁✝ → x ∈ l₂✝ih₂₃:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝ih₁₂:x ∈ l₁✝ → x ∈ l₂✝ih₂₃:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₂✝; α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝ih₁₂:x ∈ l₁✝ → x ∈ l₂✝ih₂₃:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₁✝; All goals completed! 🐙

In this chapter, we will introduce tactics that will shrink this proof from around eighteen lines to one.

10.1. The lia Tactic🔗

The lia tactic implements a decision procedure for linear integer arithmetic: propositional formulas whose atoms are linear constraints over the natural numbers and integers. This is exactly the fragment of first-order logic (see the Logic chapter) obtained by restricting connectives and quantifiers to arithmetic building blocks.

If the goal is a universally quantified formula made out of

  • numeric constants, addition (+ and succ), subtraction (- and pred), and multiplication by constants,

  • equality (= and ≠) and ordering (≤ and <), and

  • the logical connectives ∧, ∨, ¬, and →,

then invoking lia will either solve the goal, or fail because the goal is actually false: within this fragment, lia is a complete decision procedure. lia reasons about the goal together with any hypotheses already in the local context: each hypothesis is used exactly as if it had been written into the goal as an antecedent with →.

Outside this fragment, lia can fail even when the goal is true — for example, on n * n ≥ n, which multiplies two variables together rather than a constant and a variable. Such a failure only means lia couldn't decide the goal, not that the goal is false. Note that, when failing, lia may mention another tactic, called grind. This is another, more powerful tactic that subsumes lia, but we will not use it here.

Anything in the goal or hypotheses that isn't built from these arithmetic pieces — including an arbitrary proposition like x ∈ l — lia simply treats as an opaque atom. So lia can also solve goals that are purely propositional, with no arithmetic in them at all, as long as the only way such atoms are combined is with ∧, ∨, ¬, and →.

example (m n o p : Nat) : m + n ≤ n + o ∧ o + 3 = p + 3 → m ≤ p := m:Natn:Nato:Natp:Nat⊢ m + n ≤ n + o ∧ o + 3 = p + 3 → m ≤ p All goals completed! 🐙 example (m n : Nat) : m + n = n + m := m:Natn:Nat⊢ m + n = n + m All goals completed! 🐙 example (m n p : Nat) : m + (n + p) = m + n + p := m:Natn:Natp:Nat⊢ m + (n + p) = m + n + p All goals completed! 🐙 example (a b c d : Prop) : (a → b) → (b → c) → (c → d) → (a → d) := a:Propb:Propc:Propd:Prop⊢ (a → b) → (b → c) → (c → d) → a → d All goals completed! 🐙 example (α : Type) (x : α) (l₁ l₂ l₃ : List α) (h₁ : x ∈ l₁ → x ∈ l₂) (h₂ : x ∈ l₂ → x ∈ l₃) : x ∈ l₁ → x ∈ l₃ := α:Typex:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ → x ∈ l₂h₂:x ∈ l₂ → x ∈ l₃⊢ x ∈ l₁ → x ∈ l₃ All goals completed! 🐙

The lia tactic can solve many of the cases of our old Perm3.In example.

theorem Perm3_In_better_with_lia (α : Type) (x : α) (l₁ l₂ : List α) (hPerm : Perm3 l₁ l₂) (hIn : x ∈ l₁) : x ∈ l₂ := α:Typex:αl₁:List αl₂:List αhPerm:Perm3 l₁ l₂hIn:x ∈ l₁⊢ x ∈ l₂ induction hPerm with α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x ∈ []⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] /- In addition to basic arithmetic, `lia` can also discharge goals that are simple facts about logic. -/ α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] All goals completed! 🐙 -- was right; left; assumption α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] All goals completed! 🐙 -- was left; assumption α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] All goals completed! 🐙 -- was right; right; left; assumption α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x ∈ []⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] All goals completed! 🐙 -- was contradiction α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ []α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = x✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] All goals completed! 🐙 -- was left; assumption α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = y✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] All goals completed! 🐙 -- was right; right; left; assumption α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x = z✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] All goals completed! 🐙 -- was right; right; assumption α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αh:x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] All goals completed! 🐙 -- was contradiction α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝ih₁₂:x ∈ l₁✝ → x ∈ l₂✝ih₂₃:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ All goals completed! 🐙 -- was apply ih₂₃; apply ih₁₂; apply hIn

10.2. Tactic Combinators🔗

In Induction, we saw how to use the <;> combinator in order to apply the same tactic to every subgoal in a proof. As a reminder, consider this example, where cases on b and c each leaves two subgoals that are discharged identically:

example (b c : Bool) : (b && c) = (c && b) := b:Boolc:Bool⊢ (b && c) = (c && b) c:Bool⊢ (false && c) = (c && false)c:Bool⊢ (true && c) = (c && true) c:Bool⊢ (false && c) = (c && false)c:Bool⊢ (true && c) = (c && true) ⊢ (true && false) = (false && true)⊢ (true && true) = (true && true) ⊢ (false && false) = (false && false)⊢ (false && true) = (true && false)⊢ (true && false) = (false && true)⊢ (true && true) = (true && true) All goals completed! 🐙

We can use this combinator to further simplify our Perm3 proof:

theorem Perm3_In_better_with_lia_semi (α : Type) (x : α) (l₁ l₂ : List α) (hPerm : Perm3 l₁ l₂) (hIn : x ∈ l₁) : x ∈ l₂ := α:Typex:αl₁:List αl₂:List αhPerm:Perm3 l₁ l₂hIn:x ∈ l₁⊢ x ∈ l₂ induction hPerm with α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = y✝ ∨ x = x✝ ∨ x = z✝ ∨ x ∈ [] All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝ih₁₂:x ∈ l₁✝ → x ∈ l₂✝ih₂₃:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ All goals completed! 🐙

The <;> is not the only combinator that Lean has to offer. In general, combinators allow us to build tactics out of smaller ones. Getting used to them takes a little energy, but it lets us scale up to more complex definitions and more interesting properties without drowning in boring, repetitive detail.

10.2.1. The try Combinator🔗

The first such combinator we'll discuss is try. If t is a tactic, then try t is a tactic that is just like t except that, if t fails, try t successfully does nothing at all (rather than failing).

example {a : Prop} (h : a) : a := a:Proph:a⊢ a try a:Proph:a⊢ a -- `rfl` would fail here, but `try` swallows it... All goals completed! 🐙 -- ...so we can still finish some other way. example : 1 = 1 := ⊢ 1 = 1 try All goals completed! 🐙 -- here `try rfl` just does `rfl`

There is not much reason to use try in completely manual proofs like these, but it is very useful together with the <;> combinator.

inductive Silly : Nat → Prop where | mk1 {n : Nat} (h : n > 1) : Silly n | mk2 {n : Nat} (h : 1 ∈ []) : Silly n | mk3 {n : Nat} (h : ∃ m, n = m + 2) : Silly n example {n : Nat} (h : Silly n) : n ≠ 1 := n:Nath:Silly n⊢ n ≠ 1 inversion h with | mk1 => All goals completed! 🐙 | mk2 => All goals completed! 🐙 | mk3 => All goals completed! 🐙

Here, we can use the lia tactic to close some of these goals, but not all of them. So, a more compact way to write this proof would be:

example {n} (h : Silly n) : n ≠ 1 := n:Nath:Silly n⊢ n ≠ 1 n:Nath✝:n > 1⊢ n ≠ 1n:Nath✝:1 ∈ []⊢ n ≠ 1n:Nath✝:∃ m, n = m + 2⊢ n ≠ 1 n:Nath✝:n > 1⊢ n ≠ 1n:Nath✝:1 ∈ []⊢ n ≠ 1n:Nath✝:∃ m, n = m + 2⊢ n ≠ 1 try All goals completed! 🐙 -- `lia` doesn't know that `1 ∈ []` is impossible, -- but we can use `contradiction` All goals completed! 🐙

We can further simplify our Perm3.In example with try.

theorem Perm3_In_better_with_try (α : Type) (x : α) (l₁ l₂ : List α) (hPerm : Perm3 l₁ l₂) (hIn : x ∈ l₁) : x ∈ l₂ := α:Typex:αl₁:List αl₂:List αhPerm:Perm3 l₁ l₂hIn:x ∈ l₁⊢ x ∈ l₂ induction hPerm with (try α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] All goals completed! 🐙) α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝h₁₂_ih✝:x ∈ l₁✝ → x ∈ l₂✝h₂₃_ih✝:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ All goals completed! 🐙

Note that try lia <;> try rw [...] <;> lia doesn't work because <;> short circuits. A failure in the first lia prevents the rest of the sequence from executing, meaning the try rw [...] never fires. (try lia <;> ... is parsed try (lia <;> (...)), and it's the outermost try that catches the failure in this case.) We'll see a solution to this problem further below.

example (α : Type) (x : α) (l₁ l₂ : List α) (hPerm : Perm3 l₁ l₂) (hIn : x ∈ l₁) : x ∈ l₂ := unsolved goals α:Typex:αl₁ l₂:List αx✝ y✝ z✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝] α:Typex:αl₁ l₂:List αx✝ y✝ z✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝]α:Typex:αl₁:List αl₂:List αhPerm:Perm3 l₁ l₂hIn:x ∈ l₁⊢ x ∈ l₂ α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝]α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝]α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝h₁₂_ih✝:x ∈ l₁✝ → x ∈ l₂✝h₂₃_ih✝:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝]α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝]α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝h₁₂_ih✝:x ∈ l₁✝ → x ∈ l₂✝h₂₃_ih✝:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ try All goals completed! 🐙 <;> try rw [List.mem_cons, List.mem_cons, List.mem_cons] at * <;> lia 
unsolved goals
α:Typex:αl₁ l₂:List αx✝ y✝ z✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝]

α:Typex:αl₁ l₂:List αx✝ y✝ z✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝]

10.2.2. The repeat Combinator🔗

The repeat combinator takes another tactic or parenthesized sequence of tactics and keeps applying it until it fails.

Here is an example proving that 10 is in a long list using repeat:

example : 10 ∈ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] := ⊢ 10 ∈ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] repeat ⊢ 10 = 10 ∨ 10 ∈ [] try ⊢ 10 = 10; All goals completed! 🐙 -- `try` makes this optional, which is necessary for the -- last repetition where `left; rfl` succeeds try ⊢ 10 ∈ [10]

The tactic repeat t never fails: if the tactic t doesn't apply to the original goal, then repeat t succeeds without changing the goal at all (i.e., it repeats zero times).

example : 10 ∈ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] := ⊢ 10 ∈ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] -- this is a no-op repeat All goals completed! 🐙 repeat ⊢ 10 = 10 ∨ 10 ∈ [] try ⊢ 10 = 10; All goals completed! 🐙 try ⊢ 10 ∈ [10]

The tactic repeat t does not have any upper bound on the number of times it applies t. If t is a tactic that always succeeds (and makes progress), then repeat t will loop forever.

example (m n : Nat) : m + n = n + m := unsolved goals m n:Nat⊢ m + n = n + mby /- Uncomment the next line to see the infinite loop occur. You will then need to recomment it to make Lean listen to you again. -/ -- repeat rewrite [Nat.add_comm]

Wait — did we just write an infinite loop in Lean?!?!

Sort of.

While evaluation in Lean's term language is guaranteed to terminate, tactic evaluation is not. This does not affect Lean's logical consistency, however, since the job of repeat and other tactics is to guide Lean in constructing proofs; if the construction process diverges (i.e., it does not terminate), this simply means that we have failed to construct a proof at all, not that we have constructed a bad proof.

10.2.3. The first Combinator🔗

The first combinator takes a sequence of tactics and tries them in order, stopping after the first success. As a silly example:

example (n m : Nat) : n * (m + 1) = n * m + n := n:Natm:Nat⊢ n * (m + 1) = n * m + n first | All goals completed! 🐙 | left | lia | induction n

Neither rfl nor left succeeds on this goal, but lia does, so first stops after lia and never tries induction. As with try, first is most useful in combination with other combinators. For example, we can rewrite our previous examples that used repeat and try like so:

example : 10 ∈ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] := ⊢ 10 ∈ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] repeat first | All goals completed! 🐙 | ⊢ 10 ∈ [10]

The first tactic here will attempt to close the goal with an application of List.mem_cons_self, if it can, and otherwise apply List.mem_cons_of_mem to proceed to checking the next element in the list. Note that the order here is important! If we had instead written:

example : 10 ∈ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] := unsolved goals ⊢ 10 ∈ []⊢ 10 ∈ [1, 2, 3, 4, 5, 6, 7, 8, 9, 10] repeat first | ⊢ 10 ∈ [] | ⊢ 10 ∈ [] -- unprovable state!

Here, when we reach the goal 10 ∈ [10], instead of closing the goal with List.mem_cons_self like before, we would instead first try apply List.mem_cons_of_mem, which would also succeed. This leaves us with the goal 10 ∈ [], which is of course false.

With first, we can solve the earlier issue with try where it would stop executing the sequence on the first failure.

theorem Perm3_In_better_with_first (α : Type) (x : α) (l₁ l₂ : List α) (hPerm : Perm3 l₁ l₂) (hIn : x ∈ l₁) : x ∈ l₂ := α:Typex:αl₁:List αl₂:List αhPerm:Perm3 l₁ l₂hIn:x ∈ l₁⊢ x ∈ l₂ α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝]α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝]α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝h₁₂_ih✝:x ∈ l₁✝ → x ∈ l₂✝h₂₃_ih✝:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝]α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝]α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝h₁₂_ih✝:x ∈ l₁✝ → x ∈ l₂✝h₂₃_ih✝:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ first | α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝h₁₂_ih✝:x ∈ l₁✝ → x ∈ l₂✝h₂₃_ih✝:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝ ∨ x ∈ []⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ ∨ x ∈ [] All goals completed! 🐙 | All goals completed! 🐙

Our Perm3.In example is now quite short! Can we still do better?

10.3. The simp Tactic🔗

The simp tactic is Lean's simplifier. It is one of the most powerful tools in the language, and it is used heavily in real Lean developments.

The tactic simplifies the target (the goal and/or one or more hypotheses) by repeatedly rewriting it using a set of lemmas. At each step it tries every lemma in its available set the way first would, applies whichever one matches via rw, and repeats until no lemma applies anywhere. Like repeat, it fails outright if it never manages to apply a rewrite ("simp made no progress"), rather than succeeding as a no-op the way try simp would.

The simp tactic's available set of lemmas begins with a default set and can be extended to include theorems labeled @[simp]. Indeed, the characterizing lemmas we've been writing for our definitions all throughout this book are examples of these simplification lemmas, or simp lemmas as they're called by Lean programmers, only we have refrained from annotating them as such (until now!).

namespace simp_lemmas_example /- `add_zero` and `add_succ` are the `simp` lemmas for `+`. -/ @[simp] theorem add_zero (n : Nat) : n + 0 = n := n:Nat⊢ n + 0 = n All goals completed! 🐙 @[simp] theorem add_succ (n m : Nat) : n + (m + 1) = (n + m) + 1 := n:Natm:Nat⊢ n + (m + 1) = n + m + 1 All goals completed! 🐙

Instead of manually rewriting by the characterizing lemmas in the example below, simp does it automatically.

theorem add_succ_nested (n m : Nat) : n + (m + 1 + 1) = (n + m + 1) + 1 := n:Natm:Nat⊢ n + (m + 1 + 1) = n + m + 1 + 1 All goals completed! 🐙

The other way to extend simp's set of available lemmas is to list them explicitly, by writing simp [<theorems>]. If you want simp to only use those, you can use simp only [<theorems>]. As with rw, you can also supply a definition to simp to simplify using that definition.

theorem add_succ_nested_2 (n m : Nat) : n + (m + 1 + 1) = (n + m + 1) + 1 := n:Natm:Nat⊢ n + (m + 1 + 1) = n + m + 1 + 1 All goals completed! 🐙

If you want to know what simp is doing, you can run simp?.

theorem add_succ_nested_3 (n m : Nat) : n + (m + 1 + 1) = (n + m + 1) + 1 := n:Natm:Nat⊢ n + (m + 1 + 1) = n + m + 1 + 1 Try this: [apply] simp only [add_succ, Nat.add_zero, Nat.add_left_cancel_iff]All goals completed! 🐙 end simp_lemmas_example

In the InfoView, you will see

Try this:
  [apply] simp only [add_succ, Nat.add_zero, Nat.add_left_cancel_iff]

Click the [apply] button to replace simp? with the suggested replacement. You should always do this for your final proof scripts, just as was recommended for rw? and exact? in the UsingLean chapter.

Interestingly, we can see for this example that simp used the Nat version of add_zero, not our own, added above, and also pulled in Nat.add_left_cancel_iff, which is not strictly needed. But the combination works, even if it is not minimal.

As with apply and rw, simp can also simplify hypotheses — invoking simp as simp [<lemmas>] at h runs the simplifier at hypothesis h.

example α x (l₁ l₂ l₃ : List α) (h₁ : x ∈ l₁ ++ l₂) (Variable name `h₂` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _h₂ Note: This linter can be disabled with `set_option linter.unusedVariables false`h₂ : x ∈ l₂ ++ l₃) : x ∈ l₁ ++ l₃ ∨ x ∈ l₂ := α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ++ l₂h₂:x ∈ l₂ ++ l₃⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂ α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ++ l₃h₁:x ∈ l₁ ∨ x ∈ l₂⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂; α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ∨ x ∈ l₂h₂:x ∈ l₂ ∨ x ∈ l₃⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂; α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ∨ x ∈ l₂h₂:x ∈ l₂ ∨ x ∈ l₃⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂; All goals completed! 🐙

We could equally well have written

example α x (l₁ l₂ l₃ : List α) (h₁ : x ∈ l₁ ++ l₂) (Variable name `h₂` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _h₂ Note: This linter can be disabled with `set_option linter.unusedVariables false`h₂ : x ∈ l₂ ++ l₃) : x ∈ l₁ ++ l₃ ∨ x ∈ l₂ := α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ++ l₂h₂:x ∈ l₂ ++ l₃⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂ α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ∨ x ∈ l₂h₂:x ∈ l₂ ∨ x ∈ l₃⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂; All goals completed! 🐙

If we want to mutually simplify everywhere, we can use simp_all, which simplifies in all hypotheses and in the goal at the same time. The tactic simp_all is not the same as simp at *. The latter simplifies each target independently, whereas simp_all additionally lets the (simplified) hypotheses simplify each other and the goal, iterating to a joint fixpoint.

Here's an example that illustrates the difference:

example (a b : Nat) (h1 : a = 0) (h2 : a + b = 5) : b = 5 := a:Natb:Nath1:a = 0h2:a + b = 5⊢ b = 5 `simp` made no progressa:Natb:Nath1:a = 0h2:a + b = 5⊢ b = 5

This fails with:

`simp` made no progress

But simp_all closes the goal:

example (a b : Nat) (h1 : a = 0) (h2 : a + b = 5) : b = 5 := a:Natb:Nath1:a = 0h2:a + b = 5⊢ b = 5 All goals completed! 🐙

We can dramatically simplify our Perm3_In_shortest theorem using simp_all:

theorem Perm3_In_shortest (α : Type) (x : α) (l₁ l₂ : List α) (hPerm : Perm3 l₁ l₂) (hIn : x ∈ l₁) : x ∈ l₂ := α:Typex:αl₁:List αl₂:List αhPerm:Perm3 l₁ l₂hIn:x ∈ l₁⊢ x ∈ l₂ α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝]α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝]α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝h₁₂_ih✝:x ∈ l₁✝ → x ∈ l₂✝h₂₃_ih✝:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [y✝, x✝, z✝]α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x ∈ [x✝, y✝, z✝]⊢ x ∈ [x✝, z✝, y✝]α:Typex:αl₁:List αl₂:List αl₁✝:List αl₂✝:List αl₃✝:List αh₁₂✝:Perm3 l₁✝ l₂✝h₂₃✝:Perm3 l₂✝ l₃✝h₁₂_ih✝:x ∈ l₁✝ → x ∈ l₂✝h₂₃_ih✝:x ∈ l₂✝ → x ∈ l₃✝hIn:x ∈ l₁✝⊢ x ∈ l₃✝ All goals completed! 🐙 α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝⊢ x = y✝ ∨ x = x✝ ∨ x = z✝α:Typex:αl₁:List αl₂:List αx✝:αy✝:αz✝:αhIn:x = x✝ ∨ x = y✝ ∨ x = z✝⊢ x = x✝ ∨ x = z✝ ∨ x = y✝ All goals completed! 🐙

10.3.1. Idiomatic simp Usage🔗

Because simp is such a powerful tactic, the Lean community has developed a number of conventions surrounding appropriate usage. One such convention is around terminal simp usage.

A call to simp is considered terminal either when it is the last tactic used to close a goal or when it is followed only by other automatic (also called "flexible") tactics like simp or lia. In idiomatic Lean, all nonterminal uses of simp should use the only qualifier and specify exactly which lemmas are being used to simplify. Use of simp without only should only occur in terminal positions.

In our example from before, the use of simp is terminal (and therefore okay) because it is followed only by other simps and lia:

example α x (l₁ l₂ l₃ : List α) (h₁ : x ∈ l₁ ++ l₂) (Variable name `h₂` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _h₂ Note: This linter can be disabled with `set_option linter.unusedVariables false`h₂ : x ∈ l₂ ++ l₃) : x ∈ l₁ ++ l₃ ∨ x ∈ l₂ := α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ++ l₂h₂:x ∈ l₂ ++ l₃⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂ α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ++ l₃h₁:x ∈ l₁ ∨ x ∈ l₂⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂; α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ∨ x ∈ l₂h₂:x ∈ l₂ ∨ x ∈ l₃⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂; α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ∨ x ∈ l₂h₂:x ∈ l₂ ∨ x ∈ l₃⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂; All goals completed! 🐙

On the other hand, if we instead decline to use lia and solve the goal manually, this example uses simp in a nonterminal position and is considered poor style:

example α x (l₁ l₂ l₃ : List α) (h₁ : x ∈ l₁ ++ l₂) (Variable name `h₂` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _h₂ Note: This linter can be disabled with `set_option linter.unusedVariables false`h₂ : x ∈ l₂ ++ l₃) : x ∈ l₁ ++ l₃ ∨ x ∈ l₂ := α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ++ l₂h₂:x ∈ l₂ ++ l₃⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂ α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ++ l₃h₁:x ∈ l₁ ∨ x ∈ l₂⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂; α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ∨ x ∈ l₂h₂:x ∈ l₂ ∨ x ∈ l₃⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂; α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ∨ x ∈ l₂h₂:x ∈ l₂ ∨ x ∈ l₃⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂ cases h₁ with α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₁⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂ α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₁⊢ x ∈ l₁ ∨ x ∈ l₃; α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₁⊢ x ∈ l₁; All goals completed! 🐙 α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₂⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂ α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₂⊢ x ∈ l₂; All goals completed! 🐙

Using simp this way is brittle because if we add new simp lemmas to our library, this can change the way that our hypotheses and goals are simplified. Because our proof after the simps relies on the precise structure of the goals and hypotheses, these changes could cause the proof to break as the structure of the development evolves.

We can fix the style of this proof by changing the simps to specify which theorems they are using to simplify:

example α x (l₁ l₂ l₃ : List α) (h₁ : x ∈ l₁ ++ l₂) (Variable name `h₂` is not explicitly referenced. Hint: The binding can be removed (if unused) or named `_` (if used implicitly). Alternatively, prefix the name with `_` to silence this warning: [apply] _h₂ Note: This linter can be disabled with `set_option linter.unusedVariables false`h₂ : x ∈ l₂ ++ l₃) : x ∈ l₁ ++ l₃ ∨ x ∈ l₂ := α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ++ l₂h₂:x ∈ l₂ ++ l₃⊢ x ∈ l₁ ++ l₃ ∨ x ∈ l₂ -- the * here targets all hypotheses and the goal α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₁:x ∈ l₁ ∨ x ∈ l₂h₂:x ∈ l₂ ∨ x ∈ l₃⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂ cases h₁ with α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₁⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂ α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₁⊢ x ∈ l₁ ∨ x ∈ l₃; α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₁⊢ x ∈ l₁; All goals completed! 🐙 α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₂⊢ (x ∈ l₁ ∨ x ∈ l₃) ∨ x ∈ l₂ α:Type u_1x:αl₁:List αl₂:List αl₃:List αh₂:x ∈ l₂ ∨ x ∈ l₃h:x ∈ l₂⊢ x ∈ l₂; All goals completed! 🐙

This usage of simp only is better because the addition of new simp lemmas won't cause this proof to change.

Another rule around proper simp usage applies to the appropriate definition of simp lemmas.

All of the theorems marked with the @[simp] attribute in a Lean library compose the simp set for that library, and the result of simplifying an expression iteratively using all of the theorems in the simp set is the simp normal form of that expression.

It's important for the stability of proofs using simp that all the theorems in the simp set progress towards this normal form. Accordingly, library designers often first consider what they want that normal form to look like, and then structure their theorem definitions accordingly. As a simple example, the simp normal form for lists prefers to use the ++ notation instead of List.append, so there is a simp theorem List.append_eq whose type is List.append_eq {α : Type u} {as bs : List α} : as.append bs = as ++ bs.

In this case, the simp normal form appears on the right, while the expression in need of simplification appears on the left. We can thus think of this theorem as simplifying from left to right. Not every simp lemma in the standard library has a simp normal form on its right-hand side, but all make progress towards simp normal form when applied.

For our purposes, in this textbook and in later ones, we will take care to define our simp lemmas such that they respect this left-to-right simplification behavior.

10.4. The trivial Tactic🔗

A final automated tactic to have in your toolkit is trivial, which tries a number of different simple tactics (such as rfl or contradiction) to close the current goal. Some examples:

example : 1 = 1 := ⊢ 1 = 1 All goals completed! 🐙 example : (1, 2).fst = 1 := ⊢ (1, 2).fst = 1 All goals completed! 🐙 example (a b : Prop) : ¬ a → a → b := a:Propb:Prop⊢ ¬a → a → b a:Propb:Proph₁:¬ah₂:a⊢ b; All goals completed! 🐙

10.5. Case Study: Regular Expressions🔗

As a culminating exercise for this chapter and as practice using the automation techniques we discussed above on a real proof, we examine the theory of regular expressions, eventually working up to a proof of the pumping lemma.

10.5.1. Definitions🔗

Regular expressions are a formal language for describing sets of strings. Their syntax is defined as follows:

inductive RegExp (α : Type) : Type where | EmptySet | EmptyStr | Char (c : α) | App (r1 r2 : RegExp α) | Union (r1 r2 : RegExp α) | Star (r : RegExp α) deriving BEq, DecidableEq, Repr -- prevents printing dot-chained, method-call-style like r1.App r2 attribute [pp_nodot] RegExp.Char RegExp.App RegExp.Union RegExp.Star namespace RegExp

Note that this definition is polymorphic: regular expressions in RegExp α describe strings with characters drawn from α — which in this exercise we represent as lists with elements from α.

(Technical aside: we depart slightly from standard practice in that we do not require the type α to be finite. This results in a somewhat different theory of regular expressions, but the difference is not significant for present purposes.)

We connect regular expressions and strings by defining when a regular expression matches some string.

Informally, this looks as follows:

  • The regular expression EmptySet does not match any string.

  • EmptyStr matches the empty string [].

  • Char x matches the one-character string [x].

  • If re₁ matches s₁, and re₂ matches s₂, then App re₁ re₂ matches s₁ ++ s₂.

  • If at least one of re₁ and re₂ matches s, then Union re₁ re₂ matches s.

  • Finally, if we can write some string s as the concatenation of a sequence of strings s = s₁ ++ ... ++ sₖ, and the expression re matches each one of the strings sᵢ, then Star re matches s.

    In particular, the sequence of strings may be empty, so Star re always matches the empty string [] no matter what re is.

We can easily translate this intuition into a set of rules, where we write s =~ re to say that re matches s:

        ─────────────── (mEmpty)
        [] =~ EmptyStr

        ─────────────── (mChar)
        [x] =~ (Char x)

    s₁ =~ re₁     s₂ =~ re₂
  ─────────────────────────── (mApp)
  (s₁ ++ s₂) =~ (App re₁ re₂)

           s₁ =~ re₁
    ───────────────────── (mUnionL)
    s₁ =~ (Union re₁ re₂)

           s₂ =~ re₂
    ───────────────────── (mUnionR)
    s₂ =~ (Union re₁ re₂)

      ──────────────── (mStar0)
      [] =~ (Star re)

s₁ =~ re     s₂ =~ (Star re)
──────────────────────────── (mStarApp)
  (s₁ ++ s₂) =~ (Star re)

This directly corresponds to the following inductive definition:

inductive ExpMatch {α : Type} : List α → RegExp α → Prop where | mEmpty : ExpMatch [] EmptyStr | mChar (c : α) : ExpMatch [c] (Char c) | mApp (s₁ s₂ : List α) {re₁ re₂ : RegExp α} (h₁ : ExpMatch s₁ re₁) (h₂ : ExpMatch s₂ re₂) : ExpMatch (s₁ ++ s₂) (App re₁ re₂) | mUnionL (s₁ : List α) {re₁ re₂ : RegExp α} (h₁ : ExpMatch s₁ re₁) : ExpMatch s₁ (Union re₁ re₂) | mUnionR (s₂ : List α) {re₁ re₂ : RegExp α} (h₂ : ExpMatch s₂ re₂) : ExpMatch s₂ (Union re₁ re₂) | mStar0 (re : RegExp α) : ExpMatch [] (Star re) | mStarApp (s₁ s₂ : List α) {re : RegExp α} (h₁ : ExpMatch s₁ re) (h₂ : ExpMatch s₂ (Star re)) : ExpMatch (s₁ ++ s₂) (Star re) open ExpMatch infix:40 " =~ " => ExpMatch
Quiz

Notice that this clause in our informal definition...

"The expression EmptySet does not match any string."

... is not explicitly reflected in the above definition. Do we need to add something?

(A) Yes, we should add a rule for this.

(B) No, one of the other rules already covers this case.

(C) No, the lack of a rule actually gives us the behavior we want.

Show solution
example α (s: List α) : ¬ (s =~ EmptySet) := α:Types:List α⊢ ¬s =~ EmptySet α:Types:List αcontra:s =~ EmptySet⊢ False; All goals completed! 🐙

Notice that these rules are not quite the same as the intuition that we gave at the beginning of the section. First, we don't need to include a rule explicitly stating that no string is matched by EmptySet; indeed, the syntax of inductive definitions doesn't even allow us to give such a "negative rule." We just don't happen to include any rule that would have the effect of EmptySet matching some string.

Second, the intuition we gave for Union and Star corresponds to two constructors each: mUnionL / mUnionR, and mStar0 / mStarApp. The result is logically equivalent to the original intuition but more convenient to use in Lean, since the recursive occurrences of ExpMatch are given as direct arguments to the constructors, making it easier to perform induction on evidence. (The exercises below ask you to prove that the constructors given in the inductive declaration and the ones that would arise from a more literal transcription of the intuition are indeed equivalent.)

Let's illustrate these rules with a few examples.

10.5.2. Examples🔗

example : [1] =~ Char 1 := ⊢ [1] =~ Char 1 All goals completed! 🐙 example : [1, 2] =~ App (Char 1) (Char 2) := ⊢ [1, 2] =~ App (Char 1) (Char 2) ⊢ [1] =~ Char 1⊢ [2] =~ Char 2 ⊢ [1] =~ Char 1⊢ [2] =~ Char 2 All goals completed! 🐙

Notice how the last example applies mApp to the string [1] directly. Since the goal mentions [1, 2] instead of [1] ++ [2], Lean wouldn't be able to figure out how to split the string on its own.

Using inversion, we can also show that certain strings do not match a regular expression:

example : ¬([1, 2] =~ Char 1) := ⊢ ¬[1, 2] =~ Char 1 contra:[1, 2] =~ Char 1⊢ False; All goals completed! 🐙

We can define helper functions for writing down regular expressions. The reg_exp_of_list function constructs a regular expression that matches exactly the string that it receives as an argument:

def reg_exp_of_list {α} (l : List α) := match l with | [] => EmptyStr | x :: l' => App (Char x) (reg_exp_of_list l') example : [1, 2, 3] =~ reg_exp_of_list [1, 2, 3] := ⊢ [1, 2, 3] =~ reg_exp_of_list [1, 2, 3] ⊢ [1] =~ Char 1⊢ [2, 3] =~ reg_exp_of_list [2, 3]; ⊢ [2, 3] =~ reg_exp_of_list [2, 3] ⊢ [2] =~ Char 2⊢ [3] =~ reg_exp_of_list [3]; ⊢ [3] =~ reg_exp_of_list [3] ⊢ [3] =~ Char 3⊢ [] =~ reg_exp_of_list []; ⊢ [] =~ reg_exp_of_list [] All goals completed! 🐙
Exercise★(regexp_match_of_list)

As a quick exercise, prove that every list matches reg_exp_of_list of itself:

theorem declaration uses `sorry`regexp_match_of_list α (l : List α) : l =~ reg_exp_of_list l := α:Typel:List α⊢ l =~ reg_exp_of_list l All goals completed! 🐙

We can also prove general facts about ExpMatch. For instance, the following lemma shows that every string s matched by re is also matched by Star re.

theorem MStar1 α s (re : RegExp α) (h : s =~ re) : s =~ Star re := α:Types:List αre:RegExp αh:s =~ re⊢ s =~ Star re α:Types:List αre:RegExp αh:s =~ re⊢ s ++ [] =~ Star re α:Types:List αre:RegExp αh:s =~ re⊢ s =~ reα:Types:List αre:RegExp αh:s =~ re⊢ [] =~ Star re α:Types:List αre:RegExp αh:s =~ re⊢ s =~ re All goals completed! 🐙 α:Types:List αre:RegExp αh:s =~ re⊢ [] =~ Star re All goals completed! 🐙

(Note the use of List.append_nil to change the goal of the theorem to exactly the shape expected by mStarApp.)

The following lemmas show that the intuition about matching given at the beginning of the section can be obtained from the formal inductive definition.

Exercise★(EmptySet_is_empty)
theorem declaration uses `sorry`EmptySet_is_empty α (s : List α) : ¬(s =~ EmptySet) := α:Types:List α⊢ ¬s =~ EmptySet All goals completed! 🐙
Exercise★(MUnion')
theorem declaration uses `sorry`MUnion' α (s : List α) (re₁ re₂ : RegExp α) : s =~ re₁ ∨ s =~ re₂ → s =~ Union re₁ re₂ := α:Types:List αre₁:RegExp αre₂:RegExp α⊢ s =~ re₁ ∨ s =~ re₂ → s =~ Union re₁ re₂ All goals completed! 🐙

The next lemma is stated in terms of the List.foldr function on lists: if ss : List (List α) represents a sequence of strings s₁, ..., sₙ, then List.foldr (· ++ ·) [] ss is the result of concatenating them all together.

Exercise★★(MStar')
theorem declaration uses `sorry`MStar' α (ss : List (List α)) (re : RegExp α) (h : ∀ s, s ∈ ss → s =~ re) : ss.foldr (· ++ ·) [] =~ Star re := α:Typess:List (List α)re:RegExp αh:∀ (s : List α), s ∈ ss → s =~ re⊢ List.foldr (fun x1 x2 => x1 ++ x2) [] ss =~ Star re All goals completed! 🐙
Exercise★(EmptyStr_not_needed) (Optional, Manually graded)

It turns out that the EmptyStr constructor is actually not needed, since the regular expression matching the empty string can also be defined from Star and EmptySet:

def EmptyStr' {α : Type} := @Star α (EmptySet)

State and prove that this EmptyStr' definition matches exactly the same strings as the EmptyStr constructor.

Since the definition of ExpMatch has a recursive structure, we might expect that proofs involving regular expressions will often require induction on evidence.

For example, suppose we want to prove the following intuitive fact: if a string s is matched by a regular expression re, then all elements of s must occur as character literals somewhere in re.

To state this as a theorem, we first define a function reChars that lists all characters that occur in a regular expression:

def reChars {α : Type} (re : RegExp α) : List α := match re with | EmptySet => [] | EmptyStr => [] | Char x => [x] | App re₁ re₂ => reChars re₁ ++ reChars re₂ | Union re₁ re₂ => reChars re₁ ++ reChars re₂ | Star re => reChars re

Now, the main theorem:

theorem in_re_match {α : Type} {s : List α} {re : RegExp α} {x : α} (hmatch : s =~ re) (hin : x ∈ s) : x ∈ reChars re := α:Types:List αre:RegExp αx:αhmatch:s =~ rehin:x ∈ s⊢ x ∈ re.reChars induction hmatch with α:Types:List αre:RegExp αx:αhin:x ∈ []⊢ x ∈ EmptyStr.reChars All goals completed! 🐙 α:Types:List αre:RegExp αx:αc:αhin:x ∈ [c]⊢ x ∈ (Char c).reChars α:Types:List αre:RegExp αx:αc:αhin:x ∈ [c]⊢ x ∈ [c]; All goals completed! 🐙 α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝ih₁:x ∈ s₁✝ → x ∈ re₁✝.reCharsih₂:x ∈ s₂✝ → x ∈ re₂✝.reCharshin:x ∈ s₁✝ ++ s₂✝⊢ x ∈ (App re₁✝ re₂✝).reChars /- Something interesting happens in the `mApp` case. We obtain _two_ induction hypotheses: one that applies when `x` occurs in `s₁` (which is matched by `re₁`), and a second one that applies when `x` occurs in `s₂` (matched by `re₂`). -/ α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝ih₁:x ∈ s₁✝ → x ∈ re₁✝.reCharsih₂:x ∈ s₂✝ → x ∈ re₂✝.reCharshin:x ∈ s₁✝ ∨ x ∈ s₂✝⊢ x ∈ re₁✝.reChars ∨ x ∈ re₂✝.reChars cases hin with α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝ih₁:x ∈ s₁✝ → x ∈ re₁✝.reCharsih₂:x ∈ s₂✝ → x ∈ re₂✝.reCharshin₁:x ∈ s₁✝⊢ x ∈ re₁✝.reChars ∨ x ∈ re₂✝.reChars α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝ih₁:x ∈ s₁✝ → x ∈ re₁✝.reCharsih₂:x ∈ s₂✝ → x ∈ re₂✝.reCharshin₁:x ∈ s₁✝⊢ x ∈ re₁✝.reChars; All goals completed! 🐙 α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝ih₁:x ∈ s₁✝ → x ∈ re₁✝.reCharsih₂:x ∈ s₂✝ → x ∈ re₂✝.reCharshin₂:x ∈ s₂✝⊢ x ∈ re₁✝.reChars ∨ x ∈ re₂✝.reChars α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝ih₁:x ∈ s₁✝ → x ∈ re₁✝.reCharsih₂:x ∈ s₂✝ → x ∈ re₂✝.reCharshin₂:x ∈ s₂✝⊢ x ∈ re₂✝.reChars; All goals completed! 🐙 α:Types:List αre:RegExp αx:αs₁✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝ih:x ∈ s₁✝ → x ∈ re₁✝.reCharshin:x ∈ s₁✝⊢ x ∈ (Union re₁✝ re₂✝).reChars α:Types:List αre:RegExp αx:αs₁✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝ih:x ∈ s₁✝ → x ∈ re₁✝.reCharshin:x ∈ s₁✝⊢ x ∈ re₁✝.reChars ∨ x ∈ re₂✝.reChars; α:Types:List αre:RegExp αx:αs₁✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝ih:x ∈ s₁✝ → x ∈ re₁✝.reCharshin:x ∈ s₁✝⊢ x ∈ re₁✝.reChars; All goals completed! 🐙 α:Types:List αre:RegExp αx:αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₂✝:s₂✝ =~ re₂✝ih:x ∈ s₂✝ → x ∈ re₂✝.reCharshin:x ∈ s₂✝⊢ x ∈ (Union re₁✝ re₂✝).reChars α:Types:List αre:RegExp αx:αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₂✝:s₂✝ =~ re₂✝ih:x ∈ s₂✝ → x ∈ re₂✝.reCharshin:x ∈ s₂✝⊢ x ∈ re₁✝.reChars ∨ x ∈ re₂✝.reChars; α:Types:List αre:RegExp αx:αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₂✝:s₂✝ =~ re₂✝ih:x ∈ s₂✝ → x ∈ re₂✝.reCharshin:x ∈ s₂✝⊢ x ∈ re₂✝.reChars; All goals completed! 🐙 α:Types:List αre:RegExp αx:αre✝:RegExp αhin:x ∈ []⊢ x ∈ (Star re✝).reChars All goals completed! 🐙 α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝ih₁:x ∈ s₁✝ → x ∈ re✝.reCharsih₂:x ∈ s₂✝ → x ∈ (Star re✝).reCharshin:x ∈ s₁✝ ++ s₂✝⊢ x ∈ (Star re✝).reChars /- Here again we get two induction hypotheses, and they illustrate why we need induction on evidence for `ExpMatch`, rather than induction on the regular expression `re`: the latter would only provide an induction hypothesis for strings that match `re`, which would not allow us to reason about the case `x ∈ s₂`. -/ α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝ih₁:x ∈ s₁✝ → x ∈ re✝.reCharsih₂:x ∈ s₂✝ → x ∈ (Star re✝).reCharshin:x ∈ s₁✝ ∨ x ∈ s₂✝⊢ x ∈ (Star re✝).reChars cases hin with α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝ih₁:x ∈ s₁✝ → x ∈ re✝.reCharsih₂:x ∈ s₂✝ → x ∈ (Star re✝).reCharshin₁:x ∈ s₁✝⊢ x ∈ (Star re✝).reChars All goals completed! 🐙 α:Types:List αre:RegExp αx:αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝ih₁:x ∈ s₁✝ → x ∈ re✝.reCharsih₂:x ∈ s₂✝ → x ∈ (Star re✝).reCharshin₂:x ∈ s₂✝⊢ x ∈ (Star re✝).reChars All goals completed! 🐙
Exercise★(reNotEmpty) (Manually graded)

Write a recursive function reNotEmpty that tests whether a regular expression matches some string. Prove that your function is correct.

10.5.3. The generalize Tactic🔗

One potentially confusing feature of the induction tactic is that it won't let you perform an induction over a term that isn't sufficiently general. Here's an example:

example (α : Type) (s₁ s₂ : List α) (re : RegExp α) : s₁ =~ Star re → s₂ =~ Star re → s₁ ++ s₂ =~ Star re := α:Types₁:List αs₂:List αre:RegExp α⊢ s₁ =~ Star re → s₂ =~ Star re → s₁ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ Star re⊢ s₂ =~ Star re → s₁ ++ s₂ =~ Star re /- Now, just doing an `inversion` on `h₁` won't get us very far in the recursive cases. (Try it!) So we need induction (on evidence). We might try this, but Lean won't let us: -/ Invalid target: Index in target's type is not a variable (consider using the `cases` tactic instead) Star reα:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ Star re⊢ s₂ =~ Star re → s₁ ++ s₂ =~ Star re 
Invalid target: Index in target's type is not a variable (consider using the `cases` tactic instead)
  Star re

The problem here is that induction over a Prop hypothesis only works properly with hypotheses that are "fully general," i.e., ones in which all the arguments are just variables, as opposed to more specific expressions like Star re.

A possible, but awkward, way to solve this problem is "manually generalizing" over the problematic expressions by adding explicit equality hypotheses to the lemma:

example α (s₁ s₂ : List α) (re re' : RegExp α) : re' = Star re → s₁ =~ re' → s₂ =~ Star re → s₁ ++ s₂ =~ Star re := unsolved goals α:Types₁ s₂:List αre re':RegExp αh₃:s₂ =~ Star reh₁:EmptyStr = Star re⊢ [] ++ s₂ =~ Star re α:Types₁ s₂:List αre re':RegExp αh₃:s₂ =~ Star rec✝:αh₁:Char c✝ = Star re⊢ [c✝] ++ s₂ =~ Star re α:Types₁ s₂:List αre re':RegExp αh₃:s₂ =~ Star res₁✝ s₂✝:List αre₁✝ re₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝h₁_ih✝:re₁✝ = Star re → s₁✝ ++ s₂ =~ Star reh₂_ih✝:re₂✝ = Star re → s₂✝ ++ s₂ =~ Star reh₁:App re₁✝ re₂✝ = Star re⊢ s₁✝ ++ s₂✝ ++ s₂ =~ Star re α:Types₁ s₂:List αre re':RegExp αh₃:s₂ =~ Star res₁✝:List αre₁✝ re₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₁_ih✝:re₁✝ = Star re → s₁✝ ++ s₂ =~ Star reh₁:Union re₁✝ re₂✝ = Star re⊢ s₁✝ ++ s₂ =~ Star re α:Types₁ s₂:List αre re':RegExp αh₃:s₂ =~ Star res₂✝:List αre₁✝ re₂✝:RegExp αh₂✝:s₂✝ =~ re₂✝h₂_ih✝:re₂✝ = Star re → s₂✝ ++ s₂ =~ Star reh₁:Union re₁✝ re₂✝ = Star re⊢ s₂✝ ++ s₂ =~ Star re α:Types₁ s₂:List αre re':RegExp αh₃:s₂ =~ Star rere✝:RegExp αh₁:Star re✝ = Star re⊢ [] ++ s₂ =~ Star re α:Types₁ s₂:List αre re':RegExp αh₃:s₂ =~ Star res₁✝ s₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝h₁_ih✝:re✝ = Star re → s₁✝ ++ s₂ =~ Star reh₂_ih✝:Star re✝ = Star re → s₂✝ ++ s₂ =~ Star reh₁:Star re✝ = Star re⊢ s₁✝ ++ s₂✝ ++ s₂ =~ Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp α⊢ re' = Star re → s₁ =~ re' → s₂ =~ Star re → s₁ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αre':RegExp αh₁:re' = Star reh₂:s₁ =~ re'h₃:s₂ =~ Star re⊢ s₁ ++ s₂ =~ Star re /- We can now proceed by performing induction over evidence directly, because the argument to the first hypothesis is sufficiently general, which means that we can discharge most cases by inverting the `re' = Star re` equality in the context. -/ α:Types₁:List αs₂:List αre:RegExp αre':RegExp αh₃:s₂ =~ Star reh₁:EmptyStr = Star re⊢ [] ++ s₂ =~ Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αh₃:s₂ =~ Star rec✝:αh₁:Char c✝ = Star re⊢ [c✝] ++ s₂ =~ Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αh₃:s₂ =~ Star res₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝h₁_ih✝:re₁✝ = Star re → s₁✝ ++ s₂ =~ Star reh₂_ih✝:re₂✝ = Star re → s₂✝ ++ s₂ =~ Star reh₁:App re₁✝ re₂✝ = Star re⊢ s₁✝ ++ s₂✝ ++ s₂ =~ Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αh₃:s₂ =~ Star res₁✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₁_ih✝:re₁✝ = Star re → s₁✝ ++ s₂ =~ Star reh₁:Union re₁✝ re₂✝ = Star re⊢ s₁✝ ++ s₂ =~ Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αh₃:s₂ =~ Star res₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₂✝:s₂✝ =~ re₂✝h₂_ih✝:re₂✝ = Star re → s₂✝ ++ s₂ =~ Star reh₁:Union re₁✝ re₂✝ = Star re⊢ s₂✝ ++ s₂ =~ Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αh₃:s₂ =~ Star rere✝:RegExp αh₁:Star re✝ = Star re⊢ [] ++ s₂ =~ Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αh₃:s₂ =~ Star res₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝h₁_ih✝:re✝ = Star re → s₁✝ ++ s₂ =~ Star reh₂_ih✝:Star re✝ = Star re → s₂✝ ++ s₂ =~ Star reh₁:Star re✝ = Star re⊢ s₁✝ ++ s₂✝ ++ s₂ =~ Star re /- This works, but it makes the statement of the lemma a bit ugly. Fortunately, there is a better way... -/

The tactic generalize h : e = x causes Lean to (1) replace all occurrences of the expression e by the variable x, and (2) add an equation h : e = x to the context. Here's how we can use it to show the above result:

theorem star_app α (s₁ s₂ : List α) (re : RegExp α) : s₁ =~ Star re → s₂ =~ Star re → s₁ ++ s₂ =~ Star re := α:Types₁:List αs₂:List αre:RegExp α⊢ s₁ =~ Star re → s₂ =~ Star re → s₁ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ Star re⊢ s₂ =~ Star re → s₁ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αre':RegExp αheq:Star re = re'h₁:s₁ =~ re'⊢ s₂ =~ re' → s₁ ++ s₂ =~ re' /- We now have `heq : Star re = re'`; `heq` is contradictory in most cases, allowing us to conclude immediately via `contradiction`. -/ α:Types₁:List αs₂:List αre:RegExp αre':RegExp αheq:Star re = EmptyStr⊢ s₂ =~ EmptyStr → [] ++ s₂ =~ EmptyStrα:Types₁:List αs₂:List αre:RegExp αre':RegExp αc✝:αheq:Star re = Char c✝⊢ s₂ =~ Char c✝ → [c✝] ++ s₂ =~ Char c✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝h₁_ih✝:Star re = re₁✝ → s₂ =~ re₁✝ → s₁✝ ++ s₂ =~ re₁✝h₂_ih✝:Star re = re₂✝ → s₂ =~ re₂✝ → s₂✝ ++ s₂ =~ re₂✝heq:Star re = App re₁✝ re₂✝⊢ s₂ =~ App re₁✝ re₂✝ → s₁✝ ++ s₂✝ ++ s₂ =~ App re₁✝ re₂✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₁_ih✝:Star re = re₁✝ → s₂ =~ re₁✝ → s₁✝ ++ s₂ =~ re₁✝heq:Star re = Union re₁✝ re₂✝⊢ s₂ =~ Union re₁✝ re₂✝ → s₁✝ ++ s₂ =~ Union re₁✝ re₂✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₂✝:s₂✝ =~ re₂✝h₂_ih✝:Star re = re₂✝ → s₂ =~ re₂✝ → s₂✝ ++ s₂ =~ re₂✝heq:Star re = Union re₁✝ re₂✝⊢ s₂ =~ Union re₁✝ re₂✝ → s₂✝ ++ s₂ =~ Union re₁✝ re₂✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αre✝:RegExp αheq:Star re = Star re✝⊢ s₂ =~ Star re✝ → [] ++ s₂ =~ Star re✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝h₁_ih✝:Star re = re✝ → s₂ =~ re✝ → s₁✝ ++ s₂ =~ re✝h₂_ih✝:Star re = Star re✝ → s₂ =~ Star re✝ → s₂✝ ++ s₂ =~ Star re✝heq:Star re = Star re✝⊢ s₂ =~ Star re✝ → s₁✝ ++ s₂✝ ++ s₂ =~ Star re✝ α:Types₁:List αs₂:List αre:RegExp αre':RegExp αheq:Star re = EmptyStr⊢ s₂ =~ EmptyStr → [] ++ s₂ =~ EmptyStrα:Types₁:List αs₂:List αre:RegExp αre':RegExp αc✝:αheq:Star re = Char c✝⊢ s₂ =~ Char c✝ → [c✝] ++ s₂ =~ Char c✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₂✝:s₂✝ =~ re₂✝h₁_ih✝:Star re = re₁✝ → s₂ =~ re₁✝ → s₁✝ ++ s₂ =~ re₁✝h₂_ih✝:Star re = re₂✝ → s₂ =~ re₂✝ → s₂✝ ++ s₂ =~ re₂✝heq:Star re = App re₁✝ re₂✝⊢ s₂ =~ App re₁✝ re₂✝ → s₁✝ ++ s₂✝ ++ s₂ =~ App re₁✝ re₂✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αre₁✝:RegExp αre₂✝:RegExp αh₁✝:s₁✝ =~ re₁✝h₁_ih✝:Star re = re₁✝ → s₂ =~ re₁✝ → s₁✝ ++ s₂ =~ re₁✝heq:Star re = Union re₁✝ re₂✝⊢ s₂ =~ Union re₁✝ re₂✝ → s₁✝ ++ s₂ =~ Union re₁✝ re₂✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₂✝:List αre₁✝:RegExp αre₂✝:RegExp αh₂✝:s₂✝ =~ re₂✝h₂_ih✝:Star re = re₂✝ → s₂ =~ re₂✝ → s₂✝ ++ s₂ =~ re₂✝heq:Star re = Union re₁✝ re₂✝⊢ s₂ =~ Union re₁✝ re₂✝ → s₂✝ ++ s₂ =~ Union re₁✝ re₂✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αre✝:RegExp αheq:Star re = Star re✝⊢ s₂ =~ Star re✝ → [] ++ s₂ =~ Star re✝α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝h₁_ih✝:Star re = re✝ → s₂ =~ re✝ → s₁✝ ++ s₂ =~ re✝h₂_ih✝:Star re = Star re✝ → s₂ =~ Star re✝ → s₂✝ ++ s₂ =~ Star re✝heq:Star re = Star re✝⊢ s₂ =~ Star re✝ → s₁✝ ++ s₂✝ ++ s₂ =~ Star re✝ try α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝h₁_ih✝:Star re = re✝ → s₂ =~ re✝ → s₁✝ ++ s₂ =~ re✝h₂_ih✝:Star re = Star re✝ → s₂ =~ Star re✝ → s₂✝ ++ s₂ =~ Star re✝heq:Star re = Star re✝⊢ s₂ =~ Star re✝ → s₁✝ ++ s₂✝ ++ s₂ =~ Star re✝ -- The interesting cases are those that correspond to `Star`. case mStar0 _ α:Types₁:List αs₂:List αre:RegExp αre':RegExp αre✝:RegExp αheq:Star re = Star re✝⊢ s₂ =~ Star re✝ → [] ++ s₂ =~ Star re✝ α:Types₁:List αs₂:List αre:RegExp αre':RegExp αre✝:RegExp αheq:Star re = Star re✝h₂:s₂ =~ Star re✝⊢ [] ++ s₂ =~ Star re✝; α:Types₁:List αs₂:List αre:RegExp αre':RegExp αre✝:RegExp αheq:Star re = Star re✝h₂:s₂ =~ Star re✝⊢ s₂ =~ Star re✝; All goals completed! 🐙 case mStarApp _ _ _ _ _ _ ih₂ α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝h₁_ih✝:Star re = re✝ → s₂ =~ re✝ → s₁✝ ++ s₂ =~ re✝ih₂:Star re = Star re✝ → s₂ =~ Star re✝ → s₂✝ ++ s₂ =~ Star re✝heq:Star re = Star re✝⊢ s₂ =~ Star re✝ → s₁✝ ++ s₂✝ ++ s₂ =~ Star re✝ α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αre✝:RegExp αh₁✝:s₁✝ =~ re✝h₂✝:s₂✝ =~ Star re✝h₁_ih✝:Star re = re✝ → s₂ =~ re✝ → s₁✝ ++ s₂ =~ re✝ih₂:Star re = Star re✝ → s₂ =~ Star re✝ → s₂✝ ++ s₂ =~ Star re✝heq:re = re✝⊢ s₂ =~ Star re✝ → s₁✝ ++ s₂✝ ++ s₂ =~ Star re✝; α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star re⊢ s₂ =~ Star re → s₁✝ ++ s₂✝ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ s₁✝ ++ s₂✝ ++ s₂ =~ Star re; α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ s₁✝ ++ (s₂✝ ++ s₂) =~ Star re α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ s₁✝ =~ reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ s₂✝ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ s₁✝ =~ re All goals completed! 🐙 α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ s₂✝ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ Star re = Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ Star re = Star reα:Types₁:List αs₂:List αre:RegExp αre':RegExp αs₁✝:List αs₂✝:List αh₁✝:s₁✝ =~ reh₂✝:s₂✝ =~ Star reh₁_ih✝:Star re = re → s₂ =~ re → s₁✝ ++ s₂ =~ reih₂:Star re = Star re → s₂ =~ Star re → s₂✝ ++ s₂ =~ Star reh₂:s₂ =~ Star re⊢ s₂ =~ Star re All goals completed! 🐙 /- Note that the induction hypothesis `ih₂` on the `mStarApp` case mentions an additional premise `Star re'' = Star re`, which results from the equality generated by `generalize`. -/

Do not confuse generalize with the generalizing clause on induction introduced in the Tactics chapter. The generalizing clause would not help us here — induction on s₁ =~ Star re would still fail because Star re is a compound expression, not a bare variable.

Exercise★(exp_match_ex2) (Optional)

The MStar'' lemma below (combined with its converse, the MStar' exercise above) shows that our definition of ExpMatch for Star is equivalent to the informal one given previously.

theorem declaration uses `sorry`MStar'' α (s : List α) (re : RegExp α) (h : s =~ Star re) : exists ss : List (List α), s = List.foldr (· ++ ·) [] ss ∧ ∀ s', s' ∈ ss → s' =~ re := α:Types:List αre:RegExp αh:s =~ Star re⊢ ∃ ss, s = List.foldr (fun x1 x2 => x1 ++ x2) [] ss ∧ ∀ (s' : List α), s' ∈ ss → s' =~ re All goals completed! 🐙

10.5.4. The "Weak" Pumping Lemma🔗

One of the first really interesting theorems in the theory of regular expressions is the so-called pumping lemma, which states, informally, that any sufficiently long string s matching a regular expression re can be "pumped" by repeating some middle section of s an arbitrary number of times to produce a new string also matching re. For the sake of simplicity, this exercise considers a slightly weaker theorem than is usually stated in courses on automata theory — hence the name weak_pumping. The stronger one can be found below.

To get started, we need to define "sufficiently long." Since we are working in a constructive logic, we actually need to be able to calculate, for each regular expression re, a minimum length for strings s to guarantee "pumpability."

def pumpingConstant {α : Type} (re : RegExp α) : Nat := match re with | EmptySet => 1 | EmptyStr => 1 | Char _ => 2 | App re₁ re₂ => re₁.pumpingConstant + re₂.pumpingConstant | Union re₁ re₂ => re₁.pumpingConstant + re₂.pumpingConstant | Star r => r.pumpingConstant

You may find these lemmas about the pumping constant useful when proving the pumping lemma below.

theorem pumping_constant_ge_1 {α : Type} (re : RegExp α) : re.pumpingConstant ≥ 1 := α:Typere:RegExp α⊢ re.pumpingConstant ≥ 1 induction re with (All goals completed! 🐙; try All goals completed! 🐙) theorem pumping_constant_0_false {α : Type} (re : RegExp α) (h : re.pumpingConstant = 0) : False := α:Typere:RegExp αh:re.pumpingConstant = 0⊢ False α:Typere:RegExp αh:re.pumpingConstant = 0this:re.pumpingConstant ≥ 1⊢ False; All goals completed! 🐙

Next, it is useful to define an auxiliary function that repeats a string (appends it to itself) some number of times. Note how we define simp lemmas for napp to go with its definition.

def napp {α : Type} (n : Nat) (l : List α) : List α := match n with | 0 => [] | n' + 1 => l ++ napp n' l @[simp] theorem napp_zero {α : Type} (l : List α) : napp 0 l = [] := α:Typel:List α⊢ napp 0 l = [] All goals completed! 🐙 @[simp] theorem napp_succ {α : Type} (n : Nat) (l : List α) : napp (n + 1) l = l ++ napp n l := α:Typen:Natl:List α⊢ napp (n + 1) l = l ++ napp n l All goals completed! 🐙

These auxiliary lemmas might also be useful in your proof of the pumping lemma.

@[simp] theorem napp_plus {α : Type} (n m : Nat) (l : List α) : napp (n + m) l = napp n l ++ napp m l := α:Typen:Natm:Natl:List α⊢ napp (n + m) l = napp n l ++ napp m l induction n with All goals completed! 🐙 theorem napp_star {α : Type} (m : Nat) (s₁ s₂ : List α) (re : RegExp α) (hs₁ : s₁ =~ re) (hs₂ : s₂ =~ Star re) : napp m s₁ ++ s₂ =~ Star re := α:Typem:Nats₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star re⊢ napp m s₁ ++ s₂ =~ Star re induction m with α:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star re⊢ napp 0 s₁ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star re⊢ s₂ =~ Star re; All goals completed! 🐙 α:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star rem:Natih:napp m s₁ ++ s₂ =~ Star re⊢ napp (m + 1) s₁ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star rem:Natih:napp m s₁ ++ s₂ =~ Star re⊢ s₁ ++ napp m s₁ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star rem:Natih:napp m s₁ ++ s₂ =~ Star re⊢ s₁ ++ (napp m s₁ ++ s₂) =~ Star re α:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star rem:Natih:napp m s₁ ++ s₂ =~ Star re⊢ s₁ =~ reα:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star rem:Natih:napp m s₁ ++ s₂ =~ Star re⊢ napp m s₁ ++ s₂ =~ Star re α:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star rem:Natih:napp m s₁ ++ s₂ =~ Star re⊢ s₁ =~ reα:Types₁:List αs₂:List αre:RegExp αhs₁:s₁ =~ rehs₂:s₂ =~ Star rem:Natih:napp m s₁ ++ s₂ =~ Star re⊢ napp m s₁ ++ s₂ =~ Star re All goals completed! 🐙

The (weak) pumping lemma itself says that, if s =~ re and if the length of s is at least the pumping constant of re, then s can be split into three substrings s₁ ++ s₂ ++ s₃ in such a way that s₂ can be repeated any number of times and the result, when combined with s₁ and s₃, will still match re. Since s₂ is also guaranteed not to be the empty string, this gives us a (constructive!) way to generate strings matching re that are as long as we like.

This proof is quite long, so to make it more tractable we've broken it up into a number of subproofs, which we then assemble to prove the main lemma.

Your job is to complete the proofs of the helper lemmas; the main lemma relies on these.

Exercise★★(weak_pumping_char)
theorem declaration uses `sorry`weak_pumping_char {α : Type} (x : α) (h : (Char x).pumpingConstant ≤ [x].length) : ∃ s₁ s₂ s₃ : List α, [x] = s₁ ++ s₂ ++ s₃ ∧ s₂ ≠ [ ] ∧ (∀ m : Nat, s₁ ++ napp m s₂ ++ s₃ =~ Char x) := α:Typex:αh:(Char x).pumpingConstant ≤ [x].length⊢ ∃ s₁ s₂ s₃, [x] = s₁ ++ s₂ ++ s₃ ∧ s₂ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₂ ++ s₃ =~ Char x All goals completed! 🐙
Exercise★★★★(weak_pumping_app)
theorem declaration uses `sorry`weak_pumping_app {α : Type} (s₁ s₂ : List α) (re₁ re₂ : RegExp α) (h₁ : s₁ =~ re₁) (h₂ : s₂ =~ re₂) (ih₁ : re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄ : List α, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [ ] ∧ (∀ m : Nat, s₂ ++ napp m s₃ ++ s₄ =~ re₁)) (ih₂ : re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄ : List α, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [ ] ∧ (∀ m : Nat, s₁ ++ napp m s₃ ++ s₄ =~ re₂)) (hLen : (App re₁ re₂).pumpingConstant ≤ (s₁ ++ s₂).length) : ∃ s₀ s₃ s₄ : List α, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [ ] ∧ (∀ m : Nat, s₀ ++ napp m s₃ ++ s₄ =~ App re₁ re₂) := α:Types₁:List αs₂:List αre₁:RegExp αre₂:RegExp αh₁:s₁ =~ re₁h₂:s₂ =~ re₂ih₁:re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ re₁ih₂:re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ re₂hLen:(App re₁ re₂).pumpingConstant ≤ (s₁ ++ s₂).length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ App re₁ re₂ α:Types₁:List αs₂:List αre₁:RegExp αre₂:RegExp αh₁:s₁ =~ re₁h₂:s₂ =~ re₂ih₁:re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ re₁ih₂:re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ re₂hLen:(App re₁ re₂).pumpingConstant ≤ (s₁ ++ s₂).lengthh:re₁.pumpingConstant ≤ s₁.length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ App re₁ re₂α:Types₁:List αs₂:List αre₁:RegExp αre₂:RegExp αh₁:s₁ =~ re₁h₂:s₂ =~ re₂ih₁:re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ re₁ih₂:re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ re₂hLen:(App re₁ re₂).pumpingConstant ≤ (s₁ ++ s₂).lengthh:re₂.pumpingConstant ≤ s₂.length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ App re₁ re₂ case inl α:Types₁:List αs₂:List αre₁:RegExp αre₂:RegExp αh₁:s₁ =~ re₁h₂:s₂ =~ re₂ih₁:re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ re₁ih₂:re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ re₂hLen:(App re₁ re₂).pumpingConstant ≤ (s₁ ++ s₂).lengthh:re₁.pumpingConstant ≤ s₁.length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ App re₁ re₂ All goals completed! 🐙 case inr α:Types₁:List αs₂:List αre₁:RegExp αre₂:RegExp αh₁:s₁ =~ re₁h₂:s₂ =~ re₂ih₁:re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ re₁ih₂:re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ re₂hLen:(App re₁ re₂).pumpingConstant ≤ (s₁ ++ s₂).lengthh:re₂.pumpingConstant ≤ s₂.length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ App re₁ re₂ All goals completed! 🐙
Exercise★★★(weak_pumping_union_l)
theorem declaration uses `sorry`weak_pumping_union_l {α : Type} (s₁ : List α) (re₁ re₂ : RegExp α) (h₁ : s₁ =~ re₁) (ih : re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄ : List α, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [ ] ∧ (∀ m : Nat, s₂ ++ napp m s₃ ++ s₄ =~ re₁)) (hLen : (Union re₁ re₂).pumpingConstant ≤ s₁.length) : ∃ s₀ s₂ s₃ : List α, s₁ = s₀ ++ s₂ ++ s₃ ∧ s₂ ≠ [ ] ∧ (∀ m : Nat, s₀ ++ napp m s₂ ++ s₃ =~ Union re₁ re₂) := α:Types₁:List αre₁:RegExp αre₂:RegExp αh₁:s₁ =~ re₁ih:re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ re₁hLen:(Union re₁ re₂).pumpingConstant ≤ s₁.length⊢ ∃ s₀ s₂ s₃, s₁ = s₀ ++ s₂ ++ s₃ ∧ s₂ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₂ ++ s₃ =~ Union re₁ re₂ α:Types₁:List αre₁:RegExp αre₂:RegExp αh₁:s₁ =~ re₁ih:re₁.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ re₁hLen:(Union re₁ re₂).pumpingConstant ≤ s₁.lengthh:re₁.pumpingConstant ≤ s₁.length⊢ ∃ s₀ s₂ s₃, s₁ = s₀ ++ s₂ ++ s₃ ∧ s₂ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₂ ++ s₃ =~ Union re₁ re₂ All goals completed! 🐙
Exercise★★★(weak_pumping_union_r)
theorem declaration uses `sorry`weak_pumping_union_r {α : Type} (s₂ : List α) (re₁ re₂ : RegExp α) (h₂ : s₂ =~ re₂) (ih : re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄ : List α, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [ ] ∧ (∀ m : Nat, s₁ ++ napp m s₃ ++ s₄ =~ re₂)) (hLen : (Union re₁ re₂).pumpingConstant ≤ s₂.length) : ∃ s₁ s₀ s₃ : List α, s₂ = s₁ ++ s₀ ++ s₃ ∧ s₀ ≠ [ ] ∧ (∀ m : Nat, s₁ ++ napp m s₀ ++ s₃ =~ Union re₁ re₂) := α:Types₂:List αre₁:RegExp αre₂:RegExp αh₂:s₂ =~ re₂ih:re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ re₂hLen:(Union re₁ re₂).pumpingConstant ≤ s₂.length⊢ ∃ s₁ s₀ s₃, s₂ = s₁ ++ s₀ ++ s₃ ∧ s₀ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₀ ++ s₃ =~ Union re₁ re₂ -- symmetric to the previous α:Types₂:List αre₁:RegExp αre₂:RegExp αh₂:s₂ =~ re₂ih:re₂.pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ re₂hLen:(Union re₁ re₂).pumpingConstant ≤ s₂.lengthh:re₂.pumpingConstant ≤ s₂.length⊢ ∃ s₁ s₀ s₃, s₂ = s₁ ++ s₀ ++ s₃ ∧ s₀ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₀ ++ s₃ =~ Union re₁ re₂ All goals completed! 🐙
Exercise★★(weak_pumping_star_zero)
theorem declaration uses `sorry`weak_pumping_star_zero {α : Type} (re : RegExp α) (h : (Star re).pumpingConstant ≤ @List.length α []) : ∃ s₁ s₂ s₃ : List α, [ ] = s₁ ++ s₂ ++ s₃ ∧ s₂ ≠ [ ] ∧ (∀ m : Nat, s₁ ++ napp m s₂ ++ s₃ =~ Star re) := α:Typere:RegExp αh:(Star re).pumpingConstant ≤ [].length⊢ ∃ s₁ s₂ s₃, [] = s₁ ++ s₂ ++ s₃ ∧ s₂ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₂ ++ s₃ =~ Star re All goals completed! 🐙
Exercise★★★★★(weak_pumping_star_app)
theorem declaration uses `sorry`weak_pumping_star_app {α : Type} (s₁ s₂ : List α) (re : RegExp α) (h₁ : s₁ =~ re) (h₂ : s₂ =~ Star re) (ih₁ : re.pumpingConstant ≤ List.length s₁ → ∃ s₂ s₃ s₄ : List α, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [ ] ∧ (∀ m : Nat, s₂ ++ napp m s₃ ++ s₄ =~ re)) (ih₂ : (Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄ : List α, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [ ] ∧ (∀ m : Nat, s₁ ++ napp m s₃ ++ s₄ =~ Star re)) (hLen : (Star re).pumpingConstant ≤ (s₁ ++ s₂).length) : ∃ s₀ s₃ s₄ : List α, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [ ] ∧ (∀ m : Nat, s₀ ++ napp m s₃ ++ s₄ =~ .Star re) := α:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ reh₂:s₂ =~ Star reih₁:re.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ reih₂:(Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ Star rehLen:(Star re).pumpingConstant ≤ (s₁ ++ s₂).length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ Star re α:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ reh₂:s₂ =~ Star reih₁:re.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ reih₂:(Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ Star rehLen:(Star re).pumpingConstant ≤ s₁.length + s₂.length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ Star re α:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ reh₂:s₂ =~ Star reih₁:re.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ reih₂:(Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ Star rehLen:(Star re).pumpingConstant ≤ s₁.length + s₂.lengthhs₁len0:s₁.length = 0⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ Star reα:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ reh₂:s₂ =~ Star reih₁:re.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ reih₂:(Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ Star rehLen:(Star re).pumpingConstant ≤ s₁.length + s₂.lengths₁len:s₁.length ≠ 0hs₁re₁:s₁.length < re.pumpingConstant⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ Star reα:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ reh₂:s₂ =~ Star reih₁:re.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ reih₂:(Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ Star rehLen:(Star re).pumpingConstant ≤ s₁.length + s₂.lengthhs₁re₁:re.pumpingConstant ≤ s₁.length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ Star re α:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ reh₂:s₂ =~ Star reih₁:re.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ reih₂:(Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ Star rehLen:(Star re).pumpingConstant ≤ s₁.length + s₂.lengthhs₁len0:s₁.length = 0⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ Star re All goals completed! 🐙 α:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ reh₂:s₂ =~ Star reih₁:re.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ reih₂:(Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ Star rehLen:(Star re).pumpingConstant ≤ s₁.length + s₂.lengths₁len:s₁.length ≠ 0hs₁re₁:s₁.length < re.pumpingConstant⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ Star re All goals completed! 🐙 α:Types₁:List αs₂:List αre:RegExp αh₁:s₁ =~ reh₂:s₂ =~ Star reih₁:re.pumpingConstant ≤ s₁.length → ∃ s₂ s₃ s₄, s₁ = s₂ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₂ ++ napp m s₃ ++ s₄ =~ reih₂:(Star re).pumpingConstant ≤ s₂.length → ∃ s₁ s₃ s₄, s₂ = s₁ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₃ ++ s₄ =~ Star rehLen:(Star re).pumpingConstant ≤ s₁.length + s₂.lengthhs₁re₁:re.pumpingConstant ≤ s₁.length⊢ ∃ s₀ s₃ s₄, s₁ ++ s₂ = s₀ ++ s₃ ++ s₄ ∧ s₃ ≠ [] ∧ ∀ (m : Nat), s₀ ++ napp m s₃ ++ s₄ =~ Star re All goals completed! 🐙
Exercise★★★(weak_pumping)
theorem declaration uses `sorry`weak_pumping {α : Type} {re : RegExp α} {s : List α} (hmatch : s =~ re) (hlen : re.pumpingConstant ≤ s.length) : ∃ s₁ s₂ s₃ : List α, s = s₁ ++ s₂ ++ s₃ ∧ s₂ ≠ [] ∧ ∀ m, s₁ ++ napp m s₂ ++ s₃ =~ re := α:Typere:RegExp αs:List αhmatch:s =~ rehlen:re.pumpingConstant ≤ s.length⊢ ∃ s₁ s₂ s₃, s = s₁ ++ s₂ ++ s₃ ∧ s₂ ≠ [] ∧ ∀ (m : Nat), s₁ ++ napp m s₂ ++ s₃ =~ re All goals completed! 🐙

10.5.5. The "Strong" Pumping Lemma🔗

Exercise★★★★★(strong_pumping) (Advanced, Optional)

Now here is the usual version of the pumping lemma. In addition to requiring that s₂ ≠ [], it also strengthens the result to include the claim that s₁.length + s₂.length ≤ re.pumpingConstant.

theorem declaration uses `sorry`pumping {α : Type} {re : RegExp α} {s : List α} (hmatch : s =~ re) (hlen : re.pumpingConstant ≤ s.length) : ∃ s₁ s₂ s₃ : List α, s = s₁ ++ s₂ ++ s₃ ∧ s₂ ≠ [] ∧ s₁.length + s₂.length ≤ re.pumpingConstant ∧ ∀ m, s₁ ++ napp m s₂ ++ s₃ =~ re := α:Typere:RegExp αs:List αhmatch:s =~ rehlen:re.pumpingConstant ≤ s.length⊢ ∃ s₁ s₂ s₃, s = s₁ ++ s₂ ++ s₃ ∧ s₂ ≠ [] ∧ s₁.length + s₂.length ≤ re.pumpingConstant ∧ ∀ (m : Nat), s₁ ++ napp m s₂ ++ s₃ =~ re All goals completed! 🐙
end RegExp

10.5.6. Palindromes Revisited🔗

Exercise★★★★★(palindrome_converse) (Optional)

Here is one possible definition of the palindrome inductive predicate, Pal, which we saw in the last chapter.

namespace PalConv inductive Pal {α : Type} : List α → Prop where | nil : Pal [] | singleton {x : α} : Pal [x] | cons_snoc {x : α} {l : List α} (h : Pal l) : Pal (x :: (l ++ [x]))

We previously proved that ∀ l, Pal l → l = l.reverse. The converse is also true, but significantly more difficult to prove, due to the lack of evidence. Using the definition of Pal above, prove that

∀ l, l = l.reverse → Pal l
Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC