Saulo.v

Set Implicit Arguments.
Set Asymmetric Patterns.

Section Sequence.

Variable E: Set.

Inductive Sequence: nat -> Set :=
  | SequenceLeaf: E -> E -> Sequence 0
  | SequenceNode: forall n, Sequence n -> Sequence n -> Sequence (S n).

Definition Sequence_case0 (P : Sequence 0 -> Set) : (forall x y, P (SequenceLeaf x y)) -> forall l, P l.
  intros H l.
  revert P H.
  refine match l with
         | SequenceLeaf x y => fun P H => (H x y)
         | SequenceNode _ _ _ => I
         end.
Defined.
  
Definition Sequence_caseS n (P : Sequence (S n) -> Set) : (forall l r, P (SequenceNode l r)) -> forall l, P l.
  intros H l.
  revert P H.
  refine match l with 
         | SequenceLeaf _ _ => I
         | SequenceNode _ x y => fun P H => H x y
         end.
Defined.

Inductive List: nat -> Set :=
  | ListLeaf: E -> List 0
  | ListNode: forall n, E -> List n -> List (S n).

Definition List_case0 (P : List 0 -> Set) : (forall x, P (ListLeaf x)) -> forall l, P l.
  intros H l.
  revert P H.
  refine match l with
         | ListLeaf x => fun P H => (H x)
         | ListNode _ _ _ => I
         end.
Defined.
  
Definition List_caseS n (P : List (S n) -> Set) : (forall l r, P (ListNode l r)) -> forall l, P l.
  intros H l.
  revert P H.
  refine match l with 
         | ListLeaf  _ => I
         | ListNode _ x y => fun P H => H x y
         end.
Defined.
End Sequence.

Inductive Digit := 
  | D0
  | D1.

Fixpoint get E n (t: Sequence E n) :  List Digit n -> E :=
  match t with
  | SequenceLeaf e0 e1 => List_case0 _ (fun x => match x with
                                             | D0 => e0
                                             | D1 => e1
                                             end)
  | SequenceNode e l r => List_caseS _ (fun d l' => match d with
                                                | D0 => get l l'
                                                | D1 => get r l'
                                                end)
  end.