A useful example of "induction ... using ..." (?)

Stream: Lean for teaching

[Frederic Peschanski]

I don't know if it is a correct place for sharing "course tips" ... sorry if it is not.

In the context of a course "specification and verification of programs" I am giving since 2021 using Lean4 (replacing Coq ...) at Sorbonne University (for CS students), I was looking for a good example of when the tactic induction ... using ... would be useful. Triggered by this stack overflow question, I ended up with what follows.

It is a little bit longer than I expected (I did not try to make it as concise at what would be needed), but it might be useful if you want to illustrate this feature of the induction tactic.

I am of course interested by other similar examples ...

-- I use a separate LList type to be self-contained
inductive LList (α : Type u) where
  | nil : LList α
  | cons (x:α) (xs:LList α): LList α
deriving Repr

open LList

def lappend (xs ys : LList α) :=
  match xs with
  | nil => ys
  | cons x xs => LList.cons x (lappend xs ys)

theorem lappend_nil (xs : LList α):
  lappend xs nil = xs :=
by
  induction xs
  case nil => simp [lappend]
  case cons x xs Hind =>
    simp [lappend, Hind]

theorem lappend_assoc (xs ys zs : LList α):
  lappend xs (lappend ys zs) = lappend (lappend xs ys) zs :=
by
  induction xs
  case nil => simp [lappend]
  case cons x xs Hind =>
    simp [lappend, Hind]

def snoc (x : α) (xs : LList α) := lappend xs (cons x nil)

def rev (xs : LList α) :=
  match xs with
  | nil => nil
  | cons x xs => snoc x (rev xs)

theorem rev_snoc (x : α) (xs : LList α):
  rev (snoc x xs) = cons x (rev xs) :=
by
  induction xs
  case nil => simp [rev, lappend, snoc]
  case cons y xs Hind =>
    simp [rev, lappend, snoc] at Hind
    simp [Hind, lappend, snoc, rev]

theorem rev_rev (xs : LList α):
  rev (rev xs) = xs :=
by
  induction xs
  case nil => simp [rev]
  case cons x xs Hind =>
    simp [rev, snoc]
    show rev (snoc x (rev xs)) = cons x xs
    simp [rev_snoc, Hind]

-- a first induction principle, easy to prove but unusable because
-- the conclusion is not in a `(motive <var>)` form ...
theorem list_ind_rev_snoc (P : LList α → Prop):
    P nil
    → (∀ x xs, P xs → P (snoc x xs))
    → ∀ xs : LList α, P (rev xs) :=
by
  intros Hnil Hsnoc xs
  induction xs
  case nil => assumption
  case cons x xs Hind =>
    simp [rev]
    apply Hsnoc
    assumption

-- this is ugly but it is a valid induction principle now...
theorem list_ind_rev_rev_snoc (P : LList α → Prop):
    P nil
    → (∀ x xs, P (rev xs) → P (snoc x (rev xs)))
    → ∀ xs : LList α, P xs :=
by
  intros Hnil Hsnoc xs
  have Hrev: rev (rev xs) = xs := by apply rev_rev
  rw [←Hrev]
  apply list_ind_rev_snoc
  · assumption
  · intros y ys HP
    clear Hrev
    have Hrev: rev (rev ys) = ys := by apply rev_rev
    rw [←Hrev]
    apply Hsnoc
    · simp [Hrev, HP]

-- this one is trivial, but it's the key I was missing at first
theorem list_ind_snoc_lemma (P : LList α → Prop):
 (∀ x xs, P xs → P (snoc x xs))
 → (∀ x xs, P (rev xs) → P (snoc x (rev xs))) :=
by
  intros H1 x xs
  apply H1

-- this is what I wanted first ... but I ended up going the "rev" way
theorem list_ind_snoc (P : LList α → Prop):
    P nil
    → (∀ x xs, P xs → P (snoc x xs))
    → ∀ xs : LList α, P xs :=
by
  intros Hnil Hsnoc'
  have Hsnoc: (∀ x xs, P (rev xs) → P (snoc x (rev xs))) := by
    apply list_ind_snoc_lemma ; assumption
  apply list_ind_rev_rev_snoc <;> assumption

