Search code examples
coq

Proving a theorem containing not exists

I try to prove a theorem from a paper I'm reading (Bennett, Having a Part Twice Over, 2013), but I don't know how to solve a subgoal.

Here is the code that I am supposed to use for the proof:

Parameter Entity: Set.
Parameter F : Entity -> Entity -> Prop.
Parameter Ps : Entity -> Entity -> Prop.
Definition P x y := exists s, F x s /\ Ps s y.
Definition PP x y := P x y /\ ~ P y x.
Definition PPs x y := Ps x y /\ ~ F y x.
   
(* Mutual Occupancy is Identity *)
Axiom A6 : forall x y z1 z2,
  (Ps z1 y /\ F x z1) /\ (Ps z2 x /\ F y z2) -> x = y.

(* Single Occupancy *)
Axiom A7 : forall x y,
  Ps x y -> exists! z, F z x.

(* Anti-Symmetry *)
Theorem T8 : forall x y,
  (P x y /\ P y x) -> x = y.
Proof.
  unfold P.
  firstorder.
  apply A6 with (z1 := x1) (z2 := x0).
  auto.
Qed.

And here is the theorem and my incomplete proof:

(* Composites <-> Slot-Composites *)
Theorem T12 : forall y,
  ((exists x, PP x y) <-> (exists z, PPs z y)).
Proof.
  unfold PP; unfold PPs; unfold P.
  intro b.
  split.
  (* left to right *)
  - intro Ea.
    destruct Ea as (a, PPab).
    destruct PPab as (Pab, nPba).
    destruct Pab as (c, Pab).
    destruct Pab as (Fac, Pscb).
    exists c.
    split.
    -- apply Pscb.
    -- admit.           (* Here! *)
  (* right to left *)
  - intro Ea.
    destruct Ea as (a, PPsab).
    destruct PPsab as (Psab, nFba).
    apply A7 in Psab as Ec.
    destruct Ec as (c, Fca).
    destruct Fca as (Fca, Uc).
    exists c.
    split.
    -- exists a.
       split.
       --- apply Fca.
       --- apply Psab.
    -- admit.            (* And here! *)
Admitted.

So there are two subgoals that I can't prove. In each, there is ~ (exists s : Entity, F b s /\ Ps s a) either as an hypothesis or as the subgoal. I am stuck at this point. According to the proof in the paper, I'm supposed to used at some point theorem T8, but I don’t understand how.

The state on first unsolved subgoal is

1 subgoal
b, a, c : Entity
Fac : F a c
Pscb : Ps c b
nPba : ~ (exists s : Entity, F b s /\ Ps s a)
______________________________________(1/1)
~ F b c

On the second one:

1 subgoal
b, a : Entity
Psab : Ps a b
c : Entity
Fca : F c a
Uc : forall x' : Entity, F x' a -> c = x'
nFba : ~ F b a
______________________________________(1/1)
~ (exists s : Entity, F b s /\ Ps s c)

As a guide, here is the proof written in the paper: enter image description here enter image description here

So how am I supposed to do? (If the answer could use simple tactics instead of super-powerful and automatic tactics, it’s better. This way I could understand.)

Solution

  • It turns out that you have everything you need to finish you goal. Here is a proof of you theorem, voluntarily not automated. Some insights:

    • Not-formulas ~P are actually equal to P -> False and you can treat them as so (using intros, apply, etc). You can see this if you try to unfold not itself.
    • You can group unfolds: unfold P, PP, PPs
    • You can intros and destruct at the same time : intros [A B] is equivalent to intros H. destruct H as (A,B).
    • You can chain tactics with ;: tactic1; tactic2. If tactic1 creates several subgoals, then tactic2 will be applied to every one.
    • When a tactic (like split) creates several subgoals, you can also use different tactics for every branch by using split; [ tactic1 | tactic2 ]. Works also if your tactic creates more than 2 goals.
    • pose proof allows you to add a result to your hypothesis without applying it directly to the goal (contrary yo apply)
    • assert (H: _) or assert _ as H allows you to do forward reasoning: you can state a result that you want. It will create two goals, one for the stated result, and one for the previous goal with the result as an added hypothesis H
    (* Composites <-> Slot-Composites *)
Theorem T12 : forall y,
  ((exists x, PP x y) <-> (exists z, PPs z y)).
Proof.
  unfold PP, PPs, P. (* you can group unfolds *)
  intros b.
  split.
  - intros [a [[c [Fac Pscb]] nPba]]. (* using brackets allows you to destruct and intros at the same time *)
    exists c.
    split; [ assumption |]. 
    pose proof (A7 _ _ Pscb) as [d [Fdc Uc]].
    intros Fbc. 
    pose proof (Uc a Fac). subst.
    pose proof (Uc b Fbc). subst. 
    apply nPba.
    exists c; split.
    + apply Fbc.
    + apply Pscb.
  - intros [a [Psab nFba]].
    pose proof (A7 _ _ Psab) as [c [Fca Uc]].
    exists c.
    split.
    + exists a; split; eauto.
    + intros [d [Fbd Psdc]].
      apply nFba.
      assert (b = c) as Heqbc.
      * (* proof of b = c *)
        eapply A6 with (z1 := d) (z2 := a).
        repeat split; assumption.
      * rewrite Heqbc in *.
        apply Fca.        
Qed.

    If you are doing a large development around those results, you'll probably find it useful to define your own automated tactics for the goals (or rewrites) you encounter often. Some Coq libraries are also designed for helping you shortening proofs, like SSReflect (https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#) or LibTactics (https://softwarefoundations.cis.upenn.edu/sf-4.0/UseTactics.html) for example. They require to learn a few more keywords and techniques than vanilla Coq, but are very useful. For the sake of the example, a little more automated proof could look something like this using SSReflect :

    (* Composites <-> Slot-Composites *)
Theorem T12 : forall y,
  ((exists x, PP x y) <-> (exists z, PPs z y)).
Proof.
  unfold PP, PPs, P => b; split.
  - move => [a [[c [Fac Pscb]] nPba]].
    move : (A7 Pscb) => [d [Fdc Uc]].
    exists c; split => // => Fbc.
    apply nPba.
    exists c; split => //.
    rewrite -(Uc _ Fac) (Uc _ Fbc) => //.
  - move => [a [Psab nFba]].
    move: (A7 Psab) => [c [Fca Uc]].
    exists c; split; eauto.
    move => [d [Fbd Psdc]].
    assert (b = c) ; subst; eauto using A6.
Qed.

    Feel free to comment other questions that you may have !

    Clement