Когда средство проверки завершения сокращает средство доступа к записи

Я спотыкаюсь о поведении средства проверки завершения Coq, которое я не могу объяснить себе. Рассмотреть возможность:

Require Import Coq.Lists.List.

Record C a := {  P : a -> bool }.

Arguments P {_}.

Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C).

Definition list_C  {a} (a_C : C a) : C (list a) := {| P := list_P a_C |}.

(* Note that *)
Eval cbn in       fun a C => (P (list_C C)).
(* evaluates to:  fun a C  => list_P C *)

Inductive tree a := Node : a -> list (tree a) -> tree a.

(* Works, using a local record *)
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool :=
    let tree_C := Build_C _ (tree_P1 a_C) in
    let list_C' := Build_C _ (list_P tree_C) in
    match t with Node _ x ts => orb (P a_C x) (P list_C' ts) end.

(* Works too, using list_P directly *)
Fixpoint tree_P2 {a} (a_C : C a) (t : tree a) : bool :=
    let tree_C := Build_C _ (tree_P2 a_C) in
    match t with Node _ x ts => orb (P a_C x) (list_P tree_C ts) end.

(* Does not work, using a globally defined record. Why not? *)
Fixpoint tree_P3 {a} (a_C : C a) (t : tree a) : bool :=
    let tree_C := Build_C _ (tree_P3 a_C) in
    match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end.

Первый и второй примеры показывают, что при попытке понять, завершается ли точка фиксации, Coq может разрешать методы доступа к записи, в основном оценивая то, что мы написали в tree_P1, по тому, что мы написали в tree_P2.

Но это, кажется, работает только в том случае, если запись создается локально (let tree_C :=…), а не в том случае, если она определена с использованием Definition.

Но Fixpoint может прекрасно просматривать другие определения, например. через list_P. Так что же особенного в записях, и могу ли я заставить Coq принимать tree_P3?


termination coq
person Joachim Breitner    schedule 02.11.2017    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Почитав средство проверки завершения в Coq, я думаю, что нашел решение:

Средство проверки завершения всегда будет разворачивать локальные определения и выполнять бета-свертку. Вот почему tree_P1 работает.

Средство проверки завершения также при необходимости разворачивает вызываемые определения (например, list_C', P, existsb), поэтому tree_P2 работает.

Однако средство проверки завершения не будет разворачивать определения, которые появляются в предложении match … with, например list_C. Вот минимальный пример для этого:

(* works *)
Fixpoint foo1 (n : nat) : nat :=
  let t := Some True in 
  match Some True with | Some True => 0
                       | None => foo1 n end.

(* works *)
Fixpoint foo2 (n : nat) : nat :=
  let t := Some True in 
  match t with | Some True => 0
               | None => foo2 n end.

(* does not work *)
Definition t := Some True.

Fixpoint foo3 (n : nat) : nat :=
  match t with | Some True => 0
               | None => foo3 n end.

Обходной путь для исходного кода состоит в том, чтобы убедиться, что все определения вызываются (а не сопоставляются с образцом), чтобы убедиться, что средство проверки завершения их развернет. Мы можем сделать это, переключившись на стиль передачи продолжения:

Require Import Coq.Lists.List.

Record C_dict a := {  P' : a -> bool }.

Definition C a : Type := forall r, (C_dict a -> r) -> r.

Definition P {a} (a_C : C a) : a -> bool :=
  a_C _ (P' _).

Definition list_P {a} (a_C : C a) : list a -> bool := existsb (P a_C).

Definition list_C  {a} (a_C : C a) : C (list a) :=
   fun _ k => k {| P' := list_P a_C |}.

Inductive tree a := Node : a -> list (tree a) -> tree a.

(* Works now! *)
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool :=
    let tree_C := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in
    match t with Node _ x ts => orb (P a_C x) (P (list_C tree_C) ts) end.

Это работает даже с классами типов, поскольку разрешение классов типов не зависит от следующих проблем:

Require Import Coq.Lists.List.

Record C_dict a := {  P' : a -> bool }.

Definition C a : Type := forall r, (C_dict a -> r) -> r.
Existing Class C.

Definition P {a} {a_C : C a} : a -> bool := a_C _ (P' _).

Definition list_P {a} `{C a} : list a -> bool := existsb P.

Instance list_C  {a} (a_C : C a) : C (list a) :=
   fun _ k => k {| P' := list_P |}.

Inductive tree a := Node : a -> list (tree a) -> tree a.

(* Works now! *)
Fixpoint tree_P1 {a} (a_C : C a) (t : tree a) : bool :=
    let tree_C : C (tree a) := fun _ k => k (Build_C_dict _ (tree_P1 a_C)) in
    match t with Node _ x ts => orb (P x) (P ts) end.
person Joachim Breitner    schedule 03.11.2017

arrow_upward
1
arrow_downward

По вопросу 1. Я считаю, что в tree_P1 определение экземпляра класса находится внутри конструкции fix и сокращается на момент проверки завершения.

Следующее определение отвергается, как Вы справедливо указываете.

Fixpoint tree_P1' {a} `{C a} (t : tree a) : bool :=
    let tree_C := Build_C _ tree_P1' in
    match t with Node _ x ts => orb (P x) (@P _ (* mark *) _ ts) end.

В этом определении экземпляр класса, необходимый после комментария (* mark *), заполняется определением, которое у вас есть в строке 7. Но это определение находится вне конструкции fix и не будет сокращено средством проверки завершения таким же образом. В результате в коде останется вхождение tree_P1', не примененное ни к одному из аргументов дерева, и средство проверки завершения не сможет определить, что это вхождение используется только для аргументов, которые меньше исходного аргумента.

Это дикая догадка, потому что мы не можем видеть тело отвергаемой функции.

person Yves    schedule 03.11.2017