title: Coq: Comparing an Int to a Nat in Separation Logic Foundations
body: <p>Going through <a href="https://softwarefoundations.cis.upenn.edu/slf-current/toc.html" rel="nofollow noreferrer">Separation Logic Foundations</a> and I'm stuck on the exercise triple_mlength in <a href="https://softwarefoundations.cis.upenn.edu/slf-current/Repr.html" rel="nofollow noreferrer">Repr.v</a>. I think my current problem is that I don't know how to handle ints and nats in Coq.</p>
  <pre><code>Lemma triple_mlength: forall (L: list val) (p:loc),
  triple (mlength p)
         (MList L p)
         (fun r =&gt; \[r = val_int (length L)] \* (MList L p))
  </code></pre>
  <p>Check (fun L =&gt; val_int (length L)) doesn't throw an error, so that means length is capable of being an int. However, length is opaque and I can't unfold it.</p>
  <p>My current context and goal:</p>
  <pre><code>x : val
  p : loc
  C : p &lt;&gt; null
  x0 : loc
  H : p &lt;&gt; null
  xs : list val
  IH : forall y : list val,
       list_sub y (x :: xs) -&gt;
       forall p, triple (mlength p) 
                        (MList y p) 
                        (fun r:val =&gt; \[r = length y] \* MList y p)
  ______________________________________________________________
  length xs + 1 = length (x :: xs)
  </code></pre>
  <p>Unsetting print notation the goal transforms into:</p>
  <pre><code>eq (Z.add (length xs) (Zpos xH)) (length (cons x xs))
  </code></pre>
  <p>which I think is trying to add (1:Z) to (length xs: nat), then compare it to (length (cons x xs) : nat)</p>
  <p>Types:</p>
  <pre><code>Inductive nat : Set := O : nat
                       | S : nat -&gt; nat
  
  Inductive Z : Set := Z0 : int 
                     | Zpos : positive -&gt; int 
                     | Zneg : positive -&gt; int
  
  list: forall A, list A -&gt; nat
  
  length: forall A, list A -&gt; nat
  
  val_int: int -&gt; val
  </code></pre>
  <p>Coq version is 8.12.2</p>