Coq : 합계에서 중첩 된 괄호를 모두 제거합니다.

a + (b + (c + d))과 같은 합계가 있다고 가정합니다. 보조 언어를 적용하려면 a + b + c + d으로 변환하고 싶습니다.Coq : 합계에서 중첩 된 괄호를 모두 제거합니다.

수동으로 Nat.add_assoc을 사용하는 것은 지루한 작업입니다. 더 똑똑한 방법이 있습니까?

repeat rewrite Nat.add_assoc.

또는보다 간결 : 그것은 더 이상 적용 할 수 없을 때까지 내가 사용하는 것이

2016-11-18 Shuzheng

'쉽지만 좋은하지'방법은 replace (a + (b + (c + d)))) with (a + b + c + d) by now omega

가

2016-11-18 12:13:55 Vinz

왜 좋지 않은가요? 또한'with auto with *'를 사용하여 할 수 있습니다. –

'오메가'가 생성 한 출력 용어를 살펴 본다면 이해하게 될 것입니다. 대부분의 경우 지나치게 복잡하고 재 작성을 사용하는 작은 증거는 훨씬 작습니다. 그러나 그것은 개인적인 견해의 문제입니다.) – Vinz

by omega는 잘 작동 할 것입니다. '링으로'도 문제를 해결한다. 전자는 수입 할 오메가 모듈이 필요합니다. 후자 -'Arith '. –

가

당신은 몇 가지 전술을 반복하는의 repeat 전술을 사용할 수있다 버전 :

rewrite !Nat.add_assoc.

repeat의 변형과 동일합니다.

이 접근 방식의 단점은 목표의 모든 부분을 다시 씁니다. 따라서 수식의 일부만 선택하여 다시 쓰는 것이 좋습니다.

2016-11-18 12:20:15

답변