Можно ли переименовать термин coq?
Извините, я не уверен, что заголовок является адекватным вопросом.
Я проходил через «Основы логики». В лемме «double_plus» я решил это с помощью этого решения:
Lemma double_plus : forall n, double n = n + n .
Proof.
induction n.
- simpl. reflexivity.
- simpl. rewrite <- plus_n_Sm. rewrite IHn. reflexivity.
Qed.
На этапе индукции моя цель: double (S n) = S n + S n.
Я хотел бы знать, можно ли предположить, что (S n) есть k, и сделать с этим что-то вроде:
(* double k = k + k *)
rewrite IH. (*k + k = k + k*)
reflexivity.
Ответы 1
Вы можете использовать тактику набора .
Например
set (k := S n) in *.
изменит все вхождения S n и заменит его на k. Обратите внимание, что при этом информация k := S n по-прежнему будет сохраняться в контексте.
Вы можете забыть эту информацию, используя clearbody k.
Подобные тактики включают помнить и обобщать.
Что касается вашего заголовка, обратите внимание, что переименовать — это также тактика, которую вы можете использовать, но только для переименования, например. n на k (т. е. вы можете менять имена, а не термины).