0

I am stucked by a proof using coq. I have the following definitions:

Require Import List.
Require Import Nat.

Fixpoint Inb(x: nat) (A: list nat) :=
 match A with
 | nil => false
 | h :: t => if h =? x then true else (Inb x t)
 end.

Definition In (x: nat) (A: list nat) := 
  Inb x A = true.

Then I want to proof the theorem:

Theorem inside_thm: forall x, In x (3::4::nil) -> x = 3 \/ x = 4.

However, I got stucked and no idea of how can I proof it.

Could you please give me a guide and write an example to solve it?

3 Answers 3

1

For instance, you may start with a few helpful lemmas about In.

Lemma In1 x y l : In x (y::l) <-> y = x \/ In x l. 
  Proof.    
   unfold In;  simpl; rewrite <- PeanoNat.Nat.eqb_eq. 
    case (y =? x).  
     - split;  auto. 
     - split.
       + auto. 
       + destruct 1; [discriminate | auto]. 
Qed.

Lemma In2 x : ~ In x nil. 
Proof. 
 discriminate. 
Qed. 

Then your lemma can be easily proved.

Theorem inside_thm: forall x, In x (3::4::nil) -> x = 3 \/ x = 4.
Proof.
  intros x H; rewrite In1 in H. 
  (* ... *)
1

Another, very specific, approach to proving this particular theorem could be to:

  1. first, assume that x = 3 and then show, in that case, that the statement is trivially true, after rewriting everywhere x by 3;
  2. now, under the hypothesis that x is not equalt to 3, do the same, assuming now that x = 4;
  3. finally, show that, if x is neither 3 nor 4, the statement remains valid, since, by expanding the definitions of In and Inb, you can show that all the tests in the Coq-generated if statement are false (Coq is able to unroll all the calls to Inb, since the list argument is a constant in your case), yielding false = true as an hypothesis in the goal, which makes it trivially true.
1

You have to think about how natural numbers and booleans work in Coq. The whole difficulty with boolean conditionals is that you have to establish constructively whether or not the conditional holds in order to determine the value of the expression. Likewise, a hallmark of the inductive construction of natural numbers is that you can determine (constructively) whether or not a natural number is 0, whether it is 1, whether it is 2, whether it is 3, etc., and you have to use such a chain of reasoning in order to unwind the boolean expression In x (3::4::nil) into an outcome like x = 3 ∨ x = 4.

With all that said, your proof can be done very simply by repeatedly testing whether x is 0, 1, 2, 3, ... until the proof finishes. One convenient idiom for doing so is

Theorem inside_thm: forall x, In x (3::4::nil) -> x = 3 \/ x = 4.
Proof. intros; repeat (destruct x; try intuition discriminate). Qed.

By contrast, if you're using the built-in List.In which is defined with propositional expressions, then the corresponding theorem is trivial enough for Coq to figure out by itself:

Theorem inside_thm2 : forall x, List.In x (3::4::nil) -> x = 3 \/ x = 4.
Proof. firstorder. Qed.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.