The Coq mailing list

["Jean.Duprat" <duprat AT ens-lyon.fr>]

Hi,

Theorem invariant_trans can be proved by cases :
Require Export Omega.

Lemma invariant_trans :
  forall l1 l2 rf0 offset0 rf1 offset1,
    invariant rf0 offset0 rf1 offset1 l1 ->
    invariant rf0 (offset0+l1) rf1 (offset1+l1) l2 ->
    invariant rf0 offset0 rf1 offset1 (l1+l2).
Proof.
intros l1 l2 rf0 offset0 rf1 offset1 H1 H2 idx Hi0 Hi1.
destruct (le_lt_dec l1 idx).
 replace idx with (l1 + (idx - l1)); repeat rewrite plus_assoc.
  apply H2; omega.
  omega.
 apply H1; omega.
Qed.

Yours

	Jean Duprat

topwl AT free.fr wrote:

Hello,

I have a problem with a proof.
I simplified the problem.
I don't arrive to prove invariant_trans lemma.
I think that it is by induction ...

thank you for your assistance.
Martin


Parameter valeur : Set.
Parameter lecture  : nat -> nat -> valeur -> Prop.

Definition invariant
  (rf0: nat) (offset0: nat) (rf1: nat) (offset1: nat) (length: nat) : Prop :=
  forall idx:nat,
    O<=idx -> idx<length ->
  forall val:valeur,
   (lecture rf0 (offset0+idx) val) <->
   (lecture rf1 (offset1+idx) val).


Lemma invariant_trans :
  forall l1 l2 rf0 offset0 rf1 offset1,

    invariant rf0 offset0 rf1 offset1 l1 ->
    invariant rf0 (offset0+l1) rf1 (offset1+l1) l2 ->
    invariant rf0 offset0 rf1 offset1 (l1+l2).
Proof.
...