## Stream: Lean for teaching

### Topic: A useful example of "induction ... using ..." (?)

#### Frederic Peschanski (Dec 12 2023 at 23:33):

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 (Dec 12 2023 at 23:45):

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 (Dec 12 2023 at 23:49):

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

#### Yury G. Kudryashov (Dec 13 2023 at 04:29):

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 (Dec 13 2023 at 04:32):

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 (Dec 13 2023 at 08:10):

These are excellent examples ... thank you !

#### Frederic Peschanski (Dec 13 2023 at 08:18):

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 (Dec 13 2023 at 08:25):

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

#### Mario Carneiro (Dec 13 2023 at 08:25):

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

#### Frederic Peschanski (Dec 13 2023 at 08:43):

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 (Dec 13 2023 at 08:56):

yes, that is expected

#### Mario Carneiro (Dec 13 2023 at 08:56):

the type error is not

#### Mario Carneiro (Dec 13 2023 at 08:56):

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

#### Mario Carneiro (Dec 13 2023 at 08:56):

it's a bit weird that it is not here

#### Frederic Peschanski (Dec 13 2023 at 10:53):

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 (Dec 13 2023 at 10:54):

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

#### Mario Carneiro (Dec 13 2023 at 10:55):

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 (Dec 13 2023 at 10:56):

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

Last updated: Dec 20 2023 at 11:08 UTC