CoqIde의 "Ring"전술이 허용되지 않습니다.

Question

Coq를 배우고 있으며, 처음으로 ring 전술을 사용해야합니다. Require Ring. 또는 Require ArithRing. 뒤에 목표를 가지고있는 방정식의 오른쪽을 단순화하기 위해 사용했지만 Coq는 존재하지 않는 참조를 취합니다. 나는 (내가 ring과 ring_simplify 여러 번 시도) 여기에 코드 내 조각을 복사

Lemma sum_n_p : forall n, 2 * sum_n n + n = n * n. 

(* sum_n n is inductively defined as the sum of all numbers between 1 and n *) 

Proof. 
intros n. 
induction n as [ |m IHm]. 
+simpl. 
reflexivity. 
+assert (SnSn : S m * S m = m * m + 2 * m + 1). 
ring_simplify in [S m * S m = m * m + 2 * m + 1]. (*or just ring. , neither works*) 
rewrite SnSn. 
rewrite <- IHm. 
simpl. 
ring. 
Qed. 

Answer 1

그 전술을 호출하려면, 당신은 그 모듈을 가져와야합니다, 단지 그들을 필요로하지 :

Require Import ArithRing Ring. 

나는 그 라인들을 추가 한 후에 당신의 증명을 시험해 보았지만, Coq는 다른 에러에 빠지게되었습니다. Coq가 승인하기 전에 스크립트를 조정해야 할 수도 있습니다.