# HoareAsLogicHoare Logic as a Logic

*theorems*about the evaluation behavior of programs, and proofs of program correctness (validity of Hoare triples) were constructed by combining these theorems directly in Coq.

*that*logic. We can do this by giving an inductive definition of

*valid derivations*in this new logic.

*Logical Foundations*(

*Software Foundations*, volume 1).

Inductive hoare_proof : Assertion → com → Assertion → Type :=

| H_Skip : ∀P,

hoare_proof P (SKIP) P

| H_Asgn : ∀Q V a,

hoare_proof (Q [V ⊢> a]) (V ::= a) Q

| H_Seq : ∀P c Q d R,

hoare_proof P c Q → hoare_proof Q d R → hoare_proof P (c;;d) R

| H_If : ∀P Q b c

_{1}c

_{2},

hoare_proof (fun st ⇒ P st ∧ bassn b st) c

_{1}Q →

hoare_proof (fun st ⇒ P st ∧ ~(bassn b st)) c

_{2}Q →

hoare_proof P (TEST b THEN c

_{1}ELSE c

_{2}FI) Q

| H_While : ∀P b c,

hoare_proof (fun st ⇒ P st ∧ bassn b st) c P →

hoare_proof P (WHILE b DO c END) (fun st ⇒ P st ∧ ¬(bassn b st))

| H_Consequence : ∀(P Q P' Q' : Assertion) c,

hoare_proof P' c Q' →

