dselsam

-- PERMANENT
CREATE TABLE sat_problems (
  problem_id BIGINT NOT NULL AUTO_INCREMENT,
  source VARCHAR(128) NOT NULL,
  n_vars BIGINT NOT NULL,
  n_clauses BIGINT NOT NULL,
  bcname VARCHAR(128) NOT NULL,
  bname VARCHAR(2048) NOT NULL,
  PRIMARY KEY(problem_id),
  CONSTRAINT bname_unique UNIQUE(bcname, bname)

dselsam

import Lean
import Std.Data.HashSet

open Lean Lean.PrettyPrinter.Delaborator
open Std (HashSet)

namespace CollectTerms

structure State where
  visitedExpr : HashSet Expr  := {}

dselsam

-- Fail annotations refer to e70e924327c3b42d28dd8a59340a89cbafb3d5b6
namespace ElabArithGoalsNoMathlib

constant Rat     : Type
constant Real    : Type
constant Complex : Type

notation "ℕ" => Nat
notation "ℤ" => Int
notation "ℚ" => Rat

dselsam

import Mathlib.all
import PostPort

namespace ElabArithGoals

open Mathlib hiding coe

variable (k k₁ k₂ k₃ : ℕ)
variable (n n₁ n₂ n₃ : ℕ)
variable (z z₁ z₂ z₃ : ℤ)

dselsam

/-
Design challenge: how to represent problems that require "determining" a set.
------------------------------------------------------------------------------

Consider the following problem:

"""
[IMO 2019, Problem 1]
Let ℤ be the set of integers. Determine all functions f : ℤ → ℤ such that, for all integers a and b,
f(2a) + 2f(b) = f(f(a+b))

dselsam

inductive Term : Type
| const : Nat -> Term
| app   : List Term -> Term

namespace Term
instance : Inhabited Term := ⟨Term.const 0⟩
partial def hasToString : Term -> String | (const n) := "CONST(" ++ toString n ++ ")" | (app ts)  := "APP"
instance : HasToString Term := ⟨hasToString⟩
end Term

dselsam

inductive Term : Type
| const : Nat -> Term
| app   : List Term -> Term

namespace Term
instance : Inhabited Term := ⟨Term.const 0⟩
partial def hasToString : Term -> String | (const n) := "[CONST]" | (app ts)  := "[APP]"
instance : HasToString Term := ⟨hasToString⟩
end Term