时间戳

首页 > 解决方案 > Coq 开发的案例构造

coq - Coq 开发的案例构造

问题描述

似乎在某个时候有一个文件 SfLib.v 用于软件基础课程。但是，在我的情况下，此文件中提出的 case 命令没有通过：

Require Omega.   (* needed for using the [omega] tactic *)
Require Export Bool.
Require Export List.
Require Export Arith.
Require Export Arith.EqNat.  (* Contains [beq_nat], among other things *)

(** * From Basics.v *)

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "Case" constr(name) := Case_aux Case name.
Tactic Notation "SCase" constr(name) := Case_aux SCase name.
Tactic Notation "SSCase" constr(name) := Case_aux SSCase name.
Tactic Notation "SSSCase" constr(name) := Case_aux SSSCase name.
Tactic Notation "SSSSCase" constr(name) := Case_aux SSSSCase name.
Tactic Notation "SSSSSCase" constr(name) := Case_aux SSSSSCase name.
Tactic Notation "SSSSSSCase" constr(name) := Case_aux SSSSSSCase name.
Tactic Notation "SSSSSSSCase" constr(name) := Case_aux SSSSSSSCase name.

Fixpoint ble_nat (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => ble_nat n' m'
      end
  end.

Theorem andb_true_elim1 : forall b c,
  andb b c = true -> b = true.
Proof.
  intros b c H.
  destruct b.
  Case "b = true".
    reflexivity.
  Case "b = false".
    rewrite <- H. reflexivity.  Qed.

在第一种情况下，我得到No interpretation for string "b = true".

之前尝试使用 Case 时在 coq 错误中解决了这个问题。来自软件基础书籍的示例。但是，那里的解决方案不再起作用。我应该摆脱所有的案例陈述吗？

标签： coq

解决方案

也许从那以后发生了一些变化，但现在我们需要Import符号。

(* 8.9, 8.10, and newer *)
From Coq Require String.
Export String.StringSyntax.  (* [Export] means to [Import] the StringSyntax module, but also make it automatically available to whoever imports this file as well. *)
Open Scope string_scope.

(* 8.8 and older (still works with 8.9, 8.10, but pollutes the namespace) *)
From Coq Require Export String.
Open Scope string_scope.

然而，正如移除模块所证明的那样，这个技巧的好处是很小的。大多数人只是使用项目符号，如果他们愿意发表评论，则使用评论来指明案例。

上面Open Scope是使用的，这对于像 SF 这样的独立项目可能很好，但是对于大型和开放的项目，为了避免符号的意外，我建议只使用Local Open Scope（然后需要出现在每个文件中），或者保留Open Scope在内部模块（仍然需要显式导入，但可以与其他模块一起重新导出）。

推荐阅读