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.
124 lines
2.6 KiB
Text
124 lines
2.6 KiB
Text
import Lean
|
||
/-!
|
||
# Proper handling of delayed assignment metavariables in `match` elaboration
|
||
|
||
https://github.com/leanprover/lean4/issues/5925
|
||
https://github.com/leanprover/lean4/issues/6354
|
||
|
||
These all had the error `(kernel) declaration has metavariables '_example'`
|
||
due to underapplied delayed assignment metavariables never being instantiated.
|
||
-/
|
||
|
||
namespace Test1
|
||
/-!
|
||
Simplified version of example from issue 6354.
|
||
-/
|
||
|
||
structure A where
|
||
p: Prop
|
||
q: True
|
||
|
||
example := (λ ⟨_,_⟩ ↦ True.intro : (A.mk (And True True) (by exact True.intro)).p → True)
|
||
|
||
end Test1
|
||
|
||
|
||
namespace Test2
|
||
/-!
|
||
Example from issue 6354 (by @roos-j)
|
||
-/
|
||
|
||
structure A where
|
||
p: Prop
|
||
q: True
|
||
|
||
structure B extends A where
|
||
q': p → True
|
||
|
||
example: B where
|
||
p := True ∧ True
|
||
q := by exact True.intro
|
||
q' := λ ⟨_,_⟩ ↦ True.intro
|
||
|
||
end Test2
|
||
|
||
|
||
namespace Test3
|
||
/-!
|
||
Example from issue 6354 (by @b-mehta)
|
||
-/
|
||
|
||
class Preorder (α : Type) extends LE α, LT α where
|
||
le_refl : ∀ a : α, a ≤ a
|
||
lt := fun a b => a ≤ b ∧ ¬b ≤ a
|
||
|
||
class PartialOrder (α : Type) extends Preorder α where
|
||
le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b
|
||
|
||
inductive MyOrder : Nat × Nat → Nat × Nat → Prop
|
||
| within {x u m : Nat} : x ≤ u → MyOrder (x, m) (u, m)
|
||
|
||
instance : PartialOrder (Nat × Nat) where
|
||
le := MyOrder
|
||
le_refl x := .within (Nat.le_refl _)
|
||
le_antisymm | _, _, .within _, .within _ => Prod.ext (Nat.le_antisymm ‹_› ‹_›) rfl
|
||
|
||
end Test3
|
||
|
||
|
||
namespace Test4
|
||
/-!
|
||
Example from issue 5925 (by @Komyyy)
|
||
-/
|
||
|
||
def Injective (f : α → β) : Prop :=
|
||
∀ ⦃a₁ a₂⦄, f a₁ = f a₂ → a₁ = a₂
|
||
|
||
axiom my_mul_right_injective {M₀ : Type} [Mul M₀] [Zero M₀] {a : M₀} (ha : a ≠ 0) :
|
||
Injective fun (x : M₀) ↦ a * x
|
||
|
||
def mul2 : { f : Nat → Nat // Injective f } := ⟨fun x : Nat ↦ 2 * x, my_mul_right_injective nofun⟩
|
||
|
||
end Test4
|
||
|
||
|
||
namespace Test5
|
||
/-!
|
||
Example from issue 5925 (by @mik-jozef)
|
||
-/
|
||
|
||
structure ValVar (D: Type) where
|
||
d: D
|
||
x: Nat
|
||
|
||
def Set (T : Type) := T → Prop
|
||
|
||
structure Salg where
|
||
D: Type
|
||
I: Nat
|
||
|
||
def natSalg: Salg := { D := Nat, I := 42 }
|
||
|
||
inductive HasMem (salg: Salg): Set (Set (ValVar salg.D))
|
||
| hasMem
|
||
(set: Set (ValVar salg.D))
|
||
(isElem: set ⟨d, x⟩)
|
||
:
|
||
HasMem salg set
|
||
|
||
def valVarSet: Set (ValVar Nat) :=
|
||
fun ⟨d, x⟩ => x = 0 ∧ d = 0 ∧ d ∉ []
|
||
|
||
-- Needed to add a unification hint to this test
|
||
-- because of https://github.com/leanprover/lean4/pull/6024
|
||
unif_hint (s : Salg) where
|
||
s =?= natSalg
|
||
|-
|
||
Salg.D s =?= Nat
|
||
|
||
def valVarSetHasMem: HasMem natSalg valVarSet :=
|
||
HasMem.hasMem
|
||
valVarSet
|
||
(show valVarSet _ from ⟨rfl, rfl, nofun⟩)
|
||
|
||
end Test5
|