# How much Coq do I need to know to learn SF Hoare Logic?

**URL:** <https://discourse.rocq-prover.org/t/how-much-coq-do-i-need-to-know-to-learn-sf-hoare-logic/204>\
**Category:** Using Rocq\
**Created:** [March 7, 2019, 7:17pm UTC](https://discourse.rocq-prover.org/t/how-much-coq-do-i-need-to-know-to-learn-sf-hoare-logic/204 "2019-03-07T19:17:08Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [March 7, 2019, 7:17pm UTC](https://discourse.rocq-prover.org/t/how-much-coq-do-i-need-to-know-to-learn-sf-hoare-logic/204/1 "2019-03-07T19:17:08Z")

</div>

How much of the first chapter of SF do I need to know to tackle Hoare logic?  
in volume 2  
or which chapters of volume 1 are a must for Hoare Logic?

---

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [March 7, 2019, 7:47pm UTC](https://discourse.rocq-prover.org/t/how-much-coq-do-i-need-to-know-to-learn-sf-hoare-logic/204/2 "2019-03-07T19:47:04Z")

</div>

I’d recommend following the [Chapter Dependencies](https://softwarefoundations.cis.upenn.edu/lf-current/deps.html). If you’re in a hurry, the informal explanations are well-written for you to understand Hoare Logic without knowing Coq. The syntax for inference rule was introduced in [IndProp](https://softwarefoundations.cis.upenn.edu/current/lf-current/IndProp.html#lab206) chapter. Maybe @bcpierce could provide better suggestions.

---

<div class="post-metadata">

**Author:** ![brando90](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/brando90/32/183_2.png) [@brando90](https://discourse.rocq-prover.org/u/brando90)\
**Post date:** [March 7, 2019, 8:03pm UTC](https://discourse.rocq-prover.org/t/how-much-coq-do-i-need-to-know-to-learn-sf-hoare-logic/204/3 "2019-03-07T20:03:57Z")

</div>

I really wanted to learn it WITH coq though, hence my question. Though, thanks for the response! 🙂