recursion - Coq新手: How to iterate trough binary-tree in 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的证明。至少是这么理解的。

现在我明白了

我不知道也许我离它并不远

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 以查看它选择最左边的那个)。

祝你好运!