title: How to finish the TLAPS proof for a refinement mapping involving records?
body: <p>I have some difficulty in proving a refinement mapping involving records.
  Below are the simplified illustrating <a href="https://github.com/hengxin/tlaps-examples/tree/master/Record" rel="nofollow noreferrer">TLA specs@github</a> (Note that this post is also in <a href="https://groups.google.com/d/msg/tlaplus/rmmH9vFwH_0/rY18YWMGDQAJ" rel="nofollow noreferrer">tlaplus-googlegroup</a>, without replies yet.):</p>
  
  <hr>
  
  <p><code>SimpleVoting.tla:</code></p>
  
  <p>It maintains for each participant a <code>maxBal</code> which is a natural number.
  In <code>IncreaseMaxBal(p, b)</code>, <code>maxBal[p]</code> is increased to a larger value <code>b</code>.</p>
  
  <pre><code>---------------------------- MODULE SimpleVoting ----------------------------
  EXTENDS Naturals
  -----------------------------------------------------------------------------
  CONSTANT Participant
  
  VARIABLE maxBal
  
  TypeOK == maxBal \in [Participant -&gt; Nat]
  -----------------------------------------------------------------------------
  Init == maxBal = [p \in Participant |-&gt; 0]
  
  IncreaseMaxBal(p, b) ==
    /\ maxBal[p] &lt; b
    /\ maxBal' = [maxBal EXCEPT ![p] = b]
  -----------------------------------------------------------------------------
  Next == \E p \in Participant, b \in Nat : IncreaseMaxBal(p, b)
  
  Spec == Init /\ [][Next]_maxBal
  =============================================================================
  </code></pre>
  
  <hr>
  
  <p><code>Record.tla:</code></p>
  
  <p>It maintains a 2D "array" <code>state</code>, where <code>state[p][q]</code> is the State of <code>q</code> from the view of <code>p</code> and a State is a record:
  <code>State == [maxBal : Nat, maxVBal : Nat]</code>.</p>
  
  <p>In <code>Prepare(p, b)</code>, <code>state[p][p].maxBal</code> is increased to a larger value <code>b</code>.</p>
  
  <pre><code>------------------------------- MODULE Record -------------------------------
  EXTENDS Naturals, TLAPS
  ---------------------------------------------------------------------------
  CONSTANTS Participant  \* the set of partipants
  
  VARIABLES state \* state[p][q]: the state of q \in Participant from the view of p \in Participant
  
  State == [maxBal: Nat, maxVBal: Nat]
  
  TypeOK == state \in [Participant -&gt; [Participant -&gt; State]]
  ---------------------------------------------------------------------------
  InitState == [maxBal |-&gt; 0, maxVBal |-&gt; 0]
  
  Init == state = [p \in Participant |-&gt; [q \in Participant |-&gt; InitState]] 
  
  Prepare(p, b) == 
      /\ state[p][p].maxBal &lt; b
      /\ state' = [state EXCEPT ![p][p].maxBal = b]
  ---------------------------------------------------------------------------
  Next == \E p \in Participant, b \in Nat : Prepare(p, b)
  
  Spec == Init /\ [][Next]_state
  ---------------------------------------------------------------------------
  </code></pre>
  
  <hr>
  
  <p>Intuitively, <code>Record</code> maintains <code>maxBal[p]</code> of <code>SimpleVoting</code> as <code>state[p][p].maxBal</code>. Therefore, I want to show that <code>Record</code> refines <code>SimpleVoting</code> under the following refinement mapping:</p>
  
  <pre><code>maxBal == [p \in Participant |-&gt; state[p][p].maxBal]
  
  SV == INSTANCE SimpleVoting
  </code></pre>
  
  <p>However, step <code>&lt;3&gt;2</code> in the following proof fails.</p>
  
  <pre><code>THEOREM Spec =&gt; SV!Spec
    &lt;1&gt;1. Init =&gt; SV!Init
      BY DEF Init, SV!Init, maxBal, InitState
    &lt;1&gt;2. [Next]_state =&gt; [SV!Next]_maxBal
      &lt;2&gt;1. UNCHANGED state =&gt; UNCHANGED maxBal
        BY DEF maxBal
      &lt;2&gt;2. Next =&gt; SV!Next
        &lt;3&gt; SUFFICES ASSUME NEW p \in Participant, NEW b \in Nat,
                            Prepare(p, b)
                     PROVE  SV!IncreaseMaxBal(p, b)
          BY DEF Next, SV!Next
        &lt;3&gt;1. maxBal[p] &lt; b
          BY DEF Prepare, maxBal
        &lt;3&gt;2. maxBal' = [maxBal EXCEPT ![p] = b] \* failed here!
          BY DEF Prepare, maxBal
        &lt;3&gt;3. QED
          BY &lt;3&gt;1, &lt;3&gt;2 DEF SV!IncreaseMaxBal
      &lt;2&gt;3. QED
        BY &lt;2&gt;1, &lt;2&gt;2
    &lt;1&gt;3. QED
  </code></pre>
  
  <p>The obligation at <code>&lt;3&gt;2</code> is as follows. Isn't the <code>state' = [state EXCEPT ![p] = ...]</code> in the assumption the same as the conclusion <code>[p_1 \in Participant |-&gt; state[p_1][p_1].maxBal]' ...</code>? What is missing? What is wrong with my proof?</p>
  
  <pre><code>ASSUME NEW CONSTANT Participant,
         NEW VARIABLE state,
         NEW CONSTANT p \in Participant,
         NEW CONSTANT b \in Nat,
         /\ state[p][p].maxBal &lt; b
         /\ state'
            = [state EXCEPT
                 ![p] = [state[p] EXCEPT
                           ![p] = [state[p][p] EXCEPT !.maxBal = b]]] 
  PROVE  [p_1 \in Participant |-&gt; state[p_1][p_1].maxBal]'
         = [[p_1 \in Participant |-&gt; state[p_1][p_1].maxBal] EXCEPT ![p] = b]
  </code></pre>