Есть ли в Изабель тактика переписывания?

Например, в Coq есть rewrite, и мы также можем поставить стрелки `‹ -:

Inductive bool: Set :=
  | true
  | false.

Lemma equality_of_functions_commutes:
  forall (f: bool->bool) x y,
    (f x) = (f y) -> (f y) = (f x).
Proof.
  intros.
  rewrite H.
  reflexivity.
Qed.

источник: https://pjreddie.com/coq-tactics/#rewrite


theorem-proving isabelle
person Charlie Parker    schedule 18.03.2020    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Я не верю, что он такой же сильный, как версия Coq, но

переписать теоремы. Однако вы не можете легко переписать предположения в прикладном стиле.

person Mathias Fleury    schedule 18.03.2020
comment
как насчет рефлексивности? - person Charlie Parker; 18.03.2020
comment
Вероятно, наиболее близким к рефлексивности является apply (simp (no_asm)), но очень неестественно использовать это вместо apply simp. - person Mathias Fleury; 19.03.2020
comment
Это просто побочное замечание: кажется, что для конкретного приложения Пиноккио может быть лучше использовать apply(rule refl) или просто .. вместо simp (no_ams) или simp, учитывая, что два термина, полученные в результате применения переписывания, будут полностью идентичными. Конечно, в целом кажется, что simp (no_asm) действительно настолько близок к reflexivity Coq. - person user9716869; 20.03.2020