Require Import Semantics. Import ZArith List String. Open Scope Z_scope. Open Scope list_scope. Open Scope string_scope. Example swap := sequence (assign "z" "x") (sequence (assign "x" "y") (assign "y" "z")). Goal ax_sem nil (a_conj (beq "x" "old_x") (beq "y" "old_y")) swap (a_conj (beq "x" "old_y") (beq "y" "old_x")). unfold swap. econstructor. (* better to go backwards *) 2:econstructor. 3:constructor. 2:constructor. (** Problem ! the precondition is not of the form required by ax2 *) (* apply ax2. *) Lemma c_imp_refl : forall defs A, valid defs (c_imp A A). Proof. unfold valid;simpl. auto. Qed. (** using ax5 with no pre-condition weakening *) Ltac backwards := (eapply ax5;[ idtac | constructor | eapply c_imp_refl]). backwards. intros g;simpl. tauto. Qed. Example square := sequence (assign "x" 0) (sequence (assign "i" 0) (sequence (assign "d" 1) (while (blt "i" "arg") (sequence (assign "x" (zplus"x" "d")) (sequence (assign "d" (zplus "d" 2)) (assign "i" (zplus "i" 1))))))). Compute f_star 56 (("arg",7)::("x",0)::("i",0)::("d",0)::nil) square. Lemma square_ok : ax_sem nil (blt 0 "arg") square (beq "x" (zmult "arg" "arg")). unfold square. Definition invariant_1 := (a_conj (beq "x" (zmult "i" "i")) (blt "i" (zplus "arg" 1))). Lemma loop_invariant_1 : ax_sem nil invariant_1 (while (blt "i" "arg") (sequence (assign "x" (zplus "x" "d")) (sequence (assign "d" (zplus "d" 2)) (assign "i" (zplus "i" 1))))) (a_conj (a_not (blt "i" "arg" )) invariant_1 ). apply ax4. econstructor. 2:unfold invariant_1. 2:econstructor. 3:econstructor. 2:econstructor. simpl. backwards. intros g;simpl. intro H;decompose [and] H;clear H. rewrite H2. split. Abort. Definition invariant := (a_conj (beq "x" (zmult "i" "i")) (a_conj (beq "d" (zplus "i" (zplus "i" 1))) (blt "i" (zplus "arg" 1)))). Lemma loop_invariant : ax_sem nil invariant (while (blt "i" "arg") (sequence (assign "x" (zplus "x" "d")) (sequence (assign "d" (zplus "d" 2)) (assign "i" (zplus "i" 1))))) (a_conj (a_not (blt "i" "arg" )) invariant ). apply ax4. econstructor. 2:unfold invariant. 2:econstructor. 3:econstructor. 2:econstructor. simpl. backwards. intros g;simpl. intro H;decompose [and] H. rewrite H2, H1. split. ring. split. ring. omega. Qed. repeat (econstructor 3). Ltac while_back invariant test := eapply ax5 with (P':= invariant)(Q':= a_conj (a_not test) invariant);[apply c_imp_refl | | ]. 4 : while_back invariant (blt "i" "arg"). 4:apply loop_invariant. Focus 4. unfold invariant;intros g;simpl. generalize (g "i") (g "arg") (g "x");intros. decompose [and] H. assert (z = z0). omega. subst z;auto. Focus 2. econstructor. 2:econstructor. backwards. simpl. intros g. simpl. omega. Qed.