-- this is where thing become interesting
theorem lappend_snoc (xs ys : LList α):
  ∀ y : α, lappend xs (snoc y ys) = snoc y (lappend xs ys) :=
by
  induction ys using list_ind_snoc
  case a => simp [lappend_nil, snoc, lappend]
  case a x ys Hind =>
    intro y
    simp [Hind, snoc, lappend_assoc]

-- and there you are stack overflow !
theorem rev_lappend (xs ys : LList α):
  rev (lappend xs ys) = lappend (rev ys) (rev xs) :=
by
  induction ys using list_ind_snoc
  case a => simp [rev, lappend, lappend_nil]
  case a x ys Hind =>
    simp [rev_snoc, lappend, ←Hind, lappend_snoc]

[François G. Dorais]

Not about lists and perhaps not as interesting but there are a few examples in Std: https://github.com/leanprover/std4/blob/483fd2846f9fe5107011ece0cc3d8d88af1a8603/Std/Data/Nat/Lemmas.lean#L704C1-L727C1

[François G. Dorais]

This type of diagonal induction is also useful for proving theorems about zip.

[Yury G. Kudryashov]

We have several induction principles for docs#Finset. The default "destruct into a Multiset and a proof of NoDup" is the least useful one.

[Yury G. Kudryashov]

Also, you can add an induction principle

theorem cauchy_induction (p : Nat → Prop) (one : p 1) (mul_two : ∀ n, p n → p (2 * n)) (lt : ∀ m n, m < n → p n → p m) :
    ∀ n, p n := sorry -- get `p (2 ^ (n + 1))` from `one` and `mul_two`, then use `lt`

then use it to prove the AM-GM inequality: the mul_two step is basically 2ab ≤ a²+b² and the lt step can be done by setting the last n - m numbers to the arithmetic mean of the first m numbers.

[Frederic Peschanski]

These are excellent examples ... thank you !

[Frederic Peschanski]

Looking at recDiagAux I get it that it is better to give names to assumptions, e.g. :

theorem list_ind_snoc (P : LList α → Prop)
  (nil : P nil)
  (ind : (∀ x xs, P xs → P (snoc x xs))):
  ∀ xs : LList α, P xs :=
by
  ...

so that the case names are e.g. nil and ind (inductive...)

[Mario Carneiro]

it's also better to use the names of existing functions when possible, so that hover works

[Mario Carneiro]

so in that example I would suggest using the names nil and snoc

[Frederic Peschanski]

Mario Carneiro said:

so in that example I would suggest using the names nil and snoc

When I do that, there seems to be a name collision maybe because snoc is a def and not a constructor ?

α: Type u_1
P: LList α → Prop
nil: P LList.nil
snoc: ∀ (x : α) (xs : LList α), P xs → P (_root_.snoc x xs)
⊢ ∀ (xs : LList α), P xs

(and a type error ...)

I don't know exactly what happens here...

[Mario Carneiro]

yes, that is expected

[Mario Carneiro]

the type error is not

[Mario Carneiro]

I think it only works if snoc is a definition in the LList namespace

[Mario Carneiro]

it's a bit weird that it is not here

[Frederic Peschanski]

Mario Carneiro said:

I think it only works if snoc is a definition in the LList namespace

This works, thanks !

namespace LList
def snoc (x : α) (xs : LList α) := lappend xs (cons x nil)
end LList

However, I need to do that :

theorem list_ind_snoc (P : LList α → Prop)
  (nil : P nil)
  (snoc : (∀ x xs, P xs → P (snoc x xs))):
  ∀ xs : LList α, P xs :=
by
  have Hsnoc: (∀ x xs, P (rev xs) → P (LList.snoc x (rev xs))) := by
    apply list_ind_snoc_lemma ; assumption
  apply list_ind_rev_rev_snoc <;> assumption

(remark the LList.snoc otherwise I get the same type error ... probably because the namespace is opened...)

[Mario Carneiro]

I don't know what this is being compared to, or what the type error was

[Mario Carneiro]

You probably want list_ind_snoc to also be in the LList namespace, in which case you won't need to use LList.snoc in the proof

[Mario Carneiro]

you can also use .snoc to avoid writing the namespace even if it's not open