sara lee (Nov 10 2021 at 17:41): 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.
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: Oct 13 2024 at 01:02 UTC