代码之家 › 专栏 › 技术社区 › Bromind

以道具居住者为争论焦点

coq

Bromind · 技术社区 · 6 年前

考虑一下 find 在里面 the standard library ,作为类型 find: forall A : Type, (A -> bool) -> list A -> option A .

当然, 找到 必须返回 option A 而不是一个 A 因为我们不知道列表中是否有“有效”元素。

现在,假设我找到了 找到 痛苦,因为我们必须处理这个选项,即使我们确信这个元素存在于列表中。

因此,我想定义 myFind 哪一项可以证明列表中有这样一个元素。可能是这样的:

Variable A: Type.
Fixpoint myFind 
  (f: A -> bool) 
  (l: list A) 
  (H: exists a, In a l /\ f a = true): A :=
...

如果我没有弄错的话,这样的签名非正式地说:“给我一个函数、一个列表,以及一个证明列表中有一个“有效”元素的证据。”。

我的问题是:如何使用提供的假设并定义我的固定点?

我想的是:

match l with
| nil => (* Use H to prove this case is not possible *)
| hd :: tl => 
  if f hd
  then hd
  else 
    (* Use H and the fact that f hd = false 
       to prove H': exists a, In a tl /\ f a = true *)
    myFind f tl H'
end.

另一个好处是知道我是否可以直接在类型中设置一个关于结果的属性,例如,在我们的例子中,一个证明返回值 r 确实如此 f r = true .

2 回复 | 直到 6 年前

Anton Trunov 6 年前

我们可以执行这个 myFind 通过对输入列表进行结构递归来执行函数。如果列表为空,则 False_rect 归纳原理是我们的朋友,因为它让我们从逻辑世界转换到计算世界。一般来说,如果在建项的类型存在于 Type ,但如果我们有不一致,系统会允许我们。

我们可以使用 护航模式 (关于StAcExpod解释这个模式有很多很棒的答案)和辅助引理。 find_not_head .

在下面的实现中,我使用了两次护航模式:顶层的模式用于让Coq知道第一个输入列表是空的 match -分支——观察 H 两个分支都不同。

From Coq Require Import List.
Import ListNotations.
Set Implicit Arguments.

(* so we can write `f a` instead of `f a = true` *)
Coercion is_true : bool >-> Sortclass.

Section Find.
Variables (A : Type) (f : A -> bool).

(* auxiliary lemma *)
Fact find_not_head h l : f h = false ->
  (exists a, In a (h :: l) /\ f a) ->
  exists a, In a l /\ f a.
Proof. intros E [a [[contra | H] fa_true]]; [congruence | now exists a]. Qed.

Fixpoint myFind (l : list A) (H : exists a : A, In a l /\ f a) : {r : A | f r} :=
  match l with
  | [] => fun H : exists a : A, In a [] /\ f a =>
           False_rect {r : A | f r} 
                      match H with
                      | ex_intro _ _ (conj contra _) =>
                        match contra with end
                      end
  | h :: l => fun H : exists a : A, In a (h :: l) /\ f a =>
               (if f h as b return (f h = b -> {r : A | f r})
                then fun Efh => exist _ h Efh
                else fun Efh => myFind l (find_not_head Efh H)) eq_refl
  end H.
End Find.

下面是一个简单的测试:

From Coq Require Import Arith.
Section FindTest.
Notation l := [1; 2; 0; 9].
Notation f := (fun n => n =? 0).
Fact H : exists a, In a l /\ f a.
Proof. exists 0; intuition. Qed.

Compute myFind f l H.
(*
     = exist (fun r : nat => f r) 0 eq_refl
     : {r : nat | f r}
*)
End FindTest.

larsr 6 年前

你也可以使用 Program 以帮助您交互地构造证明参数。你在程序中尽可能多地填写,然后离开 _ 你可以用证明策略来填补空白。

Require Import List Program.

Section Find.

  Variable A : Type.
  Variable test : A -> bool.

Program Fixpoint FIND l (H:exists a, test a = true /\ In a l) :  {r | test r = true} :=
  match l with
  | [] => match (_:False) with end
  | a::l' => if dec (test a) then a else FIND l' _
  end.

Next Obligation.
  firstorder; congruence.
Defined.

End Find.

程序 当你做案例分析时(它知道护航模式),不容易忘记信息,但是它并不完美,因此 dec 在 if 陈述。

(注意Coq是如何处理第一个义务的,构造一个类型为 False ,全靠自己!)