Нельзя использовать инверсию для индуктивного предиката

Я застрял на простом доказательстве индуктивного предиката. Я должен доказать, что натуральный 0 не является положительным, где натуральный — это список битов, а 0 — это любой список, содержащий только биты, равные 0.

H1: pos Empt
____________ (1/1)
Nat

Эта глава Сертифицированное программирование с зависимыми типами предлагает использовать inversion, но я получаю сообщение об ошибке.

Require Import Coq.Program.Program.

Inductive Bit: Type :=
  | Zer: Bit
  | One: Bit.

Inductive List (type1: Type): Type :=
  | Empt: List type1
  | Fill: type1 -> List type1 -> List type1.

Implicit Arguments Empt [[type1]].

Implicit Arguments Fill [[type1]].

Definition Nat: Type := List Bit.

Inductive pos: Nat -> Prop :=
  | pos_1: forall nat1: Nat, pos (Fill One nat1)
  | pos_2: forall nat1: Nat, pos nat1 -> forall bit1: Bit, pos (Fill bit1 nat1).

Program Fixpoint pred (nat1: Nat) (H1: pos nat1): Nat :=
  match nat1 with
  | Empt => _
  | Fill Zer nat2 => Fill One (pred nat2 H1)
  | Fill One nat2 => Fill Zer nat2
  end.

Next Obligation.
inversion H1.

dependent-type coq
person user1494846    schedule 27.11.2012    source источник
comment
Странный. Я могу использовать инверсию вне обязательства. Theorem T1: pos Empt -> False. Proof. intro H1. inversion H1. Qed.   -  person user1494846    schedule 27.11.2012

Ответы (1)


arrow_upward
1
arrow_downward

Ваш Theorem T1 не эквивалентен Obligation. В последнем вы должны построить элемент Nat, который сам является Type (кстати, почему вы не используете здесь Set? Похоже, вы не манипулируете типами более высокого порядка в этой разработке).

Как говорится в сообщении об ошибке, вы не можете выполнить анализ случая (inversion построен на этом) для элемента Prop для этого (см., в частности, раздел 4.5.4 руководство по Coq). Однако в этом случае вы не заинтересованы в создании настоящего Nat, вы просто хотите доказать, что этот случай невозможен. Для этого вы можете apply False_rect (или False_rec, если вы решите использовать Set, а не Type), что оставит вас для доказательства False. False будучи Prop, вы можете использовать inversion H1.

Обратите внимание, что во второй ветви вашего определения pred есть проблема: вы не можете использовать (pred nat2 H1), так как H1 не является доказательством pos nat2. Вероятно, самый простой способ — оставить дыру и здесь: (pred nat2 _), которую можно тривиально решить с помощью inversion (на этот раз вы должны построить терм типа pos nat2, т. е. что-то, что живет в Prop).

person Virgile    schedule 27.11.2012
comment
Не знал, что есть разница между Set и Type. - person user1494846; 27.11.2012
comment
Type на самом деле представляет собой иерархию сортов Type(i), где Type(i) имеет Type(i+1), а Coq делает все возможное, чтобы скрыть вычисления над индексами. Set можно более или менее рассматривать как Type(0) (т.е. вы явно говорите, что не хотите играть с иерархией Type). См. раздел 4.1.1 для более подробной информации. - person Virgile; 28.11.2012