Дает ли что-нибудь использование тактики разворота с последующим сбросом в Coq?

Если вы посмотрите документацию для обоих fold (https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.fold) и unfold (https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.unfold ) вы можете видеть, что они не ожидают такого же аргумента. В то время как unfold принимает идентификатор в качестве аргумента, fold принимает термин.

Поэтому, если у вас есть def x y в вашей цели, вы можете unfold def получить доступ к ее определению, но тогда вам, возможно, придется использовать fold (def x y), чтобы вернуться к исходной цели.

В любом случае нет гарантии, что unfold def ; fold (def x y) ни к чему не приведет, так как возможны и другие вхождения развернутого def x y в цель.

Вот конкретный пример, чтобы увидеть fold и unfold в действии. Если цель меняется после тактики, я добавляю новую цель в комментарий после тактики. Обратите также внимание на использование Fail progress tac, утверждающего, что выполнение тактики tac вообще не повлияет на цель.

Definition foo (b : bool) :=
  if b then 0 else 1.

Goal foo true + 1 = foo false.
Proof.
  unfold foo.
  (* 0 + 1 = 1 *)
  Fail progress fold foo.
  fold (foo true).
  (* foo true + S (foo true) = S (foo true) *)
  Fail progress fold (foo false).
  unfold foo.
  (* 0 + 1 = 1 *)
  fold (foo false).
  (* 0 + foo false = foo false *)
  fold (foo true).
  (* foo true + foo false = foo false *)
  unfold foo at 2.
  (* foo true + 1 = foo false *)

Как видите, fold foo ничего не сделает, а fold true и fold false сделают, конечно, тоже жадно, любое 0 превратится в fold true.

Определенно. unfold def встраивает определение def и также выполняет некоторые основные сокращения, например. если def было применено к чему-либо до того, как оно было встроено.

Definition hold {T} (x : T) : Prop := True.
Goal (not False -> hold not).
unfold not.
(* inline not: (fun A : Prop => A -> False) False -> hold (fun A : Prop => A -> False)
   and reduce: (False -> False) -> hold (fun A : Prop => A -> False) *)

Однако fold def не отменяет сокращение приложений def. Если вы сейчас сделаете

fold not.

он не свернет False -> False обратно в not False. Он найдет только not под hold, поэтому вы получите (False -> False) -> hold not в качестве цели. (fold (not False) уменьшит not False до False -> False, найдет это, а затем, в конце концов, даст цель not False -> hold (fun A : Prop => A -> False, но, опять же, это не отменит должным образом unfold). Итак, по сути, последовательность unfold def. fold def. встраивает и упрощает использование def там, где оно использовалось (например, применялось), и пытается оставить другие варианты использования нетронутыми.

Другой пример, на этот раз с йота-редукцией (уменьшением разрушения) вместо бета-редукции.

Definition def : bool := true.
Definition truth (b : bool) : Prop := if b then True else False.
Goal ((if def then True else False) -> truth def).
unfold def.
(* inline def: (if true then True else False) -> truth true
   and reduce: True -> truth true *)
fold def.
(* goal: True -> truth def *)

В первом случае cbn. и unfold not. fold not. cbn. разные (и ни в том, ни в другом случае cbn ничего не делает). В этом последнем случае cbn. просто ведет нас прямо к True -> True независимо от того, где мы его поместили.