Library iris.program_logic.weakestpre_fix
From Coq Require Import Wf_nat.
From iris.program_logic Require Import weakestpre wsat.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 10 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
From iris.program_logic Require Import weakestpre wsat.
Local Hint Extern 10 (_ ≤ _) ⇒ omega.
Local Hint Extern 10 (_ ⊥ _) ⇒ set_solver.
Local Hint Extern 10 (✓{_} _) ⇒
repeat match goal with
| H : wsat _ _ _ _ |- _ ⇒ apply wsat_valid in H; last omega
end; solve_validN.
This files provides an alternative definition of wp in terms of a fixpoint
of a contractive function, rather than a CoInductive type. This is how we define
wp on paper. We show that the two versions are equivalent.