2
Require Import Program.
4
Inductive Tree : Set :=
5
| Br : Tree -> Tree -> Tree
9
(* given a tree, we want to know which lists can
10
be used to navigate exactly to a node *)
11
Inductive Exact : Tree -> list bool -> Prop :=
12
| exDone n : Exact (No n) nil
13
| exLeft l r p: Exact l p -> Exact (Br l r) (true::p)
14
| exRight l r p: Exact r p -> Exact (Br l r) (false::p)
17
Definition unreachable A : False -> A.
22
Program Fixpoint fetch t p (x:Exact t p) {struct t} :=
25
| No p' , _::_ => unreachable nat _
26
| Br l r, nil => unreachable nat _
27
| Br l r, true::t => fetch l t _
28
| Br l r, false::t => fetch r t _
31
Next Obligation. inversion x. Qed.
32
Next Obligation. inversion x. Qed.
33
Next Obligation. inversion x; trivial. Qed.
34
Next Obligation. inversion x; trivial. Qed.