Делает ли что-нибудь использование разворачивания tacti c с последующим складыванием в Coq? - PullRequest
Новая
       86

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

0 голосов
/ 01 августа 2020

Достигнет ли unfold def. fold def. чего-нибудь в доказательстве Coq?

Иными словами: будет ли когда-нибудь разница между этими двумя последовательностями применения тактик?:

  • unfold def. fold def. cbn.
  • cbn.

Ответы [ 2 ]

2 голосов
/ 02 августа 2020

Если вы посмотрите документацию для 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 в действии. Если цель меняется после tacti c, я помещаю новую цель в комментарий после tacti c. Также обратите внимание на использование Fail progress tac, которое утверждает, что выполнение tacti c 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.

0 голосов
/ 02 августа 2020

Определенно. unfold def встраивает определение def, а также выполняет некоторые базовые c сокращения, например, если 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, где бы мы его ни поместили.

...