The Coq mailing list

[topwl AT free.fr]

Hello,

I thank you for your answer.
but I'm sorry, I was mistaken in my problem.

I have a transitivity problem with copy definition.
I try to proof it for one week. I don't have a new idea.
If you have an indication, an idea or other

Thanks very much,
Martin



Require Import ZArith.
Parameter memory : Set.
Parameter valeur : Set.
Parameter lecture  : memory -> nat -> nat -> valeur -> Prop.


(* offset <= idx < offset + len *)
Definition check
 (offset: nat) (idx: nat) (len: nat) : bool :=
 (Zle_bool (Z_of_nat offset) (Z_of_nat idx))
 && (Zlt_bool (Z_of_nat idx) (Z_of_nat (offset+len))).


Definition copy
  (min mout : memory) (mem_length: nat)
  (adrSrc: nat) (adrDest: nat) (offset: nat) (len:nat) : Prop :=
  forall idx:nat,
    idx<mem_length ->
    forall val:valeur,
      lecture min adrSrc idx val ->
      if (check offset idx len)
        then
          lecture mout adrDest idx val
        else
          (lecture min adrDest idx val) <->
          (lecture mout adrDest idx val).


Lemma copy_trans :
 forall min mem mout mem_length adrSrc adrDest offset l1 l2,
   copy min mem mem_length adrSrc adrDest offset l1 ->
   copy mem mout mem_length adrSrc adrDest (offset+l1) l2 ->
   copy min mout mem_length adrSrc adrDest offset (l1+l2).