The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

Hi all,

I'm having trouble with high memory usage. I've attached a
self-contained cut-down example that cann't be compiled in 900 MB:

$ ulimit -v 900000 
$ time coqc z.v       
Fatal error: out of memory.
coqc z.v  78.28s user 1.15s system 99% cpu 1:19.44 total
$ time coqc -dont-load-proofs z.v
Out of memory.
coqc -dont-load-proofs z.v  79.05s user 1.17s system 99% cpu 1:20.24 total

Essentially I have a datatype with 8 constructors, I dependently destruct
an entangled pair of them. This leaves only 17 of the 64 cases unsolved.
I admit the 17 cases and then try to save the proof.

Am I doing something silly? Is there a way to reduce the memory usage?

I have v8.3 (13693).


Thanks
Ian


Module Export z.

Require Import Equality.
Require Import List.

Parameter NameSet : Set.
Parameter SignedName : Set.
Parameter SignedNameSet : Set.
Parameter SignedNameSetIn : SignedName -> SignedNameSet -> Prop.

Parameter PatchType : NameSet -> NameSet -> Type.

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

Parameter commute : forall {from mid1 mid2 to : NameSet},
                    PatchType from mid1 -> PatchType mid1 to
                 -> PatchType from mid2 -> PatchType mid2 to -> Prop.

Parameter invert : forall {from to : NameSet}, PatchType from to -> PatchType 
to from.

Notation "<< p , q >> <~> << q' , p' >>" := (commute p q q' p')
    (at level 60, no associativity).

Inductive Sequence (from to : NameSet) : Type
    := Nil : Sequence from to
     | Cons : forall {mid : NameSet}
                     (p : PatchType from mid)
                     (qs : Sequence mid to),
              Sequence from to.
Implicit Arguments Nil [from to].
Implicit Arguments Cons [from mid to].
Notation "s :> t" := (Cons s t)
    (at level 60, right associativity).
Notation "[]" := Nil
    (no associativity).

Reserved Notation "<< ps >> <~~> << qs >>"
    (at level 60, no associativity).
