在coq中编写隐式证明对象的不可能模式

Question

我试图使用coq作为依赖类型的编程语言.我创建了以下小程序:

Inductive Good : list nat -> Set := 
  | GoodNonEmpty : forall h t, Good (h :: t).

Definition get_first(l : list nat)(good : Good l) : nat := 
  match l with
    | h :: t => h
    | nil => 
      match good with 
      end
  end. 

我为非空列表定义了一个类型,并创建了一个函数,它获取了这样一个列表的第一个元素,前提是它有一个非空的证据.我处理好头部项目由两个项目组成的情况,但我无法处理空列表的不可能的情况.我怎么能在coq中做到这一点？

Answer 1

一种比你尝试更简单的方法是:

Definition get_first (l : list nat) (good : Good l) : nat :=
  match good with
  | GoodNonEmpty h _ => h
  end.

这是一种以您想要的方式完成它的方法.您会注意到,证明"Good nil"不存在是非常冗长的.

Definition get_first (l : list nat) (good : Good l) : nat :=
  (
    match l as l' return (Good l' -> nat) with
    | nil =>
      fun (goodnil : Good nil) =>
        (
          match goodnil in (Good l'') return (nil = l'' -> nat) with
          | GoodNonEmpty h t =>
            fun H => False_rect _ (nil_cons H)
          end
        )
        (@eq_refl _ nil)
    | h :: _ => fun _ => h
    end
  ) good.

你可以肯定地在外面定义一些并重用它.我不知道最好的做法.也许有人可以用更短的方式来做同样的事情.

编辑:

顺便说一句,你可以在证明模式下以更简单的方式得到几乎相同的结果:

Definition get_first' (l : list nat) (good : Good l) : nat.
Proof.
  destruct l. inversion good. exact n.
Defined.

然后你可以:

Print get_first'.

要了解Coq如何定义它.但是,对于更复杂的事情,您可能最好关注#coq IRC频道提出的gdsfhl作为解决方案:

http://paste.in.ua/4782/

您可以看到他使用refine策略来提供术语的部分骨架来编写,并推迟丢失的证明.