- Definition arrange_empty_tree : forall {T}{A}(q:Tree A)(t:Tree ??T),
- t = mapTree (fun _:A => None) q ->
- Arrange t [].
- intros T A q.
- induction q; intros.
- simpl in H.
- rewrite H.
- apply RId.
- simpl in *.
- destruct t; try destruct o; inversion H.
- set (IHq1 _ H1) as x1.
- set (IHq2 _ H2) as x2.
- eapply RComp.
- eapply RRight.
- rewrite <- H1.
- apply x1.
- eapply RComp.
- apply RCanL.
- rewrite <- H2.
- apply x2.
- Defined.
-
-(* Definition unarrange_empty_tree : forall {T}{A}(t:Tree ??T)(q:Tree A),
- t = mapTree (fun _:A => None) q ->
- Arrange [] t.
- Defined.*)
-
- Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
- sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
- intro T.
- refine (fix foo t :=
- match t with
- | T_Leaf x => _
- | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
- end).
- intros.
- destruct x.
- right; apply tt.
- left.
- exists (T_Leaf tt).
- auto.
- destruct b1'.
- destruct b2'.
- destruct s.
- destruct s0.
- subst.
- left.
- exists (x,,x0).
- reflexivity.
- right; auto.
- right; auto.
- Defined.
-