如何模式匹配存在以转换证明

Question

我正在使用 coq，我正在尝试创建一个函数，该函数可用于在列表中查找某些内容，并且 return 与之相关联的证明指定的元素在列表中.

在我的例子中，我有一个元组列表，我想根据元组的第一个元素进行查找。

所以首先我定义了一个 assoc 归纳谓词来证明一个元素在列表中。这有两种情况。元素要么在列表的头部，要么在列表的尾部。

Inductive assoc (A : Set) (B : Set) : list (A * B) -> A -> B -> Prop :=
  | assocHead : forall (l : list (A * B)) (a : A) (b : B), assoc A B (cons (a,b) l) a b
  | assocTail : forall (l : list (A * B)) (a x : A) (b y : B), assoc A B l a b -> assoc A B ((x,y) :: l) a b.

然后我定义了一个 lookup 函数，它给出了一个元组列表、第一个元素和一个相等谓词 returns None 或 Some 以及查找的元素和一个证明该元素在列表中。

Program Fixpoint lookup
  (A : Set)
  (B : Set)
  (dec : (forall x y : A, {x = y} + {x <> y}))
  (l : list (A * B))
  (a : A)
  {struct l}
  : option {b : B | assoc A B l a b}
:= match l with
   | [] => None
   | (pair v t) :: tl => if dec v a
                           then (Some (exist (assoc A B ((pair v t) :: tl) a) t (assocHead A B tl a t)))
                           else match (lookup A B dec tl a) with
                           -- In the case below we have proven it's in the
                           -- tail of the list.
                           -- How to use that to create new proof with assocTail?
                           | Some (exist _ _ _) => None
                           | None => None
                           end
   end.

上面的写法编译得很好。但是我不知道如何使用列表 tl 中的证明来创建它在总列表中的新证明。我在 exist 的第三个参数中尝试了各种模式匹配，但我永远无法让它工作。

感谢任何帮助！

Answer 1

通过递归调用对 exist 对进行模式匹配后，您知道该对的第一个组件也是结果的第一个组件。然后第二部分是您可以作为单独义务填写的证明。

match lookup ... with
| Some (exist _ b _) => Some (exist _ b _ (* this underscore becomes an obligation *))
| None => None
end

这允许 Program Definition 命令完成，然后你必须证明一个义务（引理）来实际完成该定义。请务必使用 Defined 而不是 Qed 终止证明，因为防护检查器不知何故需要您的证明是透明的。

Next Obligation.
  (* finish the proof *)
Defined.

Program Fixpoint lookup
  (A : Set)
  (B : Set)
  (dec : (forall x y : A, {x = y} + {x <> y}))
  (l : list (A * B))
  (a : A)
  {struct l}
  : option {b : B | assoc A B l a b}
:= match l with
   | [] => None
   | (pair v t) :: tl =>
     if dec v a
     then (Some (exist (assoc A B ((pair v t) :: tl) a) t (assocHead A B tl a t)))
     else match (lookup A B dec tl a) with
          | Some (exist _ b _) => Some (exist _ b _)
          | None => None
          end
   end.

Next Obligation.
  apply assocTail.
  assumption.
Defined.

Answer 2

首先，这样写assoc可能更好

Inductive assoc {A B : Type} (k : A) (v : B) : list (A * B) -> Prop :=
| assoc_head : forall l, assoc k v ((k, v) :: l)
| assoc_tail : forall l x, assoc k v l -> assoc k v (x :: l).
Arguments assoc_head {A B} {k v}, {A B} k v, A B k v.
Arguments assoc_tail {A B} {k v} {l}, {A B} {k v} l, {A B} k v l, A B k v l.

基本上，:左边可以放的东西越多，处理类型就越容易（参数越多，索引越少）。我实际上会更进一步写

Inductive elem {A : Type} (x : A) : list A -> Prop :=
| in_here : forall l, elem x (x :: l)
| in_there : forall l y, elem x l -> elem x (y :: l).
Definition assoc {A B : Type} (k : A) (v : B) l := elem (k, v) l.

但这正在偏离轨道。

无论如何，您不需要在代码中检查 exists 的第三个参数。你给assoc_tail就可以了。完成。

#[program] Fixpoint lookup
  {A B : Type} (dec : forall x y : A, {x = y} + {x <> y})
  (l : list (A * B)) (k : A) {struct l}
: option {v : B | assoc k v l}
:=
  match l with
  | [] => None
  | (k', v') as h :: l =>
    if dec k' k (* writing the first argument to exist is usually just clutter *)
      then Some (exist _ v' (assoc_head k' v' l))
      else
        match lookup dec l k with
        | Some (exist _ v prf) => Some (exist _ v (assoc_tail h prf))
        | None => None
        end
  end.

请注意 Program 的部分神奇之处在于它应该让您编写实际的程序而无需首先担心证明部分。特别是，你应该想象像 x : {v : B | assoc k v l} 这样的精化类型的值只是 x : B，然后精化的证明部分稍后处理。

#[program] Fixpoint lookup
  {A B : Type} (dec : forall x y : A, {x = y} + {x <> y})
  (l : list (A * B)) (k : A) {struct l}
: option {v : B | assoc k v l}
:=
  match l with
  | [] => None
  | (k', v') :: l =>
    if dec k' k
      then Some v'
      else
        match lookup dec l k with (* looks weird but is still necessary *)
        | Some v => Some v
        | None => None
        end
  end.
Solve Obligations with program_simpl; now constructor.

在这一点上，lookup 比 return 和 option!

做得更好

#[local] Hint Constructors assoc : core.
#[local] Unset Program Cases.

#[program] Fixpoint lookup
  {A B : Type} (dec : forall x y : A, {x = y} + {x <> y})
  (l : list (A * B)) (k : A) {struct l}
: {v : B | assoc k v l} + {~exists v : B, assoc k v l}
:=
  match l with
  | [] => inright _ (* Underscores as an "escape hatch" to an obligation *)
  | (k', v') :: l =>
    if dec k' k
      then inleft v'
      else
        match lookup dec l k with
        | inleft v => inleft v
        | inright no => inright _
        end
  end.
Next Obligation.
  intros [v no].
  inversion no.
Qed.
Next Obligation.
  intros [v nono].
  inversion nono as [? | ? ? nono']; eauto.
Qed.

Answer 3

库中已经有谓词 In 指定列表是否包含元素，因此您真的不需要定义新的 assoc 谓词。

你可以尝试使用 refine 策略，我发现这对逐步建立术语很有帮助。这有点像使用 Program 但感觉不那么神奇。您尽可能多地编写术语（即 destruct 将生成的匹配语句），并在 _ 中放置您想要获得证明义务的地方。您可以对义务使用证明策略，看看您建立了什么样的术语。这可能很有启发性。

我完成了这个程序：

Require Import List.

Fixpoint lookup {A B} (dec: forall (a a':A), {a=a'}+{a<>a'})
         (l:list (A*B)) (a:A) {struct l} : option {b | In (a,b) l}.
  refine (
      match l with
      | nil => None
      | cons (a',b) l' =>
        match dec a a' with
        | left _ y => Some (exist _ b (or_introl _))
        | right _ y  =>
          match lookup _ _ dec l' a with
          | None => None
          | Some (exist _ b' H') => Some (exist _ b' (or_intror H'))
          end
        end
      end).
  congruence.
Defined.

请注意，出于教学原因，我在术语中留下了一个 _，这是用 congruence 策略处理的。

如何模式匹配存在以转换证明

How to pattern match exist to transform proofs

recursion

pattern-matching

coq

coq-tactic