S x = S y에서 x = y으로 목표를 변경하고 싶습니다. inversion과 같지만 가설 대신 목표가됩니다.Coq에서 'S x = S y'에서 'x = y'로 목표를 변경하는 전술
x = y이있는 경우 rewrite과 reflexivity을 사용하면 목표를 증명할 수 있기 때문에 이러한 전략이 합법적 인 것처럼 보입니다.
현재 새로운 가정을 소개하기 위해 항상 assert (x = y)을 사용하고 있지만, x과 y이 복잡한 표현 인 경우 작성하는 것이 지루합니다.
전술 apply f_equal. 당신은 어떤 생성자 또는 기능에, 원하는 것을 할 것입니다.
lema f_equal은 모든 기능이 f 일 때 항상 x = y -> f x = f y임을 보여줍니다.
Proposition myprop (x y: nat) (H : x = y) : S x = S y.
Proof.
apply f_equal. assumption.
Qed.
(. injection 전술은 반대의 의미를 구현 - 일부 기능을위한, 그리고 생성자에 특히 f x = f y -> x = y 있음)
당신은 injection 전술 좀보고 할 수 있습니다 : http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic126
이 정확하지 않은 : 이것은 당신이 f x = f yx = y에에서 목표를 줄일 수 있습니다 : "injection"은'fx = fy -> x = y' 형식의 함축을 구현합니다 (그리고 이것은 임의의 함수'f'에 대해서는 보유하지 않습니다, 단지 생성자를위한 특별한 경우에만). OP가 묘사하는 것은 단지 모든 함축적 인 의미를 지닌 'x = y -> f x = f y'라는 역관계 의미를 사용하는 것입니다. –
PLL
예. 죄송합니다. 질문을 잘못 읽고 가설에서 'S x = S y'가 나오는 문제라고 생각했습니다. – Virgile
일부 입력을 저장하는'f_equal' 전술을 사용할 수도 있습니다. – hugomg