mirror of
https://github.com/polarity-lang/polarity.git
synced 2025-08-04 18:48:13 +00:00
c786a6704f
* Add CST and parsing for infix declarations * Add infix declarations to symbol table * Add Infix decls to ast * Make testsuite run through again * Implement infix declarations * Validate binding structure of infix decls * Generate docs * Add testcases * Make tests run through again * Add checking of infix declarations * Add testcases * Check that RHS is defined * Fix clippy hints * Add hover information * Add infix to syntax of web editor --------- Co-authored-by: Tim Süberkrüb <dev@timsueberkrueb.io>
581 lines
25 KiB
Text
581 lines
25 KiB
Text
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
|
|
Var(x: Nat),
|
|
/// Lambda abstractions
|
|
Lam(body: Exp),
|
|
/// Function applications
|
|
App(lhs rhs: Exp),
|
|
}
|
|
|
|
/// Types of the object language
|
|
data Typ {
|
|
/// Function type
|
|
FunT(t1 t2: Typ),
|
|
VarT(x: Nat),
|
|
}
|
|
|
|
/// **Typing contexts**.
|
|
/// Because we use de Bruijn indices the typing context does not contain variable names.
|
|
data Ctx {
|
|
/// The empty context
|
|
Nil,
|
|
/// Adding a typed binding to the context
|
|
Cons(t: Typ, ts: Ctx),
|
|
}
|
|
|
|
/// Appending two contexts
|
|
def Ctx.append(other: Ctx): Ctx {
|
|
Nil => other,
|
|
Cons(t, ts) => Cons(t, ts.append(other)),
|
|
}
|
|
|
|
/// Computing the length of a context
|
|
def Ctx.len: Nat {
|
|
Nil => Z,
|
|
Cons(_, ts) => S(ts.len),
|
|
}
|
|
|
|
/// Substituting an expression for a variable in an expression.
|
|
def Exp.subst(v: Nat, by: Exp): Exp {
|
|
Var(x) => x.cmp(v).subst_result(x, by),
|
|
Lam(e) => Lam(e.subst(S(v), by)),
|
|
App(e1, e2) => App(e1.subst(v, by), e2.subst(v, by)),
|
|
}
|
|
|
|
def Ordering.subst_result(x: Nat, by: Exp): Exp {
|
|
LT => Var(x),
|
|
EQ => by,
|
|
GT => Var(x.pred),
|
|
}
|
|
|
|
data Elem(x: Nat, t: Typ, ctx: Ctx) {
|
|
Here(t: Typ, ts: Ctx): Elem(Z, t, Cons(t, ts)),
|
|
There(x: Nat, t t2: Typ, ts: Ctx, prf: Elem(x, t, ts)): Elem(S(x), t, Cons(t2, ts)),
|
|
}
|
|
|
|
/// The typing judgement.
|
|
/// HasType(ctx, e, t) means `ctx |- e : t`
|
|
data HasType(ctx: Ctx, e: Exp, t: Typ) {
|
|
TVar(ctx: Ctx, x: Nat, t: Typ, elem: Elem(x, t, ctx)): HasType(ctx, Var(x), t),
|
|
TLam(ctx: Ctx, t1 t2: Typ, e: Exp, body: HasType(Cons(t1, ctx), e, t2))
|
|
: HasType(ctx, Lam(e), FunT(t1, t2)),
|
|
TApp(ctx: Ctx,
|
|
t1 t2: Typ,
|
|
e1 e2: Exp,
|
|
e1_t: HasType(ctx, e1, FunT(t1, t2)),
|
|
e2_t: HasType(ctx, e2, t1),
|
|
)
|
|
: HasType(ctx, App(e1, e2), t2),
|
|
}
|
|
|
|
/// The evaluation relation
|
|
/// Eval(e1,e2) means that e1 evaluates to e2
|
|
data Eval(e1 e2: Exp) {
|
|
EBeta(e1 e2: Exp): Eval(App(Lam(e1), e2), e1.subst(Z, e2)),
|
|
ECongApp1(e1 e1': Exp, h: Eval(e1, e1'), e2: Exp): Eval(App(e1, e2), App(e1', e2)),
|
|
ECongApp2(e1 e2 e2': Exp, h: Eval(e2, e2')): Eval(App(e1, e2), App(e1, e2')),
|
|
}
|
|
|
|
/// Characterizes the subset of Values.
|
|
data IsValue(e: Exp) {
|
|
/// Every lambda abstraction is a value
|
|
VLam(e: Exp): IsValue(Lam(e)),
|
|
}
|
|
|
|
data Progress(e: Exp) {
|
|
PVal(e: Exp, h: IsValue(e)): Progress(e),
|
|
PStep(e1 e2: Exp, h: Eval(e1, e2)): Progress(e1),
|
|
}
|
|
|
|
def (e: Exp).progress(t: Typ): HasType(Nil, e, t) -> Progress(e) {
|
|
Var(x) =>
|
|
\ap(_,_,h_t) => h_t.match {
|
|
TVar(_, _, _, elem) => elem.empty_absurd(x, t).ex_falso(Progress(Var(x))),
|
|
TLam(_, _, _, _, _) absurd,
|
|
TApp(_, _, _, _, _, _, _) absurd,
|
|
},
|
|
Lam(e) => \ap(_,_,_) => PVal(Lam(e), VLam(e)),
|
|
App(e1, e2) =>
|
|
\ap(_,_,h_t) => h_t.match {
|
|
TVar(_, _, _, _) absurd,
|
|
TLam(_, _, _, _, _) absurd,
|
|
TApp(_, t1, t2, _, _, e1_t, e2_t) =>
|
|
e1.progress(FunT(t1, t2))
|
|
.ap(HasType(Nil, e1, FunT(t1, t2)), Progress(e1), e1_t).match {
|
|
PStep(_, e1', e1_eval_e1') =>
|
|
PStep(App(e1, e2), App(e1', e2), ECongApp1(e1, e1', e1_eval_e1', e2)),
|
|
PVal(_, is_val) =>
|
|
is_val.match {
|
|
VLam(e) => PStep(App(Lam(e), e2), e.subst(Z, e2), EBeta(e, e2)),
|
|
},
|
|
},
|
|
},
|
|
}
|
|
|
|
def (e1: Exp).preservation(e2: Exp, t: Typ)
|
|
: HasType(Nil, e1, t) -> Eval(e1, e2) -> HasType(Nil, e2, t) {
|
|
Var(_) =>
|
|
\ap(_,_,h_t) => \ap(_,_,h_eval) => h_eval.match {
|
|
EBeta(_, _) absurd,
|
|
ECongApp1(_, _, _, _) absurd,
|
|
ECongApp2(_, _, _, _) absurd,
|
|
},
|
|
Lam(_) =>
|
|
\ap(_,_,h_t) => \ap(_,_,h_eval) => h_eval.match {
|
|
EBeta(_, _) absurd,
|
|
ECongApp1(_, _, _, _) absurd,
|
|
ECongApp2(_, _, _, _) absurd,
|
|
},
|
|
App(e1, e2) =>
|
|
\ap(_,_,h_t) => h_t.match {
|
|
TVar(_, _, _, _) absurd,
|
|
TLam(_, _, _, _, _) absurd,
|
|
TApp(_, t1, t2, _, _, h_lam, h_e2) =>
|
|
\ap(_,_,h_eval) => h_eval.match {
|
|
ECongApp1(_, e1', h, _) =>
|
|
TApp(Nil,
|
|
t1,
|
|
t2,
|
|
e1',
|
|
e2,
|
|
e1.preservation(e1', FunT(t1, t2))
|
|
.ap(HasType(Nil, e1, FunT(t1, t2)),
|
|
Eval(e1, e1') -> HasType(Nil, e1', FunT(t1, t2)),
|
|
h_lam)
|
|
.ap(Eval(e1, e1'), HasType(Nil, e1', FunT(t1, t2)), h),
|
|
h_e2),
|
|
ECongApp2(_, _, e2', h) =>
|
|
TApp(Nil,
|
|
t1,
|
|
t2,
|
|
e1,
|
|
e2',
|
|
h_lam,
|
|
e2.preservation(e2', t1)
|
|
.ap(HasType(Nil, e2, t1),
|
|
Eval(e2, e2') -> HasType(Nil, e2', t1),
|
|
h_e2)
|
|
.ap(Eval(e2, e2'), HasType(Nil, e2', t1), h)),
|
|
EBeta(e1, _) =>
|
|
h_lam.match {
|
|
TVar(_, _, _, _) absurd,
|
|
TApp(_, _, _, _, _, _, _) absurd,
|
|
TLam(_, _, _, _, h_e1) =>
|
|
e1.subst_lemma(Nil, Nil, t1, t2, e2)
|
|
.ap(HasType(Cons(t1, Nil), e1, t2),
|
|
HasType(Nil, e2, t1) -> HasType(Nil, e1.subst(Z, e2), t2),
|
|
h_e1)
|
|
.ap(HasType(Nil, e2, t1), HasType(Nil, e1.subst(Z, e2), t2), h_e2),
|
|
},
|
|
},
|
|
},
|
|
}
|
|
|
|
def (e: Exp).subst_lemma(ctx1 ctx2: Ctx, t1 t2: Typ, by_e: Exp)
|
|
: HasType(ctx1.append(Cons(t1, ctx2)), e, t2) -> HasType(Nil,
|
|
by_e,
|
|
t1) -> HasType(ctx1.append(ctx2),
|
|
e.subst(ctx1.len, by_e),
|
|
t2) {
|
|
Var(x) =>
|
|
\ap(_,_,h_e) => \ap(_,_,h_by) => h_e.match {
|
|
TLam(_, _, _, _, _) absurd,
|
|
TApp(_, _, _, _, _, _, _) absurd,
|
|
TVar(_, _, _, h_elem) =>
|
|
x.cmp_reflect(ctx1.len).match {
|
|
IsLT(_, _, h_eq_lt, h_lt) =>
|
|
h_eq_lt.transport(Ordering,
|
|
LT,
|
|
x.cmp(ctx1.len),
|
|
comatch {
|
|
.ap(_, _, cmp) =>
|
|
HasType(ctx1.append(ctx2),
|
|
cmp.subst_result(x, by_e),
|
|
t2),
|
|
},
|
|
ctx2.weaken_append(ctx1, Var(x), t2)
|
|
.ap(HasType(ctx1, Var(x), t2),
|
|
HasType(ctx1.append(ctx2), Var(x), t2),
|
|
TVar(ctx1,
|
|
x,
|
|
t2,
|
|
ctx1.elem_append_first(Cons(t1, ctx2), t2, x)
|
|
.ap(LE(S(x), ctx1.len),
|
|
Elem(x,
|
|
t2,
|
|
ctx1.append(Cons(t1,
|
|
ctx2))) -> Elem(x,
|
|
t2,
|
|
ctx1),
|
|
h_lt)
|
|
.ap(Elem(x,
|
|
t2,
|
|
ctx1.append(Cons(t1, ctx2))),
|
|
Elem(x, t2, ctx1),
|
|
h_elem)))),
|
|
IsEQ(_, _, h_eq_eq, h_eq) =>
|
|
h_eq_eq.transport(Ordering,
|
|
EQ,
|
|
x.cmp(ctx1.len),
|
|
comatch {
|
|
.ap(_, _, cmp) =>
|
|
HasType(ctx1.append(ctx2),
|
|
cmp.subst_result(x, by_e),
|
|
t2),
|
|
},
|
|
ctx1.append(ctx2)
|
|
.weaken_append(Nil, by_e, t2)
|
|
.ap(HasType(Nil, by_e, t2),
|
|
HasType(ctx1.append(ctx2), by_e, t2),
|
|
ctx1.ctx_lookup(ctx2, t2, t1)
|
|
.ap(Elem(ctx1.len,
|
|
t2,
|
|
ctx1.append(Cons(t1, ctx2))),
|
|
Eq(Typ, t1, t2),
|
|
h_eq.transport(Nat,
|
|
x,
|
|
ctx1.len,
|
|
comatch {
|
|
.ap(_, _, x) =>
|
|
Elem(x,
|
|
t2,
|
|
ctx1.append(Cons(t1,
|
|
ctx2)))
|
|
},
|
|
h_elem))
|
|
.transport(Typ,
|
|
t1,
|
|
t2,
|
|
comatch {
|
|
.ap(_, _, t) =>
|
|
HasType(Nil, by_e, t)
|
|
},
|
|
h_by))),
|
|
IsGT(_, _, h_eq_gt, h_gt) =>
|
|
h_eq_gt.transport(Ordering,
|
|
GT,
|
|
x.cmp(ctx1.len),
|
|
comatch {
|
|
.ap(_, _, cmp) =>
|
|
HasType(ctx1.append(ctx2),
|
|
cmp.subst_result(x, by_e),
|
|
t2),
|
|
},
|
|
TVar(ctx1.append(ctx2),
|
|
x.pred,
|
|
t2,
|
|
ctx1.elem_append_pred(ctx2, t2, t1, x)
|
|
.ap(LE(S(ctx1.len), x),
|
|
Elem(x,
|
|
t2,
|
|
ctx1.append(Cons(t1,
|
|
ctx2))) -> Elem(x.pred,
|
|
t2,
|
|
ctx1.append(ctx2)),
|
|
h_gt)
|
|
.ap(Elem(x, t2, ctx1.append(Cons(t1, ctx2))),
|
|
Elem(x.pred, t2, ctx1.append(ctx2)),
|
|
h_elem))),
|
|
},
|
|
},
|
|
Lam(body) =>
|
|
\ap(_,_,h_e) => \ap(_,_,h_by) => h_e.match {
|
|
TVar(_, _, _, _) absurd,
|
|
TApp(_, _, _, _, _, _, _) absurd,
|
|
TLam(_, a, b, _, h_body) =>
|
|
TLam(ctx1.append(ctx2),
|
|
a,
|
|
b,
|
|
body.subst(S(ctx1.len), by_e),
|
|
body.subst_lemma(Cons(a, ctx1), ctx2, t1, b, by_e)
|
|
.ap(HasType(Cons(a, ctx1).append(Cons(t1, ctx2)), body, b),
|
|
HasType(Nil, by_e, t1) -> HasType(Cons(a, ctx1).append(ctx2),
|
|
body.subst(S(ctx1.len), by_e),
|
|
b),
|
|
h_body)
|
|
.ap(HasType(Nil, by_e, t1),
|
|
HasType(Cons(a, ctx1).append(ctx2), body.subst(S(ctx1.len), by_e), b),
|
|
h_by)),
|
|
},
|
|
App(e1, e2) =>
|
|
\ap(_,_,h_e) => \ap(_,_,h_by) => h_e.match {
|
|
TVar(_, _, _, _) absurd,
|
|
TLam(_, _, _, _, _) absurd,
|
|
TApp(_, a, b, _, _, h_e1, h_e2) =>
|
|
TApp(ctx1.append(ctx2),
|
|
a,
|
|
b,
|
|
e1.subst(ctx1.len, by_e),
|
|
e2.subst(ctx1.len, by_e),
|
|
e1.subst_lemma(ctx1, ctx2, t1, FunT(a, b), by_e)
|
|
.ap(HasType(ctx1.append(Cons(t1, ctx2)), e1, FunT(a, b)),
|
|
HasType(Nil, by_e, t1) -> HasType(ctx1.append(ctx2),
|
|
e1.subst(ctx1.len, by_e),
|
|
FunT(a, b)),
|
|
h_e1)
|
|
.ap(HasType(Nil, by_e, t1),
|
|
HasType(ctx1.append(ctx2), e1.subst(ctx1.len, by_e), FunT(a, b)),
|
|
h_by),
|
|
e2.subst_lemma(ctx1, ctx2, t1, a, by_e)
|
|
.ap(HasType(ctx1.append(Cons(t1, ctx2)), e2, a),
|
|
HasType(Nil, by_e, t1) -> HasType(ctx1.append(ctx2),
|
|
e2.subst(ctx1.len, by_e),
|
|
a),
|
|
h_e2)
|
|
.ap(HasType(Nil, by_e, t1),
|
|
HasType(ctx1.append(ctx2), e2.subst(ctx1.len, by_e), a),
|
|
h_by)),
|
|
},
|
|
}
|
|
|
|
def (ctx2: Ctx).weaken_append(ctx1: Ctx, e: Exp, t: Typ)
|
|
: HasType(ctx1, e, t) -> HasType(ctx1.append(ctx2), e, t) {
|
|
Nil =>
|
|
\ap(_,_,h_e) => ctx1.append_nil
|
|
.transport(Ctx,
|
|
ctx1,
|
|
ctx1.append(Nil),
|
|
comatch { .ap(_, _, ctx) => HasType(ctx, e, t) },
|
|
h_e),
|
|
Cons(t', ts) =>
|
|
\ap(_,_,h_e) => ctx1.append_assoc(Cons(t', Nil), ts)
|
|
.transport(Ctx,
|
|
ctx1.append(Cons(t', Nil)).append(ts),
|
|
ctx1.append(Cons(t', ts)),
|
|
comatch { .ap(_, _, ctx) => HasType(ctx, e, t) },
|
|
ts.weaken_append(ctx1.append(Cons(t', Nil)), e, t)
|
|
.ap(HasType(ctx1.append(Cons(t', Nil)), e, t),
|
|
HasType(ctx1.append(Cons(t', Nil)).append(ts), e, t),
|
|
e.weaken_cons(ctx1, t', t)
|
|
.ap(HasType(ctx1, e, t),
|
|
HasType(ctx1.append(Cons(t', Nil)), e, t),
|
|
h_e))),
|
|
}
|
|
|
|
def (e: Exp).weaken_cons(ctx: Ctx, t1 t2: Typ)
|
|
: HasType(ctx, e, t2) -> HasType(ctx.append(Cons(t1, Nil)), e, t2) {
|
|
Var(x) =>
|
|
\ap(_,_,h_e) => h_e.match {
|
|
TLam(_, _, _, _, _) absurd,
|
|
TApp(_, _, _, _, _, _, _) absurd,
|
|
TVar(_, _, _, h_elem) =>
|
|
TVar(ctx.append(Cons(t1, Nil)), x, t2, h_elem.elem_append(x, t1, t2, ctx)),
|
|
},
|
|
Lam(e) =>
|
|
\ap(_,_,h_e) => h_e.match {
|
|
TVar(_, _, _, _) absurd,
|
|
TApp(_, _, _, _, _, _, _) absurd,
|
|
TLam(_, a, b, _, h_e) =>
|
|
TLam(ctx.append(Cons(t1, Nil)),
|
|
a,
|
|
b,
|
|
e,
|
|
e.weaken_cons(Cons(a, ctx), t1, b)
|
|
.ap(HasType(Cons(a, ctx), e, b),
|
|
HasType(Cons(a, ctx).append(Cons(t1, Nil)), e, b),
|
|
h_e)),
|
|
},
|
|
App(e1, e2) =>
|
|
\ap(_,_,h_e) => h_e.match {
|
|
TVar(_, _, _, _) absurd,
|
|
TLam(_, _, _, _, _) absurd,
|
|
TApp(_, a, b, _, _, h_e1, h_e2) =>
|
|
TApp(ctx.append(Cons(t1, Nil)),
|
|
a,
|
|
b,
|
|
e1,
|
|
e2,
|
|
e1.weaken_cons(ctx, t1, FunT(a, b))
|
|
.ap(HasType(ctx, e1, FunT(a, b)),
|
|
HasType(ctx.append(Cons(t1, Nil)), e1, FunT(a, b)),
|
|
h_e1),
|
|
e2.weaken_cons(ctx, t1, a)
|
|
.ap(HasType(ctx, e2, a), HasType(ctx.append(Cons(t1, Nil)), e2, a), h_e2)),
|
|
},
|
|
}
|
|
|
|
def Elem(n, t2, ctx).elem_append(n: Nat, t1 t2: Typ, ctx: Ctx)
|
|
: Elem(n, t2, ctx.append(Cons(t1, Nil))) {
|
|
Here(t, ts) => Here(t, ts.append(Cons(t1, Nil))),
|
|
There(n, _, t', ts, h) =>
|
|
There(n, t2, t', ts.append(Cons(t1, Nil)), h.elem_append(n, t1, t2, ts)),
|
|
}
|
|
|
|
def (ctx1: Ctx).append_assoc(ctx2 ctx3: Ctx)
|
|
: Eq(Ctx, ctx1.append(ctx2).append(ctx3), ctx1.append(ctx2.append(ctx3))) {
|
|
Nil => Refl(Ctx, ctx2.append(ctx3)),
|
|
Cons(x, xs) =>
|
|
xs.append_assoc(ctx2, ctx3)
|
|
.cong(Ctx,
|
|
Ctx,
|
|
xs.append(ctx2).append(ctx3),
|
|
xs.append(ctx2.append(ctx3)),
|
|
comatch { .ap(_, _, xs) => Cons(x, xs) }),
|
|
}
|
|
|
|
def (ctx: Ctx).append_nil: Eq(Ctx, ctx, ctx.append(Nil)) {
|
|
Nil => Refl(Ctx, 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): Void {
|
|
Here(_, _) absurd,
|
|
There(_, _, _, _, _) absurd,
|
|
}
|
|
|
|
def Elem(Z, t1, Cons(t2, ctx)).elem_unique(ctx: Ctx, t1 t2: Typ): Eq(Typ, t2, t1) {
|
|
Here(_, _) => Refl(Typ, t1),
|
|
There(_, _, _, _, _) absurd,
|
|
}
|
|
|
|
def (ctx1: Ctx).ctx_lookup(ctx2: Ctx, t1 t2: Typ)
|
|
: Elem(ctx1.len, t1, ctx1.append(Cons(t2, ctx2))) -> Eq(Typ, t2, t1) {
|
|
Nil => \ap(_,_,h) => h.elem_unique(ctx2, t1, t2),
|
|
Cons(t, ts) =>
|
|
\ap(_,_,h) => h.match {
|
|
Here(_, _) absurd,
|
|
There(_, _, _, _, h) =>
|
|
ts.ctx_lookup(ctx2, t1, t2)
|
|
.ap(Elem(ts.len, t1, ts.append(Cons(t2, ctx2))), Eq(Typ, t2, t1), h),
|
|
},
|
|
}
|
|
|
|
def (ctx1: Ctx).elem_append_first(ctx2: Ctx, t: Typ, x: Nat)
|
|
: LE(S(x), ctx1.len) -> Elem(x, t, ctx1.append(ctx2)) -> Elem(x, t, ctx1) {
|
|
Nil =>
|
|
\ap(_,_,h_lt) => \ap(_,_,h_elem) => h_lt.match {
|
|
LERefl(_) absurd,
|
|
LESucc(_, _, _) absurd,
|
|
},
|
|
Cons(t', ts) =>
|
|
\ap(_,_,h_lt) => \ap(_,_,h_elem) => h_elem.match {
|
|
Here(_, _) => Here(t, ts),
|
|
There(x', _, _, _, h) =>
|
|
There(x',
|
|
t,
|
|
t',
|
|
ts,
|
|
ts.elem_append_first(ctx2, t, x')
|
|
.ap(LE(S(x'), ts.len),
|
|
Elem(x', t, ts.append(ctx2)) -> Elem(x', t, ts),
|
|
h_lt.le_unsucc(x, ts.len))
|
|
.ap(Elem(x', t, ts.append(ctx2)), Elem(x', t, ts), h)),
|
|
},
|
|
}
|
|
|
|
def (ctx1: Ctx).elem_append_pred(ctx2: Ctx, t1 t2: Typ, x: Nat)
|
|
: LE(S(ctx1.len), x) -> Elem(x, t1, ctx1.append(Cons(t2, ctx2))) -> Elem(x.pred,
|
|
t1,
|
|
ctx1.append(ctx2)) {
|
|
Nil =>
|
|
\ap(_,_,h_gt) => \ap(_,_,h_elem) => h_elem.match {
|
|
Here(_, _) =>
|
|
h_gt.match {
|
|
LERefl(_) absurd,
|
|
LESucc(_, _, _) absurd,
|
|
},
|
|
There(_, _, _, _, h) => h,
|
|
},
|
|
Cons(t, ts) =>
|
|
\ap(_,_,h_gt) => \ap(_,_,h_elem) => h_elem.match {
|
|
Here(_, _) =>
|
|
h_gt.match {
|
|
LERefl(_) absurd,
|
|
LESucc(_, _, _) absurd,
|
|
},
|
|
There(x', _, _, _, h) =>
|
|
h_gt.le_unsucc(S(ts.len), x')
|
|
.s_pred(ts.len, x')
|
|
.transport(Nat,
|
|
S(x'.pred),
|
|
x',
|
|
comatch { .ap(_, _, x) => Elem(x, t1, Cons(t, ts).append(ctx2)) },
|
|
There(x'.pred,
|
|
t1,
|
|
t,
|
|
ts.append(ctx2),
|
|
ts.elem_append_pred(ctx2, t1, t2, x')
|
|
.ap(LE(S(ts.len), x'),
|
|
Elem(x', t1, ts.append(Cons(t2, ctx2))) -> Elem(x'.pred,
|
|
t1,
|
|
ts.append(ctx2)),
|
|
h_gt.le_unsucc(S(ts.len), x'))
|
|
.ap(Elem(x', t1, ts.append(Cons(t2, ctx2))),
|
|
Elem(x'.pred, t1, ts.append(ctx2)),
|
|
h))),
|
|
},
|
|
}
|
|
|
|
|
|
codata Fun(a b: Type) {
|
|
Fun(a, b).ap(a b: Type, x: a): b,
|
|
}
|
|
|
|
infix _ -> _ := Fun(_,_)
|
|
|
|
data Eq(a: Type, x y: a) {
|
|
Refl(a: Type, x: a): Eq(a, x, x),
|
|
}
|
|
|
|
def Eq(a, x, y).sym(a: Type, x y: a): Eq(a, y, x) { Refl(a, x) => Refl(a, x) }
|
|
|
|
def Eq(a, x, y).transport(a: Type, x y: a, p: a -> Type, prf: p.ap(a, Type, x)): p.ap(a, Type, y) {
|
|
Refl(a, x) => prf,
|
|
}
|
|
|
|
def Eq(a, x, y).cong(a b: Type, x y: a, f: a -> b): Eq(b, f.ap(a, b, x), f.ap(a, b, y)) {
|
|
Refl(a, x) => Refl(b, f.ap(a, b, x)),
|
|
}
|
|
|
|
def Eq(Nat, x, y).eq_s(x y: Nat): Eq(Nat, S(x), S(y)) { Refl(_, _) => Refl(Nat, S(x)) }
|
|
|
|
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)),
|
|
}
|
|
|
|
def Nat.cmp(y: Nat): Ordering {
|
|
Z =>
|
|
y.match {
|
|
Z => EQ,
|
|
S(_) => LT,
|
|
},
|
|
S(x) =>
|
|
y.match {
|
|
Z => GT,
|
|
S(y) => x.cmp(y),
|
|
},
|
|
}
|
|
|
|
data CmpReflect(x y: Nat) {
|
|
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(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(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)),
|
|
IsEQ(_, _, h1, h2) => IsEQ(S(x), S(y), h1, h2.eq_s(x, y)),
|
|
IsGT(_, _, h1, h2) => IsGT(S(x), S(y), h1, h2.le_succ(S(y), x)),
|
|
},
|
|
},
|
|
}
|
|
|
|
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),
|
|
}
|