The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I have the following proof state:

s : state
H : realizeState
      (@AbsPredicate (@nil absType) ((!!P) ==== @AbsNatVal (@nil absType) 0) **
       @AbsExists (@nil absType) AbsNat
         (@AbsPredicate (AbsNat :: @nil absType)
            (@AbsEqualD AbsNat (AbsNat :: @nil absType) IsAbsNat AbsNat
               (!!T) (!!RR)) **
          @AbsExists (AbsNat :: @nil absType) AbsNat
            (@AbsPredicate (AbsNat :: AbsNat :: @nil absType)
               (@AbsEqualD AbsNat (AbsNat :: AbsNat :: @nil absType) IsAbsNat
                  AbsNat (!!I)
                  (@AbsNatValD AbsNat (AbsNat :: AbsNat :: @nil absType)
                     IsAbsNat 0)) **
             @AbsExists (AbsNat :: AbsNat :: @nil absType) AbsNat
               (@AbsR (AbsNat :: AbsNat :: AbsNat :: @nil absType) (!!RR)
                  Size_t (F_l :: F_r :: @nil nat)
                  (@AbsHeapValD AbsHeap
                     (AbsNat :: AbsNat :: AbsNat :: @nil absType) IsAbsHeap
                     h1))))) s
H2 : @hasV0State (@nil absType ++ AbsNat :: @nil absType)
       (@AbsExists (AbsNat :: @nil absType) AbsNat
          (@AbsPredicate (AbsNat :: AbsNat :: @nil absType)
             (@AbsEqualD AbsNat (AbsNat :: AbsNat :: @nil absType) IsAbsNat
                AbsNat (!!I)
                (@AbsNatValD AbsNat (AbsNat :: AbsNat :: @nil absType)
                   IsAbsNat 0)) **
           @AbsExists (AbsNat :: AbsNat :: @nil absType) AbsNat
             (@AbsR (AbsNat :: AbsNat :: AbsNat :: @nil absType) (!!RR)
                Size_t (F_l :: F_r :: @nil nat)
                (@AbsHeapValD AbsHeap
                   (AbsNat :: AbsNat :: AbsNat :: @nil absType) IsAbsHeap h1))))
______________________________________(1/1)
False

I then do an "inversion H2" and get the following result:

1 subgoal
h1 : heap
h2 : heap
h3 : heap
s : state
H : realizeState
      (@AbsPredicate (@nil absType) ((!!P) ==== @AbsNatVal (@nil absType) 0) **
       @AbsExists (@nil absType) AbsNat
         (@AbsPredicate (AbsNat :: @nil absType)
            (@AbsEqualD AbsNat (AbsNat :: @nil absType) IsAbsNat AbsNat
               (!!T) (!!RR)) **
          @AbsExists (AbsNat :: @nil absType) AbsNat
            (@AbsPredicate (AbsNat :: AbsNat :: @nil absType)
               (@AbsEqualD AbsNat (AbsNat :: AbsNat :: @nil absType) IsAbsNat
                  AbsNat (!!I)
                  (@AbsNatValD AbsNat (AbsNat :: AbsNat :: @nil absType)
                     IsAbsNat 0)) **
             @AbsExists (AbsNat :: AbsNat :: @nil absType) AbsNat
               (@AbsR (AbsNat :: AbsNat :: AbsNat :: @nil absType) (!!RR)
                  Size_t (F_l :: F_r :: @nil nat)
                  (@AbsHeapValD AbsHeap
                     (AbsNat :: AbsNat :: AbsNat :: @nil absType) IsAbsHeap
                     h1))))) s
H2 : @hasV0State (@nil absType ++ AbsNat :: @nil absType)
       (@AbsExists (AbsNat :: @nil absType) AbsNat
          (@AbsPredicate (AbsNat :: AbsNat :: @nil absType)
             (@AbsEqualD AbsNat (AbsNat :: AbsNat :: @nil absType) IsAbsNat
                AbsNat (!!I)
                (@AbsNatValD AbsNat (AbsNat :: AbsNat :: @nil absType)
                   IsAbsNat 0)) **
           @AbsExists (AbsNat :: AbsNat :: @nil absType) AbsNat
             (@AbsR (AbsNat :: AbsNat :: AbsNat :: @nil absType) (!!RR)
                Size_t (F_l :: F_r :: @nil nat)
                (@AbsHeapValD AbsHeap
                   (AbsNat :: AbsNat :: AbsNat :: @nil absType) IsAbsHeap h1))))
