Email Gateway (Aug 19 2022 at 09:38): Email Gateway (Aug 19 2022 at 09:38):From: James Cooper <not.fenimore@gmail.com>
Hello,
I'm new to the Isabelle system, so this might be a bit simplistic, but I've
looked through the tutorials and references and can't really find an
explanation. It's possible I'm just missing something, so if anyone can
explain what that is I'd be very grateful.
Basically, I'm trying to build a little interpreter, but the interpreter
and typechecker need to use "inductive" rather than e.g. "primrec" or
"function" because they do not provably terminate. That's fine, but the
proof rules for "inductive_rule.induct" don't seem to work straight for me.
(I'm on the Isabelle jEdit IDE for Mac, if it makes a difference.)
For instance, my typechecking predicate looks like
inductive typecheck :: "type env => expr => type => bool"
where chkNum: "typecheck env (NumExpr n) NumType"
| chkStr: "typecheck env (StrExpr s) StringType"
| chkVar: "lookup env v = Some t ==> typecheck
| chkLength: "typecheck env a StringType ==> typecheck env (LengthExpr
a) NumType"
etc.
where there's exactly one case for each expression type in the second
argument. So I want to prove a little set of inversion lemmas,
lemma num_const_invert: "typecheck env (NumExpr n) t ==> t = NumType"
etc.
Since the typechecking rules are syntax-directed, this seems like it should
be simple: induct on the typechecking rules, have the chkNum case trivially
and watch every other case produce e.g. "StringExpr s = NumExpr n" as an
assumption and proof by contradiction. Instead, the expression argument
gets wiped out and "apply (induction rule: type check.induct)" produces
which is obviously insoluble. As best I can tell it's inducting over a
generic term "typecheck env expr t", and the knowledge that expr is
really NumExpr n has been lost; as a result it's trying to prove that
typecheck always produces a NumType, with predictably strange results.
Any idea what's going on here? Am I doing something wrong? What's the
right way to define a nonterminating function of this kind and prove
things over it?
James Cooper
Last updated: Nov 21 2024 at 12:39 UTC