A simple formulation of Hoare logic for a WHILE-language, with a proof of /relative completeness/:

If a triple { P } s { Q } is valid in the model, then it is derivable
using the rules in Hoare.v (see the inductive type `hoare_triple`).

Requires std++: <https://gitlab.mpi-sws.org/iris/stdpp>.
(Tested with git version f8719169e3ed75123d88c59d292ddd0972351ad3).


BEWARE!!! I wrote this formalization when I started my PhD, and I
didn't know much about (idiomatic) Coq back then. As a result, the
code is quite shitty.