Coq 新手：如何在 Coq 中迭代二叉树

如何解决Coq 新手：如何在 Coq 中迭代二叉树

我是 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?