(∀st, P st → P' st) →

(∀st, Q' st → Q st) →

hoare_proof P c Q.

We don't need to include axioms corresponding to
hoare_consequence_pre or hoare_consequence_post, because
these can be proven easily from H_Consequence.

Lemma H_Consequence_pre : ∀(P Q P': Assertion) c,

hoare_proof P' c Q →

(∀st, P st → P' st) →

hoare_proof P c Q.

Lemma H_Consequence_post : ∀(P Q Q' : Assertion) c,

hoare_proof P c Q' →

(∀st, Q' st → Q st) →

hoare_proof P c Q.

hoare_proof P' c Q →

(∀st, P st → P' st) →

hoare_proof P c Q.

Proof.

intros. eapply H_Consequence.

apply X. apply H. intros. apply H

intros. eapply H_Consequence.

apply X. apply H. intros. apply H

_{0}. Qed.Lemma H_Consequence_post : ∀(P Q Q' : Assertion) c,

hoare_proof P c Q' →

(∀st, Q' st → Q st) →

hoare_proof P c Q.

Proof.

intros. eapply H_Consequence.

apply X. intros. apply H

intros. eapply H_Consequence.

apply X. intros. apply H

_{0}. apply H. Qed.
As an example, let's construct a proof object representing a
derivation for the hoare triple

{{(X=3) [X ⊢> X + 2] [X ⊢> X + 1]}}

X::=X+1 ;; X::=X+2

{{X=3}}.

We can use Coq's tactics to help us construct the proof object.
X::=X+1 ;; X::=X+2

{{X=3}}.

Example sample_proof :

hoare_proof

((fun st:state ⇒ st X = 3) [X ⊢> X + 2] [X ⊢> X + 1])

(X ::= X + 1;; X ::= X + 2)

(fun st:state ⇒ st X = 3).

Proof.

eapply H_Seq; apply H_Asgn.

Qed.

Print sample_proof.

(*

====>

H_Seq

(((fun st : state => st X = 3) X ⊢> X + 2) X ⊢> X + 1)

(X ::= X + 1)

((fun st : state => st X = 3) X ⊢> X + 2)

(X ::= X + 2)

(fun st : state => st X = 3)

(H_Asgn

((fun st : state => st X = 3) X ⊢> X + 2)

X (X + 1))

(H_Asgn

(fun st : state => st X = 3)

X (X + 2))

*)

hoare_proof

((fun st:state ⇒ st X = 3) [X ⊢> X + 2] [X ⊢> X + 1])

(X ::= X + 1;; X ::= X + 2)

(fun st:state ⇒ st X = 3).

Proof.

eapply H_Seq; apply H_Asgn.

Qed.

Print sample_proof.

(*

====>

H_Seq

(((fun st : state => st X = 3) X ⊢> X + 2) X ⊢> X + 1)

(X ::= X + 1)

((fun st : state => st X = 3) X ⊢> X + 2)

(X ::= X + 2)

(fun st : state => st X = 3)

(H_Asgn

((fun st : state => st X = 3) X ⊢> X + 2)

X (X + 1))

(H_Asgn

(fun st : state => st X = 3)

X (X + 2))

*)

# Properties

#### Exercise: 2 stars, standard (hoare_proof_sound)

Prove that derivations constructed with hoare_proof correspond to valid Hoare triples. In other words, hoare_proof derivations are*sound*. Hint: We already proved the soundness of each individual proof rule in Hoare as theorems hoare_skip, hoare_asgn, etc.; leverage those proofs.

Theorem hoare_proof_sound : ∀P c Q,

hoare_proof P c Q → {{P}} c {{Q}}.

Proof.

(* FILL IN HERE *) Admitted.

☐
hoare_proof P c Q → {{P}} c {{Q}}.

Proof.

(* FILL IN HERE *) Admitted.

*provable*in Hoare Logic. Note that the proof is more complex than the semantic proof in Hoare: we actually need to perform an induction over the structure of the command c.

Theorem H_Post_True_deriv:

∀c P, hoare_proof P c (fun _ ⇒ True).

Proof.

intro c.

induction c; intro P.

- (* SKIP *)

eapply H_Consequence.

apply H_Skip.

intros. apply H.

(* Proof of True *)

intros. apply I.

- (* ::= *)

eapply H_Consequence_pre.

apply H_Asgn.

intros. apply I.

- (* ;; *)

eapply H_Consequence_pre.

eapply H_Seq.

apply (IHc1 (fun _ ⇒ True)).

apply IHc2.

intros. apply I.

- (* TEST *)

apply H_Consequence_pre with (fun _ ⇒ True).

apply H_If.

apply IHc1.

apply IHc2.

intros. apply I.

- (* WHILE *)

eapply H_Consequence.

eapply H_While.

eapply IHc.

intros; apply I.

intros; apply I.

Qed.

∀c P, hoare_proof P c (fun _ ⇒ True).

Proof.

intro c.

induction c; intro P.

- (* SKIP *)

eapply H_Consequence.

apply H_Skip.

intros. apply H.

(* Proof of True *)

intros. apply I.

- (* ::= *)

eapply H_Consequence_pre.

apply H_Asgn.

intros. apply I.

- (* ;; *)

eapply H_Consequence_pre.

eapply H_Seq.

apply (IHc1 (fun _ ⇒ True)).

apply IHc2.

intros. apply I.

- (* TEST *)

apply H_Consequence_pre with (fun _ ⇒ True).

apply H_If.

apply IHc1.

apply IHc2.

intros. apply I.

- (* WHILE *)

eapply H_Consequence.

eapply H_While.

eapply IHc.

intros; apply I.

intros; apply I.

Qed.

Similarly, we can show that {{False}} c {{Q}} is provable for
any c and Q.

Lemma False_and_P_imp: ∀P Q,

False ∧ P → Q.

Proof.

intros P Q [CONTRA HP].

destruct CONTRA.

Qed.

Tactic Notation "pre_false_helper" constr(CONSTR) :=

eapply H_Consequence_pre;

[eapply CONSTR | intros ? CONTRA; destruct CONTRA].

Theorem H_Pre_False_deriv:

∀c Q, hoare_proof (fun _ ⇒ False) c Q.

Proof.

intros c.

induction c; intro Q.

- (* SKIP *) pre_false_helper H_Skip.

- (* ::= *) pre_false_helper H_Asgn.

- (* ;; *) pre_false_helper H_Seq. apply IHc1. apply IHc2.

- (* TEST *)

apply H_If; eapply H_Consequence_pre.

apply IHc1. intro. eapply False_and_P_imp.

apply IHc2. intro. eapply False_and_P_imp.

- (* WHILE *)

eapply H_Consequence_post.

eapply H_While.

eapply H_Consequence_pre.

apply IHc.

intro. eapply False_and_P_imp.

intro. simpl. eapply False_and_P_imp.

Qed.

False ∧ P → Q.

Proof.

intros P Q [CONTRA HP].

destruct CONTRA.

Qed.

Tactic Notation "pre_false_helper" constr(CONSTR) :=

eapply H_Consequence_pre;

[eapply CONSTR | intros ? CONTRA; destruct CONTRA].

Theorem H_Pre_False_deriv:

∀c Q, hoare_proof (fun _ ⇒ False) c Q.

Proof.

intros c.

induction c; intro Q.

- (* SKIP *) pre_false_helper H_Skip.

- (* ::= *) pre_false_helper H_Asgn.

- (* ;; *) pre_false_helper H_Seq. apply IHc1. apply IHc2.

- (* TEST *)

apply H_If; eapply H_Consequence_pre.

apply IHc1. intro. eapply False_and_P_imp.

apply IHc2. intro. eapply False_and_P_imp.

- (* WHILE *)

eapply H_Consequence_post.

eapply H_While.

eapply H_Consequence_pre.

apply IHc.

intro. eapply False_and_P_imp.

intro. simpl. eapply False_and_P_imp.

Qed.

As a last step, we can show that the set of hoare_proof axioms
is sufficient to prove any true fact about (partial) correctness.
More precisely, any semantic Hoare triple that we can prove can
also be proved from these axioms. Such a set of axioms is said to
be
Our proof is inspired by this one:
To carry out the proof, we need to invent some intermediate
assertions using a technical device known as

*relatively complete*. That is, the axioms are complete*relative to*what we can prove in the underlying assertion language. If there are gaps in what can be proved in that language, then we blame it, not the Hoare logic axioms.http://www.ps.uni-saarland.de/courses/sem-ws_{11}/script/Hoare.html

*weakest preconditions*(which are also discussed in Hoare2). Given a command c and a desired postcondition assertion Q, the weakest precondition wp c Q is an assertion P such that {{P}} c {{Q}} holds, and moreover, for any other assertion P', if {{P'}} c {{Q}} holds then P' → P. We can more directly define this as follows:
Definition wp (c:com) (Q:Assertion) : Assertion :=

fun s ⇒ ∀s', s =[ c ]⇒ s' → Q s'.

fun s ⇒ ∀s', s =[ c ]⇒ s' → Q s'.

To get accustomed to this definition of wp, prove the
next two simple theorems.

#### Exercise: 1 star, standard (wp_is_precondition)

Theorem wp_is_precondition : ∀c Q,

{{wp c Q}} c {{Q}}.

Proof. (* FILL IN HERE *) Admitted.

Theorem wp_is_weakest : ∀c Q P',

{{P'}} c {{Q}} → ∀st, P' st → wp c Q st.

Proof. (* FILL IN HERE *) Admitted.

#### Exercise: 2 stars, standard (wp_invariant)

Lemma wp_invariant : ∀b c Inv Q,

Inv = wp (WHILE b DO c END) Q

→ {{ fun st ⇒ Inv st ∧ bassn b st }} c {{ Inv }}.

Proof. (* FILL IN HERE *) Admitted.

☐
Inv = wp (WHILE b DO c END) Q

→ {{ fun st ⇒ Inv st ∧ bassn b st }} c {{ Inv }}.

Proof. (* FILL IN HERE *) Admitted.

Lemma bassn_eval_false : ∀b st, ¬bassn b st → beval st b = false.

Proof.

intros b st H. unfold bassn in H. destruct (beval st b).

exfalso. apply H. reflexivity.

reflexivity.

Qed.

Proof.

intros b st H. unfold bassn in H. destruct (beval st b).

exfalso. apply H. reflexivity.

reflexivity.

Qed.

#### Exercise: 4 stars, standard (hoare_proof_complete)

Complete the proof of the theorem. Hint for the WHILE case: you need to invent a loop invariant.
Theorem hoare_proof_complete: ∀P c Q,

{{P}} c {{Q}} → hoare_proof P c Q.

Proof.

intros P c. generalize dependent P.

induction c; intros P Q HT.

- (* SKIP *)

eapply H_Consequence.

eapply H_Skip.

intros. eassumption.

intro st. apply HT. apply E_Skip.

- (* ::= *)

eapply H_Consequence.

eapply H_Asgn.

intro st. apply HT. constructor. reflexivity.

intros; assumption.

- (* ;; *)

apply H_Seq with (wp c

eapply IHc1.

intros st st' E

eapply HT. econstructor; eassumption. assumption.

eapply IHc2. intros st st' E

(* FILL IN HERE *) Admitted.

☐
{{P}} c {{Q}} → hoare_proof P c Q.

Proof.

intros P c. generalize dependent P.

induction c; intros P Q HT.

- (* SKIP *)

eapply H_Consequence.

eapply H_Skip.

intros. eassumption.

intro st. apply HT. apply E_Skip.

- (* ::= *)

eapply H_Consequence.

eapply H_Asgn.

intro st. apply HT. constructor. reflexivity.

intros; assumption.

- (* ;; *)

apply H_Seq with (wp c

_{2}Q).eapply IHc1.

intros st st' E

_{1}H. unfold wp. intros st'' E_{2}.eapply HT. econstructor; eassumption. assumption.

eapply IHc2. intros st st' E

_{1}H. apply H; assumption.(* FILL IN HERE *) Admitted.

*decidable*; that is, that there is an (terminating) algorithm (a

*decision procedure*) that can determine whether or not a given Hoare triple is valid (derivable). But such a decision procedure cannot exist!