Coq 错误 语法错误：'.'预计在 [gallina] 之后（在 [vernac_aux] 中）

Question

所以我有这个代码：

Require Import Unicode.Utf8.
Require Import String.

Inductive AExp :=
| avar : string → AExp 
| anum : nat → AExp 
| aplus : AExp → AExp → AExp 
| amul : AExp → AExp → AExp.

Coercion anum : nat >-> AExp.
Coercion avar : string >-> AExp.
Notation "A +' B" := (aplus A B) (at level 50, left associativity).
Notation "A *' B" := (amul A B) (at level 40, left associativity).

Inductive BExp :=
| btrue : BExp
| bfalse : BExp
| bnot : BExp → BExp
| band : BExp → BExp → BExp
| blessthan : AExp → AExp → BExp
| bgreaterthan : AExp → AExp → BExp.

Notation "A <' B" := (blessthan A B) (at level 80).
Notation "A >' B" := (bgreaterthan A B) (at level 80).
Infix "and'" := band (at level 82).
Notation "! A" := (bnot A) (at level 81).

Inductive Stmt :=
| assignment : string → AExp → Stmt 
| while : BExp → list Stmt → Stmt
| seq : Stmt → Stmt → Stmt
| obj_inst : string → string → Stmt
| method_invoke : string → string → list AExp → Stmt.

Notation "X ::= A" := (assignment X A) (at level 85).
Notation "S1 ;; S2" := (seq S1 S2) (at level 99, right associativity).

Inductive Method :=
| method : string → list Stmt → Method.

Inductive Class :=
| class : string → list (string * AExp) → list Method → Class.

Definition Point :=
  class "Point"
    [("x", anum 0) ("y", anum 0)]
    [
      method "move" [
        assignment "x" (aplus (avar "x") (anum 1));
        assignment "y" (aplus (avar "y") (anum 1))
      ]
    ].

Definition CreatePoint : Stmt :=
  obj_inst "p" "Point".

Definition MovePoint : Stmt :=
  method_invoke "p" "move" [].

Definition SampleProgram :=
  seq CreatePoint MovePoint.

我收到了这个错误：

语法错误：“.”预计在 [gallina] 之后（在 [vernac_aux] 中）。 我不确定是否是因为

Definition Point

。

尝试使用chatGpt，但没有成功。使用它我浪费了很多时间。 （我不知道该写什么，所以 StackOverflow 会让我发布这个问题）

Answer 1

（看起来有些旧的 Coq 代码需要更新。）

通常，如果不导入/打开符号，则无法使用它们：并且您的代码缺少列表和字符串符号。

这是对此的修复，以及对 StdLib 导入的修复，与您的代码一样，您可能会出现名称冲突/歧义：

From Coq Require Import Unicode.Utf8.
From Coq Require Import String.
From Coq Require Import List.

Import ListNotations.
Open Scope string.

...etc...

我还必须在这里修复丢失的分号：

Definition Point :=
  class "Point"
    [("x", anum 0); ("y", anum 0)]  (* <- semicolon in list *)
    [
      method "move" [
        assignment "x" (aplus (avar "x") (anum 1));
        assignment "y" (aplus (avar "y") (anum 1))
      ]
    ].

现在可以编译了...