Coq 新手：如何在 Coq 中遍历二叉树

Question

我是 coq 的新手，需要抓取一个位于二叉树叶子上且满足 P 的元素

Variable A : Set.
Variable P : A -> Prop.
Variable P_dec : forall x : A, {P x} + {~ P x}.

Inductive PTree : nat -> Set :=
  | PLeafTrue : forall (n : nat) (a : A), P a -> PTree 1
  | PLeafFalse : forall (n : nat), A -> PTree 0
  | PNode   : forall (n m : nat), PTree n -> PTree m -> PTree (n + m).

因此我需要sig P ，它应该是元素和它满足P 的证明。至少是这样理解的。

现在我得到了这个

Idk 也许我离它并没有那么远

Definition grabType n : Type :=
    match n with
    | O => unit
    | S _ => sig P
    end.


Definition grab : forall n (t : PTree (S n)), sig P :=
    fix grab n (t : PTree(S n)) : sig P :=
      match t in PTree n' return grabType n'
      with
      | PLeafFalse _ a => tt
      | PLeafTrue _ a pf => exist _ a pf
      | PNode x y l r => match x, y return PTree (plus x y) -> grabType (plus x y)
                         with
                         | O, O => fun _ => tt
                         | O, S _ => fun r' => grab _ r'
                         | S _ , O => fun l' => grab _ l'
                         | S _, S _ => fun l' => grab _ l'
                         end
      end.

但我得到了错误：

In environment
A : Set
P : A -> Prop
P_dec : forall x : A, {P x} + {~ P x}
grab : forall n : nat, PTree (S n) -> {x : A | P x}
n : nat
t : PTree (S n)
x : nat
y : nat
l : PTree x
r : PTree y
The term
 "match x return (PTree (x + y) -> grabType (x + y)) with
  | 0 =>
      match y return (PTree (0 + y) -> grabType (0 + y)) with
      | 0 => fun _ : PTree (0 + 0) => tt
      | S n0 => fun r' : PTree (0 + S n0) => grab n0 r'
      end
  | S n0 =>
      match
        y return (PTree (S n0 + y) -> grabType (S n0 + y))
      with
      | 0 =>
          fun l' : PTree (S n0 + 0) =>
          grab
            ((fix add (n m : nat) {struct n} : nat :=
                match n with
                | 0 => m
                | S p => S (add p m)
                end) n0 0) l'
      | S n1 =>
          fun l' : PTree (S n0 + S n1) =>
          grab
            ((fix add (n m : nat) {struct n} : nat :=
                match n with
                | 0 => m
                | S p => S (add p m)
                end) n0 (S n1)) l'
      end
  end" has type "PTree (x + y) -> grabType (x + y)"
while it is expected to have type "grabType (x + y)".

'''

Can this be solved?

I found some Post saying somthing like ``end r`` could be the answer.

But which combination or is there something else i missed?

Answer 1

我不确定您要实现什么，但可以构建一个函数grab : forall n : nat, PTree (S n) -> {x : A | P x}。当我有 sig 变量时，我喜欢使用 Coq 的特性，它允许您以证明模式构建程序（参见 https://coq.inria.fr/refman/language/core/definitions.html#assertions-and-proofs）。如果你打算执行你得到的函数，你必须小心不要使用任何不透明的结果。

这会给：

Fixpoint grab n (t: PTree (S n)) {struct t} : sig P.
Proof.
  inversion t.
  + subst. exists a. assumption.
  + destruct n0.
    ++ simpl in H. rewrite H in H1. apply (grab n H1).
    ++ apply (grab n0 H0).
Defined.

有一个工作示例：

Variable a b c: A.
Variable a_correct: P a.
Variable b_correct: P b.
Eval compute in
    grab 1 (
           PNode 0 2
                 (PLeafFalse 1 c)
                 (PNode 1 1
                        (PLeafTrue 42 a a_correct)
                        (PNode 0 1
                               (PLeafFalse 42 b)
                               (PLeafTrue 43 b b_correct)))
         ).

（你可以交换a 和b 看看它选择了最左边的那个）。

祝你好运！