From 2c99e4e926daa1744b7155935913fb1c625cef40 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 28 Nov 2024 09:32:15 +0100 Subject: [PATCH 1/2] feat: Bool Closes #162. --- Manual.lean | 11 ++ Manual/BasicTypes.lean | 131 +++++++++++++++++++++- Manual/Language/Classes/BasicClasses.lean | 30 +++++ 3 files changed, 169 insertions(+), 3 deletions(-) diff --git a/Manual.lean b/Manual.lean index a874eea..37a7156 100644 --- a/Manual.lean +++ b/Manual.lean @@ -153,7 +153,18 @@ file := some "the-index" String Char Nat Lean.Elab.Tactic Array Subarray IO IO.FS System System.FilePath IO.Process IO.FS.Stream ST IO.Error IO.FS.Stream.Buffer IO.FS.Handle IO.Process.SpawnArgs IO.Process.Output IO.Process.Child IO.Process.StdioConfig IO.Process.Stdio IO.Ref ST.Ref IO.FS.Metadata IO.FS.DirEntry EIO BaseIO IO.FileRight IO.FS.Stream Task Task.Priority +Bool Decidable ``` + +```exceptions +Bool.toLBool +Bool.«term_^^_» +``` + +```exceptions +Decidable.or_not_self +``` + ```exceptions String.revFindAux String.extract.go₂ String.substrEq.loop String.casesOn String.offsetOfPosAux String.extract.go₁ String.mapAux String.firstDiffPos.loop String.utf8SetAux String.revPosOfAux String.replace.loop diff --git a/Manual/BasicTypes.lean b/Manual/BasicTypes.lean index 88ea4a1..6244b51 100644 --- a/Manual/BasicTypes.lean +++ b/Manual/BasicTypes.lean @@ -144,11 +144,136 @@ tag := "char-api-classes" {docstring Bool} -:::planned 162 - * Relationship to {lean}`Prop` - * Laziness of `&&` etc +The constructors {lean}`Bool.true` and {lean}`Bool.false` are exported from the {lean}`Bool` namespace, so they can be written {lean}`true` and {lean}`false`. + +## Run-Time Representation + +Because {lean}`Bool` is an {tech}[enum inductive] type, it is represented by a single byte in compiled code. + +## Booleans and Propositions + +Both {lean}`Bool` and {lean}`Prop` represent notions of truth. +From a purely logical perspective, they are equivalent: {tech}[propositional extensionality] means that there are fundamentally only two propositions, namely {lean}`True` and {lean}`False`. +However, there is an important pragmatic difference: {lean}`Bool` classifies _values_ that can be computed by programs, while {lean}`Prop` classifies statements for which code generation doesn't make sense. +In other words, {lean}`Bool` is the notion of truth and falsehood that's appropriate for programs, while {lean}`Prop` is the notion that's appropriate for mathematics. +Because proofs are erased from compiled programs, keeping {lean}`Bool` and {lean}`Prop` distinct makes it clear which parts of a Lean file are intended for computation. + +```lean (show := false) +section BoolProp + +axiom b : Bool + +/-- info: b = true : Prop -/ +#guard_msgs in +#check (b : Prop) + +example : (true = true) = True := by simp + +#check decide +``` + +A {lean}`Bool` can be used wherever a {lean}`Prop` is expected. +There is a {tech}[coercion] from every {lean}`Bool` {lean}`b` to the proposition {lean}`b = true`. +By {lean}`propext`, {lean}`true = true` is equal to {lean}`True`, and {lean}`false = true` is equal to {lean}`False`. + +Not every proposition can be used by programs to make run-time decisions. +Otherwise, a program could branch on whether the Collatz conjecture is true or false! +Many propositions, however, can be checked algorithmically. +These propositions are called {tech}_decidable_ propositions, and have instances of the {lean}`Decidable` type class. +The function {name}`Decidable.decide` converts a proof-carrying {lean}`Decidable` result into a {lean}`Bool`. +This function is also a coercion from decidable propositions to {lean}`Bool`, so {lean}`(2 = 2 : Bool)` evaluates to {lean}`true`. + +```lean (show := false) +/-- info: true -/ +#guard_msgs in +#eval (2 = 2 : Bool) +end BoolProp +``` + +## Syntax + +:::syntax term +The infix operators `&&`, `||`, and `^^` are notations for {lean}`Bool.and`, {lean}`Bool.or`, and {lean}`Bool.xor`, respectively. + +```grammar +$_:term && $_:term +``` +```grammar +$_:term || $_:term +``` +```grammar +$_:term ^^ $_:term +``` +::: + +:::syntax term +The prefix operator `!` is notation for {lean}`Bool.not`. +```grammar +!$_:term +``` ::: + +## API Reference + +### Logical Operations + +```lean (show := false) +section ShortCircuit + +axiom BIG_EXPENSIVE_COMPUTATION : Bool +``` + +The functions {name}`cond`, {name Bool.and}`and`, and {name Bool.or}`or` are short-circuiting. +In other words, {lean}`false && BIG_EXPENSIVE_COMPUTATION` does not need to execute {lean}`BIG_EXPENSIVE_COMPUTATION` before returning `false`. +These functions are defined using the {attr}`macro_inline` attribute, which causes the compiler to replace calls to them with their definitions while generating code, and the definitions use nested pattern matching to achieve the short-circuiting behavior. + +```lean (show := false) +end ShortCircuit +``` + + +{docstring cond} + +{docstring Bool.not} + +{docstring Bool.and} + +{docstring Bool.or} + +{docstring Bool.xor} + +{docstring Bool.atLeastTwo} + +### Comparisons + +{docstring Bool.decEq} + +### Conversions + +{docstring Bool.toISize} + +{docstring Bool.toUInt8} + +{docstring Bool.toUInt16} + +{docstring Bool.toUInt32} + +{docstring Bool.toUInt64} + +{docstring Bool.toUSize} + +{docstring Bool.toInt8} + +{docstring Bool.toInt16} + +{docstring Bool.toInt32} + +{docstring Bool.toInt64} + +{docstring Bool.toNat} + + # Linked Lists %%% tag := "List" diff --git a/Manual/Language/Classes/BasicClasses.lean b/Manual/Language/Classes/BasicClasses.lean index f9b369d..be97de5 100644 --- a/Manual/Language/Classes/BasicClasses.lean +++ b/Manual/Language/Classes/BasicClasses.lean @@ -38,12 +38,42 @@ Many Lean type classes exist in order to allow built-in notations such as additi # Decidability +A proposition is {deftech}_decidable_ if it can be checked algorithmically.{index}[decidable]{index subterm:="decidable"}[proposition] +The Law of the Excluded Middle means that every proposition is true or false, but it provides no way to check which of the two cases holds, which can often be useful. +By default, only algorithmic {lean}`Decidable` instances for which code can be generated are in scope; opening the `Classical` namespace makes every proposition decidable. + {docstring Decidable} {docstring DecidableRel} {docstring DecidableEq} +{docstring Decidable.decide} + +{docstring Decidable.byCases} + +::::keepEnv +:::example "Excluded Middle and {lean}`Decidable`" +The equality of functions from {lean}`Nat` to {lean}`Nat` is not decidable: +```lean (error:=true) (name := NatFunNotDecEq) +example (f g : Nat → Nat) : Decidable (f = g) := inferInstance +``` +```leanOutput NatFunNotDecEq +failed to synthesize + Decidable (f = g) +Additional diagnostic information may be available using the `set_option diagnostics true` command. +``` + +Opening `Classical` makes every proposition decidable; however, declarations and examples that use this fact must be marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` to indicate that code should not be generated for them. +```lean +open Classical +noncomputable example (f g : Nat → Nat) : Decidable (f = g) := inferInstance +``` + +::: +:::: + + # Inhabited Types {docstring Inhabited} From 96afb9be7077878ab56256e25d7dbd9352974792 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Thu, 28 Nov 2024 09:58:25 +0100 Subject: [PATCH 2/2] chore: Collatz for Vale --- .vale/styles/Lean/Names.yml | 1 + .vale/styles/config/ignore/names.txt | 1 + 2 files changed, 2 insertions(+) diff --git a/.vale/styles/Lean/Names.yml b/.vale/styles/Lean/Names.yml index 802d5c2..fda49e7 100644 --- a/.vale/styles/Lean/Names.yml +++ b/.vale/styles/Lean/Names.yml @@ -6,6 +6,7 @@ swap: - 'de moura': 'de Moura' - 'blott': 'Blott' - 'carneiro': 'Carneiro' + - 'collatz': 'Collatz' - 'lua': 'Lua' - 'Madelaine': 'Madelaine' - 'mathlib': 'Mathlib' diff --git a/.vale/styles/config/ignore/names.txt b/.vale/styles/config/ignore/names.txt index e0a56fe..0d7f8e1 100644 --- a/.vale/styles/config/ignore/names.txt +++ b/.vale/styles/config/ignore/names.txt @@ -1,5 +1,6 @@ Blott Carneiro +Collatz Lua Madelaine Mathlib