Индуктивное определение для семейства типов

Question

Я уже некоторое время борюсь за это. У меня есть индуктивный тип:

Definition char := nat. 
Definition string := list char. 


Inductive Exp : Set := 
    | Lit : char -> Exp 
    | And : Exp -> Exp -> Exp 
    | Or : Exp -> Exp -> Exp 
    | Many: Exp -> Exp 

, из которого я определяю семейство типов индуктивно:

Inductive Language : Exp -> Set :=                                   
    | LangLit  : forall c:char, Language (Lit c) 
    | LangAnd  : forall r1 r2: Exp, Language(r1) -> Language(r2) -> Language(And r1 r2) 
    | LangOrLeft : forall r1 r2: Exp, Language(r1) -> Language(Or r1 r2) 
    | LangOrRight : forall r1 r2: Exp, Language(r2) -> Language(Or r1 r2) 
    | LangEmpty : forall r: Exp, Language (Many r) 
    | LangMany : forall r: Exp, Language (Many r) -> Language r -> Language (Many r). 

Рационального здесь является то, что дан регулярным выражением r:Exp Я пытаюсь представить язык, связанный с r как тип Language r, и я делаю это с одним индуктивным определением.

Я хотел бы, чтобы доказать:.

Lemma L1 : forall (c:char)(x:Language (Lit c)), 
    x = LangLit c. 

(Другими словами, тип Language (Lit c) имеет только один элемент, то есть язык регулярного выражения 'c' производится из одной строки "c" Конечно, нужно определить некоторую семантику конвертирования элементы Language r в string)

Теперь специфика этой проблемы не является важной и просто служит, чтобы мотивировать свой вопрос: давайте использовать nat вместо Exp в го определят тип List n, который представляет списки длины n:

Parameter A:Set. 
Inductive List : nat -> Set := 
    | ListNil : List 0 
    | ListCons : forall (n:nat), A -> List n -> List (S n). 

Здесь снова я использую один индуктивное определение, чтобы определить семейство типов List n.

Я хотел бы, чтобы доказать:

Lemma L2: forall (x: List 0), 
    x = ListNil. 

(другими словами, тип List 0 имеет только один элемент).

У меня закончились идеи по этому вопросу.

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

Answer 1

Если вы готовы принять больше, чем просто базовую логику Coq, вы можете просто использовать тактику dependent destruction, доступную в библиотеке Program (я позволил перефразировать ваш последний пример с точки зрения стандартной библиотеки векторы):

Require Coq.Vectors.Vector. 

Require Import Program. 

Lemma l0 A (v : Vector.t A 0) : v = @Vector.nil A. 
Proof. 
now dependent destruction v. 
Qed. 

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

Print Assumptions l0. 

Axioms: 
JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y 

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

Lemma l0_gen A n (v : Vector.t A n) : 
    match n return Vector.t A n -> Prop with 
    | 0 => fun v => v = @Vector.nil A 
    | _ => fun _ => True 
    end v. 
Proof. 
now destruct v. 
Qed. 

Lemma l0' A (v : Vector.t A 0) : v = @Vector.nil A. 
Proof. 
exact (l0_gen A 0 v). 
Qed. 

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

Print Assumptions l0'. 
Closed under the global context 

Что здесь произошло? Проблема, грубо говоря, в том, что в Coq мы не можем проводить анализ случаев на членах зависимых типов, индексы которых имеют определенную форму (например, 0, в вашем случае) непосредственно. Вместо этого мы должны доказать более общее утверждение, где проблемные индексы заменяются переменными. Это как раз то, что делает лемма l0_gen. Обратите внимание, что нам нужно было сделать матч на n, возвращая функцию, которая реферат на v. Это еще один пример того, что известно как "convoy pattern". Если бы мы написали

match n with 
| 0 => v = @Vector.nil A 
| _ => True 
end. 

Coq увидит v в 0 отраслей как имеющий тип Vector.t A n, что делает эту отрасль плохо напечатанной.

Выполнение таких обобщений - одна из больших проблем, выполняемых навязчивым программированием в Coq. Другие системы, такие как Agda, позволяют писать этот тип кода с гораздо меньшими усилиями, но совсем недавно было shown, что это можно сделать, не полагаясь на дополнительные аксиомы, которые Coq хотел избежать в своей базовой теории. Мы можем только надеяться, что это будет упрощено в будущих версиях.