proposition: Theorem forLoops_fact3 : forLoops nat aExp bExp state evalA evalB update fact3.
proof: Proof. unfold fact3 in |- *; repeat constructor. apply aForLoop with (aVar 1). intros s; case s. - intros s' Hevgt1 Hexec1; inversion Hexec1. inversion H2; simpl in H10; discriminate. - intros v0 s0; case s0. + intros s' Hevgt1 Hexec1; inversion Hexec1. inversion H2. simpl in H8; discriminate. + intros v1 s1 s' Hevgt1 Hexec1; inversion Hexec1. inversion H2. simpl in H8. simpl in H10. injection H8; clear H8; intros H8. subst v1; clear Hexec1; inversion H4. rewrite <- noAssign_noChange with (2 := H15). * inversion H13. simpl in H19. injection H10. intros Heq1. rewrite <- Heq1 in H19, H21. injection H19; clear H19; intros H19. rewrite <- H19 in H21; simpl in H21; injection H21. intros Heq2; rewrite <- Heq2; simpl in |- *. unfold Zwf in |- *; auto with zarith. inversion Hevgt1. generalize H23; case (Z_le_gt_dec n 0); simpl in |- *; try (intros; discriminate). intros; lia. * simpl in |- *; auto. - repeat constructor. apply aForLoop with (aVar 0). + intros s s'; lazy beta iota zeta delta [evalB] in |- *; fold evalB in |- *. intros Hevgt Hexec; inversion Hexec. inversion H2. rewrite <- noAssign_noChange with (2 := H4). * lazy beta iota zeta delta [evalA] in H8; fold evalA in H8. generalize H8; clear H8; case_eq (lookup 0 s). intros z Hlk H8; injection H8; clear H8; intros H8. lazy beta iota zeta delta [evalA] in |- *. rewrite lookup_update_eq with (1 := H10). rewrite Hlk; rewrite <- H8. generalize Hevgt; lazy beta iota zeta delta [evalA] in |- *. rewrite Hlk. case (Z_le_gt_dec z 0); simpl in |- *; try (intros; discriminate). unfold Zwf in |- *; intros; lia. intros; discriminate. * simpl in |- *; auto. + repeat constructor. Qed.
imports: ZArith Zwf Inverse_Image Wellfounded Extraction List Arith Compare_dec Lia