quox/tests/Tests/Equal.idr

441 lines
17 KiB
Idris
Raw Normal View History

2022-04-27 14:06:39 -04:00
module Tests.Equal
2023-02-11 12:15:50 -05:00
import Quox.Equal
2023-01-08 14:44:25 -05:00
import Quox.Syntax.Qty.Three
2023-02-11 12:15:50 -05:00
import public TypingImpls
2022-04-27 14:06:39 -04:00
import TAP
2023-01-08 14:44:25 -05:00
0 M : Type -> Type
M = ReaderT (Definitions Three) (Either (Error Three))
2022-04-27 14:06:39 -04:00
2023-02-10 15:40:44 -05:00
defGlobals : Definitions Three
defGlobals = fromList
[("A", mkPostulate Zero $ TYPE 0),
("B", mkPostulate Zero $ TYPE 0),
("a", mkPostulate Any $ FT "A"),
("a'", mkPostulate Any $ FT "A"),
("b", mkPostulate Any $ FT "B"),
("f", mkPostulate Any $ Arr One (FT "A") (FT "A")),
2023-02-12 15:30:08 -05:00
("id", mkDef Any (Arr One (FT "A") (FT "A")) (["x"] :\\ BVT 0)),
("eq-AB", mkPostulate Zero $ Eq0 (TYPE 0) (FT "A") (FT "B"))]
2023-02-10 15:40:44 -05:00
parameters (label : String) (act : Lazy (M ()))
2023-02-10 15:40:44 -05:00
{default defGlobals globals : Definitions Three}
testEq : Test
testEq = test label $ runReaderT globals act
2022-04-27 14:06:39 -04:00
testNeq : Test
testNeq = testThrows label (const True) $ runReaderT globals act
2022-04-27 14:06:39 -04:00
parameters (0 d : Nat) (ctx : TyContext Three d n)
subTD, equalTD : Term Three d n -> Term Three d n -> Term Three d n -> M ()
subTD ty s t = Term.sub ctx ty s t
equalTD ty s t = Term.equal ctx ty s t
2022-04-27 14:06:39 -04:00
subED, equalED : Elim Three d n -> Elim Three d n -> M ()
subED e f = Elim.sub ctx e f
equalED e f = Elim.equal ctx e f
2022-04-27 14:06:39 -04:00
parameters (ctx : TyContext Three 0 n)
subT, equalT : Term Three 0 n -> Term Three 0 n -> Term Three 0 n -> M ()
subT = subTD 0 ctx
equalT = equalTD 0 ctx
subE, equalE : Elim Three 0 n -> Elim Three 0 n -> M ()
subE = subED 0 ctx
equalE = equalED 0 ctx
2022-04-27 14:06:39 -04:00
export
tests : Test
tests = "equality & subtyping" :- [
2023-02-12 15:30:08 -05:00
note #""s{t,…}" for term substs; "sp,…›" for dim substs"#,
note #""0=1𝒥" means that 𝒥 holds in an inconsistent dim context"#,
"universes" :- [
2023-02-12 15:30:08 -05:00
testEq "★₀ = ★₀" $
equalT empty (TYPE 1) (TYPE 0) (TYPE 0),
2023-02-12 15:30:08 -05:00
testNeq "★₀ ≠ ★₁" $
equalT empty (TYPE 2) (TYPE 0) (TYPE 1),
2023-02-12 15:30:08 -05:00
testNeq "★₁ ≠ ★₀" $
equalT empty (TYPE 2) (TYPE 1) (TYPE 0),
testEq "★₀ <: ★₀" $
subT empty (TYPE 1) (TYPE 0) (TYPE 0),
testEq "★₀ <: ★₁" $
subT empty (TYPE 2) (TYPE 0) (TYPE 1),
testNeq "★₁ ≮: ★₀" $
subT empty (TYPE 2) (TYPE 1) (TYPE 0)
],
"pi" :- [
2023-02-12 15:30:08 -05:00
note #""𝐴𝐵" for (1·𝐴)𝐵"#,
note #""𝐴𝐵" for (0·𝐴)𝐵"#,
testEq "★₀ ⇾ ★₀ = ★₀ ⇾ ★₀" $
let tm = Arr Zero (TYPE 0) (TYPE 0) in
equalT empty (TYPE 1) tm tm,
testEq "★₀ ⇾ ★₀ <: ★₀ ⇾ ★₀" $
let tm = Arr Zero (TYPE 0) (TYPE 0) in
subT empty (TYPE 1) tm tm,
2023-02-12 15:30:08 -05:00
testNeq "★₁ ⊸ ★₀ ≠ ★₀ ⇾ ★₀" $
let tm1 = Arr Zero (TYPE 1) (TYPE 0)
tm2 = Arr Zero (TYPE 0) (TYPE 0) in
equalT empty (TYPE 2) tm1 tm2,
testEq "★₁ ⊸ ★₀ <: ★₀ ⊸ ★₀" $
let tm1 = Arr One (TYPE 1) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 0) in
subT empty (TYPE 2) tm1 tm2,
testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
let tm1 = Arr One (TYPE 0) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 1) in
subT empty (TYPE 2) tm1 tm2,
testEq "★₀ ⊸ ★₀ <: ★₀ ⊸ ★₁" $
let tm1 = Arr One (TYPE 0) (TYPE 0)
tm2 = Arr One (TYPE 0) (TYPE 1) in
subT empty (TYPE 2) tm1 tm2,
2023-02-12 15:30:08 -05:00
testEq "A ⊸ B = A ⊸ B" $
let tm = Arr One (FT "A") (FT "B") in
equalT empty (TYPE 0) tm tm,
2023-02-12 15:30:08 -05:00
testEq "A ⊸ B <: A ⊸ B" $
let tm = Arr One (FT "A") (FT "B") in
subT empty (TYPE 0) tm tm,
2023-02-12 15:30:08 -05:00
note "incompatible quantities",
testNeq "★₀ ⊸ ★₀ ≠ ★₀ ⇾ ★₁" $
let tm1 = Arr Zero (TYPE 0) (TYPE 0)
tm2 = Arr Zero (TYPE 0) (TYPE 1) in
equalT empty (TYPE 2) tm1 tm2,
2023-02-12 15:30:08 -05:00
testNeq "A ⇾ B ≠ A ⊸ B" $
let tm1 = Arr Zero (FT "A") (FT "B")
tm2 = Arr One (FT "A") (FT "B") in
equalT empty (TYPE 0) tm1 tm2,
2023-02-12 15:30:08 -05:00
testNeq "A ⇾ B ≮: A ⊸ B" $
let tm1 = Arr Zero (FT "A") (FT "B")
tm2 = Arr One (FT "A") (FT "B") in
subT empty (TYPE 0) tm1 tm2,
2023-02-12 15:30:08 -05:00
testEq "0=1 ⊢ A ⇾ B = A ⊸ B" $
let tm1 = Arr Zero (FT "A") (FT "B")
tm2 = Arr One (FT "A") (FT "B") in
equalT (MkTyContext ZeroIsOne [<]) (TYPE 0) tm1 tm2,
2023-02-25 09:24:45 -05:00
todo "dependent function types",
2023-02-12 15:30:08 -05:00
note "[todo] should π ≤ ρ ⊢ (ρ·A) → B <: (π·A) → B?"
],
"lambda" :- [
2023-03-04 15:02:51 -05:00
testEq "λ x ⇒ [x] = λ x ⇒ [x]" $
equalT empty (Arr One (FT "A") (FT "A"))
2023-02-11 12:15:50 -05:00
(["x"] :\\ BVT 0)
(["x"] :\\ BVT 0),
2023-03-04 15:02:51 -05:00
testEq "λ x ⇒ [x] <: λ x ⇒ [x]" $
subT empty (Arr One (FT "A") (FT "A"))
2023-02-11 12:15:50 -05:00
(["x"] :\\ BVT 0)
(["x"] :\\ BVT 0),
2023-03-04 15:02:51 -05:00
testEq "λ x ⇒ [x] = λ y ⇒ [y]" $
equalT empty (Arr One (FT "A") (FT "A"))
2023-02-11 12:15:50 -05:00
(["x"] :\\ BVT 0)
(["y"] :\\ BVT 0),
2023-03-04 15:02:51 -05:00
testEq "λ x ⇒ [x] <: λ y ⇒ [y]" $
equalT empty (Arr One (FT "A") (FT "A"))
2023-02-11 12:15:50 -05:00
(["x"] :\\ BVT 0)
(["y"] :\\ BVT 0),
2023-03-04 15:02:51 -05:00
testNeq "λ x y ⇒ [x] ≠ λ x y ⇒ [y]" $
equalT empty (Arr One (FT "A") $ Arr One (FT "A") (FT "A"))
2023-02-11 12:15:50 -05:00
(["x", "y"] :\\ BVT 1)
(["x", "y"] :\\ BVT 0),
2023-03-04 15:02:51 -05:00
testEq "λ x ⇒ [a] = λ x ⇒ [a] (Y vs N)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
2023-02-25 09:24:45 -05:00
(Lam $ SY ["x"] $ FT "a")
(Lam $ SN $ FT "a"),
2023-03-04 15:02:51 -05:00
testEq "λ x ⇒ [f [x]] = [f] (η)" $
equalT empty (Arr One (FT "A") (FT "A"))
2023-02-11 12:15:50 -05:00
(["x"] :\\ E (F "f" :@ BVT 0))
2023-02-10 15:40:44 -05:00
(FT "f")
],
2023-01-26 13:54:46 -05:00
"eq type" :- [
2023-02-12 15:30:08 -05:00
testEq "(★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : ★₁)" $
2023-01-26 13:54:46 -05:00
let tm = Eq0 (TYPE 1) (TYPE 0) (TYPE 0) in
equalT empty (TYPE 2) tm tm,
2023-02-12 15:30:08 -05:00
testEq "A ≔ ★₁ ⊢ (★₀ ≡ ★₀ : ★₁) = (★₀ ≡ ★₀ : A)"
2023-01-26 13:54:46 -05:00
{globals = fromList [("A", mkDef zero (TYPE 2) (TYPE 1))]} $
equalT empty (TYPE 2)
2023-02-10 15:40:44 -05:00
(Eq0 (TYPE 1) (TYPE 0) (TYPE 0))
2023-02-25 09:24:45 -05:00
(Eq0 (FT "A") (TYPE 0) (TYPE 0)),
todo "dependent equality types"
2023-01-26 13:54:46 -05:00
],
2023-02-12 15:30:08 -05:00
"equalities and uip" :-
2023-02-11 12:15:50 -05:00
let refl : Term q d n -> Term q d n -> Elim q d n
2023-02-22 01:40:19 -05:00
refl a x = (DLam $ S ["_"] $ N x) :# (Eq0 a x x)
2023-02-11 12:15:50 -05:00
in
[
2023-03-04 15:02:51 -05:00
note #""refl [A] x" is an abbreviation for "(δ i ⇒ x)(x ≡ x : A)""#,
2023-02-12 15:30:08 -05:00
note "binds before ∥ are globals, after it are BVs",
testEq "refl [A] a = refl [A] a" $
equalE empty (refl (FT "A") (FT "a")) (refl (FT "A") (FT "a")),
2023-02-12 15:30:08 -05:00
testEq "p : (a ≡ a' : A), q : (a ≡ a' : A) ∥ ⊢ p = q (free)"
2023-02-11 12:15:50 -05:00
{globals =
let def = mkPostulate Zero $ Eq0 (FT "A") (FT "a") (FT "a'") in
2023-02-11 12:15:50 -05:00
defGlobals `mergeLeft` fromList [("p", def), ("q", def)]} $
equalE empty (F "p") (F "q"),
2023-02-12 15:30:08 -05:00
testEq "∥ x : (a ≡ a' : A), y : (a ≡ a' : A) ⊢ x = y (bound)" $
2023-02-11 12:15:50 -05:00
let ty : forall n. Term Three 0 n := Eq0 (FT "A") (FT "a") (FT "a'") in
equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1),
2023-02-12 15:30:08 -05:00
testEq "∥ x : [(a ≡ a' : A) ∷ Type 0], y : [ditto] ⊢ x = y" $
2023-03-05 06:18:15 -05:00
let ty : forall n. Term Three 0 n :=
E (Eq0 (FT "A") (FT "a") (FT "a'") :# TYPE 0) in
equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1),
2023-02-12 15:30:08 -05:00
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : EE ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("EE", mkDef zero (TYPE 0) (FT "E"))]} $
equalE (MkTyContext new [< FT "EE", FT "EE"]) (BV 0) (BV 1),
2023-02-12 15:30:08 -05:00
testEq "E ≔ a ≡ a' : A, EE ≔ E ∥ x : EE, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("EE", mkDef zero (TYPE 0) (FT "E"))]} $
equalE (MkTyContext new [< FT "EE", FT "E"]) (BV 0) (BV 1),
2023-02-12 15:30:08 -05:00
testEq "E ≔ a ≡ a' : A ∥ x : E, y : E ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
equalE (MkTyContext new [< FT "E", FT "E"]) (BV 0) (BV 1),
2023-02-12 15:30:08 -05:00
testEq "E ≔ a ≡ a' : A ∥ x : (E×E), y : (E×E) ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'")))]} $
2023-03-05 06:18:15 -05:00
let ty : forall n. Term Three 0 n :=
Sig (FT "E") $ S ["_"] $ N $ FT "E" in
equalE (MkTyContext new [< ty, ty]) (BV 0) (BV 1),
2023-02-12 15:30:08 -05:00
testEq "E ≔ a ≡ a' : A, F ≔ E × E ∥ x : F, y : F ⊢ x = y"
{globals = defGlobals `mergeLeft` fromList
[("E", mkDef zero (TYPE 0) (Eq0 (FT "A") (FT "a") (FT "a'"))),
("W", mkDef zero (TYPE 0) (FT "E" `And` FT "E"))]} $
equalE (MkTyContext new [< FT "W", FT "W"]) (BV 0) (BV 1)
2023-02-11 12:15:50 -05:00
],
2023-01-26 13:54:46 -05:00
"term closure" :- [
2023-02-12 15:30:08 -05:00
testEq "[#0]{} = [#0] : A" $
equalT (MkTyContext new [< FT "A"]) (FT "A")
2023-02-10 15:40:44 -05:00
(CloT (BVT 0) id)
(BVT 0),
2023-02-12 15:30:08 -05:00
testEq "[#0]{a} = [a] : A" $
equalT empty (FT "A")
2023-02-10 15:40:44 -05:00
(CloT (BVT 0) (F "a" ::: id))
(FT "a"),
2023-02-12 15:30:08 -05:00
testEq "[#0]{a,b} = [a] : A" $
equalT empty (FT "A")
2023-02-10 15:40:44 -05:00
(CloT (BVT 0) (F "a" ::: F "b" ::: id))
(FT "a"),
2023-02-12 15:30:08 -05:00
testEq "[#1]{a,b} = [b] : A" $
equalT empty (FT "A")
2023-02-12 15:30:08 -05:00
(CloT (BVT 1) (F "a" ::: F "b" ::: id))
(FT "b"),
2023-03-04 15:02:51 -05:00
testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (N)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
2023-02-22 01:40:19 -05:00
(CloT (Lam $ S ["y"] $ N $ BVT 0) (F "a" ::: id))
(Lam $ S ["y"] $ N $ FT "a"),
2023-03-04 15:02:51 -05:00
testEq "(λy ⇒ [#1]){a} = λy ⇒ [a] : B ⇾ A (Y)" $
equalT empty (Arr Zero (FT "B") (FT "A"))
2023-02-11 12:15:50 -05:00
(CloT (["y"] :\\ BVT 1) (F "a" ::: id))
(["y"] :\\ FT "a")
],
2023-02-12 15:30:08 -05:00
"term d-closure" :- [
testEq "★₀‹𝟎› = ★₀ : ★₁" $
equalTD 1 empty (TYPE 1) (DCloT (TYPE 0) (K Zero ::: id)) (TYPE 0),
2023-03-04 15:02:51 -05:00
testEq "(δ i ⇒ a)𝟎 = (δ i ⇒ a) : (a ≡ a : A)" $
equalTD 1 empty
2023-02-12 15:30:08 -05:00
(Eq0 (FT "A") (FT "a") (FT "a"))
(DCloT (["i"] :\\% FT "a") (K Zero ::: id))
(["i"] :\\% FT "a"),
note "it is hard to think of well-typed terms with big dctxs"
],
"free var" :-
let au_bu = fromList
2023-03-05 10:48:29 -05:00
[("A", mkDef Any (TYPE 1) (TYPE 0)),
("B", mkDef Any (TYPE 1) (TYPE 0))]
au_ba = fromList
2023-03-05 10:48:29 -05:00
[("A", mkDef Any (TYPE 1) (TYPE 0)),
("B", mkDef Any (TYPE 1) (FT "A"))]
in [
2023-02-12 15:30:08 -05:00
testEq "A = A" $
equalE empty (F "A") (F "A"),
2023-02-12 15:30:08 -05:00
testNeq "A ≠ B" $
equalE empty (F "A") (F "B"),
2023-02-12 15:30:08 -05:00
testEq "0=1 ⊢ A = B" $
equalE (MkTyContext ZeroIsOne [<]) (F "A") (F "B"),
2023-02-12 15:30:08 -05:00
testEq "A : ★₁ ≔ ★₀ ⊢ A = (★₀ ∷ ★₁)" {globals = au_bu} $
equalE empty (F "A") (TYPE 0 :# TYPE 1),
2023-02-12 15:30:08 -05:00
testEq "A : ★₁ ≔ ★₀ ⊢ [A] = ★₀" {globals = au_bu} $
equalT empty (TYPE 1) (FT "A") (TYPE 0),
2023-02-12 15:30:08 -05:00
testEq "A ≔ ★₀, B ≔ ★₀ ⊢ A = B" {globals = au_bu} $
equalE empty (F "A") (F "B"),
2023-02-12 15:30:08 -05:00
testEq "A ≔ ★₀, B ≔ A ⊢ A = B" {globals = au_ba} $
equalE empty (F "A") (F "B"),
testEq "A <: A" $
subE empty (F "A") (F "A"),
testNeq "A ≮: B" $
subE empty (F "A") (F "B"),
testEq "A : ★₃ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", mkDef Any (TYPE 3) (TYPE 0)),
("B", mkDef Any (TYPE 3) (TYPE 2))]} $
subE empty (F "A") (F "B"),
2023-02-12 15:30:08 -05:00
note "(A and B in different universes)",
testEq "A : ★₁ ≔ ★₀, B : ★₃ ≔ ★₂ ⊢ A <: B"
{globals = fromList [("A", mkDef Any (TYPE 1) (TYPE 0)),
("B", mkDef Any (TYPE 3) (TYPE 2))]} $
subE empty (F "A") (F "B"),
testEq "0=1 ⊢ A <: B" $
subE (MkTyContext ZeroIsOne [<]) (F "A") (F "B")
],
"bound var" :- [
2023-02-12 15:30:08 -05:00
testEq "#0 = #0" $
equalE (MkTyContext new [< TYPE 0]) (BV 0) (BV 0),
2023-02-12 15:30:08 -05:00
testEq "#0 <: #0" $
subE (MkTyContext new [< TYPE 0]) (BV 0) (BV 0),
2023-02-12 15:30:08 -05:00
testNeq "#0 ≠ #1" $
equalE (MkTyContext new [< TYPE 0, TYPE 0]) (BV 0) (BV 1),
2023-02-12 15:30:08 -05:00
testNeq "#0 ≮: #1" $
subE (MkTyContext new [< TYPE 0, TYPE 0]) (BV 0) (BV 1),
2023-02-12 15:30:08 -05:00
testEq "0=1 ⊢ #0 = #1" $
equalE (MkTyContext ZeroIsOne [< TYPE 0, TYPE 0]) (BV 0) (BV 1)
],
"application" :- [
2023-02-12 15:30:08 -05:00
testEq "f [a] = f [a]" $
equalE empty (F "f" :@ FT "a") (F "f" :@ FT "a"),
testEq "f [a] <: f [a]" $
subE empty (F "f" :@ FT "a") (F "f" :@ FT "a"),
2023-03-04 15:02:51 -05:00
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = ([a ∷ A] ∷ A) (β)" $
equalE empty
2023-02-11 12:15:50 -05:00
(((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(E (FT "a" :# FT "A") :# FT "A"),
2023-03-04 15:02:51 -05:00
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a = a (βυ)" $
equalE empty
2023-02-11 12:15:50 -05:00
(((["x"] :\\ BVT 0) :# Arr One (FT "A") (FT "A")) :@ FT "a")
(F "a"),
2023-03-04 15:02:51 -05:00
testEq "(λ g ⇒ [g [a]] ∷ ⋯)) [f] = (λ y ⇒ [f [y]] ∷ ⋯) [a] (β↘↙)" $
let a = FT "A"; a2a = (Arr One a a) in
equalE empty
2023-02-11 12:15:50 -05:00
(((["g"] :\\ E (BV 0 :@ FT "a")) :# Arr One a2a a) :@ FT "f")
(((["y"] :\\ E (F "f" :@ BVT 0)) :# a2a) :@ FT "a"),
2023-03-04 15:02:51 -05:00
testEq "(λ x ⇒ [x] ∷ A ⊸ A) a <: a" $
subE empty
2023-02-11 12:15:50 -05:00
(((["x"] :\\ BVT 0) :# (Arr One (FT "A") (FT "A"))) :@ FT "a")
(F "a"),
2023-03-04 15:02:51 -05:00
note "id : A ⊸ A ≔ λ x ⇒ [x]",
testEq "id [a] = a" $ equalE empty (F "id" :@ FT "a") (F "a"),
testEq "id [a] <: a" $ subE empty (F "id" :@ FT "a") (F "a")
],
2023-03-05 06:18:15 -05:00
"dim application" :- [
testEq "eq-AB @0 = eq-AB @0" $
equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K Zero),
testNeq "eq-AB @0 ≠ eq-AB @1" $
equalE empty (F "eq-AB" :% K Zero) (F "eq-AB" :% K One),
testEq "𝑖 | ⊢ eq-AB @𝑖 = eq-AB @𝑖" $
equalED 1 empty (F "eq-AB" :% BV 0) (F "eq-AB" :% BV 0),
testNeq "𝑖 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
equalED 1 empty (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
testEq "𝑖, 𝑖=0 | ⊢ eq-AB @𝑖 = eq-AB @0" $
let ctx = MkTyContext (set (BV 0) (K Zero) new) [<] in
equalED 1 ctx (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
testNeq "𝑖, 𝑖=1 | ⊢ eq-AB @𝑖 ≠ eq-AB @0" $
let ctx = MkTyContext (set (BV 0) (K One) new) [<] in
equalED 1 ctx (F "eq-AB" :% BV 0) (F "eq-AB" :% K Zero),
testNeq "𝑖, 𝑗 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $
equalED 2 empty (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
testEq "𝑖, 𝑗, 𝑖=𝑗 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
let ctx = MkTyContext (set (BV 0) (BV 1) new) [<] in
equalED 2 ctx (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
testNeq "𝑖, 𝑗, 𝑖=0, 𝑗=0 | ⊢ eq-AB @𝑖 ≠ eq-AB @𝑗" $
let ctx : TyContext Three 2 0 :=
MkTyContext (C [< Just $ K Zero, Just $ K Zero]) [<] in
equalED 2 empty (F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
testEq "0=1 | ⊢ eq-AB @𝑖 = eq-AB @𝑗" $
equalED 2 (MkTyContext ZeroIsOne [<])
(F "eq-AB" :% BV 1) (F "eq-AB" :% BV 0),
testEq "eq-AB @0 = A" $ equalE empty (F "eq-AB" :% K Zero) (F "A"),
testEq "eq-AB @1 = B" $ equalE empty (F "eq-AB" :% K One) (F "B"),
testEq "((δ i ⇒ a) ∷ a ≡ a) @0 = a" $
equalE empty
(((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K Zero)
(F "a"),
testEq "((δ i ⇒ a) ∷ a ≡ a) @0 = ((δ i ⇒ a) ∷ a ≡ a) @1" $
equalE empty
(((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K Zero)
(((DLam $ SN $ FT "a") :# Eq0 (FT "A") (FT "a") (FT "a")) :% K One)
],
2023-01-26 13:54:46 -05:00
2023-02-12 15:30:08 -05:00
"annotation" :- [
2023-03-04 15:02:51 -05:00
testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = [f] ∷ A ⊸ A" $
equalE empty
2023-02-12 15:30:08 -05:00
((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
(FT "f" :# Arr One (FT "A") (FT "A")),
testEq "[f] ∷ A ⊸ A = f" $
equalE empty (FT "f" :# Arr One (FT "A") (FT "A")) (F "f"),
2023-03-04 15:02:51 -05:00
testEq "(λ x ⇒ f [x]) ∷ A ⊸ A = f" $
equalE empty
2023-02-12 15:30:08 -05:00
((["x"] :\\ E (F "f" :@ BVT 0)) :# Arr One (FT "A") (FT "A"))
(F "f")
],
2023-02-12 15:30:08 -05:00
"elim closure" :- [
testEq "#0{a} = a" $
equalE empty (CloE (BV 0) (F "a" ::: id)) (F "a"),
2023-02-12 15:30:08 -05:00
testEq "#1{a} = #0" $
equalE (MkTyContext new [< FT "A"])
(CloE (BV 1) (F "a" ::: id)) (BV 0)
2023-02-12 15:30:08 -05:00
],
2023-02-12 15:30:08 -05:00
"elim d-closure" :- [
2023-03-05 06:18:15 -05:00
note "0·eq-AB : (A ≡ B : ★₀)",
testEq "(eq-AB #0)𝟎 = eq-AB 𝟎" $
equalED 1 empty
2023-03-05 06:18:15 -05:00
(DCloE (F "eq-AB" :% BV 0) (K Zero ::: id))
(F "eq-AB" :% K Zero),
testEq "(eq-AB #0)𝟎 = A" $
equalED 1 empty (DCloE (F "eq-AB" :% BV 0) (K Zero ::: id)) (F "A"),
testEq "(eq-AB #0)𝟏 = B" $
equalED 1 empty (DCloE (F "eq-AB" :% BV 0) (K One ::: id)) (F "B"),
testNeq "(eq-AB #0)𝟏 ≠ A" $
equalED 1 empty (DCloE (F "eq-AB" :% BV 0) (K One ::: id)) (F "A"),
testEq "(eq-AB #0)#0,𝟎 = (eq-AB #0)" $
equalED 2 empty
2023-03-05 06:18:15 -05:00
(DCloE (F "eq-AB" :% BV 0) (BV 0 ::: K Zero ::: id))
(F "eq-AB" :% BV 0),
testNeq "(eq-AB #0)𝟎 ≠ (eq-AB 𝟎)" $
equalED 2 empty
2023-03-05 06:18:15 -05:00
(DCloE (F "eq-AB" :% BV 0) (BV 0 ::: K Zero ::: id))
(F "eq-AB" :% K Zero),
2023-02-12 15:30:08 -05:00
testEq "#0𝟎 = #0 # term and dim vars distinct" $
equalED 1 (MkTyContext new [< FT "A"])
(DCloE (BV 0) (K Zero ::: id)) (BV 0),
2023-02-12 15:30:08 -05:00
testEq "a𝟎 = a" $
equalED 1 empty (DCloE (F "a") (K Zero ::: id)) (F "a"),
2023-02-12 15:30:08 -05:00
testEq "(f [a])𝟎 = f𝟎 [a]𝟎" $
2023-02-19 11:51:44 -05:00
let th = K Zero ::: id in
equalED 1 empty
2023-02-12 15:30:08 -05:00
(DCloE (F "f" :@ FT "a") th)
(DCloE (F "f") th :@ DCloT (FT "a") th)
],
"clashes" :- [
2023-02-12 15:30:08 -05:00
testNeq "★₀ ≠ ★₀ ⇾ ★₀" $
equalT empty (TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
2023-02-12 15:30:08 -05:00
testEq "0=1 ⊢ ★₀ = ★₀ ⇾ ★₀" $
equalT (MkTyContext ZeroIsOne [<])
(TYPE 1) (TYPE 0) (Arr Zero (TYPE 0) (TYPE 0)),
todo "others"
2022-04-27 14:06:39 -04:00
]
]