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.
26 lines
1.2 KiB
Text
26 lines
1.2 KiB
Text
inductive Lex (ra : α → α → Prop) (rb : β → β → Prop) : α × β → α × β → Prop where
|
||
| left {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Lex ra rb (a₁, b₁) (a₂, b₂)
|
||
| right (a) {b₁ b₂} (h : rb b₁ b₂) : Lex ra rb (a, b₁) (a, b₂)
|
||
|
||
|
||
def lexAccessible1 {ra : α → α → Prop} {rb : β → β → Prop} (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by
|
||
induction aca a generalizing b with
|
||
| intro xa aca iha =>
|
||
induction acb b with
|
||
| intro xb acb ihb =>
|
||
apply Acc.intro (xa, xb)
|
||
intro p lt
|
||
cases lt with
|
||
| left b1 b2 h => apply iha _ h
|
||
| @right a b1 b2 h => apply ihb _ h
|
||
|
||
def lexAccessible2 {ra : α → α → Prop} {rb : β → β → Prop} (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by
|
||
induction (aca a) generalizing b with
|
||
| intro xa aca iha =>
|
||
induction (acb b) with
|
||
| intro xb acb ihb =>
|
||
apply Acc.intro (xa, xb)
|
||
intro p lt
|
||
cases lt with
|
||
| @left a1 b1 a2 b2 h => apply iha _ h
|
||
| right _ h => apply ihb _ h
|