Proofs with opaque Bool functions

Stream: lean4

[Mac]

How does one prove results utilizing opaque Bool functions? For example, String.contains "zero" 'e'? My guess was to use Lean.ofReduceBool, but I couldn't figure out how exactly one uses it:

example : String.contains "zero" 'e' := by
  apply Lean.ofReduceBool _
  -- what goes here to do the kernel reduction?
  done

Neither rfl, simp, or decide work. I am probably missing something basic, but I unfortunately don't know what.

[Gabriel Ebner]

I don't think it's possible yet to prove anything about partial defs, on the logical side they look exactly like constants. (The partial def in question here is String.anyAux btw.)

[Mac]

@Gabriel Ebner While I get that it is not possible to prove much of anything about the implementation of String.contains due to String.anyAux, shouldn't constant expressions using it still be reducible through reduceBool, since that invokes the Lean interpreter to reduce it (and the interpreter can evaluate such an expression)?

[Gabriel Ebner]

Now I see what you mean. There are still some rough edges here, but this works:

def x := "zero".contains 'e'
example : Lean.reduceBool x := rfl

[Gabriel Ebner]

When the kernel tries to reduce a term Lean.reduceBool c, it will invoke the Lean interpreter to evaluate c.
The kernel will not use the interpreter if c is not a constant.

[Mario Carneiro]

I think there is a macro that does that for you

[Mario Carneiro]

example : "zero".contains 'e' := by nativeDecide

[Mac]

So, I used nativeDecide in my use case and it worked like a charm -- or so I thought. But then I got this error:

def name10.arr :=
  #["zero","one","two","three","four","five","six","seven","eight","nine"]

def name10 (n : Fin 10) : String :=
  name10.arr.get n

theorem name10_mod_2_contains_e :
∀ n, name10 n |>.contains 'e' := by
  intro n
  cases n with
  | mk n h =>
    repeat (cases n; simp [name10, Array.get, List.get]; nativeDecide; rename_i n)
    contradiction

/--
application type mismatch
  Lean.ofReduceBool name10_mod_2_contains_e._nativeDecide_3 true (Eq.refl true)
argument has type
  true = true
but function has type
  Lean.reduceBool name10_mod_2_contains_e._nativeDecide_3 = true → name10_mod_2_contains_e._nativeDecide_3 = true
-/

Any idea what is going on here?

[Mario Carneiro]

it looks like the apply bug

[Mario Carneiro]

reduced:

theorem name10_mod_2_contains_e :
  String.contains "two" 'e' = true := by nativeDecide

It appears the issue is that "two" does not in fact contain the letter e

[Mac]

oops! forgot to add the condition that it is only suppose to be the odd ones :laughing: