Let be a function from the natural numbers to the booleans. Suppose that for all , if is true, then is true. Prove that either:
- is false for all .
- There exists such that .
This proof has applications, too. For example, let denote the truth value of " does not contain consecutive 's in its decimal representation." Either , or there exists such that . Therefore, has a constant time algorithm, but the exact algorithm remains unknown.
Definitions
-- header.lean
def Simple (f : Nat → Bool) : Prop :=
f = (fun _ => false) ∨
∃ n, f = (fun x => if x < n then false else true)
def NonconstructiveConstantTime : Prop :=
∀ p : Nat → Bool,
(∀ n, p n → p (n + 1)) →
Simple p
macro "check0123456789abcdef" t:ident : command => `(
example : NonconstructiveConstantTime := $t
#print axioms $t
)
Note: The macro's name is randomly generated on each submission, and will follow the format check[0-9a-f]{16}
.
Proof Format
Your goal is to define a term proof
with the type NonconstructiveConstantTime
. You may use this template for your submission:
-- submission.lean
open Classical
def proof : NonconstructiveConstantTime := by
admit
The judge will automatically prepend import header
to your submission.
You may use the following axioms: Classical.choice
, Quot.sound
, propext
Checker
-- entry.lean
import header
import submission
check0123456789abcdef proof -- 'proof' depends on axioms: [Classical.choice, Quot.sound, propext]
If you find a way to fool the checker, please open a ticket by clicking the "Report an issue" button at the bottom of the page, then put your submission in the ticket.
Comments