当我证明一些定理时,我的目标随着我应用越来越多的策略而演变.一般来说,目标往往分为子目标,子目标更简单.在最后一点,Coq决定目标得到证实.这个"经证实"的目标可能如何？这些目标似乎很好:
a = a. (* Any object is identical to itself (?) *)
myFunc x y = myFunc x y. (* Result of the same function with the same params
is always the same (?) *)
还有什么可以在这里或者可能是例子从根本上是错误的？
换句话说,当我最终申请时reflexivity,Coq只是说** Got it **没有任何解释.有没有办法获得更多关于它实际上做了什么的细节或者为什么它决定目标被证明了？
我一直在努力解决这个问题.我有一个归纳类型:
Definition char := nat.
Definition string := list char.
Inductive Exp : Set :=
| Lit : char -> Exp
| And : Exp -> Exp -> Exp
| Or : Exp -> Exp -> Exp
| Many: Exp -> Exp
我从中定义了一系列类型:
Inductive Language : Exp -> Set :=
| LangLit : forall c:char, Language (Lit c)
| LangAnd : forall r1 r2: Exp, Language(r1) -> Language(r2) -> Language(And r1 r2)
| LangOrLeft : forall r1 r2: Exp, Language(r1) …我正在使用nats的元组（特别是三元组nat*nat*nat），并且希望有一种按字典顺序比较元组的方法。与此等效：
Inductive lt3 : nat*nat*nat -> nat*nat*nat -> Prop :=
| lt3_1 : forall n1 n2 n3 m1 m2 m3, n1 < m1 -> lt3 (n1,n2,n3) (m1,m2,m3)
| lt3_2 : forall n1 n2 n3 m2 m3, n2 < m2 -> lt3 (n1,n2,n3) (n1,m2,m3)
| lt3_3 : forall n1 n2 n3 m3, n3 < m3 -> lt3 (n1,n2,n3) (n1,n2,m3).
我想证明一些基本特性，例如传递性和充分根据。标准库中是否有可以完成大部分工作的内容？如果没有，我对有根据的最感兴趣。我将如何证明呢？
我在Coq中使用MathComp库进行反射时遇到了一些非常简单的证明.
假设我想证明这个引理:
From mathcomp Require Import ssreflect ssrbool ssrnat.
Lemma example m n: n.+1 < m -> n < m.
Proof.
have predn_ltn_k k: (0 < k.-1) -> (0 < k).
by case: k.
rewrite -subn_gt0 subnS => submn_pred_gt0.
by rewrite -subn_gt0; apply predn_ltn_k.
Qed.
对于这样一个简单的任务,这种方法对我来说似乎有些"非正统".有更好/更简单的方法吗？
说我有以下关系：
Inductive my_relation: nat -> Prop :=
constr n: my_relation n.
我想证明以下几点：
Lemma example:
(forall n, my_relation n -> my_relation (S n)) -> (exists n, my_relation n) -> exists n, my_relation (S n).
Proof.
intros.
介绍之后，我具有以下环境：
1 subgoal
H : forall n : nat, my_relation n -> my_relation (S n)
H0 : exists n : nat, my_relation n
______________________________________(1/1)
exists n : nat, my_relation (S n)
我的问题是：是否有可能在存在量词下重写H？如果不是，是否有解决此类问题的策略（该特定问题并非真正相关，但是存在的问题是您必须证明exists使用另一种问题exists，并且在非正式情况下可以“推论”一种方法来重写该问题）exists。假设进入exists目标）？
例如，如果尝试尝试rewrite H in H0. …
我试图理解Coq定理：
Theorem thm0 : UseCl Pos (PredVP (UsePN john_PN) walk_V) ->
UseCl Pos (PredVP (UsePN john_PN) walk_V).
intro H.
exact H.
Qed.
来自https://github.com/GU-CLASP/FraCoq/blob/master/Tutorial.org
箭头符号是什么意思->？据我了解，然后Coq使用两个箭头https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html：1）双箭头定义类型构造函数，2）单箭头->定义新类型。但是这个定理是陈述，而不是类型定义。为什么会有这个箭头？如何将此陈述理解为Coq定理？
在Coq作为一名数学家,我本来期待的
Set -> Set : Set
但我想这是因为我的数学家帽子已经开启了.我该怎么做才能让它发挥作用？
我是否应该考虑设置不同并使用不同类型的Set？
我正在尝试在Coq中使用以下函数来实现使用n个元素构建Braun树的功能，但是Coq给了我一个错误，它无法猜测到fix参数的降低：
Fixpoint copy (x : V) (n : nat) : BraunTree :=
let
fix copy2 (a : V) (i : nat) : (BraunTree * BraunTree) :=
match i with
| 0 => (T a E E,E)
| _ => match Nat.odd i with
| true => let m := ((i - 1) / 2) in
let (s,t) := copy2 a m in
((T a s t),(T a t t))
| false => let m := ((i - 2) / 2) …我想not A通过假设A和发现来证明False。将目标not A转化为最短，最通用的方法是A -> False什么？
我尝试过exfalso，但是并没有增加A我的假设...
证明助手的主要功能是什么？
我只是想知道证明检查的内部逻辑。例如，有关此类助手的图形用户界面的主题使我不感兴趣。
对于编译器，我也提出了类似的问题：https : //softwareengineering.stackexchange.com/questions/165543/how-to-write-a-very-basic-compiler
我的担心是一样的，但对于校对系统。