Stream: Coq users

Topic: false statements about list_max


view this post on Zulip sara lee (Nov 10 2021 at 17:41):

We can prove below statements are false ?

Lemma contra_1: forall b k2 l ,
b > nth (S k2) l 0 ->
b <= max b (list_max l)-> False.

Lemma contra_2: forall b l ,
b > nth 0 l 0 ->
max b (list_max l) <= b-> False.

view this post on Zulip Lessness (Nov 10 2021 at 17:55):

No, we can't prove that your two lemmas are correct.

Require Import List.

Lemma contra_1_not_true: (forall b k2 l ,
b > nth (S k2) l 0 ->
b <= max b (list_max l)-> False) -> False.
Proof.
  intros. pose proof (H 1 0 nil). apply H0.
  + simpl. auto.
  + simpl. auto.
Qed.

Lemma contra_2_not_true: (forall b l ,
b > nth 0 l 0 ->
max b (list_max l) <= b -> False) -> False.
Proof.
  intros. pose proof (H 1 nil). apply H0.
  + simpl. auto.
  + simpl. auto.
Qed.

As you can see, I managed to prove negations of both lemmas.


Last updated: Jan 27 2023 at 00:03 UTC