Require Import List.
Require Import Bool.

Set Implicit Arguments.
Unset Strict Implicit.

Section LETTER_DEF.

Inductive letter : Set :=
  | A : letter
  | B : letter
  | C : letter
  | D : letter
  | E : letter
  | F : letter
  | G : letter
  | H : letter
  | I : letter
  | J : letter
  | K : letter
  | L : letter
  | M : letter
  | N : letter
      
  | P : letter
  | Q : letter
  | R : letter
      
  | T : letter
  | U : letter
  | V : letter
  | W : letter
  | X : letter
  | Y : letter
  | Z : letter.

Definition eq_letter (l1 l2 : letter) : bool :=
  match l1, l2 with
  | A, A => true
  | B, B => true
  | C, C => true
  | D, D => true
  | E, E => true
  | F, F => true
  | G, G => true
  | H, H => true
  | I, I => true
  | J, J => true
  | K, K => true
  | L, L => true
  | M, M => true
  | LETTER_DEF.N, LETTER_DEF.N => true
      
  | P, P => true
  | Q, Q => true
  | R, R => true
      
  | T, T => true
  | U, U => true
  | V, V => true
  | W, W => true
  | X, X => true
  | Y, Y => true
  | Z, Z => true
  | _, _ => false
  end.

End LETTER_DEF.

Section STRING_DEF.

Definition string := list letter.

Definition voidstring : string := nil.

Fixpoint eq_string (str1 str2 : string) {struct str2} : bool :=
  match str1, str2 with
  | nil, nil => true
  | l1 :: str11, l2 :: str21 =>
      if eq_letter l1 l2 then eq_string str11 str21 else false
  | _, _ => false
  end.

Fixpoint prefix_string (target prefix : string) {struct prefix} : bool :=
  match target, prefix with
  | nil, nil => true
  | l1 :: str1, l2 :: str2 =>
      if eq_letter l1 l2 then prefix_string str1 str2 else false
  | _, _ => false
  end.

Fixpoint extract_string (target prefix : string) {struct prefix} : string :=
  match target, prefix with
  | _, nil => target
  | l1 :: str1, l2 :: str2 =>
      if eq_letter l1 l2 then extract_string str1 str2 else voidstring
  | nil, l2 :: str2 => voidstring
  end.

End STRING_DEF.