81 lines
2.8 KiB
Plaintext
81 lines
2.8 KiB
Plaintext
import LSpec
|
||
import Lean
|
||
import Test.Common
|
||
|
||
open Lean
|
||
open Pantograph
|
||
|
||
namespace Pantograph.Test.Tactic.Congruence
|
||
|
||
def test_congr_arg (env: Environment): IO LSpec.TestSeq :=
|
||
let expr := "λ (n m: Nat) (h: n = m) => n * n = m * m"
|
||
runMetaMSeq env do
|
||
let expr ← parseSentence expr
|
||
Meta.lambdaTelescope expr $ λ _ body => do
|
||
let mut tests := LSpec.TestSeq.done
|
||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||
let test ← runTermElabMInMeta do
|
||
let newGoals ← runTacticOnMVar Tactic.congruenceArg target.mvarId!
|
||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||
[
|
||
(`α, "Sort ?u.70"),
|
||
(`a₁, "?α"),
|
||
(`a₂, "?α"),
|
||
(`f, "?α → Nat"),
|
||
(`h, "?a₁ = ?a₂"),
|
||
(`conduit, "(?f ?a₁ = ?f ?a₂) = (n * n = m * m)"),
|
||
])
|
||
tests := tests ++ test
|
||
return tests
|
||
def test_congr_fun (env: Environment): IO LSpec.TestSeq :=
|
||
let expr := "λ (n m: Nat) => (n + m) + (n + m) = (n + m) * 2"
|
||
runMetaMSeq env do
|
||
let expr ← parseSentence expr
|
||
Meta.lambdaTelescope expr $ λ _ body => do
|
||
let mut tests := LSpec.TestSeq.done
|
||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||
let test ← runTermElabMInMeta do
|
||
let newGoals ← runTacticOnMVar Tactic.congruenceFun target.mvarId!
|
||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||
[
|
||
(`α, "Sort ?u.159"),
|
||
(`f₁, "?α → Nat"),
|
||
(`f₂, "?α → Nat"),
|
||
(`h, "?f₁ = ?f₂"),
|
||
(`a, "?α"),
|
||
(`conduit, "(?f₁ ?a = ?f₂ ?a) = (n + m + (n + m) = (n + m) * 2)"),
|
||
])
|
||
tests := tests ++ test
|
||
return tests
|
||
def test_congr (env: Environment): IO LSpec.TestSeq :=
|
||
let expr := "λ (a b: Nat) => a = b"
|
||
runMetaMSeq env do
|
||
let expr ← parseSentence expr
|
||
Meta.lambdaTelescope expr $ λ _ body => do
|
||
let mut tests := LSpec.TestSeq.done
|
||
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
||
let test ← runTermElabMInMeta do
|
||
let newGoals ← runTacticOnMVar Tactic.congruence target.mvarId!
|
||
pure $ LSpec.check "goals" ((← newGoals.mapM (λ x => mvarUserNameAndType x)) =
|
||
[
|
||
(`α, "Sort ?u.10"),
|
||
(`f₁, "?α → Nat"),
|
||
(`f₂, "?α → Nat"),
|
||
(`a₁, "?α"),
|
||
(`a₂, "?α"),
|
||
(`h₁, "?f₁ = ?f₂"),
|
||
(`h₂, "?a₁ = ?a₂"),
|
||
(`conduit, "(?f₁ ?a₁ = ?f₂ ?a₂) = (a = b)"),
|
||
])
|
||
tests := tests ++ test
|
||
return tests
|
||
|
||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||
[
|
||
("congrArg", test_congr_arg env),
|
||
("congrFun", test_congr_fun env),
|
||
("congr", test_congr env),
|
||
]
|
||
|
||
end Pantograph.Test.Tactic.Congruence
|