Logical Foundations

10. Automation: More Automation🔗

Consider the proof below. Notice all the repetition and near-repetition...

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🔗

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🔗

Recall the <;> combinator...

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! 🐙
Note to developers (Benjamin Pierce @bcpierce00)
INCOMING BOCHUM MATERIAL summarized by Claude (old/bochum-lf-updates/AltAuto.v): the
   Bochum LF updates extend AltAuto's discussion of the sequencing
   tactical with new material on Rocq's "local form with `..`":

     T; [T1 .. | Tn]

   which applies T1 to the first goal, Tn to the last, and T1 to all
   goals in between (variants: T; [T1 | .. | Tn] applies nothing in
   between; the `..` may also appear first, last, or alone).  The new
   material illustrates this by revisiting star_app from IndProp:

     Lemma star_app'': forall T (s1 s2 : list T) (re : reg_exp T),
       s1 =~ Star re ->
       s2 =~ Star re ->
       s1 ++ s2 =~ Star re.
     Proof.
       intros T s1 s2 re H1.
       remember (Star re) as re' eqn:Eq.
       induction H1
         as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
             |s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
             |re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2];
         [discriminate .. | intros H; apply H | idtac]. (* <=== *)
       (* MStarApp *)
       intros H1. rewrite <- app_assoc.
       apply MStarApp.
       + apply Hmatch1.
       + apply IH2.
         * apply Eq.
         * apply H1.
     Qed.

   (first shown in its long form with all seven cases spelled out, then
   shortened as above).  Bochum also adds a QUIETSOLUTION alternate
   solution to AltAuto's re_opt exercise that uses nested `..` lists
   instead of `try`, and rewords the introduction of `T; T'` to say
   simply that it is "equivalent to locally performing T' on all the
   subgoals".

   To incorporate: Lean has no direct analogue of the positional
   `[T1 .. | Tn]` goal-selector list; the closest idioms are
   case-labelled alternatives (`case ... =>`/`next`), `all_goals`,
   and `first`.  A future pass should decide whether to add a
   parallel discussion here (e.g. using `star_app` below, proving the
   six non-MStarApp cases uniformly) or to record the Rocq material
   as intentionally unported.

10.2.1. The try Combinator🔗

