CODEWITHSUNDEEP
coq
rosi javi
rosi javi

Reputation: 35

How to prove statement is wrong

Trying to prove the following lemma I got stuck. Usully theorems about lists are proven using induction, but I don't know where to move next. I am trying to prove a statement, which is wrong. Therefore trying to prove it false. Here is lemma statement.Plz guide me in closing this sub-lemma.

Theorem list_length :
  forall (l:list nat),
    (length l =? 0) = false ->
    (length l - length l =? 0) = false.
Proof.
  intros. induction (length l).
  simpl in *. apply H. simpl. 
  rewrite IHn0. auto.  simpl in H.

Upvotes: 0

Views: 156

Answers (2)

Yves
Yves

Reputation: 4236

As you rightly noticed, the hypothesis I named abs in my version of the script is false and you should be able to derive anything from this. The only difficulty is to make Coq see it. You need to a theorem to explain that (something - something) is always 0. I give you the search command for this. Then, you have to know that Coq will finish the proof using computation. Here, 0 =? 0 computes to true. Then abs modulo computation is true = false. The tactic discriminate has been designed specifically to finish proofs in this case.

Search (?x - ?x).

Theorem index_val_0:
  forall (l:list nat), (length l =? 0) = false ->
    (length l - length l=?0)=false-> 
    (index_value(length l - length l-1) l =? 0) = true.
Proof.
intros l lnnil abs.
Fail discriminate.
rewrite Nat.sub_diag in abs.
discriminate.
Qed.

Upvotes: 1

Tiago Campos
Tiago Campos

Reputation: 538

The first problem is that forall (l:list nat), (length l =? 0) = false -> (length l - length l =? 0) = false is unprovable if you notice the case when the length of the list is 0, is actually true but to others cases is not.

If you're trying to prove the statement but it's wrong, so you just have to negate.

Theorem list_length :
  forall (l:list nat),
    ~ (length l - length l =? 0) = false.
   intros.
   intro H.
   (*now, do your magic here *)

By now, the proof is very trivial. I will let you finish this proof now.

Upvotes: 1

Related Questions