From Coq Require Import PArith.

Inductive TNode (A: Type) : Type :=
| TNode001: TNode A -> TNode A
| TNode010: A -> TNode A
| TNode011: A -> TNode A -> TNode A
| TNode100: TNode A -> TNode A
| TNode101: TNode A -> TNode A ->TNode A
| TNode110: TNode A -> A -> TNode A
| TNode111: TNode A -> A -> TNode A -> TNode A.
Arguments TNode001 {A} _.
Arguments TNode010 {A} _.
Arguments TNode011 {A} _ _.
Arguments TNode100 {A} _.
Arguments TNode101 {A} _ _.
Arguments TNode110 {A} _ _.
Arguments TNode111 {A} _ _ _.

Inductive Trie (A: Type): Type :=
| Tempty : Trie A
| Troot: TNode A -> Trie A.
Arguments Tempty {A}.
Arguments Troot {A} _.

Definition trie_builder {A} (l: Trie A) (o: option A) (r: Trie A) : Trie A :=
match l,o,r with
| Tempty, None, Tempty => Tempty
| Tempty, None, Troot r' => Troot (TNode001 r')
| Tempty, Some x, Tempty => Troot (TNode010 x)
| Tempty, Some x, Troot r' => Troot (TNode011 x r')
| Troot l', None, Tempty => Troot (TNode100 l')
| Troot l', None, Troot r' => Troot (TNode101 l' r')
| Troot l', Some x, Tempty => Troot (TNode110 l' x)
| Troot l', Some x, Troot r' => Troot (TNode111 l' x r')
end.
Global Arguments trie_builder: simpl never.

Fixpoint tnode_singleton {A} (p: positive) (a: A) :=
 match p with
| xH => TNode010 a
| xO q => TNode100 (tnode_singleton q a)
| xI q => TNode001 (tnode_singleton q a)
end.

Definition trie_singleton {A} (p: positive) (a: A) := Troot (tnode_singleton p a).
Global Arguments trie_singleton: simpl never.

Fixpoint trie_alter {A} (t: Trie A) (f: option A -> option A) (p: positive)  : Trie A :=
match t with
| Tempty => match f None with
            | None => Tempty
            | Some a => trie_singleton p a
            end
| Troot n =>
    match p, n with
    | xH, TNode001 r => trie_builder Tempty (f None) (Troot r)
    | xH, TNode010 a => trie_builder Tempty (f (Some a)) Tempty
    | xH, TNode011 a r => trie_builder Tempty (f (Some a)) (Troot r)
    | xH, TNode100 l => trie_builder (Troot l) (f None) Tempty
    | xH, TNode101 l r => trie_builder (Troot l) (f None) (Troot r)
    | xH, TNode110 l a => trie_builder (Troot l) (f (Some a)) Tempty
    | xH, TNode111 l a r => trie_builder (Troot l) (f (Some a)) (Troot r)
    | xO q, TNode001 r => trie_builder (trie_alter Tempty f q ) None (Troot r)
    | xO q, TNode010 a => trie_builder (trie_alter Tempty f q ) (Some a) Tempty
    | xO q, TNode011 a r => trie_builder (trie_alter Tempty f q) (Some a) (Troot r)
    | xO q, TNode100 l => trie_builder (trie_alter (Troot l) f q) None Tempty
    | xO q, TNode101 l r => trie_builder (trie_alter (Troot l) f q) None (Troot r)
    | xO q, TNode110 l y => trie_builder (trie_alter (Troot l) f q) (Some y) Tempty
    | xO q, TNode111 l y r => trie_builder (trie_alter (Troot l) f q) (Some y) (Troot r)
    | xI q, TNode001 r => trie_builder Tempty None (trie_alter (Troot r) f q )
    | xI q, TNode010 a => trie_builder Tempty (Some a) (trie_alter Tempty f q)
    | xI q, TNode011 a r => trie_builder Tempty (Some a) (trie_alter (Troot r) f q)
    | xI q, TNode100 l => trie_builder (Troot l) None (trie_alter Tempty f q )
    | xI q, TNode101 l r => trie_builder (Troot l) None (trie_alter (Troot r) f q )
    | xI q, TNode110 l a => trie_builder (Troot l) (Some a) (trie_alter Tempty f q )
    | xI q, TNode111 l a r => trie_builder (Troot l) (Some a) (trie_alter (Troot r) f q )
    end
end.
Arguments trie_alter _ !_/_ _.  (*This line does not really matter, I tried to force unfolding*)
Lemma foo: forall A g p, g None = None -> trie_alter (@ Tempty A) g p  = Tempty.
Proof.
intros. simpl.
Admitted.

match f None with
            | None => Tempty
            | Some a => trie_singleton p a
            end