The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

I am stuck, with a goal:
    << p :> s >> <~~>* << p :> s >>
which I want to prove with
    apply Same.
where Same is defined as:
    := Same : forall (s : Sequence patchUniverse from to contains),
              (<<s>> <~~>* <<s>>)

Unfortunately, this fails with
    Error: Impossible to unify "p :> s" with "p :> s".
as the two (p :> s) terms are not as identical as they appear. With
notations off, they differ in the obligation functions that they
contain:
    Error: Impossible to unify
 "Cons p s
    (EnlargeTransitiveCommuteRelation2_obligation_4 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)
    (EnlargeTransitiveCommuteRelation2_obligation_5 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)
    (EnlargeTransitiveCommuteRelation2_obligation_6 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)" with
 "Cons p s
    (EnlargeTransitiveCommuteRelation2_obligation_1 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)
    (EnlargeTransitiveCommuteRelation2_obligation_2 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)
    (EnlargeTransitiveCommuteRelation2_obligation_3 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)".

I can see why it doesn't work, but I can't see how I can reasonably
solve it. Has anyone got any suggestions please? I've attached the
cut-down example.


Thanks
Ian


Module Export patch_universes.

Require Import Program.
Require Export FSets.
Require Export FSetDecide.
Require Export FSetProperties.
Require Import FSetWeakList.

Parameter Name : Set.
Axiom eq_Name_dec : forall (n : Name) (o : Name), {n = o} + {n <> o}.

Inductive Sign : Set
    := Positive | Negative.

Inductive SignedName : Set
    := MkSignedName : forall (s : Sign)
                             (n : Name),
                      SignedName.

Lemma eq_SignedName_dec : forall (sn1 : SignedName) (sn2 : SignedName),
                          {sn1 = sn2} + {sn1 <> sn2}.
Proof with auto.
intros.
destruct sn1;
destruct s;
destruct sn2;
destruct s.
            destruct (eq_Name_dec n n0).
                left.
                f_equal...
            right.
            intro.
            inversion H...
        right.
        intro.
        inversion H...
    right.
    intro.
    inversion H...
destruct (eq_Name_dec n n0).
    left.
    f_equal...
right.
intro.
inversion H...
Qed.

Module DecidableName.
Definition t := Name.
Definition eq := @eq Name.
Definition eq_refl := @refl_equal Name.
Definition eq_sym := @sym_eq Name.
Definition eq_trans := @trans_eq Name.
Definition eq_dec := eq_Name_dec.
End DecidableName.

Module NameSetMod := Make(DecidableName).

Notation NameSet := (NameSetMod.t).
Notation NameSetEqual := (NameSetMod.Equal).

Module NameSetDec := WDecide (NameSetMod).

Module DecidableSignedName.
Definition t := SignedName.
Definition eq := @eq SignedName.
Definition eq_refl := @refl_equal SignedName.
Definition eq_sym := @sym_eq SignedName.
Definition eq_trans := @trans_eq SignedName.
Definition eq_dec := eq_SignedName_dec.
End DecidableSignedName.

Module SignedNameSetMod := Make(DecidableSignedName).
Notation SignedNameSet := (SignedNameSetMod.t).
Notation SignedNameSetIn := (SignedNameSetMod.In).
Notation SignedNameSetAdd := (SignedNameSetMod.add).
Notation SignedNameSetRemove := (SignedNameSetMod.remove).
Notation SignedNameSetEqual := (SignedNameSetMod.Equal).
Notation SignedNameSetEqRefl := (SignedNameSetMod.eq_refl).

Record PatchUniverse : Type := mkPatchUniverse {
    pu_type : (NameSet -> NameSet -> Set);

    pu_nameOf : forall {from to : NameSet}, pu_type from to -> SignedName
}.

