mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 18:34:06 +00:00
08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
42 lines
1.4 KiB
Lean4
42 lines
1.4 KiB
Lean4
/-! Equational theorem generation regression test.-/
|
||
|
||
structure PrefixTable (α : Type _) extends Array (α × Nat) where
|
||
/-- Validity condition to help with termination proofs -/
|
||
valid : (h : i < toArray.size) → toArray[i].2 ≤ i
|
||
|
||
def PrefixTable.step [BEq α] (t : PrefixTable α) (x : α) (kf : Fin (t.size+1)) : Fin (t.size+1) :=
|
||
match kf with
|
||
| ⟨k, hk⟩ =>
|
||
let cont := fun () =>
|
||
match k with
|
||
| 0 => ⟨0, Nat.zero_lt_succ _⟩
|
||
| k + 1 =>
|
||
have h2 : k < t.size := Nat.lt_of_succ_lt_succ hk
|
||
let k' := t.toArray[k].2
|
||
have hk' : k' < k + 1 := Nat.lt_succ_of_le (t.valid h2)
|
||
step t x ⟨k', Nat.lt_trans hk' hk⟩
|
||
if hsz : k < t.size then
|
||
if x == t.toArray[k].1 then
|
||
⟨k+1, Nat.succ_lt_succ hsz⟩
|
||
else cont ()
|
||
else cont ()
|
||
termination_by kf.val
|
||
|
||
/--
|
||
info: PrefixTable.step.eq_def.{u_1} {α : Type u_1} [BEq α] (t : PrefixTable α) (x : α) (kf : Fin (t.size + 1)) :
|
||
t.step x kf =
|
||
match kf with
|
||
| ⟨k, hk⟩ =>
|
||
have cont := fun x_1 =>
|
||
match k, hk with
|
||
| 0, hk => ⟨0, ⋯⟩
|
||
| k.succ, hk =>
|
||
have h2 := ⋯;
|
||
let k' := t.toArray[k].snd;
|
||
have hk' := ⋯;
|
||
t.step x ⟨k', ⋯⟩;
|
||
if hsz : k < t.size then if (x == t.toArray[k].fst) = true then ⟨k + 1, ⋯⟩ else cont () else cont ()
|
||
-/
|
||
#guard_msgs in
|
||
#check PrefixTable.step.eq_def
|