33 lines
902 B
Text
33 lines
902 B
Text
open Lean
|
||
|
||
partial def mkBigAnd (n : Nat) (p : Syntax) : MacroM Syntax :=
|
||
loop 0 n
|
||
where
|
||
loop (low high : Nat) : MacroM Syntax := do
|
||
if low == high then
|
||
`($p[natLit! $(quote low)])
|
||
else
|
||
let mid := (low + high)/2
|
||
`($(← loop low mid) ∧ $(← loop (mid + 1) high))
|
||
|
||
macro "bigAnd! " n:num p:ident : term => mkBigAnd n.toNat p
|
||
|
||
partial def mkBigOrNot (n : Nat) (p : Syntax) : MacroM Syntax :=
|
||
loop 0 n
|
||
where
|
||
loop (low high : Nat) : MacroM Syntax := do
|
||
if low == high then
|
||
`(¬ $p[natLit! $(quote low)])
|
||
else
|
||
let mid := (low + high)/2
|
||
`($(← loop low mid) ∨ $(← loop (mid + 1) high))
|
||
|
||
macro "bigOrNot! " n:num p:ident : term => mkBigOrNot n.toNat p
|
||
|
||
@[simp] axiom not_and (p q : Prop) : (¬ (p ∧ q)) = (¬ p ∨ ¬ q)
|
||
|
||
theorem ex (p : Array Prop) : (¬ bigAnd! 2000 p) = bigOrNot! 2000 p := by
|
||
simp only [not_and]
|
||
rfl
|
||
|
||
-- #print ex
|