The Coq mailing list

[<bartdevylder AT gmail.com>]

Dear listmembers,

I am puzzled why the auto tactic does not solve a subgoal which only involves
applying "apply" twice with a Hypothesis from the current context. I didn't
find a solution/explanation in the documentation or mailing lists.

Concretely, this is the state I'm stuck in:

2 subgoals
s : state
v : volumeName
H : uniqueLocation s
H0 : consistent1 s
v1 : volumeName
v2 : volumeName
H1 : v1 <> v2
______________________________________(1/2)
match s v1 with
| volstate n1 p1 _ _ =>
    match s v2 with
    | volstate n2 p2 _ _ => n1 <> n2 \/ p1 <> p2
    end
end
______________________________________(2/2)
consistent1 (attach s v)

generated by the following partial proof:

Theorem attachConsistent :
   forall s v, consistent s -> consistent (attach s v).
Proof.
intros. unfold consistent in H. destruct H.
unfold consistent. split.
unfold uniqueLocation. intros. repeat rewrite -> attachEq.

Now,
apply H. apply H1.
solves the first subgoal, but auto does not find this.

Is there any other tactic I could use in this case?

Thanks in advance,
Bart


Ps For completeness, this is the whole file (making use of the "Software
foundation library")


Require Export SfLib.
Require Import ClassicalFacts.
Require List.
Require Import LibTactics.

Definition volumeName := nat.
Definition resourceName := nat.
Definition node := nat.
Definition port := nat.

Inductive role : Type :=
  | source : role
  | target : role.

Inductive replicationConfig : Type :=
  | unreplicated : replicationConfig
  | replicated : role -> volumeName -> replicationConfig.

Inductive ip :=
   | bogus : ip
   | regular : node -> ip.

Inductive resourceConfig :=
   | resconf : resourceName -> volumeName -> ip -> port -> resourceConfig.

Inductive drbdVolumeState : Set :=
   | detached : drbdVolumeState
   | attached : resourceConfig -> drbdVolumeState.

Inductive volumeState :=
   | volstate : node -> port -> replicationConfig -> drbdVolumeState ->
volumeState.

Definition state : Set := volumeName -> volumeState.

Definition uniqueLocation (s : state) : Prop :=
   forall v1 v2, v1 <> v2 ->
      match s v1, s v2 with
          volstate n1 p1 _ _, volstate n2 p2 _ _ => n1 <> n2 \/ p1 <> p2
      end.

Definition consistent1 (s : state) : Prop :=
    forall v, match s v with
                | volstate _ _ _ detached => True
                | volstate n p _ (attached (resconf resourcename peer bogus
poort)) =>
                                              resourcename = v /\
                                              peer = v /\
                                              poort = p
                | volstate n p _ (attached (resconf resourcename peervolume
(regular peernode) poort)) =>
                             peernode <> n   (** replicated to other node **)
               end.

Definition consistent (s : state) : Prop := uniqueLocation s /\ consistent1 s.

Definition attach (s : state) (v : volumeName) : state :=
   fun w => if beq_nat v w
            then s w
            else s w.

Theorem attachEq : forall s v w, (attach s v) w = s w.
Proof.
intros.
unfold attach.
destruct (beq_nat v w); auto.
Qed.

Theorem attachConsistent :
   forall s v, consistent s -> consistent (attach s v).
Proof.
intros. unfold consistent in H. destruct H.
unfold consistent. split.
unfold uniqueLocation. intros. repeat rewrite -> attachEq.