Inductive CommuteRelates {from to : NameSet}
                       : Sequence from to
                      -> Sequence from to
                      -> Prop
    := SwapNow : forall {op opq oq : NameSet}
                        {p : PatchType from op}
                        {q : PatchType op opq}
                        {q' : PatchType from oq}
                        {p' : PatchType oq opq}
                        {rs : Sequence opq to},
                 <<p, q>> <~> <<q', p'>>
              -> <<p :> q :> rs>> <~~> <<q' :> p' :> rs>>
     | SwapLater : forall {mid : NameSet}
                          (p : PatchType from mid)
                          {qs : Sequence mid to}
                          {rs : Sequence mid to},
                   CommuteRelates (from := mid) qs rs
                -> CommuteRelates (p :> qs)
                                  (p :> rs)
where "<< ps >> <~~> << qs >>"
    := (@CommuteRelates _ _ ps qs).

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

Inductive ContextedPatch (from : NameSet)
                       : Type
    := MkContextedPatch : forall {mid to : NameSet}
                                 (c : Sequence from mid)
                                 (p : PatchType mid to),
                 ContextedPatch from.

Definition contextedPatch_name {from : NameSet}
                               (c : ContextedPatch from) : SignedName
 := match c with
    | MkContextedPatch _ _ _ p => pu_nameOf p
    end.
Axiom cheat : forall {a}, a.

Inductive CommutePast : forall {from mid : NameSet},
                      PatchType from mid
                   -> ContextedPatch mid
                   -> ContextedPatch from
                   -> Prop
    := CommutePastNil :
                 forall (from mid mid' to : NameSet)
                        (p : PatchType from mid)
                        (ident : PatchType mid to)
                        (ident' : PatchType from mid')
                        (p' : PatchType mid' to)
                        (H : <<p, ident>> <~> <<ident', p'>>),
                 CommutePast p
                             (MkContextedPatch _ [] ident)
                             (MkContextedPatch _ [] ident')
    |  CommutePastCons :
                 forall (o op opq opqr opqrs oq oqr oqrs : NameSet)
                        (p : PatchType o op)
                        (contextQ : PatchType op opq)
                        (contextRs : Sequence opq opqr)
                        (ident : PatchType opqr opqrs)

                        (contextQ' : PatchType o oq)
                        (contextRs' : Sequence oq oqr)
                        (ident' : PatchType oqr oqrs)
                        (p' : PatchType oq opq)

                        (H : CommutePast p'
                             (MkContextedPatch _ contextRs ident)
                             (MkContextedPatch _ contextRs' ident')),
                 CommutePast p
                             (MkContextedPatch _ (contextQ :> contextRs) 
ident)
                             (MkContextedPatch _ (contextQ' :> contextRs') 
ident').

Inductive CommuteManyPast : forall {from mid : NameSet},
                            Sequence from mid
                         -> ContextedPatch mid
                         -> ContextedPatch from
                         -> Prop
    := CommuteNilPast : forall (from : NameSet)
                               (cp : ContextedPatch from),
                        CommuteManyPast [] cp cp
     | CommuteConsPast : forall (o op opq : NameSet)
                                (p : PatchType o op)
                                (qs : Sequence op opq)
                                (cp : ContextedPatch opq)
                                (cp' : ContextedPatch op)
                                (cp'' : ContextedPatch o)
                                (CommuteQsPast : CommuteManyPast qs cp cp')
                                (CommutePPast : CommutePast p cp' cp''),
                         CommuteManyPast (p :> qs) cp cp''.

Definition addToContext {from mid : NameSet}
                        (p : PatchType from mid)
                        (c : ContextedPatch mid)
                      : ContextedPatch from
 := cheat.

Parameter addSequenceToContext :
              forall {from mid : NameSet}
                     (ps : Sequence from mid)
                     (c : ContextedPatch mid),
              ContextedPatch from.

Inductive Catch (from to : NameSet)
              : Type
    := MkCatch : forall (p : PatchType from to),
                 Catch from to
     | Conflictor : forall (effect : Sequence from to)
                           (conflicts : list (ContextedPatch to))
                           (ident : ContextedPatch to),
                    Catch from to.
Implicit Arguments MkCatch [from to].
Implicit Arguments Conflictor [from to].

Parameter invertSequence : forall {from to : NameSet}
                                  (ps : Sequence from to),
                           Sequence to from.

Inductive commuteOneMany : forall {from mid1 mid2 to : NameSet}
                                  (p   : PatchType from mid1)
                                  (qs  : Sequence mid1 to  )
                                  (qs' : Sequence from mid2)
                                  (p'  : PatchType mid2 to),
                           Prop
    := commuteOneNil :
           forall {o op : NameSet}
                  (p : PatchType o op),
           commuteOneMany p [] [] p
     | commuteOneCons :
           forall {o op opq opqr oq oqr : NameSet}
                  (p : PatchType o op)
                  (p' : PatchType oq opq)
                  (p'' : PatchType oqr opqr)
                  (q : PatchType op opq)
                  (q' : PatchType o oq)
                  (rs : Sequence opq opqr)
                  (rs' : Sequence oq oqr)
                  (pq_commute_q'p' : <<p, q>> <~> <<q', p'>>)
                  (p'qs_commute_qs'p'' : commuteOneMany p' rs rs' p''),
           commuteOneMany p (q :> rs) (q' :> rs') p''.

Inductive commuteManyOne : forall {from mid1 mid2 to : NameSet}
                                  (ps  : Sequence from mid1 )
                                  (q   : PatchType mid1 to)
                                  (q'  : PatchType from mid2)
                                  (ps' : Sequence mid2 to   ),
                           Prop
    := commuteNilOne :
           forall {o oq : NameSet}
                  (q : PatchType o oq),
           commuteManyOne [] q q []
     | commuteConsOne :
           forall {o op opq opqr or opr : NameSet}
                  (p : PatchType o op)
                  (p' : PatchType or opr)
                  (qs : Sequence op opq)
                  (qs' : Sequence opr opqr)
                  (r : PatchType opq opqr)
                  (r' : PatchType op opr)
                  (r'' : PatchType o or)
                  (qsr_commute_r'qs' : commuteManyOne qs r r' qs')
                  (pr'_commute_r''p' : <<p, r'>> <~> <<r'', p'>>),
           commuteManyOne (p :> qs) r r'' (p' :> qs').

Parameter sequenceCommute : forall {from mid mid' to : NameSet},
                            Sequence from  mid  ->
                            Sequence mid   to   ->
                            Sequence from  mid' ->
                            Sequence mid'  to   ->
                            Prop.

Parameter conflictsWith : forall {from : NameSet},
                          ContextedPatch from ->
                          ContextedPatch from ->
                          Prop.

Parameter conflictsNames : forall {from : NameSet}
                                  (conflicts : list (ContextedPatch from)),
                           SignedNameSet.

Inductive CatchCommute1
        : forall {from mid1 mid2 to : NameSet},
          Catch from mid1
       -> Catch mid1 to
       -> Catch from mid2
       -> Catch mid2 to
       -> Prop
    := MkCatchCommute1 :
           forall {from to1 to2 : NameSet}
                  (p : PatchType from to1)
                  (q : PatchType from to2)
                  (namesDifferent : pu_nameOf p <> pu_nameOf q),
           CatchCommute1 (MkCatch p)
                         (Conflictor ((invert p) :> [])
                                     (cons (MkContextedPatch _ [] p) nil)
                                     (MkContextedPatch _ [] q))
                         (MkCatch q)
                         (Conflictor ((invert q) :> [])
                                     (cons (MkContextedPatch _ [] q) nil)
                                     (MkContextedPatch _ (Nil(from := from)) 
p)).

Inductive CatchCommute2
        : forall {from mid1 mid2 to : NameSet},
          Catch from mid1
       -> Catch mid1 to
       -> Catch from mid2
       -> Catch mid2 to
       -> Prop
     := MkCatchCommute2 :
           forall {from mid to : NameSet}
                  (p : PatchType from mid)
                  (qEffect : Sequence mid to)
                  (qConflicts : list (ContextedPatch to))
                  (qIdentity : ContextedPatch to)
                  (qEffect' : Sequence from to)
                  (qConflicts' : list (ContextedPatch to))
                  (qIdentity' : ContextedPatch to)
                  (pEffect' : Sequence to to)
                  (pConflicts' : list (ContextedPatch to))
                  (pIdentity' : ContextedPatch to)
                  (namesDifferent : pu_nameOf p <> contextedPatch_name 
qIdentity)
                 ,
           <<qEffect>> <~~>* <<invert p :> qEffect'>>
        -> qConflicts = (MkContextedPatch _ (invertSequence qEffect') p) :: 
qConflicts'
        -> qIdentity' = qIdentity
        -> pEffect' = []
        -> pConflicts' = qIdentity :: nil
        -> pIdentity' = MkContextedPatch _ (invertSequence qEffect') p
        -> ~(qConflicts' = nil)
        -> CatchCommute2 (MkCatch p)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity)
                         (Conflictor qEffect'
                                     qConflicts'
                                     qIdentity')
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity').

Inductive CatchCommute3
        : forall {from mid1 mid2 to : NameSet},
          Catch from mid1
       -> Catch mid1 to
       -> Catch from mid2
       -> Catch mid2 to
       -> Prop
     := MkCatchCommute3 :
           forall {from mid to : NameSet}
                  (pEffect : Sequence from to)
                  (pConflicts : list (ContextedPatch to))
                  (pIdentity : ContextedPatch to)
                  (qEffect : Sequence to to)
                  (qConflicts : list (ContextedPatch to))
                  (qIdentity : ContextedPatch to)
                  (q' : PatchType from mid)
                  (pEffect' : Sequence mid to)
                  (pConflicts' : list (ContextedPatch to))
                  (pIdentity' : ContextedPatch to)
                  (namesDifferent : contextedPatch_name pIdentity <> 
contextedPatch_name qIdentity)
                 ,
           qEffect = []
        -> qConflicts = pIdentity :: nil
        -> qIdentity = MkContextedPatch _ (invertSequence pEffect) q'
        -> <<pEffect'>> <~~>* <<invert q' :> pEffect>>
        -> pConflicts' = (MkContextedPatch _ (invertSequence pEffect) q') :: 
pConflicts
        -> pIdentity' = pIdentity
        -> ~(pConflicts = nil)
        -> CatchCommute3 (Conflictor pEffect
                                     pConflicts
                                     pIdentity)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity)
                         (MkCatch q')
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity').
Notation "<< p , q >> <~>3 << q' , p' >>"
    := (CatchCommute3 p q q' p')
    (at level 60, no associativity).

Inductive CatchCommute4
        : forall {from mid1 mid2 to : NameSet},
          Catch from mid1
       -> Catch mid1 to
       -> Catch from mid2
       -> Catch mid2 to
       -> Prop
     := MkCatchCommute4 :
           forall {o or ors orst ort : NameSet}

                  (pEffect : Sequence o ors)
                  (pConflicts : list (ContextedPatch ors))
                  (pIdentity : ContextedPatch ors)
                  (qEffect : Sequence ors orst)
                  (qConflicts : list (ContextedPatch orst))
                  (qOtherConflicts : list (ContextedPatch orst))
                  (qIdentity : ContextedPatch orst)
                  (qEffect' : Sequence o ort)
                  (qConflicts' : list (ContextedPatch ort))
                  (qIdentity' : ContextedPatch ort)
                  (pEffect' : Sequence ort orst)
                  (pConflicts' : list (ContextedPatch orst))
                  (pIdentity' : ContextedPatch orst)
                  (commonEffect : Sequence o or)
                  (pOnlyEffect : Sequence or ors)
                  (qOnlyEffect : Sequence or ort)

                  (namesDifferent : contextedPatch_name pIdentity <> 
contextedPatch_name qIdentity),
           qConflicts = addSequenceToContext (invertSequence qEffect) 
pIdentity :: qOtherConflicts
        -> qConflicts' = map (addSequenceToContext pEffect') qOtherConflicts
        -> qIdentity' = addSequenceToContext pEffect' qIdentity
        -> pConflicts' = qIdentity :: map (addSequenceToContext 
(invertSequence qEffect)) pConflicts
        -> pIdentity' = addSequenceToContext (invertSequence qEffect) 
pIdentity
        -> sequenceCommute pOnlyEffect qEffect qOnlyEffect pEffect'
        -> ~(pConflicts = nil)
        -> ~(qConflicts' = nil)
        -> CatchCommute4 (Conflictor pEffect
                                     pConflicts
                                     pIdentity)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity)
                         (Conflictor qEffect'
                                     qConflicts'
                                     qIdentity')
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity').

Inductive CatchCommute5
        : forall {from mid1 mid2 to : NameSet},
          Catch from mid1
       -> Catch mid1 to
       -> Catch from mid2
       -> Catch mid2 to
       -> Prop
     := MkCatchCommute5 :
           forall {from mid1 mid2 to : NameSet}
                  (p : PatchType from mid1)
                  (q : PatchType mid1 to)
                  (q' : PatchType from mid2)
                  (p' : PatchType mid2 to),
           commute p q q' p' ->
           CatchCommute5 (MkCatch p) (MkCatch q) (MkCatch q') (MkCatch p').

Inductive CatchCommute6
        : forall {from mid1 mid2 to : NameSet},
          Catch from mid1
       -> Catch mid1 to
       -> Catch from mid2
       -> Catch mid2 to
       -> Prop
    := MkCatchCommute6 :
           forall {from mid1 mid2 to : NameSet}
                  (p : PatchType from mid1)
                  (qEffect : Sequence mid1 to)
                  (qConflicts : list (ContextedPatch to))
                  (qIdentity : ContextedPatch to)
                  (qEffect' : Sequence from mid2)
                  (qConflicts' : list (ContextedPatch mid2))
                  (qIdentity' : ContextedPatch mid2)
                  (p' : PatchType mid2 to)
                  (namesDifferent : pu_nameOf p <> contextedPatch_name 
qIdentity)
                  (noConflict : ~SignedNameSetIn (pu_nameOf p) 
(conflictsNames qConflicts)),
           commuteOneMany p qEffect qEffect' p' ->
           CommutePast p' qIdentity qIdentity' ->
           qConflicts' = map (addToContext p') qConflicts ->
           ~(qConflicts = nil) ->
           CatchCommute6 (MkCatch p)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity)
                         (Conflictor qEffect'
                                     qConflicts'
                                     qIdentity')
                         (MkCatch p').

Inductive CatchCommute7
        : forall {from mid1 mid2 to : NameSet},
          Catch from mid1
       -> Catch mid1 to
       -> Catch from mid2
       -> Catch mid2 to
       -> Prop
     := MkCatchCommute7 :
           forall {from mid1 mid2 to : NameSet}
                  (pEffect : Sequence from mid1)
                  (pConflicts : list (ContextedPatch mid1))
                  (pIdentity : ContextedPatch mid1)
                  (q : PatchType mid1 to)
                  (q' : PatchType from mid2)
                  (pEffect' : Sequence mid2 to)
                  (pConflicts' : list (ContextedPatch to))
                  (pIdentity' : ContextedPatch to)
                  (namesDifferent : contextedPatch_name pIdentity <> 
pu_nameOf q),
           commuteManyOne pEffect q q' pEffect' ->
           CommutePast (invert q) pIdentity pIdentity' ->
           pConflicts' = map (addToContext (invert q)) pConflicts ->
           ~(pConflicts = nil) ->
           CatchCommute7 (Conflictor pEffect
                                     pConflicts
                                     pIdentity)
                         (MkCatch q)
                         (MkCatch q')
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity').

Inductive CatchCommute8
        : forall {from mid1 mid2 to : NameSet},
          Catch from mid1
       -> Catch mid1 to
       -> Catch from mid2
       -> Catch mid2 to
       -> Prop
     := MkCatchCommute8 :
           forall {from common mid1 mid2 to : NameSet}
                  (pEffect : Sequence from mid1)
                  (pConflicts : list (ContextedPatch mid1))
                  (pIdentity : ContextedPatch mid1)
                  (qEffect : Sequence mid1 to)
                  (qConflicts : list (ContextedPatch to))
                  (qIdentity : ContextedPatch to)
                  (qEffect' : Sequence from mid2)
                  (qConflicts' : list (ContextedPatch mid2))
                  (qIdentity' : ContextedPatch mid2)
                  (pEffect' : Sequence mid2 to)
                  (pConflicts' : list (ContextedPatch to))
                  (pIdentity' : ContextedPatch to)
                  (commonEffect : Sequence from common)
                  (pOnlyEffect : Sequence common mid1)
                  (qOnlyEffect : Sequence common mid2)
                  (namesDifferent : contextedPatch_name pIdentity <> 
contextedPatch_name qIdentity),

           sequenceCommute pOnlyEffect qEffect qOnlyEffect pEffect' ->

           CommuteManyPast (invertSequence qEffect) pIdentity pIdentity' ->
           CommuteManyPast pEffect' qIdentity qIdentity' ->

           pConflicts' = map (addSequenceToContext (invertSequence qEffect)) 
pConflicts ->
           qConflicts' = map (addSequenceToContext pEffect') qConflicts ->

           ~(conflictsWith pIdentity (addSequenceToContext qEffect 
qIdentity)) ->

           ~(pConflicts = nil) ->
           ~(qConflicts = nil) ->

           CatchCommute8 (Conflictor pEffect
                                     pConflicts
                                     pIdentity)
                         (Conflictor qEffect
                                     qConflicts
                                     qIdentity)
                         (Conflictor qEffect'
                                     qConflicts'
                                     qIdentity')
                         (Conflictor pEffect'
                                     pConflicts'
                                     pIdentity').

Inductive CatchCommute
                       {from mid1 mid2 to : NameSet}
                       (p : Catch from mid1)
                       (q : Catch mid1 to)
                       (q' : Catch from mid2)
                       (p' : Catch mid2 to)
                     : Prop
    := isCatchCommute1 : forall (catchCommuteDetails : CatchCommute1 p q q' 
p'),
                         CatchCommute p q q' p'
     | isCatchCommute2 : forall (catchCommuteDetails : CatchCommute2 p q q' 
p'),
                         CatchCommute p q q' p'
     | isCatchCommute3 : forall (catchCommuteDetails : CatchCommute3 p q q' 
p'),
                         CatchCommute p q q' p'
     | isCatchCommute4 : forall (catchCommuteDetails : CatchCommute4 p q q' 
p'),
                         CatchCommute p q q' p'
     | isCatchCommute5 : forall (catchCommuteDetails : CatchCommute5 p q q' 
p'),
                         CatchCommute p q q' p'
     | isCatchCommute6 : forall (catchCommuteDetails : CatchCommute6 p q q' 
p'),
                         CatchCommute p q q' p'
     | isCatchCommute7 : forall (catchCommuteDetails : CatchCommute7 p q q' 
p'),
                         CatchCommute p q q' p'
     | isCatchCommute8 : forall (catchCommuteDetails : CatchCommute8 p q q' 
p'),
                         CatchCommute p q q' p'.
Notation "<< p , q >> <~> << q' , p' >>"
    := (CatchCommute p q q' p')
    (at level 60, no associativity).

Lemma CatchCommuteConsistent1_3 :
      forall {o op opq opqr opr oq oqr : NameSet}
             {p1 : Catch o op}
             {q1 : Catch op opq}
             {r1 : Catch opq opqr}
             {q2 : Catch opr opqr}
             {r2 : Catch op opr}
             {q3 : Catch o oq}
             {r3 : Catch oq oqr}
             {p3 : Catch oqr opqr}
             {p5 : Catch oq opq}
             (catchCommuteDetails : <<q1, r1>> <~>3 <<r2, q2>>)
             (commute2 : <<p1, q1>> <~> <<q3, p5>>)
             (commute3 : <<p5, r1>> <~> <<r3, p3>>),
      (exists or : NameSet,
       (exists r4 : Catch o or,
        (exists q4 : Catch or oqr,
         (exists p6 : Catch or opr,
          <<q3, r3>> <~> <<r4, q4>> /\
          <<p1, r2>> <~> <<r4, p6>> /\
          <<p6, q2>> <~> <<q4, p3>>)))).
Proof with auto.
intros.
dependent destruction commute2;
dependent destruction commute3;
dependent destruction catchCommuteDetails;
dependent destruction catchCommuteDetails0;
dependent destruction catchCommuteDetails1.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
admit.
Qed.

End z.