feat(logic): make some decidability proofs [inline] (leanprover-commu…

…nity#1393)

* feat(logic): make some decidability proofs [inline]

* inline more decidability proofs

* test

* import logic.basic in test

src/logic/basic.lean

@@ -18,6 +18,11 @@ maybe it is useful for writing automation.
 
 section miscellany
 
+/- We add the `inline` attribute to optimize VM computation using these declarations. For example,
+  `if p ∧ q then ... else ...` will not evaluate the decidability of `q` if `p` is false. -/
+attribute [inline] and.decidable or.decidable decidable.false xor.decidable iff.decidable
+  decidable.true implies.decidable not.decidable ne.decidable
+
 variables {α : Type*} {β : Type*}
 
 @[reducible] def hidden {a : α} := a

test/logic_inline.lean

@@ -0,0 +1,13 @@
+/-
+Copyright (c) 2019 Keeley Hoek. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Keeley Hoek, Floris van Doorn
+-/
+
+import logic.basic
+meta def error_msg (s : string) : bool := @undefined_core bool $ s ++ ".decidable not inlined"
+
+meta def examine (b : Prop) [decidable b] : bool := b
+
+#eval examine $ ff ∧ (error_msg "and")
+#eval examine $ tt ∨ (error_msg "or")