Add evaluation datasets

.gitattributes

@@ -1 +1,2 @@
 data/*.sql.xz filter=lfs diff=lfs merge=lfs -text
+data/*.sql.tar.gz filter=lfs diff=lfs merge=lfs -text

data/Prop_name.txt

@@ -0,0 +1,100 @@
+Nat.add_comm
+Nat.lt_asymm
+Nat.div_eq_sub_div
+Nat.gcd_mul_left
+Fin.val_add_one_le_of_lt
+Nat.mul_div_left
+Nat.add_div_right
+Nat.div_eq_of_lt_le
+Nat.mul_div_le
+Nat.exists_eq_add_of_le
+Nat.add_one_le_add_one_iff
+Nat.div_eq_of_lt_le
+Nat.nextPowerOfTwo_dec
+Nat.add_lt_add_of_le_of_lt
+Nat.add_sub_cancel_right
+Nat.sub_le_iff_le_add
+Nat.mul_left_cancel
+Nat.mul_lt_mul_of_lt_of_le
+Nat.pow_lt_pow_of_lt
+Nat.dvd_gcd
+Nat.add_left_comm
+Nat.add_right_comm
+Nat.add_left_cancel
+Nat.add_right_cancel
+Nat.eq_zero_of_add_eq_zero
+Nat.eq_zero_of_add_eq_zero_left
+Nat.mul_zero
+Nat.mul_succ
+Nat.mul_add_one
+Nat.zero_mul
+Nat.succ_mul
+Fin.ne_of_val_ne
+Fin.val_ne_of_ne
+Fin.modn_lt
+Fin.val_lt_of_le
+Fin.pos
+Fin.ne_of_val_ne
+Fin.val_inj
+Fin.val_congr
+Fin.val_le_of_le
+Fin.val_le_of_ge
+Fin.val_add_one_le_of_lt
+Fin.val_add_one_le_of_gt
+Fin.exists_iff
+Nat.exists_ne_zero
+Nat.exists_eq_add_one
+Nat.exists_add_one_eq
+Nat.forall_lt_succ_right'
+Nat.forall_lt_succ_right
+Nat.forall_lt_succ_left'
+Nat.forall_lt_succ_left
+Nat.exists_lt_succ_right'
+Nat.exists_lt_succ_right
+Nat.exists_lt_succ_left'
+Nat.exists_lt_succ_left
+Nat.add_add_add_comm
+Nat.one_add
+Nat.succ_eq_one_add
+Nat.succ_add_eq_add_succ
+Nat.eq_zero_of_add_eq_zero_right
+Nat.add_eq_zero_iff
+Nat.add_left_cancel_iff
+Nat.add_right_cancel_iff
+Nat.add_left_eq_self
+Nat.add_right_eq_self
+Nat.self_eq_add_right
+Nat.self_eq_add_left
+Nat.add_le_add_iff_left
+Nat.lt_of_add_lt_add_right
+Nat.lt_of_add_lt_add_left
+Nat.add_lt_add_iff_left
+Nat.add_lt_add_iff_right
+Nat.add_lt_add_of_le_of_lt
+Nat.add_lt_add_of_lt_of_le
+Nat.pos_of_lt_add_right
+Nat.pos_of_lt_add_left
+Nat.lt_add_right_iff_pos
+Nat.lt_add_left_iff_pos
+Nat.add_pos_left
+Nat.add_pos_right
+Nat.add_self_ne_one
+Nat.sub_one
+Nat.one_sub
+Nat.succ_sub_sub_succ
+Nat.add_sub_sub_add_right
+Nat.sub_right_comm
+Nat.add_sub_cancel_right
+Nat.add_sub_cancel'
+Nat.succ_sub_one
+Nat.one_add_sub_one
+Nat.sub_sub_self
+Nat.sub_add_comm
+Nat.sub_eq_zero_iff_le
+Nat.sub_pos_iff_lt
+Nat.sub_le_iff_le_add
+Nat.sub_le_iff_le_add'
+Nat.le_sub_iff_add_le
+Int.lcm_ne_zero
+Int.dvd_lcm_left
+Int.dvd_lcm_right

data/README.md

@@ -0,0 +1,84 @@
+\# Data
+
+
+
+This directory contains the database dumps and test sets used in this repository.
+
+
+
+\## Files
+
+
+
+\- `mathlib\_filtered\_backup0515.sql.xz`  
+
+  PostgreSQL dump of the `mathlib\_filtered` table. This table contains the filtered Mathlib theorem corpus used as the retrieval candidate library.
+
+
+
+\- `wl\_encodings\_new\_backup0515.sql.xz`  
+
+  PostgreSQL dump of the precomputed WL/tree encodings used by the retrieval pipeline.
+
+
+
+\- `expressions.txt`  
+
+  Query expressions for Test Set A. Each line is one Lean-style query expression.
+
+
+
+\- `Prop\_name.txt`  
+
+  Ground-truth theorem names for Test Set A. Line `i` corresponds to line `i` in `expressions.txt`.
+
+
+
+\- `test\_set\_B\_tactic\_step.sql.tar.gz`  
+
+  Compressed PostgreSQL backup for Test Set B. It contains proof-step records used to reconstruct the evaluation examples.
+
+
+
+\## Test Set A
+
+
+
+Test Set A is a small manually constructed benchmark for premise selection.
+
+
+
+It consists of two line-aligned files:
+
+
+
+```text
+
+expressions.txt
+
+Prop\_name.txt
+
+
+
+The correspondence is:
+
+
+
+expressions.txt line i  -> query expression
+
+Prop\_name.txt   line i  -> target theorem name
+
+Test Set B
+
+
+
+Test Set B is provided as a compressed PostgreSQL backup:
+
+
+
+test\_set\_B\_tactic\_step.sql.tar.gz
+
+
+
+It is built from proof-step records extracted from Lean proof traces.
+

data/expressions.txt

@@ -0,0 +1,100 @@
+q((n m : Nat) → (n + 1) + m = m + (n + 1))
+q({a b c : Nat} →  (h : a + c < b) → ¬ b < a + c)
+q({b a : Nat} →  (h₁ : 0 < b) → (h₂ : b ≤ a.succ) → a.succ / b = (a.succ - b) / b + 1)
+q((m n k : Nat) →  (m.succ * n).gcd (m.succ * k) = m.succ * n.gcd k)
+q({n : Nat} → {a b : Fin n.succ} → (h : a < b) → ↑a + 1 ≤ ↑b)
+q((m : Nat) → {n : Nat} → (H : 0 < n.pred) → m * n.pred / n.pred = m)
+q((x : Nat) → {z₁ z₂ : Nat} → (H : 0 < z₁ + z₂) → (x + (z₁ + z₂)) / (z₁ + z₂) = x / (z₁ + z₂) + 1)
+q({k n m : Nat}→  (lo : k.pred * n.succ ≤ m) → (hi : m < (k.pred + 1) * n.succ) → m / n.succ = k.pred)
+q((m n r : Nat) →  n * ((m + r) / n) ≤ m + r)
+q({m n : Nat} → (h : m ≤ n.succ) → ∃ k, n.succ = m + k)
+q({a b : Nat} → a + 2 ≤ b + 2 ↔ a ≤ b)
+q({k n m : Nat} → (hi : m < (k + 1) * n) → (lo : k * n ≤ m) →  m / n = k)
+q({n power : Nat} → (h₂ : power < n) → (h₁ : power > 0) → n - power * 2 < n - power)
+q({a b c d : Nat} → (hlt : c < d) → (hle : a ≤ b) → a + c < b + d)
+q((n m : Nat) →  n = n + m - m)
+q({a b c : Nat} → a ≤ c + b ↔ a - b ≤ c)
+q({n m k : Nat} → (h : n * m.succ = n * k) → (np : 0 < n) → m.succ = k)
+q({a c b d : Nat} → (hbd : b ≤ d.succ) → (hac : a < c) → (hd : 0 < d.succ) → a * b < c * d.succ)
+q({a n m : Nat} → (w : n < m) → (h : 1 < a.pred) → a.pred ^ n < a.pred ^ m)
+q({k m n : Nat} → k.succ ∣ m → k.succ ∣ n → k.succ ∣ m.gcd n)
+q((b c : Nat) → 1 + (b + c) = b + (1 + c))
+q((n b c : Nat) → (n + b) + c = (n + c) + b)
+q({a b : Nat} → a + b = a + 1 → b = 1)
+q({a b : Nat} → a + (b + 1) = (b + 1) + a → a = b)
+q({a : Nat} → a + 0 = 0 → a = 0)
+q({a n: Nat} → a + (n + 1) = 0 → (n + 1) = 0)
+q((b : Nat) → b * 0 = 0)
+q((a n : Nat) → a * (n + 1).succ = a * (n + 1) + a)
+q((a : Nat) → a * (1 + 1) = a * 1 + a)
+q((a : Nat) → 0 * 0 = 0)
+q((n m : Nat) → (n + 1).succ * m = (n + 1) * m + m)
+q((n : Nat) → (i j : Fin n) → i.val ≠ j.val → i ≠ j)
+q((n : Nat) → (i j : Fin n) → i ≠ j → i.val ≠ j.val)
+q({n m : Nat} → (i : Fin n) → m > 0 → (Fin.modn i m).val < m)
+q((b n : Nat) → (i : Fin b) → b ≤ n → i.val < n)
+q((n : Nat) → (i : Fin n) → 0 < n)
+q((n : Nat) → (i j : Fin n) → i.val ≠ j.val → i ≠ j)
+q((n : Nat) → {a b : Fin n} → a.1 = b.1 ↔ a = b)
+q({n : Nat} → {a b : Fin n} → a = b → (a : Nat) = (b : Nat))
+q({n : Nat} → {a b : Fin n} → a ≤ b → (a : Nat) ≤ (b : Nat))
+q({n : Nat} → {a b : Fin n} → a ≥ b → (b : Nat) ≤ (a : Nat))
+q({n : Nat} → {a b : Fin n} → a < b → (a : Nat) + 1 ≤ (b : Nat))
+q({n : Nat} → {a b : Fin n} → a > b → (b : Nat) + 1 ≤ (a : Nat))
+q((n : Nat) → {p : Fin n → Prop} → (∃ i, p i) ↔ ∃ i, ∃ h, p ⟨i, h⟩)
+q((P : Nat → Prop) → (∃ n, ¬ n = 0 ∧ P n) ↔ ∃ n, P (n + 1))
+q((a : Nat) → (∃ n, a = n + 1) ↔ 0 < a)
+q((a : Nat) → (∃ n, n + 1 = a) ↔ 0 < a)
+q((n : Nat) → (p : (m : Nat) → (m < n + 1) → Prop) → (∀ m (h : m < n + 1), p m h) ↔ (∀ m (h : m < n), p m (by omega)) ∧ p n (by omega))
+q((n : Nat) → (p : Nat → Prop) → (∀ m, m < n + 1 → p m) ↔ (∀ m, m < n → p m) ∧ p n)
+q((n : Nat) → (p : (m : Nat) → (m < n + 1) → Prop) → (∀ m (h : m < n + 1), p m h) ↔ p 0 (by omega) ∧ (∀ m (h : m < n), p (m + 1) (by omega)))
+q((n : Nat) → (p : Nat → Prop) → (∀ m, m < n + 1 → p m) ↔ p 0 ∧ (∀ m, m < n → p (m + 1)))
+q((n : Nat) → (p : (m : Nat) → (m < n + 1) → Prop) → (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m (by omega)) ∨ p n (by omega))
+q((n : Nat) → (p : Nat → Prop) → (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n)
+q((n : Nat) → (p : (m : Nat) → (m < n + 1) → Prop) → (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 (by omega) ∨ (∃ m, ∃ (h : m < n), p (m + 1) (by omega)))
+q((n : Nat) → (p : Nat → Prop) → (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ (∃ m, m < n ∧ p (m + 1)))
+q((a b c d : Nat) → (a + b) + (c + d) = (a + c) + (b + d))
+q((n : Nat) → 1 + n = n.succ)
+q((n : Nat) → n.succ = 1 + n)
+q((a b : Nat) → a.succ + b = a + b.succ)
+q((n m : Nat) → n + m = 0 → n = 0)
+q((n m : Nat) → n + m = 0 ↔ n = 0 ∧ m = 0)
+q((n m k : Nat) → n + m = n + k ↔ m = k)
+q((n m k : Nat) → m + n = k + n ↔ m = k)
+q((a b : Nat) → a + b = b ↔ a = 0)
+q((a b : Nat) → a + b = a ↔ b = 0)
+q((a b : Nat) → a = a + b ↔ b = 0)
+q((a b : Nat) → a = b + a ↔ b = 0)
+q((n m k : Nat) → n + m ≤ n + k ↔ m ≤ k)
+q((k n m : Nat) → k + n < m + n → k < m)
+q((n k m : Nat) → n + k < n + m → k < m)
+q((k n m : Nat) → k + n < k + m ↔ n < m)
+q((k n m : Nat) → n + k < m + k ↔ n < m)
+q((a b c d : Nat) → a ≤ b → c < d → a + c < b + d)
+q((a b c d : Nat) → a < b → c ≤ d → a + c < b + d)
+q((n k : Nat) → n < n + k → 0 < k)
+q((n k : Nat) → n < k + n → 0 < k)
+q((n k : Nat) → n < n + k ↔ 0 < k)
+q((n k : Nat) → n < k + n ↔ 0 < k)
+q((m n : Nat) → 0 < m → 0 < m + n)
+q((m n : Nat) → 0 < n → 0 < m + n)
+q((n : Nat) → n + n ≠ 1)
+q((n : Nat) → n - 1 = n.pred)
+q((n : Nat) → 1 - n = if n = 0 then 1 else 0)
+q((n m k : Nat) → n.succ - m - k.succ = n - m - k)
+q((n m k l : Nat) → (n + l) - m - (k + l) = n - m - k)
+q((m n k : Nat) → m - n - k = m - k - n)
+q((n m : Nat) → (n + m) - m = n)
+q((n m : Nat) → m ≤ n → m + (n - m) = n)
+q((n : Nat) → n.succ - 1 = n)
+q((n : Nat) → (1 + n) - 1 = n)
+q((n m : Nat) → m ≤ n → n - (n - m) = m)
+q((n m k : Nat) → k ≤ n → n + m - k = n - k + m)
+q((n m : Nat) → n - m = 0 ↔ n ≤ m)
+q((n m : Nat) → 0 < n - m ↔ m < n)
+q((a b c : Nat) → a - b ≤ c ↔ a ≤ c + b)
+q((a b c : Nat) → a - b ≤ c ↔ a ≤ b + c)
+q((n k m : Nat) → k ≤ m → n ≤ m - k ↔ n + k ≤ m)
+q((n m : Int) → m + 1 ≠ 0 → n ≠ 0 → Int.lcm (m + 1) n ≠ 0)
+q({a : Int} → a ∣ Int.lcm a 1)
+q({a : Int} → 1 ∣ Int.lcm a 1 )