proposition: Theorem noAssign_noChange : forall (n:nat) (i:inst nat aExp bExp), noAssign n i = true -> forall s s':state, exec nat aExp bExp state evalA evalB update s i s' -> evalA s (aVar n) = evalA s' (aVar n).
proof: Proof. intros n i Heq s s' Hexec; generalize n Heq; clear Heq n; elim Hexec. - auto. - simpl in |- *; intros s0 s1 v n' a Heval Hupdate n; case (eq_nat_dec v n). + discriminate. + intros; symmetry in |- *; apply lookup_update_diff with v n'; auto. - simpl in |- *; intros s0 s1 s2 i1 i2 Hex1 Hrec1 Hex2 Hrec2 n. generalize (Hrec1 n) (Hrec2 n); clear Hrec1 Hrec2. case (noAssign n i1); simpl in |- *; try (intros; discriminate). case (noAssign n i2); simpl in |- *; try (intros; discriminate). transitivity (lookup n s1); auto. - auto. - simpl in |- *; intros s0 s1 s2 i' b Heval Hex1 Hrec1 Hex2 Hrec2 n; generalize (Hrec1 n) (Hrec2 n); clear Hrec1 Hrec2. intros; transitivity (lookup n s1); auto. Qed.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction List Arith Compare_dec Lia