The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I have abstracted out the appropriate definitions from my model.  I'm trying to figure out a good approach for this proof.  I'm pretty sure that it requires classical logic.  The key to the proof is to show that "v < vars" in the theorem at the end.  To do this, I'd like to assume that v >= vars and then construct an m and m' that are counter examples to the first hypothesis.  How can I set this up?  I've included all the relevant definitions.  Hopefully, some Coq guru can solve this quickly.

                            - Ken

Definition Map := (prod (list nat) (list heap)).

Fixpoint var_in_pos (n : nat) (l : list nat) : nat :=
    match n with
      | 0 => match l with
               | nil => 0
               | (f::r) => f
             end
      | S x => match l with
               | nil => 0
               | (f::r) => var_in_pos x r
               end
    end.

Fixpoint heap_in_pos (n : nat) (l : list heap) : heap :=
    match n with
      | 0 => match l with
               | nil => empty_heap
               | (f::r) => f
             end
      | S x => match l with
               | nil => empty_heap
               | (f::r) => heap_in_pos x r
               end
    end.

Definition hv (n : nat) (x : Map) :=
    heap_in_pos n (snd x).

Definition heap_count (x : Map) :=
    length (snd x).

Definition ev (n : nat) (x : Map) :=
    var_in_pos n (fst x).

Definition var_count (x : Map) :=
    length (fst x).

Definition changedMap (vars : nat) (heaps : nat) (m : Map) (m' : Map) : Prop :=
    (forall n, n < vars -> ev n m = ev n m') /\
    (forall n, n < heaps -> hv n m = hv n m').

Theorem stateIndependentMapChanged: forall i v mm mm' vars heaps,
    (forall (s : state) (m m' : Map),
        (forall v : nat, snd s v = None) /\
        (forall v : id, v <> i -> fst s v = None) /\ fst s i = Some (ev v m) ->
        changedMap vars heaps m m' ->
        (forall v : nat, snd s v = None) /\
        (forall v : id, v <> i -> fst s v = None) /\ fst s i = Some (ev v m')) ->
    changedMap vars heaps mm mm') ->
    ev v m = ev v m'.