英文:
Exhaustiveness matching in proof objects for induction in Coq
问题
在《软件基础》中，他们讨论了如何为归纳构建自己的证明对象：
https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html#nat_ind2
Definition nat_ind2 :
∀ (P : nat → Prop),
P 0 →
P 1 →
(∀ n : nat, P n → P (S(S n))) →
∀ n : nat , P n :=
fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒
fix f (n:nat) := match n with
0 ⇒ P0
| 1 ⇒ P1
| S (S n') ⇒ PSS n' (f n')
end.
我通过注释掉 "| 1 ⇒ P1" 来尝试这个定义。Coq然后报错："非穷尽的模式匹配：未找到匹配模式1的分支。" 当然，我预期会出现错误。但我不知道Coq是如何发现这个错误的。
我想知道Coq是如何进行穷举匹配以知道需要检查1的，因为1不是nat的构造函数之一。大致上，Coq遵循什么算法？
英文:
In Software Foundations, they discuss how to build you own proof objects for induction:
https://softwarefoundations.cis.upenn.edu/lf-current/IndPrinciples.html#nat_ind2
Definition nat_ind2 :
∀ (P : nat → Prop),
P 0 →
P 1 →
(∀ n : nat, P n → P (S(S n))) →
∀ n : nat , P n :=
fun P ⇒ fun P0 ⇒ fun P1 ⇒ fun PSS ⇒
fix f (n:nat) := match n with
0 ⇒ P0
| 1 ⇒ P1
| S (S n') ⇒ PSS n' (f n')
end.
I experimented with this definition by commenting out "| 1 ⇒ P1". Coq then gives an error: "Non exhaustive pattern-matching: no clause found for pattern 1." I was expecting an error, of course. But I don't know how Coq figures out there is an error.
I would like to know how Coq does the exhaustiveness matching to know that 1 needs to be checked, since 1 isn't part of the constructor for nat. Roughly what algorithm is Coq following?
答案1
得分: 1
I'm not sure it answers fully your question, but you may look at the way "extended" matching are dealt with (see for instance https://coq.inria.fr/distrib/current/refman/language/extensions/match.html#mult-match ).
Let's look at a simple example.
Definition f (n: nat): nat :=
match n with
2 => 2
| 1 => 23
| _ => S n
end.
With the following command, I can see how f is expressed through simple pattern matchings.
Unset Printing Matching.
Print f.
(*
f =
fun n : nat =>
match n with
| 0 => S n
| S n0 =>
match n0 with
| 0 => 23
| S n1 => match n1 with
| 0 => 2
| S _ => S n
end
end
end
: nat -> nat
*)
If you remove the clause for 1 from your example, it seems impossible to convert your match into nested simple 0 | S _ matchings `.
英文:
I'm not sure it answers fully your question, but you may look at the way "extended" matching are dealt with (see for instance https://coq.inria.fr/distrib/current/refman/language/extensions/match.html#mult-match ).
Let's look at a simple example.
Definition f (n: nat): nat :=
match n with
2 => 2
| 1 => 23
| _ => S n
end.
With the following command, I can see how f is expressed through simple pattern matchings.
Unset Printing Matching.
Print f.
(*
f =
fun n : nat =>
match n with
| 0 => S n
| S n0 =>
match n0 with
| 0 => 23
| S n1 => match n1 with
| 0 => 2
| S _ => S n
end
end
end
: nat -> nat
*)
If you remove the clause for 1 from your example, it seems impossible to
convert your match into nested simple 0 | S _ matchings `.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论