我想写一个函数,其类型是 forall n, option (n = 1)
.
我选择 option
作为替代的 reflect
避免给出否定的情况下的证明。所以 Some
扮演 ReflectT
并持有证明,而 None
不持有否定的证明。
Definition is_1 n: bool:=
match n with
1 => true |
_ => false
end.
Lemma is_1_complete : forall n, is_1 n = true -> n = 1.
intros.
destruct n. simpl in H. discriminate.
destruct n. reflexivity.
simpl in H. discriminate.
Qed.
Lemma a_nat_is_1_or_not: forall n, option (n = 1).
intros.
cut (is_1 n = true -> n = 1).
-
intros.
destruct n. exact None.
destruct n. simpl in H. exact (Some (H (eq_refl))).
exact None.
-
exact (is_1_complete n).
Qed.
我已经用战术做了。a_nat_is_1_or_not
是证明。而我认为直接写定义就可以做到这一点,所以我试了一下。
Definition a_nat_is_1_or_not' n: option (n = 1) :=
match is_1 n with
true => Some (is_1_complete n eq_refl)
| false => None
end.
但是Coq说s
Error:
In environment
n : nat
The term "eq_refl" has type "is_1 n = is_1 n"
while it is expected to have type "is_1 n = true" (cannot unify "is_1 n" and
"true").
似乎 is_1 n
无法统一到 true
在 true
本身的模式匹配的情况。
所以我试了一个更琐碎的例子。
Definition every_true_is_I x: x = I :=
match x with
I => eq_refl
end.
它的工作原理。
这两者之间的区别是什么?a_nat_is_1_or_not'
和 every_truer_is_I
我是不是遗漏了什么?我怎样才能写出一个有效的定义?forall n, is_1 n = true -> n = 1.
?
不同的是,在 a_nat_is_1_or_not'
的外部术语,其类型为 is_1 n = true -> _
. 如果你想 a_nat_is_1_or_not'
样子 every_true_is_I
,你必须确保所有出现的 is_1 n
被模式匹配所覆盖。
Definition a_nat_is_1_or_not' n: option (n = 1) :=
match is_1 n as b return ((b = true -> _) -> _) with
| true => fun H => Some (H eq_refl)
| false => fun _ => None
end (is_1_complete n).
注意 is_1_complete
已在模式匹配外实例化,因此其发生的 is_1 n
(已更名为 b
)的处理方式。
还有另一种方法,也许更习惯一些。你不需要对整个上下文进行概括,而只需要保留足够的信息来填补所有的漏洞。
Definition a_nat_is_1_or_not' n: option (n = 1) :=
match is_1 n as b return (is_1 n = b -> _) with
| true => fun H => Some (is_1_complete n H)
| false => fun _ => None
end eq_refl.
但想法是一样的. 通过实例化 eq_refl
在模式匹配之外,您不会丢失任何信息。is_1 n
.