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?

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.

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.

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

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.

Tan Yee Jian has marked this topic as resolved.

Last updated: Jun 20 2024 at 13:02 UTC