问题描述
我正在处理 coq，我正在尝试创建一个函数，该函数可用于在列表中查找某些内容并返回与之相关的证明，证明指定的元素在列表中。
就我而言，我有一个元组列表，我想根据元组的第一个元素进行查找。
所以首先我定义了一个 {
"total": 9,"rows": [
{
"id": 0,"name": "jersey","birthday": "01.05.1995","college": "NEU"
},{
"id": 1,{
"id": 2,{
"id": 3,{
"id": 4,{
"id": 5,{
"id": 6,{
"id": 7,{
"id": 8,{
"id": 9,"college": "NEU"
}
]
}
归纳谓词来证明一个元素在列表中。这有两种情况。元素要么在列表的头部，要么在尾部。
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.
函数，该函数给出了一个元组列表、一个第一个元素和一个相等谓词，返回 None 或 Some 以及查找的元素和该元素在列表中的证明。
lookup上面写的方式编译得很好。但我不知道如何使用列表 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 的第三个参数中尝试了诸如模式匹配之类的各种方法，但我永远无法让它工作。
感谢任何帮助！
解决方法
首先，像这样写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,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 可以做得比仅仅返回一个 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.
在递归调用中对 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.
库中已经有一个谓词 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 策略处理的。