Coq:理由不足错误
Coq: Insufficient Justification error
我是 Coq 的新手,遇到假设 H3 的 Insufficient Justification
错误。我尝试重写它几次,但错误仍然存在。有人可以解释为什么吗?谢谢
Section GroupTheory.
Variable G: Set.
Variable operation: G -> G -> G.
Variable e : G.
Variable inv : G -> G.
Infix "*" := operation.
Hypothesis associativity : forall x y z : G, (x * y) * z = x * (y * z).
Hypothesis identity : forall x : G, exists e : G, (x * e = x) /\ (e * x = x).
Hypothesis inverse : forall x : G, (x * inv x = e) /\ (inv x * x = e).
Theorem latin_square_property :
forall a b : G, exists x : G, a * x = b.
proof.
let a : G, b : G.
take (inv a * b).
have H1:(a * (inv a * b) = (a * inv a) * b) by associativity.
have H2:(a * inv a = e) by inverse.
have H3:(e * b = b) by identity.
have (a * (inv a * b) = (a * inv a) * b) by H1.
~= (e * b) by H2.
~= (b) by H3.
hence thesis.
end proof.
Qed.
End GroupTheory.
原因是您的 identity
公理独立于本节中定义的单位 e
,因为您已将 e
与定义中的存在量词绑定identity
公理。
我们可以修改identity
,去掉定义中的exists e
:
Hypothesis identity : forall x : G, (x * e = x) /\ (e * x = x).
之后你就可以完成证明了。
我是 Coq 的新手,遇到假设 H3 的 Insufficient Justification
错误。我尝试重写它几次,但错误仍然存在。有人可以解释为什么吗?谢谢
Section GroupTheory.
Variable G: Set.
Variable operation: G -> G -> G.
Variable e : G.
Variable inv : G -> G.
Infix "*" := operation.
Hypothesis associativity : forall x y z : G, (x * y) * z = x * (y * z).
Hypothesis identity : forall x : G, exists e : G, (x * e = x) /\ (e * x = x).
Hypothesis inverse : forall x : G, (x * inv x = e) /\ (inv x * x = e).
Theorem latin_square_property :
forall a b : G, exists x : G, a * x = b.
proof.
let a : G, b : G.
take (inv a * b).
have H1:(a * (inv a * b) = (a * inv a) * b) by associativity.
have H2:(a * inv a = e) by inverse.
have H3:(e * b = b) by identity.
have (a * (inv a * b) = (a * inv a) * b) by H1.
~= (e * b) by H2.
~= (b) by H3.
hence thesis.
end proof.
Qed.
End GroupTheory.
原因是您的 identity
公理独立于本节中定义的单位 e
,因为您已将 e
与定义中的存在量词绑定identity
公理。
我们可以修改identity
,去掉定义中的exists e
:
Hypothesis identity : forall x : G, (x * e = x) /\ (e * x = x).
之后你就可以完成证明了。