Inductive Sequence (patchUniverse : PatchUniverse)
                   (from to : NameSet)
                   (contains : SignedNameSet)
                 : Type
    := Nil : forall (fromEqTo : NameSetEqual from to)
                    (containsNothing : SignedNameSetEqual contains 
SignedNameSetMod.empty),
             Sequence patchUniverse from to contains
     | Cons : forall {from' mid : NameSet}
                     {qsContains : SignedNameSet}
                     (p : (pu_type patchUniverse) from' mid)
                     (qs : Sequence patchUniverse mid to qsContains)
                     (fromOK : NameSetEqual from from')
                     (notAlreadyThere : ~ SignedNameSetIn (pu_nameOf _ p) 
qsContains)
                     (containsOK : SignedNameSetEqual
                                       contains
                                       (SignedNameSetAdd (pu_nameOf _ p) 
qsContains)),
              Sequence patchUniverse from to contains.
Implicit Arguments Nil [patchUniverse from to contains].
Implicit Arguments Cons [patchUniverse from to contains from' mid qsContains].
Notation "s :> t" := (Cons s t _ _ _)
    (at level 60, right associativity).
Notation "[]" := (Nil _ _)
    (no associativity).

(* This is an over-simplified dummy definition. We only care
   about the transitive relation below. *)
Reserved Notation "<< p >> <~~> << q >>"
    (at level 60, no associativity).
Inductive CommuteRelates {patchUniverse : PatchUniverse}
                         {from to : NameSet}
                         {contains : SignedNameSet}
                       : Sequence patchUniverse from to contains
                      -> Sequence patchUniverse from to contains
                      -> Prop
    := SwapCheat : forall (ps qs : Sequence patchUniverse from to contains),
                   (<<ps>> <~~> <<qs>>)
where "<< p >> <~~> << q >>" := (@CommuteRelates _ _ _ _ p q).

Reserved Notation "<< p >> <~~>* << q >>"
    (at level 60, no associativity).
Inductive TransitiveCommuteRelates {patchUniverse : PatchUniverse}
                                   {from to : NameSet}
                                   {contains : SignedNameSet}
                       : Sequence patchUniverse from to contains
                      -> Sequence patchUniverse from to contains
                      -> Prop
    := Same : forall (s : Sequence patchUniverse from to contains),
              (<<s>> <~~>* <<s>>)
     | Swap : forall {s : Sequence patchUniverse from to contains}
                     {t : Sequence patchUniverse from to contains}
                     {u : Sequence patchUniverse from to contains},
              (<<s>> <~~> <<t>>)
           -> (<<t>> <~~>* <<u>>)
           -> (<<s>> <~~>* <<u>>)
where "<< p >> <~~>* << q >>" := (@TransitiveCommuteRelates _ _ _ _ p q).

Program Lemma EnlargeTransitiveCommuteRelation1 :
    forall {patchUniverse : PatchUniverse}
           {from mid to : NameSet}
           {contains contains' : SignedNameSet}
           {p : (pu_type patchUniverse) from mid}
           {qs rs : Sequence patchUniverse mid to contains'}
           (pNotInTail : ~ SignedNameSetIn (pu_nameOf _ p) contains')
           (containsOK : SignedNameSetEqual
                             contains
                             (SignedNameSetAdd
                                 (pu_nameOf _ p)
                                 contains')),
    (<<qs>> <~~>* <<rs>>)
 -> (<< (Cons p qs (NameSetMod.eq_refl _) pNotInTail containsOK) >> <~~>*
     << (Cons p rs (NameSetMod.eq_refl _) pNotInTail containsOK) >>).
Proof with auto.
intros patchUniverse from mid to contains contains' p qs rs ? ? qs_rs.
induction qs_rs.
    apply Same.
admit. (* This isn't the interesting branch, so cheat *)
Qed.

Program Definition EnlargeTransitiveCommuteRelation2 :
    forall {patchUniverse : PatchUniverse}
           {from mid to : NameSet}
           {contains contains' : SignedNameSet}
           {p : (pu_type patchUniverse) from mid}
           {qs rs : Sequence patchUniverse mid to contains'}
           (pNotInTail : ~ SignedNameSetIn (pu_nameOf _ p) contains')
           (containsOK : SignedNameSetEqual
                             contains
                             (SignedNameSetAdd
                                 (pu_nameOf _ p)
                                 contains'))
           (pqs := (p :> qs) : Sequence patchUniverse from to contains)
           (prs := (p :> rs) : Sequence patchUniverse from to contains),
    (<<qs>> <~~>* <<rs>>)
 -> (<< pqs >> <~~>* << prs >>) := _.
Next Obligation.
NameSetDec.fsetdec.
Qed.
Next Obligation.
NameSetDec.fsetdec.
Qed.
Next Obligation.
induction H.
    apply Same.

(*
Last line fails.
Goal: << p :> s >> <~~>* << p :> s >>
Fails with: Error: Impossible to unify "p :> s" with "p :> s".

Same is defined as:
    := Same : forall (s : Sequence patchUniverse from to contains),
              (<<s>> <~~>* <<s>>)

With notations off, the error is:
Error: Impossible to unify
 "Cons p s
    (EnlargeTransitiveCommuteRelation2_obligation_4 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)
    (EnlargeTransitiveCommuteRelation2_obligation_5 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)
    (EnlargeTransitiveCommuteRelation2_obligation_6 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)" with
 "Cons p s
    (EnlargeTransitiveCommuteRelation2_obligation_1 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)
    (EnlargeTransitiveCommuteRelation2_obligation_2 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)
    (EnlargeTransitiveCommuteRelation2_obligation_3 patchUniverse from mid to
       contains contains' p s s pNotInTail containsOK)".
*)