Proving a theorem in Coq using almost only rewrites - no "cleverness"

Question

I'm trying to formulate a problem so that only rewriting will be sufficient to prove the goal. I want to avoid "clever" uses of Propositions and instead use bools that can be computed by Coq.

I define a boolean test function member that returns true iff an element is in a list, and different that returns true iff no element is in both lists.

I want to prove that I can rewrite different into an expression only using member.

Theorem different_member:  forall xs ys y,
  different xs ys = ((negb (member y ys)) || negb (member y xs)).

(The (negb X || Y) form is the boolean implication).

As a warm-up and reality check I want to prove

Theorem diff_mem:
forall xs ys,
   different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.

The way to proceed is by induction on xs, but I keep messing up on the final step.

Very grateful for some help on both of the theorems! Here is the relevant part of development.

Require Import Arith.
Require Import List.
Require Import Bool.
Import List.ListNotations.
Open Scope list.
Open Scope bool.

Fixpoint member x ys :=
  match ys with
    | [] => false
    | y :: ys' => (beq_nat x y) || (member x ys')
  end.

Lemma mem1: forall x,     member x []     = false.
Proof. auto. Qed.
Lemma mem2: forall x y l, member x (y::l) = (beq_nat x y) || (member x l).
Proof. auto. Qed.

Fixpoint different xs ys :=
  match xs with
    | [] => true
    | x::xs' => (negb (member x ys)) && (different xs' ys)
  end.

Lemma diff1: forall ys, different [] ys = true.
Proof. auto. Qed.
Lemma diff2: forall x xs ys,
               different (x::xs) ys = (negb (member x ys)) && (different xs ys).
Proof. auto. Qed.


Theorem diff_mem1: forall xs ys, different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.

Proof.
Abort.

Theorem different_member:
  forall xs ys y, different xs ys =
                ((negb (member y ys)) || negb (member y xs)).
Proof.
Abort.

EDIT:

Here is a proof of the diff_mem1 theorem. (sleeping on it, and thinking before starting to bang on it in ProofGeneral sometimes helps...). The proof of the other theorem follows the same structure.

However, the question and ultimate goal is still how to solve it entirely with rewrites and hints, so that one could (almost) do induction xs; auto..

Theorem diff_mem1: forall xs ys, 
 different xs ys = true -> forall y, member y xs = true -> ~ member y ys = true.

Proof.
  induction xs as [|a xs]; intros ys Hdiff y Hxs Hys.
  - inversion Hxs.
  - (* we assume y is a member of ys, and of (a::xs) *)
    (* it is also assumed that (a::xs) is different from ys *)
    (* consider the cases y=a and y<>a *)
    remember (beq_nat y a) as Q; destruct Q.
    + (* this case is absurd since y is a member of both ys and (y::xs) *)
      apply eq_sym in HeqQ; apply beq_nat_true in HeqQ.
      subst a.
      simpl in Hdiff.
      rewrite Hys in Hdiff.
      inversion Hdiff.
    + (* this case is also absurd since y is a member of both ys and xs *)
      simpl in Hdiff, Hxs.
      rewrite <- HeqQ in Hxs.
      simpl in Hxs.
      rewrite Bool.andb_true_iff in Hdiff; destruct Hdiff as [_ Hdiff1].
      destruct (IHxs ys Hdiff1 y Hxs Hys).
Qed.

EDIT2:

I will close this as @Arthur gave the correct answer as to why I failed in the initial attempt, but for completeness I want to add a solution along the lines of what I was aiming for.

I wrote an Ltac tactic my_simple_rewrite that does a number of try rewrite with lemma_x in * (about 20 different lemmas, that are only re-written from left to right). They are simple lemmas about bools and the mem1, mem2, diff1, and diff2 from above. To prove the theorem I used it, and only specified the induction variable xs and which bool expressions to do a case analysis on (using a home-made Ltac bool_destruct), and got the following proof.

Theorem different_member:
  forall xs ys, different xs ys = true ->
                forall y, ((negb (member y ys)) || negb (member y xs)) = true.
Proof.
  induction xs as [| a xs]; intros; my_simple_rewrite.
  - congruence.
  - try
      match goal with
        | [ HH:_ |- _] => (generalize (IHxs ys HH y); intro IH)
      end;
    bool_destruct (member a ys);
    bool_destruct (member y ys);
    bool_destruct (member a xs);
    bool_destruct (member y xs);
    bool_destruct (beq_nat y a);
    my_simple_rewrite;
    congruence.
Qed.

The idea is that this can almost be automated. Picking which terms to destruct can be automated, and notice that it tries to instantiate the induction hypotheisis with anything it can throw a stick at - ("if it works, fine! otherwise try the next alternative...").

For future reference, the full development is in https://gist.github.com/larsr/10b6f4817b5117b335cc

Answer 1

The problem with your result is that it doesn't hold. For instance, try

Compute different [2] [1; 2]. (* false *)
Compute (negb (member 1 [2]) || negb (member 1 [1; 2])). (* true *)

This happens because, in order to obtain the converse, we need the right-hand side to be valid for all y. The correct form is:

forall xs ys,
  different xs ys = true <-> 
  (forall y, negb (member y xs) || negb (member x xs)).

Nevertheless, you are right that specifying certain results as boolean equations makes them more convenient to use in many situations. This style is heavily used, for instance, in the Ssreflect library, where they write theorems such as:

eqn_leq : forall m n, (m == n) = (m <= n) && (n <= m)

Here, the == and <= operators are booelan functions that test for equality and order on natural numbers. The first one is generic, and works for any type that is declared with a boolean equality function, called eqType in Ssreflect.

Here's a version of your theorem using Ssreflect:

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool.
Require Import Ssreflect.ssrnat Ssreflect.eqtype Ssreflect.seq.

Section Different.

Variable T : eqType.
Implicit Types xs ys : seq T.

Fixpoint disjoint xs ys :=
  match xs with
  | [::]     => true
  | x :: xs' => (x \notin ys) && disjoint xs' ys
  end.

Lemma disjointP xs ys :
  reflect (forall x, x \in xs -> x \notin ys)
          (disjoint xs ys).
Proof.
elim: xs=> [|x xs IH] /=; first exact: ReflectT.
apply/(iffP andP)=> [[x_nin /IH {IH} IH] x'|xsP].
  by rewrite inE=> /orP [/eqP ->|] //; auto.
apply/andP; rewrite xsP /= ?inE ?eqxx //.
apply/IH=> x' x'_in; apply: xsP.
by rewrite inE x'_in orbT.
Qed.

End Different.

I've renamed different to disjoint, and have used the Ssreflect list membership operators \in and \notin, available for lists with elements in any eqType. Note that the statement of disjointP has an implicit conversion from bool to Prop (which maps b to b = true), and that it is stated with the reflect predicate, which you can think of as being like the "if and only if" connective, but relating a Prop to a bool.

Ssreflect makes extensive use of reflect predicate and the view mechanism (the / signs you see on the proof script) to convert between boolean and propositional statements of the same fact. Thus, although we can't state the equivalence with a plain boolean equality, we can keep much of the convenience with the reflect predicate. For instance:

Goal forall n, n \in [:: 1; 2; 3] -> n \notin [:: 4; 5; 6].
Proof. by apply/disjointP. Qed.

What happened here is that Coq used disjointP to convert the above goal to disjoint [:: 1; 2; 3] [:: 4; 5; 6] (the [:: ... ] is just Ssreflect notation for lists), and could find that that goal was true just by computation.