s0 : @absState
       ((@nil absType ++ AbsNat :: @nil absType) ++ AbsNat :: @nil absType)
H1 : @hasV0State
       ((@nil absType ++ AbsNat :: @nil absType) ++ AbsNat :: @nil absType)
       s0
H0 : @existT absType
       (fun v : absType => @absState (AbsNat :: v :: @nil absType)) AbsNat s0 =
     @existT absType
       (fun v : absType => @absState (AbsNat :: v :: @nil absType)) AbsNat
       (@AbsPredicate (AbsNat :: AbsNat :: @nil absType)
          (@AbsEqualD AbsNat (AbsNat :: AbsNat :: @nil absType) IsAbsNat
             AbsNat (!!I)
             (@AbsNatValD AbsNat (AbsNat :: AbsNat :: @nil absType) IsAbsNat
                0)) **
        @AbsExists (AbsNat :: AbsNat :: @nil absType) AbsNat
          (@AbsR (AbsNat :: AbsNat :: AbsNat :: @nil absType) (!!RR) Size_t
             (F_l :: F_r :: @nil nat)
             (@AbsHeapValD AbsHeap
                (AbsNat :: AbsNat :: AbsNat :: @nil absType) IsAbsHeap h1)))
______________________________________(1/1)
False

Notice the introduction of "@existT".  H0 appears to be a hypothesis that should be able to deduce

s0 = @existT absType
       (fun v : absType => @absState (AbsNat :: v :: @nil absType)) AbsNat
       (@AbsPredicate (AbsNat :: AbsNat :: @nil absType)
          (@AbsEqualD AbsNat (AbsNat :: AbsNat :: @nil absType) IsAbsNat
             AbsNat (!!I)
             (@AbsNatValD AbsNat (AbsNat :: AbsNat :: @nil absType) IsAbsNat
                0)) **
        @AbsExists (AbsNat :: AbsNat :: @nil absType) AbsNat
          (@AbsR (AbsNat :: AbsNat :: AbsNat :: @nil absType) (!!RR) Size_t
             (F_l :: F_r :: @nil nat)
             (@AbsHeapValD AbsHeap
                (AbsNat :: AbsNat :: AbsNat :: @nil absType) IsAbsHeap h1)))

This would allow me to finish the rest of my proof.  Can someone give me a tip on how to use H to the above equality?  Below are some other definitions that may be useful in understanding this problem.

Inductive absExp {ret : absType} {vars : list absType} : Type :=
   | AbsNatValD : forall pf:(ret=AbsNat), nat -> absExp
   | AbsHeapValD : forall pf:(ret=AbsHeap), heap -> absExp
   | AbsVar : id -> absExp
   | AbsQVar : absVar vars ret -> absExp
   | AbsHeapRefD : forall pf:(ret=AbsNat), @absExp ret vars -> @absExp ret vars
   | AbsPlusD : forall pf:(ret=AbsNat), @absExp ret vars -> @absExp ret vars -> @absExp ret vars
   | AbsMinusD : forall pf:(ret=AbsNat), @absExp ret vars -> @absExp ret vars -> @absExp ret vars
   | AbsTimesD : forall pf:(ret=AbsNat), @absExp ret vars -> @absExp ret vars -> @absExp ret vars
   | AbsEqualD : forall pf:(ret=AbsNat), forall t, @absExp t vars -> @absExp t vars -> @absExp ret vars
   | AbsLessD : forall pf:(ret=AbsNat), @absExp ret vars -> @absExp ret vars -> @absExp ret vars
   | AbsRMemberD : forall pf:(ret=AbsNat), @absExp AbsNat vars -> @absExp AbsNat vars -> nat -> list nat -> @absExp AbsHeap vars -> @absExp ret vars
   | AbsRIncludeD : forall pf:(ret=AbsNat), @absExp AbsNat vars -> @absExp AbsNat vars -> nat -> list nat -> @absExp AbsHeap vars ->  @absExp ret vars
   | AbsImplyD : forall pf:(ret=AbsNat), @absExp AbsNat vars -> @absExp AbsNat vars -> @absExp ret vars
   | AbsNotD : forall pf:(ret=AbsNat), @absExp AbsNat vars -> @absExp ret vars
   | AbsAndD : forall pf:(ret=AbsNat), @absExp AbsNat vars -> @absExp AbsNat vars -> @absExp ret vars
   | AbsOrD : forall pf:(ret=AbsNat), @absExp AbsNat vars -> @absExp AbsNat vars -> @absExp ret vars.

