Coq Newbie: How to iterate trough binary-tree in Coq

Question

I'm new to coq and need to grab a element that is at a leaf of this binary tree and satisfys 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).

As result i need sig P which should be the element and the proof that it satisfys P. At least that is how understood it.

Now I got this

Idk Maybe I'm not this far away from it

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.

But I get the error:

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?

user_13155817 · Answer

I'm not exactly sure what you are trying to achieve, but building a function grab : forall n : nat, PTree (S n) -> {x : A | P x} can be done. When I have sig variables, I like to use the feature of Coq that allows you to build programs in proof mode (see https://coq.inria.fr/refman/language/core/definitions.html#assertions-and-proofs). If you plan to execute the function you get, you have to be careful not to use any opaque result.

This would give :

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.

With a working example :

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)))
         ).

(you can swap a and b to see that it picks the leftmost one).

Good luck !

Coq Newbie: How to iterate trough binary-tree in Coq

1 Answers