Принуждение в структурах данных - PullRequest
Новая
       5

Принуждение в структурах данных

3 голосов
/ 09 января 2020

Следующий код дает мне ошибку: 

Require Import Reals.
Require Import List.
Import ListNotations.

Open Scope R_scope.

Definition C := (R * R)%type.

Definition RtoC (r : R) : C := (r,0).

Coercion RtoC : R >-> C.

Definition lC : list C := [0;0;0;1].

Error: The term "[0; 0; 0; 1]" has type "list R" while it is expected to have type "list C".

Но я определил RtoC как принуждение, и я не вижу никаких проблем при использовании 

Definition myC : C := 4.

Как мне заставить Coq применить принуждение в списке?

Смежный вопрос: Если я введу Check [0;0;0;1], он возвращает list R, вставляя неявный IZR перед каждым числом. Почему Coq считает, что я хочу R с, а не Z с?

1 Ответ

1 голос
/ 28 января 2020

Я не уверен, что есть полностью удовлетворительное решение для вашего вопроса.

Действительно, как вспоминается в Coq refman :

Учитывая термин возможно, не типизируемый, нас интересует проблема определения, может ли она быть хорошо типизированной по модулю вставки соответствующих приведения.

, и получается, что в вашем примере сам термин [0;0;0;1] набирается как list R и проверяется типом "за один go"; таким образом, когда происходит несоответствие типов [0;0;0;1] : list C, так как «обратного отслеживания» нет, принуждение не может быть вставлено в элементы списка.

Так что, возможно, вы могли бы адаптировать свою формализацию другим способом или просто использовать один из следующих обходных путей:

  • Перезапись вашего термина в β-переопределение: 

    Definition lC := (fun z o => [z;z;z;o] : list C) 0 1.

  • Или вставка еще нескольких типов типов вокруг каждого элемента : 

    Definition lC := [0:C; 0:C; 0:C; 1:C].

Относительно вашего последнего вопроса

Почему Coq считает, что я хочу R с, а не Z с?

это происходит из вашей строки Open Scope R_scope., что означает, что числовые буквенные обозначения по умолчанию распознаются как принадлежащие R (который имеет дело с классической аксиоматизацией действительных чисел, формализованных в стандартной библиотеке Reals). Более конкретно, реализация изменилась в Coq 8.7, начиная с coq / coq@a4a76c2 (обсуждается в PR coq / coq # 415 ). Подводя итог, можно сказать, что литерал, такой как 5%R, теперь анализируется как IZR 5, то есть IZR (Zpos (xI (xO xH))), в то время как в Coq 8.6 он анализировался в гораздо менее краткий термин: Rplus R1 (Rmult (Rplus R1 R1) (Rplus R1 R1)).

...