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: Oct 04 2023 at 20:01 UTC