Commit 2022-11-07 03:12 99667781

feat: port data.bool.basic (#534) Issues that came up:

1. my understanding of the lean 4 naming convention is that capital/small letter choices are often dictated to you. However Lean 4 has not for bools and Not for props. This causes the following issue: in my port I have gone for the name

   theorem Not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b
   

   What should this theorem be called? The algorithm says not_eq_not which is misleading...or is it? It comes up a few times (the others are not_iff_Not and Not_not_eq)
2. When defining LinearOrder I had to do a lot of unfolding which is not present in Lean 3.

instance : LinearOrder Bool where
  le := fun a b => a = false ∨ b = true
  le_refl := by unfold LE.le; decide
  le_trans := by unfold LE.le; decide
  le_antisymm := by unfold LE.le Preorder.toLE; decide
  le_total := by unfold LE.le Preorder.toLE PartialOrder.toPreorder; decide
  decidable_le := by unfold LE.le Preorder.toLE PartialOrder.toPreorder; exact inferInstance
...

3. Again on orders: lt_iff_le_not_le is not an autoparam so I had to prove it explicitly with Iff.rfl. Do autoparams exist in Lean 4 yet? Does this need to be flagged?
4. Because the names of many functions on booleans changed (bor -> or, bnot -> not etc) I had to #align a lot of stuff. However the namespace also changed (bool -> Bool). Am I right in thinking that the few theorems like bool.lt_iff, which becomes Bool.lt_iff (i.e. the theorem name itself survived the naming change but the namespace did not) do not need to be #align ed?