solve P47 and P48

Src/Problem47.lean

@@ -0,0 +1,23 @@
+/- # Problem 47
+(Easy 🌟) Truth tables for logical expressions (part 2).
+-/
+
+def table (p : Bool → Bool → Bool) : List (List Bool) :=
+  -- sorry
+  [
+    [true, true, p true true],
+    [true, false, p true false],
+    [false, true, p false true],
+    [false, false, p false false]
+  ]
+  -- sorry
+
+-- The following codes are for test and you should not edit these.
+
+#guard table (fun a b => a && (a || b)) ==
+  [
+    [true, true, true],
+    [true, false, true],
+    [false, true, false],
+    [false, false, false]
+  ]

Src/Problem48.lean

@@ -0,0 +1,55 @@
+/- # Problem 48
+(Easy 🌟) Truth tables for logical expressions (part 3).
+
+Generalize Problem 47 in such a way that the logical expression may contain any number of logical variables. Define table/2 in a way that table(List,Expr) prints the truth table for the expression Expr, which contains the logical variables enumerated in List.
+-/
+universe u
+
+/-- monad instance of `List` -/
+instance : Monad List.{u} where
+  pure := @List.pure
+  bind := @List.bind
+  map := @List.map
+
+def Arity : (n : Nat) → Type
+  | 0 => Bool
+  | n + 1 => Bool → Arity n
+
+def tablen (n : Nat) (p : Arity n) : List (List Bool) :=
+  -- sorry
+  match n with
+  | 0 => [[p]]
+  | n + 1 => do
+    let b ← [true, false]
+    let result ← tablen n (p b) |>.map (b :: ·)
+    return result
+  -- sorry
+
+-- The following codes are for test and you should not edit these.
+
+#guard tablen 1 (fun a => a) = [[true, true], [false, false]]
+
+#guard tablen 2 (fun a b => a && b) = [
+  [true, true, true],
+  [true, false, false],
+  [false, true, false],
+  [false, false, false]
+]
+
+#guard tablen 2 (fun a b => !a || b) = [
+  [true, true, true],
+  [true, false, false],
+  [false, true, true],
+  [false, false, true]
+]
+
+#eval tablen 3 (fun a b c => a && b && c) = [
+  [true, true, true, true],
+  [true, true, false, false],
+  [true, false, true, false],
+  [true, false, false, false],
+  [false, true, true, false],
+  [false, true, false, false],
+  [false, false, true, false],
+  [false, false, false, false]
+]

md/SUMMARY.md

@@ -56,4 +56,6 @@
 
 # 46-50: Logic and codes
 
-* [46: Truth table](./build/Problem46.md)
+* [46: Truth table](./build/Problem46.md)
+* [47: Truth table part2](./build/Problem47.md)
+* [48: Truth table in general](./build/Problem48.md)