Add another example

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

examples/lean/ex2.lean

@@ -1,6 +1,17 @@
 Theorem simple (p q r : Bool) : (p ⇒ q) ∧ (q ⇒ r) ⇒ p ⇒ r :=
-    Discharge (λ H1, Discharge (λ H2, MP (Conjunct2 H1) (MP (Conjunct1 H1) H2)))
+    Discharge (λ H_pq_qr, Discharge (λ H_p,
+        let P_pq := Conjunct1 H_pq_qr,
+            P_qr := Conjunct2 H_pq_qr,
+            P_q  := MP P_pq H_p
+        in MP P_qr P_q))
 
 Set pp::implicit true
 Show Environment 1
 
+Theorem simple2 (a b c : Bool) : (a ⇒ b ⇒ c) ⇒ (a ⇒ b) ⇒ a ⇒ c :=
+    Discharge (λ H_abc, Discharge (λ H_ab, Discharge (λ H_a,
+        let P_b  := (MP H_ab H_a),
+            P_bc := (MP H_abc H_a)
+        in MP P_bc P_b)))
+
+Show Environment 1

examples/lean/ex3.lean

@@ -0,0 +1,27 @@
+Theorem and_comm (a b : Bool) : (a ∧ b) ⇒ (b ∧ a) :=
+    Discharge (λ H_ab, Conj (Conjunct2 H_ab) (Conjunct1 H_ab))
+
+Theorem or_comm (a b : Bool) : (a ∨ b) ⇒ (b ∨ a) :=
+    Discharge (λ H_ab, DisjCases H_ab
+                                 (λ H_a, Disj2 b H_a)
+                                 (λ H_b, Disj1 a H_b))
+
+(* ---------------------------------
+(EM a) is the excluded middle  a ∨ ¬a
+(MT H H_na) is Modus Tollens with
+       H    : (a ⇒ b) ⇒ a)
+       H_na : ¬a
+produces
+       ¬(a ⇒ b)
+
+NotImp1 applied to
+        (MT H H_na) : ¬(a ⇒ b)
+produces
+        a
+----------------------------------- *)
+Theorem pierce (a b : Bool) : ((a ⇒ b) ⇒ a) ⇒ a :=
+    Discharge (λ H, DisjCases (EM a)
+                              (λ H_a, H_a)
+                              (λ H_na, NotImp1 (MT H H_na)))
+
+Show Environment 3

src/shell/CMakeLists.txt

@@ -4,6 +4,7 @@ add_executable(lean lean.cpp)
 target_link_libraries(lean ${EXTRA_LIBS})
 add_test(example1 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex1.lean")
 add_test(example2 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex2.lean")
+add_test(example3 ${CMAKE_CURRENT_BINARY_DIR}/lean "${LEAN_SOURCE_DIR}/../examples/lean/ex3.lean")
 add_test(NAME leantests
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean"
          COMMAND "./test.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean")