Корпусная конструкция для разработки Coq - PullRequest
Новая
       6

Корпусная конструкция для разработки Coq

0 голосов
/ 29 января 2020

Кажется, в какой-то момент был файл SfLib.v, который использовался для курса Software Foundations. Тем не менее, команда 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. Пример из книги «Основы программного обеспечения» . Однако решение там больше не работает. Должен ли я избавиться от всех дел дела?

1 Ответ

1 голос
/ 29 января 2020

Возможно, что-то изменилось с тех пор, но теперь нам нужно 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 внутри внутренних модулей (которые все еще должны быть импортированы явно, но могут быть реэкспортируется вместе с другими). ​​

...