proposition: Theorem lookup_update_diff : forall (n m:nat) (s s':state) (v:Z), update s n v = Some s' -> n <> m -> lookup m s' = lookup m s.
proof: Proof. simple induction n. - intros m; case m. + intros s s' v H H1; elim H1; auto. + intros m' s; case s; simpl in |- *; try (intros; discriminate). * intros z tl s' v Heq; injection Heq; intros Heq1; now rewrite <- Heq1. - intros p Hrec m; case m; simpl in |- *. + intros s; case s; simpl in |- *; try (intros; discriminate). intros z l s' v; case (update l p v); simpl in |- *; try (intros; discriminate). intros s'0 Heq; injection Heq; intros Heq1; now rewrite <- Heq1. + intros m' s; case s; simpl in |- *; try (intros; discriminate). intros z l s' v; generalize (fun s':state => Hrec m' l s' v); case (update l p v); try (intros; discriminate). intros s'0 Hrec' Heq; injection Heq; intros Heq1; rewrite <- Heq1. intros Hneq; apply Hrec'; auto with arith. Qed.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction List Arith Compare_dec Lia