Не може да се използва инверсия на индуктивен предикат

Заседнал съм на просто доказателство за индуктивен предикат. Трябва да докажа, че естествената 0 не е положителна, където естествената е списък от битове, а 0 е всеки списък само с битове, които са 0s.

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) (т.е. вие изрично казвате, че не искате да играете с йерархията на Types). Вижте раздел 4.1.1 за повече подробности - person Virgile; 28.11.2012