search

isovector / certainty-by-construction

Source material for Certainty by Construction
https://leanpub.com/certainty-by-construction/
36 stars 9 forks source link

Missing exercise solution in 4.12 #12

Open SlimTim10 opened 9 months ago

SlimTim10 commented 9 months ago

In the last exercise of section 4.12:

Exercise (Trivial) Should the reader be feeling industrious, they are encouraged to prove that Sandbox-Relations.Unrelated and Sandbox-Relations.Related are also preorders.

the provided solution does not include the proof for Sandbox-Relations.Unrelated:

Solution

open Sandbox-Relations using (Related; related)
Related-preorder : IsPreorder (Related {A = A})
IsPreorder.refl Related-preorder = related
IsPreorder.trans Related-preorder _ _ = related