The try combinator swallows a tactic's failure.

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` 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! 🐙

The try and <;> combinators used together allow you to apply a tactic to some, but not all, goals...

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 repeat combinator can 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]

10.2.3. The first Combinator🔗

The first combinator applies the first successful tactic in a list:

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

We can combine first with 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 first | All goals completed! 🐙 | ⊢ 10 ∈ [10]
Note to developers (Mike Hicks @mwhicks1)

It occurs to me having gotten this far that we could really use some quizzes to test understanding of these various combinators to this point.

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.

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 using for rewriting are good ones to give to simp, which is why they are also called simplification lemmas.

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! 🐙

Writing simp only applies simp with only the provided theorems:

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]

The simp ... at ... tactic simplifies in a hypothesis.

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.

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! 🐙
Note to developers (Mike Hicks @mwhicks1)

Should we add something like the following, to explain conditional rewrites?

Recall from Tactics that rewriting with a theorem h₁ -> h₂ -> a = b uses a = b and leaves h₁ and h₂ as new subgoals. We can include such theorems in simp's available set, too, but it handles the premises differently: it tries to discharge h₁, h₂ too, recursively, using simp again (by default), and only fires the rewrite if it succeeds. If it can't discharge a premise, it just doesn't use that lemma.

Claude tested three variants of this against the real toolchain (lake env lean). The double_injective lemma from Tactics doesn't actually work here: its conclusion is the bare variable n = m, which isn't a usable rewrite pattern (simp lemmas need a real compound term on the left), so simp [double_injective] fails outright with "simp made no progress" before it ever gets anywhere near the n.double = m.double premise.

A conditional lemma that does have a proper compound left-hand side, like Nat.sub_add_cancel : n ≤ m -> m - n + n = m, tells a cleaner three-part story. With hle : n ≤ m in context:

example (n m : Nat) (hle : n ≤ m) : m - n + n = m := by
  simp [Nat.sub_add_cancel]        -- fails: "simp made no progress"

example (n m : Nat) (hle : n ≤ m) : m - n + n = m := by
  simp [Nat.sub_add_cancel, hle]   -- succeeds

example (n m : Nat) (hle : n ≤ m) : m - n + n = m := by
  simp_all [Nat.sub_add_cancel]    -- succeeds, without naming hle

The first case shows the discharge step only consults the active simp set (default set plus whatever's explicitly listed) -- not arbitrary context hypotheses -- so hle sitting right there doesn't help; simp just skips the lemma, exactly the "no error, no leftover subgoal" behavior claimed above. The second shows discharge working once hle is added to the set. The third previews simp_all (introduced a bit further down this chapter): it folds every hypothesis into the active set automatically, so it discharges the premise without hle being named at all. That third point makes this example worth placing right here rather than after simp_all -- it's a preview, and it ties the two sections together.

10.3.1. Idiomatic simp Usage🔗

Note to developers (Claude)

Worth tying this convention explicitly back to the fixpoint framing suggested near the top of this section: a terminal simp is safe precisely because nothing downstream depends on its exact resulting term -- only on whether it helped close the goal. A nonterminal simp is risky because whatever manual tactic comes next (cases h1 with | inl h => ... in the example below) depends on the specific shape simp leaves behind, and that shape isn't a stable contract -- it can change as the simp set grows, since simp just runs to whatever fixpoint the current lemma set produces. Saying that explicitly might make the "why" land harder than jumping straight to the terminal/nonterminal rule.

Don't use simp without only unless you're closing a goal or following with a flexible tactic. The example below breaks this rule:

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! 🐙

This usage of simp is brittle and can break due to upstream changes.

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! 🐙

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

Appropriately defined simp lemmas simplify left to right.

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🔗

10.5.1. Definitions🔗

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 α.

Note to developers (Daniel Sainati @dsainati1)

CH: Do you mean here that this is different because the inductive type doesn't specify α is finite? In Lean the convention is for inductives not to carry Prop-valued typeclass assumptions, enforcing this only at the theorems that use them. So this could give off a slightly wrong impression. DHS: @bcpierce00 What was the purpose of this aside in the original Rocq text? Does it make sense to keep here?

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

Note to developers (Mike Hicks @mwhicks1)

It would be convenient to declare the variables below so that inline prose throughout the rest of this section can use α, x, s, s₁, s₂, s₃, ss, re, re₁, and re₂ without repeating their type annotations, but the same problem described in Logic applies: an unused variable is silently added to the local context in basically every proof from here on, even when the theorem never mentions it, which makes theorem hover-overs in the HTML book unusable. Until we have a way to declare variables visible only for inline prose (rather than for every lean block), we leave this commented out:

-- variable
--   (α : Type)
--   (x : α)
--   (s s₁ s₂ s₃ : List α)
--   (ss : List (List α))
--   (re re₁ re₂ : RegExp α)

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! 🐙

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! 🐙 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! 🐙

Something more interesting:

theorem declaration uses `sorry`MStar1 α s (re : RegExp α) (h : s =~ re) : s =~ Star re := α:Types:List αre:RegExp αh:s =~ re⊢ s =~ Star re All goals completed! 🐙

Naturally, proofs about ExpMatch 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 declaration uses `sorry`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₂`). -/ 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₂`. -/ All goals completed! 🐙

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.

10.5.4. The "Weak" Pumping Lemma🔗

The remainder of this section in the full version of the chapter develops an extended exercise on regular expressions, leading up to a proof of 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.

10.5.5. The "Strong" Pumping Lemma🔗

end RegExp

10.5.6. Palindromes Revisited🔗

Source revision: e85fe77, committed 2026-10-06 21:16 UTC