The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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
>
>  
Hi,

 First, you can simplify a little yours statement avoiding the (always 
true) 0<=idx, etc.

 Your proof of transitivity can be done if you first prove (or admit) a 
little lemma

(I hope it's true).
Lemma lt_plus_ab : forall n a b : nat, n < a + b ->
                             n < a \/ exists y, n=a+y /\ y < b.
Admitted.


The following proof works, although, it is written in a bas style, can 
certainly be shortened.


Pierre




Require Import Arith.

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.
red.
intros idx H' val.
split.
case (lt_plus_ab idx l1 l2 H').
intro.
 red in H.
red in H0.
intro.
case (H idx  H1 val).
auto.
intro.
red in H;red in H0.
case H1;intros y (Hy,H'y).
case (H0 y H'y val).
subst idx.
repeat rewrite plus_assoc.
auto.
case (lt_plus_ab idx l1 l2 H').
intro.
 red in H.
red in H0.
intro.
case (H idx H1 val).
auto.
intros (y, (Hy,H'y)).
case (H0 y H'y val).
subst idx.
repeat rewrite plus_assoc.
auto.
Qed.




> 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.
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>