Inductive absState {vars : list absType} : Type :=
   | AbsPredicate : @absExp AbsNat vars -> absState
   | AbsExists : forall v, @absState (vars++(v::nil)) -> absState
   | AbsAll : forall v, @absState (vars++(v::nil)) -> absState
   | AbsCompose : absState -> absState -> absState
   | AbsEmpty : absState
   | AbsCell : @absExp AbsNat vars -> @absExp AbsNat vars -> absState
   | AbsR : @absExp AbsNat vars -> nat -> list nat -> @absExp AbsHeap vars -> absState.

Fixpoint hasV0Exp t tr (e : @absExp t tr) : bool :=
   match e with
   | AbsNatValD t v => false
   | AbsHeapValD t v => false
   | AbsVar vv => false
   | AbsQVar v => match v with
                  | V0 _ _ => true
                  | _ => false
                  end
   | AbsHeapRefD ttt e => hasV0Exp t tr e
   | AbsPlusD ttt l r => if hasV0Exp t tr l then true else hasV0Exp t tr r
   | AbsMinusD ttt l r => if hasV0Exp t tr l then true else hasV0Exp t tr r
   | AbsTimesD ttt l r => if hasV0Exp t tr l then true else hasV0Exp t tr r
   | AbsEqualD ttt r e1 e2 => if hasV0Exp r tr e1 then true else hasV0Exp r tr e2
   | AbsLessD ttt e1 e2 => if hasV0Exp t tr e1 then true else hasV0Exp t tr e2
   | AbsRMemberD ttt element root size fields heap =>
                if hasV0Exp AbsNat tr element then true
                else if hasV0Exp AbsNat tr root then true
                else hasV0Exp AbsHeap tr heap
   | AbsRIncludeD ttt element root size fields heap =>
                if hasV0Exp AbsNat tr element then true
                else if hasV0Exp AbsNat tr root then true
                else hasV0Exp AbsHeap tr heap
   | AbsImplyD ttt p q => if hasV0Exp AbsNat tr p  then true else hasV0Exp AbsNat tr q
   | AbsNotD ttt p => hasV0Exp AbsNat tr p
   | AbsAndD ttt p q => if hasV0Exp AbsNat tr p then true else hasV0Exp AbsNat tr q
   | AbsOrD ttt p q => if hasV0Exp AbsNat tr p then true else hasV0Exp AbsNat tr q
   end.

Inductive hasV0State {tr : list absType} : (@absState tr) -> Prop :=
  | H0SCompose1 : forall s1 s2,
                  hasV0State s1 ->
                  hasV0State (AbsCompose s1 s2)
  | H0SCompose2 : forall s1 s2,
                  hasV0State s2 ->
                  hasV0State (AbsCompose s1 s2)
  | H0SExistsN : forall s,
                 @hasV0State (tr++(AbsNat::nil)) s ->
                 hasV0State (AbsExists AbsNat s)
  | H0SExistsH : forall s,
                 @hasV0State (tr++(AbsHeap::nil)) s ->
                 hasV0State (AbsExists AbsHeap s)
  | H0SAllN : forall s,
              @hasV0State (tr++(AbsNat::nil)) s ->
              hasV0State (AbsAll AbsNat s)
  | H0SAllH : forall s,
              @hasV0State (tr++(AbsHeap::nil)) s ->
              hasV0State (AbsAll AbsHeap s)
  | H0SPredicate: forall p, hasV0Exp AbsNat tr p=true -> hasV0State (AbsPredicate p)
  | AbsCellD1 : forall loc v, (hasV0Exp AbsNat tr loc=true) -> hasV0State (AbsCell loc v)
  | AbsCellD2 : forall loc v, (hasV0Exp AbsNat tr v=true) -> hasV0State (AbsCell loc v)
  | AbsRD1 : forall root size fields heap, hasV0Exp AbsNat tr root=true -> hasV0State (AbsR root size fields heap)
  | AbsRD2 : forall root size fields heap, hasV0Exp AbsHeap tr heap=true -> hasV0State (AbsR root size fields heap).


                                                   - Ken