标签: coq-tactic

我想知道在Coq定理证明期间是否有办法引入一个全新的变量？

有关完整示例,请从此处考虑以下属性,以了解列表长度的均匀性.

Inductive ev_list {X:Type}: list X -> Prop :=
  | el_nil : ev_list []
  | el_cc  : forall x y l, ev_list l -> ev_list (x :: y :: l).

现在我想证明,对于任何列表,l如果它length是偶数,则ev_list l保持:

Lemma ev_length__ev_list': forall X (l : list X), ev (length l) -> ev_list l.
Proof.
  intros X l H.

这使:

1 subgoals
X : Type
l : list X
H : ev (length l)
______________________________________(1/1)
ev_list l …

我正在使用 Coq 8.5pl1。

举一个人为但具有说明性的例子，

(* fix so simpl will automatically unfold. *)
Definition double := fix f n := 2*n.

Theorem contrived n : double (2 + n) = 2 + double (1 + n).

现在，我只想将参数简化为 double，而不是其之外的任何部分。（例如，因为其余部分已经被仔细地放入正确的形式中。）

simpl.
   S (S (n + S (S (n + 0)))) = S (S (S (n + S (n + 0))))

这将外部 (2 + ...) 转换为 (S (S ...)) 以及展开双精度。

我可以通过执行以下操作来匹配其中之一：

match goal with | |- (double ?A) = _ => simpl A end. …

例如，我想要一种策略来遍历给定 HintDb 中的所有解析提示h，并且对于每个解析提示，它会执行pose h.. 这可能吗？如果是这样，如何？

我想出了以下玩具证明脚本：

Inductive myType : Type :=
| c : unit -> myType.

Inductive myProp : myType -> Type :=
| d : forall t, myProp (c t).
Hint Constructors myProp.

Definition myValue : myType := c tt.
Hint Unfold myValue.

Example test: myProp myValue.
Proof.
  auto 1000. (* does nothing *)
  unfold myValue.
  trivial.
Qed.

为什么我需要在myValue这里手动展开？提示是否足够？

我正在尝试自动化决定程序,以确定ASCII字符是否为空格.这是我现在拥有的.

Require Import Ascii String.

Scheme Equality for ascii.

Definition IsWhitespace (c : ascii) := (c = "009"%char) \/ (c = "032"%char).

Definition isWhitespace (c : ascii) : {IsWhitespace c} + {not (IsWhitespace c)}.
Proof.
  unfold IsWhitespace.
  pose proof (ascii_eq_dec c "009"%char) as [H1|H1];
  pose proof (ascii_eq_dec c "032"%char) as [H2|H2];
  auto.
  right. intros [H3|H3]; auto.
Admitted.

什么是使证明更简洁的好方法？

$ coqtop -nois
Welcome to Coq 8.7.0 (October 2017)

Coq < Ltac i := idtac.
Toplevel input, characters 0-4:
> Ltac i := idtac.
> ^^^^
Error: Syntax error: illegal begin of vernac.

我正在"coqtop -nois"下重新开发"Coq.Init.Prelude"和"HoTT.Basics.Overture"进行实践.我发现很难直接写表达式.这就是我想要使用战术的原因.我想知道为什么我不能使用"Ltac".

在Coq战术语言中,有什么区别

intro

和

intros？

我已经证明了Coq中多态列表的反函数的"正确性" .以下证明工作正常,但我有一些关于重写策略如何工作的问题.

这是代码:

Require Export Coq.Lists.List.
Import ListNotations.

Fixpoint rev {T:Type} (l:list T) : list T :=
  match l with
  | nil    => nil
  | h :: t => rev t ++ [h]
  end.

(* Prove rev_acc equal to above naive implementation. *)
Fixpoint rev_acc {T:Type} (l acc:list T) : list T :=
  match l with
  | nil => acc
  | h :: t => rev_acc t (h::acc)
  end.

Theorem app_assoc : forall  (T:Type) (l1 l2 …

我是一所大学的讲师，参加一门名为“ 类型系统的语言 ” 的课程，在最后一次讲解中，该教授将以下示例用于类型理论的归纳证明：

假设存在归纳定义的自然数（出于某种原因，他坚持称其为术语），而我们在它们上递归定义了一个大于函数。我们可以证明，对于每一个n，它都拥有（suc n> n）。

我准备了以下Coq代码以在类中实现此代码：

Inductive term : Set :=
  | zero
  | suc (t : term)
.

Fixpoint greaterThan (t t' : term) {struct t} : bool :=
  match t, t' with
   | zero, _ => false
   | suc t, zero => true
   | suc t, suc t' => t > t'
  end
where "t > t'" := (greaterThan t t').

Lemma successorIsGreater : forall t : term, suc t > t = …

以标准方式，我对这样的列表进行归纳

• 批准是为了lst
• 证明为x::lst

但我想要：

• 批准是为了lst
• 证明为lst ++ x::nil

x对我来说，在列表中的位置很重要。

我试图写这样的东西，但没有成功。