The Coq mailing list

[topwl AT free.fr]

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.
  intros l1.
  elim l1.

  (* CB : l1 = 0  *)
  intro l2.
  elim l2.

  (* CB : l2 = 0 *)
  intros rf0 offset0 rf1 offset1.
  simpl.
  auto.

  (* HI : l2 = n2  *)
  intros n2 Hn2.
  intros rf0 offset0 rf1 offset1.
  simpl.
  rewrite <- plus_n_O.
  rewrite <- plus_n_O.
  auto.

  (* HI : l1 = n1  *)
  intros n1 Hn1.
  intro l2.
  elim l2.

  (* CB : l2 = 0 *)
  intros rf0 offset0 rf1 offset1.
  simpl.
  rewrite <- plus_n_O.
  auto.

  (* HI : l2 = n2  *)
  intros n2 Hn2.
  intros rf0 offset0 rf1 offset1.