The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

(*

Hello all,
This should be a runnable script.

A Coq Puzzle.

Let's say I'm trying to model simple data structures in a computer's
memory. Assume the memory is made up of pairs of cells (words). Each
word contains either a single integer data, or a pointer to another
pair of words. Thus, I have definitions:

*)

Inductive Set Word := data : nat -> Word | ptr : nat -> Word.
Definition Memory := nat -> (option (Word * Word)).

(*
Now, what I'm trying to do is, given two memories, to find out if the
structure of the data in them is the same. That is, let's say memory A
maps:

  l1 -> ((ptr l2), (ptr l3))
  l2 -> ((ptr l1), (data 0))
  l3 -> ((data 1), (ptr l2))

And memory A' maps:

  l1' -> ((ptr l2'), (ptr l3'))
  l2' -> ((ptr l1'), (data 0))
  l3' -> ((data 1), (ptr l2'))

Then, I consider the graph of these data structures is the same.

In Coq,
*)

Require Arith.
Require EqNat.
Parameters l1,l2,l3:nat.
Definition A : Memory :=
 [l:nat]
 if (beq_nat l l1) then (Some ? ((ptr l2), (ptr l3))) else
 if (beq_nat l l2) then (Some ? ((ptr l1), (data (0)))) else
 if (beq_nat l l3) then (Some ? ((data (1)), (ptr l2))) else (None ?).


Parameters l1',l2',l3':nat.
Definition A' : Memory :=
 [l:nat]
 if (beq_nat l l1') then (Some ? ((ptr l2'), (ptr l3'))) else
 if (beq_nat l l2') then (Some ? ((ptr l1'), (data (0)))) else
 if (beq_nat l l3') then (Some ? ((data (1)), (ptr l2'))) else (None ?).


(*
Now, I want to define some binary predicate on a pair of Memory and
Word which is to hold when the graph structure of those words is
equivalent. For example, a first try:
*)

Inductive StrEq : (Memory * Word) -> (Memory * Word) -> Prop :=
| eq_data : (A,A',i:?) (StrEq (A, (data i)) (A', (data i)))
| eq_ptr  : (A,A',p,p',w1,w2,w1',w2':?)
            (A p)=(Some ? (w1,w2)) ->
        (A' p')=(Some ? (w1',w2')) ->
        (StrEq (A, w1) (A', w1')) ->
        (StrEq (A, w2) (A', w2')) ->
            (StrEq (A, (ptr p)) (A', (ptr p')))
.


(*
This works great, EXCEPT, that there is a possibility of cycles which
makes things complicated-- as in the definitions of A and A' given above.
And this is where I would appreciate any ideas - how to define StrEq
to handle cycles correctly (and finitely)?

I think the most important properties I want from StrEq is:
*)

Goal (A,A',l,w':?)
    (StrEq (A, (ptr l)) (A', w')) -> (EX l' | w'=(ptr l')).
Intros.
Inversion H.
Exists p'; Auto.
Save sameconstr.

Goal (A,A',l,l':?)
    (StrEq (A, (ptr l)) (A', (ptr l')))
        -> (EX w | (EX w' |
          (A l)=(Some ? w) /\
          (A' l')=(Some ? w') /\
              (StrEq (A, (Fst w)) (A', (Fst  w'))))).
Intros.
Inversion H.
Exists (w1,w2).
Exists (w1',w2').
Auto.
Save invstreq.

(*

Also, transitivity should be derivable for StrEq. I.e. (StrEq P1 P2) -> 
(StrEq P2 P3) -> (StrEq P1 P3).

Thanks in advance for any suggestions. Have fun :).

--- nadeem

*)