test: native_decide

tests/lean/run/state12.lean

@@ -0,0 +1,185 @@
+/- Enumerable and the Decidable instance may already be in Mathlib -/
+
+class Enumerable (α : Type u) where
+  elems    : List α
+  complete : ∀ a : α, a ∈ elems
+
+def List.allTrue (p : α → Prop) [(a : α) → Decidable (p a)] : List α → Bool
+  | [] => true
+  | a :: as => p a && allTrue p as
+
+theorem List.of_allTrue [(a : α) → Decidable (p a)] (hc : allTrue p as) (hin : a ∈ as) : p a := by
+  induction as with
+  | nil => contradiction
+  | cons b bs ih =>
+    cases hin with simp [allTrue] at hc
+    | head => simp [*]
+    | tail _ h => exact ih hc.2 h
+
+theorem List.allTrue_of_forall [(a : α) → Decidable (p a)] (h : ∀ a, p a) : allTrue p as := by
+  induction as <;> simp [allTrue, *]
+
+instance [Enumerable α] (p : α → Prop) [(a : α) → Decidable (p a)] : Decidable (∀ a, p a) :=
+  have : List.allTrue p Enumerable.elems → (a : α) → p a :=
+    fun h a => List.of_allTrue h (Enumerable.complete a)
+  decidable_of_decidable_of_iff (Iff.intro this List.allTrue_of_forall)
+
+inductive States | s0 | s1 | s2 | s3 | s4 | s5 | s6 | s7 | s8 | s9 | s10 | s11
+deriving DecidableEq
+
+/- We can add a `deriving` for `Enumerable` in the future. -/
+open States in
+instance : Enumerable States where
+  elems := [s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11]
+  complete a := by cases a <;> decide
+
+open States
+def f : States → States → States
+| s0, s0 => s0
+| s0, s1 => s0
+| s0, s2 => s0
+| s0, s3 => s0
+| s0, s4 => s0
+| s0, s5 => s0
+| s0, s6 => s0
+| s0, s7 => s0
+| s0, s8 => s0
+| s0, s9 => s0
+| s0, s10 => s0
+| s0, s11 => s0
+| s1, s0 => s0
+| s1, s1 => s0
+| s1, s2 => s0
+| s1, s3 => s0
+| s1, s4 => s0
+| s1, s5 => s0
+| s1, s6 => s0
+| s1, s7 => s0
+| s1, s8 => s0
+| s1, s9 => s0
+| s1, s10 => s0
+| s1, s11 => s0
+| s2, s0 => s0
+| s2, s1 => s0
+| s2, s2 => s0
+| s2, s3 => s0
+| s2, s4 => s0
+| s2, s5 => s0
+| s2, s6 => s0
+| s2, s7 => s0
+| s2, s8 => s0
+| s2, s9 => s0
+| s2, s10 => s0
+| s2, s11 => s0
+| s3, s0 => s0
+| s3, s1 => s0
+| s3, s2 => s0
+| s3, s3 => s0
+| s3, s4 => s0
+| s3, s5 => s0
+| s3, s6 => s0
+| s3, s7 => s0
+| s3, s8 => s0
+| s3, s9 => s0
+| s3, s10 => s0
+| s3, s11 => s0
+| s4, s0 => s0
+| s4, s1 => s0
+| s4, s2 => s0
+| s4, s3 => s0
+| s4, s4 => s0
+| s4, s5 => s0
+| s4, s6 => s0
+| s4, s7 => s0
+| s4, s8 => s0
+| s4, s9 => s0
+| s4, s10 => s0
+| s4, s11 => s0
+| s5, s0 => s0
+| s5, s1 => s0
+| s5, s2 => s0
+| s5, s3 => s0
+| s5, s4 => s0
+| s5, s5 => s0
+| s5, s6 => s0
+| s5, s7 => s0
+| s5, s8 => s0
+| s5, s9 => s0
+| s5, s10 => s0
+| s5, s11 => s0
+| s6, s0 => s0
+| s6, s1 => s0
+| s6, s2 => s0
+| s6, s3 => s0
+| s6, s4 => s0
+| s6, s5 => s0
+| s6, s6 => s0
+| s6, s7 => s0
+| s6, s8 => s0
+| s6, s9 => s0
+| s6, s10 => s0
+| s6, s11 => s0
+| s7, s0 => s0
+| s7, s1 => s0
+| s7, s2 => s0
+| s7, s3 => s0
+| s7, s4 => s0
+| s7, s5 => s0
+| s7, s6 => s0
+| s7, s7 => s0
+| s7, s8 => s0
+| s7, s9 => s0
+| s7, s10 => s0
+| s7, s11 => s0
+| s8, s0 => s0
+| s8, s1 => s0
+| s8, s2 => s0
+| s8, s3 => s0
+| s8, s4 => s0
+| s8, s5 => s0
+| s8, s6 => s0
+| s8, s7 => s0
+| s8, s8 => s0
+| s8, s9 => s0
+| s8, s10 => s0
+| s8, s11 => s0
+| s9, s0 => s0
+| s9, s1 => s0
+| s9, s2 => s0
+| s9, s3 => s0
+| s9, s4 => s0
+| s9, s5 => s0
+| s9, s6 => s0
+| s9, s7 => s0
+| s9, s8 => s0
+| s9, s9 => s0
+| s9, s10 => s0
+| s9, s11 => s0
+| s10, s0 => s0
+| s10, s1 => s0
+| s10, s2 => s0
+| s10, s3 => s0
+| s10, s4 => s0
+| s10, s5 => s0
+| s10, s6 => s0
+| s10, s7 => s0
+| s10, s8 => s0
+| s10, s9 => s0
+| s10, s10 => s0
+| s10, s11 => s0
+| s11, s0 => s0
+| s11, s1 => s0
+| s11, s2 => s0
+| s11, s3 => s0
+| s11, s4 => s0
+| s11, s5 => s0
+| s11, s6 => s0
+| s11, s7 => s0
+| s11, s8 => s0
+| s11, s9 => s0
+| s11, s10 => s0
+| s11, s11 => s0
+
+set_option maxHeartbeats 0
+example : ∀ x y z, f (f (f s0 x) y) z = f (f x z) (f y z) := by
+ native_decide -- This is fast, but the TCB is much bigger