## Stream: Coq users

### Topic: ✔ proving inequality by induction?

#### Tan Yee Jian (Jan 15 2023 at 02:34):

I have a problem that is, I think, analogue to showing this funny property about `nat`:

``````Lemma try : forall n (l: list nat), l <> [] -> fold_right (fun _ x => S x) n l <> n.
``````

When doing induction on `l`, I realized that the induction hypothesis is not very useful, because basically inequality is not transitive, so I cannot use the IH in a meaningful way. My pen-and-paper proof notices that the IH gives that the fold amounts to `S (S (S... n))` for some finite number of `S`, and one can definitely do `inversion` sufficiently to show the inequality. How can I use the concrete witnesses `l` to help prove the fact, or is this method flawed?

#### Huỳnh Trần Khanh (Jan 15 2023 at 04:02):

Try proving the fold_right is always greater than n, that'll get you somewhere. Probably we could even be more specific, the fold_right evaluates to n plus the length of the list.

#### Paolo Giarrusso (Jan 15 2023 at 04:44):

Indeed, this is one of the many examples where before doing induction, you must change your theorem to be stronger to make the proof possible: We say you must _strengthen the induction hypothesis_. https://mathoverflow.net/a/40688/36016 is another example.

#### Stefan Haan (Jan 15 2023 at 12:45):

It also helps to prove helpful lemmas first. In your example `fold_right (fun _ x => S x) n l` is simply `n + length l`.

``````Require Import List Lia.
Import ListNotations.

Lemma fold_right_S_length A n (l: list A):
fold_right (fun _ x => S x) n l = n + length l.
Proof.
induction l.
- apply plus_n_O.
- cbn. rewrite IHl. apply plus_n_Sm.
Qed.

Lemma try : forall n (l: list nat), l <> [] -> fold_right (fun _ x => S x) n l <> n.
Proof.
intros. rewrite fold_right_S_length.
rewrite <- length_zero_iff_nil in H. lia.
Qed.
``````

#### Tan Yee Jian (Jan 15 2023 at 14:09):

Thanks for all your help, it worked! I managed to define an analogous `<` for my inductive datatype and prove irreflexivity and transitivity, and strengthening the lemma to `> n` instead of `<> n`, then by irreflexivity I have the inequality. I enjoyed the "mathematical example" too.

#### Notification Bot (Jan 15 2023 at 14:10):

Tan Yee Jian has marked this topic as resolved.

Last updated: Jun 20 2024 at 13:02 UTC