From fe80741c3f79866058abb1490b6c7ceda76e51e1 Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 17 Dec 2024 12:41:55 +0100 Subject: [PATCH 1/2] Factor out stuff from stlc case study --- examples/stlc.pol | 43 ++++++++++++++++++------------------------- std/data/nat.pol | 7 +++++++ std/data/ordering.pol | 9 +++++++++ std/data/void.pol | 2 ++ 4 files changed, 36 insertions(+), 25 deletions(-) create mode 100644 std/data/ordering.pol diff --git a/examples/stlc.pol b/examples/stlc.pol index 5003488727..c8c1b0c018 100644 --- a/examples/stlc.pol +++ b/examples/stlc.pol @@ -1,3 +1,7 @@ +use "../std/data/void.pol" +use "../std/data/nat.pol" +use "../std/data/ordering.pol" + -- | Expressions of the object language data Exp { -- | Variables using a deBruijn representation @@ -15,7 +19,7 @@ data Typ { VarT(x: Nat) } --- | Typing contexts. +-- | **Typing contexts**. -- | Because we use de Bruijn indices the typing context does not contain variable names. data Ctx { -- | The empty context @@ -43,7 +47,7 @@ def Exp.subst(v: Nat, by: Exp): Exp { App(e1, e2) => App(e1.subst(v, by), e2.subst(v, by)) } -def Cmp.subst_result(x: Nat, by: Exp): Exp { +def Ordering.subst_result(x: Nat, by: Exp): Exp { LT => Var(x), EQ => by, GT => Var(x.pred) @@ -91,7 +95,7 @@ data Progress(e: Exp) { def (e: Exp).progress(t: Typ): HasType(Nil, e, t) -> Progress(e) { Var(x) => \h_t. h_t.match { - TVar(_, _, _, elem) => elem.empty_absurd(x, t).elim_bot(Progress(Var(x))), + TVar(_, _, _, elem) => elem.empty_absurd(x, t).ex_falso(Progress(Var(x))), TLam(_, _, _, _, _) absurd, TApp(_, _, _, _, _, _, _) absurd }, @@ -185,7 +189,7 @@ def (e: Exp).subst_lemma(ctx1 ctx2: Ctx, t1 t2: Typ, by_e: Exp) TVar(_, _, _, h_elem) => x.cmp_reflect(ctx1.len).match { IsLT(_, _, h_eq_lt, h_lt) => - h_eq_lt.transport(Cmp, + h_eq_lt.transport(Ordering, LT, x.cmp(ctx1.len), comatch { @@ -215,7 +219,7 @@ def (e: Exp).subst_lemma(ctx1 ctx2: Ctx, t1 t2: Typ, by_e: Exp) Elem(x, t2, ctx1), h_elem)))), IsEQ(_, _, h_eq_eq, h_eq) => - h_eq_eq.transport(Cmp, + h_eq_eq.transport(Ordering, EQ, x.cmp(ctx1.len), comatch { @@ -253,7 +257,7 @@ def (e: Exp).subst_lemma(ctx1 ctx2: Ctx, t1 t2: Typ, by_e: Exp) }, h_by))), IsGT(_, _, h_eq_gt, h_gt) => - h_eq_gt.transport(Cmp, + h_eq_gt.transport(Ordering, GT, x.cmp(ctx1.len), comatch { @@ -419,7 +423,7 @@ def (ctx: Ctx).append_nil: Eq(Ctx, ctx, ctx.append(Nil)) { Cons(t, ts) => ts.append_nil.eq_cons(ts, ts.append(Nil), t) } -def Elem(x, t, Nil).empty_absurd(x: Nat, t: Typ): Bot { +def Elem(x, t, Nil).empty_absurd(x: Nat, t: Typ): Void { Here(_, _) absurd, There(_, _, _, _, _) absurd } @@ -507,9 +511,6 @@ def (ctx1: Ctx).elem_append_pred(ctx2: Ctx, t1 t2: Typ, x: Nat) } } -data Bot { } - -def Bot.elim_bot(a: Type): a { } codata Fun(a b: Type) { Fun(a, b).ap(a b: Type, x: a): b @@ -535,21 +536,13 @@ def Eq(Ctx, xs, ys).eq_cons(xs ys: Ctx, t: Typ): Eq(Ctx, Cons(t, xs), Cons(t, ys Refl(_, _) => Refl(Ctx, Cons(t, xs)) } -data Nat { Z, S(n: Nat) } - -def Nat.pred: Nat { - Z => Z, - S(x) => x -} - data LE(x y: Nat) { LERefl(x: Nat): LE(x, x), LESucc(x y: Nat, h: LE(x, y)): LE(x, S(y)) } -data Cmp { LT, EQ, GT } -def Nat.cmp(y: Nat): Cmp { +def Nat.cmp(y: Nat): Ordering { Z => y.match { Z => EQ, @@ -563,20 +556,20 @@ def Nat.cmp(y: Nat): Cmp { } data CmpReflect(x y: Nat) { - IsLT(x y: Nat, h1: Eq(Cmp, LT, x.cmp(y)), h2: LE(S(x), y)): CmpReflect(x, y), - IsEQ(x y: Nat, h1: Eq(Cmp, EQ, x.cmp(y)), h2: Eq(Nat, x, y)): CmpReflect(x, y), - IsGT(x y: Nat, h1: Eq(Cmp, GT, x.cmp(y)), h2: LE(S(y), x)): CmpReflect(x, y) + IsLT(x y: Nat, h1: Eq(Ordering, LT, x.cmp(y)), h2: LE(S(x), y)): CmpReflect(x, y), + IsEQ(x y: Nat, h1: Eq(Ordering, EQ, x.cmp(y)), h2: Eq(Nat, x, y)): CmpReflect(x, y), + IsGT(x y: Nat, h1: Eq(Ordering, GT, x.cmp(y)), h2: LE(S(y), x)): CmpReflect(x, y) } def (x: Nat).cmp_reflect(y: Nat): CmpReflect(x, y) { Z => y.match as y => CmpReflect(Z, y) { - Z => IsEQ(Z, Z, Refl(Cmp, EQ), Refl(Nat, Z)), - S(y) => IsLT(Z, S(y), Refl(Cmp, LT), y.z_le.le_succ(Z, y)) + Z => IsEQ(Z, Z, Refl(Ordering, EQ), Refl(Nat, Z)), + S(y) => IsLT(Z, S(y), Refl(Ordering, LT), y.z_le.le_succ(Z, y)) }, S(x) => y.match as y => CmpReflect(S(x), y) { - Z => IsGT(S(x), Z, Refl(Cmp, GT), x.z_le.le_succ(Z, x)), + Z => IsGT(S(x), Z, Refl(Ordering, GT), x.z_le.le_succ(Z, x)), S(y) => x.cmp_reflect(y).match { IsLT(_, _, h1, h2) => IsLT(S(x), S(y), h1, h2.le_succ(S(x), y)), diff --git a/std/data/nat.pol b/std/data/nat.pol index aa0bd80a56..f661b2220f 100644 --- a/std/data/nat.pol +++ b/std/data/nat.pol @@ -33,3 +33,10 @@ def Nat.fact: Nat { Z => 1, S(pred) => S(pred).mul(pred.fact) } + +-- | The predecessor of a natural number. +-- | The predecessor of `Z` is `Z`. +def Nat.pred: Nat { + Z => Z, + S(x) => x +} diff --git a/std/data/ordering.pol b/std/data/ordering.pol new file mode 100644 index 0000000000..3289d182e4 --- /dev/null +++ b/std/data/ordering.pol @@ -0,0 +1,9 @@ +-- | The result of comparing two totally-ordered values. +data Ordering { + -- | Lesser than + LT, + -- | Equal + EQ, + -- | Greater than + GT, +} diff --git a/std/data/void.pol b/std/data/void.pol index 03cb6f6a8f..1a3045ad73 100644 --- a/std/data/void.pol +++ b/std/data/void.pol @@ -1,2 +1,4 @@ -- | The trivially uninhabitated data type. data Void { } + +def Void.ex_falso(a: Type): a { } From 300c1786a45562fa52d5f467890802dc81dba626 Mon Sep 17 00:00:00 2001 From: David Binder Date: Mon, 30 Dec 2024 15:50:43 +0100 Subject: [PATCH 2/2] Factor out more properties of natural numbers --- examples/stlc.pol | 26 -------------------------- std/data/nat.pol | 30 ++++++++++++++++++++++++++++++ 2 files changed, 30 insertions(+), 26 deletions(-) diff --git a/examples/stlc.pol b/examples/stlc.pol index c8c1b0c018..9acfe1515b 100644 --- a/examples/stlc.pol +++ b/examples/stlc.pol @@ -536,12 +536,6 @@ def Eq(Ctx, xs, ys).eq_cons(xs ys: Ctx, t: Typ): Eq(Ctx, Cons(t, xs), Cons(t, ys Refl(_, _) => Refl(Ctx, Cons(t, xs)) } -data LE(x y: Nat) { - LERefl(x: Nat): LE(x, x), - LESucc(x y: Nat, h: LE(x, y)): LE(x, S(y)) -} - - def Nat.cmp(y: Nat): Ordering { Z => y.match { @@ -579,26 +573,6 @@ def (x: Nat).cmp_reflect(y: Nat): CmpReflect(x, y) { } } -def (x: Nat).z_le: LE(Z, x) { - Z => LERefl(Z), - S(x) => LESucc(Z, x, x.z_le) -} - -def LE(x, y).le_succ(x y: Nat): LE(S(x), S(y)) { - LERefl(_) => LERefl(S(x)), - LESucc(x, y, h) => LESucc(S(x), S(y), h.le_succ(x, y)) -} - -def LE(S(x), S(y)).le_unsucc(x y: Nat): LE(x, y) { - LERefl(_) => LERefl(x), - LESucc(_, _, h) => h.s_le(x, y) -} - -def LE(S(x), y).s_le(x y: Nat): LE(x, y) { - LERefl(_) => LESucc(x, x, LERefl(x)), - LESucc(_, y', h) => LESucc(x, y', h.s_le(x, y')) -} - def LE(S(x), y).s_pred(x y: Nat): Eq(Nat, S(y.pred), y) { LERefl(_) => Refl(Nat, y), LESucc(_, y', _) => Refl(Nat, y) diff --git a/std/data/nat.pol b/std/data/nat.pol index f661b2220f..24c4c92a87 100644 --- a/std/data/nat.pol +++ b/std/data/nat.pol @@ -40,3 +40,33 @@ def Nat.pred: Nat { Z => Z, S(x) => x } + +-- | The lesser-or-equal relation on natural numbers. +data LE(x y: Nat) { + LERefl(x: Nat): LE(x, x), + LESucc(x y: Nat, h: LE(x, y)): LE(x, S(y)) +} + +-- | Z is smaller than any natural number. +def (x: Nat).z_le: LE(Z, x) { + Z => LERefl(Z), + S(x) => LESucc(Z, x, x.z_le) +} + +-- | If x <= y, then S(x) <= S(y) +def LE(x, y).le_succ(x y: Nat): LE(S(x), S(y)) { + LERefl(_) => LERefl(S(x)), + LESucc(x, y, h) => LESucc(S(x), S(y), h.le_succ(x, y)) +} + +-- | If S(x) <= S(y), then x <= y. +def LE(S(x), S(y)).le_unsucc(x y: Nat): LE(x, y) { + LERefl(_) => LERefl(x), + LESucc(_, _, h) => h.s_le(x, y) +} + +-- | If S(x) <= y, then x <= y +def LE(S(x), y).s_le(x y: Nat): LE(x, y) { + LERefl(_) => LESucc(x, x, LERefl(x)), + LESucc(_, y', h) => LESucc(x, y', h.s_le(x, y')) +}