По некоторой теореме мы знаем, что тип A равен типу B . Как я могу сообщить об этом компилятору Coq во время проверки типа?

Я хочу реализовать непустое дерево таким образом, чтобы каждый узел знал свой размер:

 Inductive Struct: positive -> Type :=
| Leaf : Struct 1%positive
| Inner: forall {n m}, Struct n -> Struct m -> Struct (n   m).
  

Я хочу создать функцию, которая генерирует дерево заданного размера логарифмической глубины. Например.

7 -> 6 1 -> (3 3) 1 -> ((2 1) (2 1)) 1 -> (((1 1) 1) ((1 1) 1)) 1

 Fixpoint nat2struct n : (Struct n) :=
  match n with
  | xH => Leaf
  | xO n => Inner (nat2struct n) (nat2struct n) 
  | xI n => Inner Leaf (Inner (nat2struct n) (nat2struct n))
  end.
  

Однако я получаю сообщение об ошибке:

Термин «Внутренний лист (Inner (nat2struct n0) (nat2struct n0))» имеет тип «Struct (1 (n0 n0))», в то время как ожидается, что он будет иметь тип «Struct n0 ~ 1».

Как я могу это исправить? Мы это знаем (1 n n) = xI n , но Coq этого не делает. Если я сформулирую эту теорему ранее, это ничего не изменит:

 Theorem nBy2p1: forall n, Pos.add 1%positive (n   n) = xI n. Proof. Admitted.
Hint Resolve nBy2p1.
  

Есть ли какие-либо подсказки для Coq, чтобы быть в курсе этой теоремы?

PS1: эта теорема уже доказана в стандартной библиотеке? Я не нашел ни одного.

PS2: Я на самом деле хочу разделить более естественно: 7 -> 4 3 -> (2 2) (2 1) -> ((1 1) (1 1)) ((1 1) 1) . Возможно ли это? Я не знаю, как это написать, чтобы Coq понимал, что функция сходится.

При проверке типов Coq использует более слабую форму равенства (иногда называемую определяющим, оценочным или вычислительным равенством). В отличие от равенства высказываний (к чему по умолчанию привязывается «=»), равенство определений разрешимо. Coq может принимать любые два термина и решать, можно ли преобразовать одно в другое. Если бы при проверке типов было разрешено пропозициональное равенство, проверка типов больше не была бы разрешимой¹.

Чтобы решить вашу проблему (а это довольно большая проблема), у вас есть несколько вариантов.

Сделайте Struct запись

Я продемонстрирую принцип, используя списки. Во-первых, у нас есть понятие списков без размера.

 Inductive UnsizedList (A: Type) :=
| unil
| ucons (a: A) (u: UnsizedList A).

Arguments unil [A], A.
Arguments ucons [A] a u, A a u.

Fixpoint length {A: Type} (u: UnsizedList A) :=
match u with
| unil => 0
| ucons _ u' => S (length u')
end.
  

Мы также можем определить размер списка, в котором каждый элемент SizedList A n имеет длину n .

 Inductive SizedList (A: Type): nat -> Type :=
| snil: SizedList A 0
| scons {n: nat} (a: A) (u: SizedList A n): SizedList A (S n).
  

Это определение сталкивается с точно такой же проблемой, как у вас. Например, если вы хотите показать, что конкатенация ассоциативна, вы не можете просто доказать concat (concat u v) w = concat u (concat v w) , поскольку две стороны равенства имеют разные типы ( (i j) k vs i (j k) ). Если бы мы могли просто сообщить Coq, какого размера мы ожидаем от списка, а затем доказать это позже, мы могли бы решить эту проблему. Вот что делает это определение, которое объединяет UnsizedList с доказательством того, что этот список имеет желаемую длину.

 Record SizedListPr (A: Type) (n: nat): Type := {
  list: UnsizedList A;
  list_len_eq: length list = n;
}.
  

Теперь мы можем иметь concat (concat u v) w = concat u (concat v w) ; нам просто нужно доказать, что обе стороны имеют длину (i j) k .

Используйте принуждения

Этот подход может стать довольно запутанным, если вы не будете осторожны, поэтому он не часто является предпочтительным подходом.

Позвольте мне определить своего рода принуждение, которое сопоставляет элементы типа P x с элементами типа P y if x = y .²

 Definition coercion {A: Type} (P: A -> Type) {x y: A} (p: x = y): P x -> P y :=
match p with
| eq_refl => fun t => t
end.
  

Здесь мы используем индукцию по термину p: x = y . Принцип индукции, по сути, гласит, что если мы можем что-то доказать, когда x и y по определению равны, то мы можем доказать это, когда они пропозиционально равны.³ Когда P x и P y совпадают, мы можем просто использовать функцию идентификации.

Теперь, например, утверждение об ассоциативности конкатенации для списков определенного размера является concat (concat u v) w = coercion (SizedList A) (add_assoc) (concat u (concat v w)) . Итак, мы приводим что-то типа SizedList A (i (j k)) к чему-то типа SizedList A ((i j) k) , используя равенство add_assoc: i (j k) = (i j) k (я опустил некоторые параметры для удобства чтения).

Какой выбор вы сделаете, зависит от вас. Обсуждение этой проблемы и связанных с ней проблем, а также некоторые дополнительные решения можно найти на странице Certified Programming with Dependent Types Равенство.

¹ Класс теорий, в которых это обычно происходит, см. в расширительной теории типов. В диссертации Мартина Хофманна дается обзор разницы между интенсиональной и экстенсиональной теориями.

² Если вы знакомы с теорией гомотопических типов, это transport .

³ В этом утверждении достаточно оговорок, указывающих на то, что различия между равенством высказываний и определениями все еще существуют.

Основываясь на ответе пользователя, это решение, к которому я пришел:

 Inductive Struct: positive -> Type :=
| Leaf : Struct 1
| Inner : forall {lsize rsize size}
    (proof: Pos.add lsize rsize = size),
    (Struct lsize) -> (Struct rsize) -> Struct size.

Local Lemma nBy2: forall {n}, Pos.add n n = xO n.
Proof.
intros.
assert (Zpos (n   n) = Zpos (n~0)). { rewrite Pos2Z.inj_add. rewrite Z.add_diag. symmetry. apply Pos2Z.inj_xO. }
inversion H. auto.
Qed.

Local Lemma nBy2p1: forall {n}, Pos.add 1 (xO n) = xI n.
Proof.
intros. simpl.
assert (Zpos (1   n~0) = Zpos (n~1)). { rewrite Pos2Z.inj_add. reflexivity. }
inversion H. auto.
Qed.

Fixpoint structCreate (size : positive) : (Struct size) :=
  match size with
  | xH => Leaf
  | xO n =>
    let child := structCreate n in
    Inner nBy2 child child
  | xI n => 
    let child := structCreate n in
    Inner nBy2p1 Leaf (Inner nBy2 child child)
  end.