如何证明 c-'a' 在 [0,26) 之内？

Question

假设我有这个代码：

#include "share/atspre_staload.hats"

val letters = arrayref_make_elt<bool>(i2sz(26), false)

implement main0() =
  begin
    println!("found('a'): ", letters[0]);
    println!("found('f'): ", letters[5]);
  end

产生输出：

found('a'): false
found('f'): false

我想改为按字符索引 letters。实际上，给定 任何字符 我想索引到 letters 只有当它是一个有效索引时。

所以这几乎可以工作：

#include "share/atspre_staload.hats"

val letters = arrayref_make_elt<bool>(i2sz(26), false)

typedef letter = [c:int | c >= 'a' && c <= 'z'] char(c)
typedef letteri = [i:int | i >= 0 && i < 26] int(i)

(* fn letter2index(c: letter): letteri = c - 'a' *)  (* #1 *)

fn letter2index(c: letter): letteri =
  case- c of
  | 'a' => 0
  | 'f' => 5

fn trychar(c: char): void =  (* #2 *)
  if c >= 'a' && c <= 'z' then
    println!("found('", c, "'): ", letters[letter2index(c)])

implement main0() =
  begin
    trychar('a');
    trychar('f');
    trychar('+');  (* #3 *)
  end

如果我将#2 处的char 更改为letter 并删除#3 处的trychar('+')，则编译成功。但是当然我宁愿在#1 处执行减法而不是大写的字母，我想将 trychar 应用于任何类型的 char，而不仅仅是 letter .

Answer 1

你想要的代码可以这样写：

#include
"share/atspre_staload.hats"

stadef
isletter(c:int): bool = ('a' <= c && c <= 'z')

val
letters = arrayref_make_elt<bool>(i2sz(26), false)

fn
letter2index
{ c:int
| isletter(c)}
(c: char(c)): int(c-'a') = char2int1(c) - char2int1('a')

fn
trychar
{c:int}
(c: char(c)): void =
if
(c >= 'a') * (c <= 'z')
then
println!("found('", c, "'): ", letters[letter2index(c)])

implement main0() =
begin
  trychar('a');
  trychar('f');
  trychar('+');
end

在您的原始代码中，量词（forall 和 exists）使用不正确。

如何证明 c-'a' 在 [0,26) 之内？

How do I prove that c-'a' is within [0,26)?

ats