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.
82 lines
3.6 KiB
Text
82 lines
3.6 KiB
Text
/-!
|
||
# Regression tests for isInstance changes in congruence lemma generation
|
||
|
||
These tests verify that `congr` works correctly for structures and classes
|
||
with class-typed fields. They catch regressions from changes to how instance
|
||
parameters are detected (e.g., using `isClass?` instead of binder info).
|
||
|
||
Both tests pass on v4.28.0-rc1 (before the isInstance changes).
|
||
|
||
## Test 1: Structure extending classes (mirrors Mathlib's GroupTopology)
|
||
|
||
When a structure extends both a data class and a Prop class, the parent class
|
||
field may be marked as `isInstance = true`. If this causes `.fixed` treatment
|
||
in congruence lemma generation, dependent Prop fields will require HEq.
|
||
|
||
**Failure mode:** `⊢ toIsContinuousMul✝¹ ≍ toIsContinuousMul✝`
|
||
|
||
## Test 2: Class with explicit class-typed field (mirrors Mathlib's PseudoEMetricSpace)
|
||
|
||
When a class has an explicit class-typed field (not from `extends`), that field
|
||
may be marked as `isInstance = true`. If this causes `.fixed` treatment, then
|
||
dependent Prop fields whose types mention that field will require HEq.
|
||
|
||
**Failure mode:** `⊢ dist_self✝¹ ≍ dist_self✝` and `⊢ uniformity_dist✝¹ ≍ uniformity_dist✝`
|
||
-/
|
||
|
||
/-! ### Test 1: Structure extending classes -/
|
||
|
||
-- Setup: mimic Mathlib's GroupTopology structure
|
||
class MyTopology (α : Type) where
|
||
isOpen : (α → Prop) → Prop
|
||
|
||
-- A Prop-valued class that depends on MyTopology
|
||
class IsContinuousMul (α : Type) [MyTopology α] : Prop where
|
||
continuous_mul : True -- simplified
|
||
|
||
-- Structure extending both a data class and a Prop class
|
||
structure MyGroupTopology (α : Type) extends MyTopology α, IsContinuousMul α
|
||
|
||
-- Key test: proving injectivity of the parent projection using `congr`
|
||
-- If the toMyTopology field gets `.fixed` treatment, the Prop-valued
|
||
-- toIsContinuousMul field will require HEq: `⊢ toIsContinuousMul✝¹ ≍ toIsContinuousMul✝`
|
||
theorem MyGroupTopology.toMyTopology_injective {α : Type} :
|
||
Function.Injective (MyGroupTopology.toMyTopology : MyGroupTopology α → MyTopology α) := by
|
||
intro f g h
|
||
cases f
|
||
cases g
|
||
congr
|
||
|
||
/-! ### Test 2: Class with explicit class-typed field -/
|
||
|
||
-- Setup: mimic Mathlib's PseudoEMetricSpace pattern
|
||
-- A class that extends one class but has another class-typed field explicitly
|
||
|
||
class MyDist (α : Type) where
|
||
dist : α → α → Nat
|
||
|
||
class MyUniformity (α : Type) where
|
||
uniformity : (α → α → Prop) → Prop
|
||
|
||
-- Class that extends MyDist but has an explicit MyUniformity field
|
||
-- This mirrors PseudoEMetricSpace which extends EDist but has explicit toUniformSpace
|
||
class MyMetricSpace (α : Type) extends MyDist α where
|
||
dist_self : ∀ x : α, dist x x = 0
|
||
-- Explicit class-typed field (NOT from extends)
|
||
toMyUniformity : MyUniformity α
|
||
-- Prop field whose type depends on toMyUniformity
|
||
uniformity_dist : toMyUniformity.uniformity (fun x y => dist x y = 0)
|
||
|
||
-- Key test: extensionality theorem using `congr`
|
||
-- If toMyUniformity gets `.fixed` treatment (because it's class-typed but not
|
||
-- a subobject field), then `congr` will produce HEq goals for dependent fields
|
||
protected theorem MyMetricSpace.ext {α : Type} {m m' : MyMetricSpace α}
|
||
(h : m.toMyDist = m'.toMyDist) (hU : m.toMyUniformity = m'.toMyUniformity) : m = m' := by
|
||
cases m
|
||
cases m'
|
||
-- After cases, we need to prove the constructors are equal
|
||
-- `congr` should produce goals for data fields (dist, toMyUniformity)
|
||
-- and automatically handle Prop fields (dist_self, uniformity_dist) via casting
|
||
-- If toMyUniformity gets `.fixed` treatment, we'd see HEq goals like:
|
||
-- `⊢ dist_self✝¹ ≍ dist_self✝` or `⊢ uniformity_dist✝¹ ≍ uniformity_dist✝`
|
||
congr 1 <;> assumption
|