roosbeef.v

Require Import List.

(* 
   currently I'm only using these letters for sake of simplicity 
   - will expand to full alphabet later 
       (although the amount of available letters ought to be arbitrary)
*)
Inductive letter : Type :=
  a | e | o | u : letter.

(* 
   each letter needs to have an accent to form a 'French letter', see fletter
*)
Inductive accent : Type :=
  acute | grave : accent.

Inductive fletter : Type :=
  FrenchLetter : letter -> accent -> fletter.


(* 
   compare represents the following ordering of letters: a,e > o > u 
   
   used in conjunction with 'highest'
*)
Definition fl_compare (x y : fletter) : comparison :=
  match x, y with
    FrenchLetter a _, FrenchLetter a _ => Eq
  | FrenchLetter e _, FrenchLetter a _ => Eq
  | FrenchLetter o _, FrenchLetter a _ => Lt
  | FrenchLetter u _, FrenchLetter a _ => Lt
  | FrenchLetter a _, FrenchLetter e _ => Eq
  | FrenchLetter e _, FrenchLetter e _ => Eq
  | FrenchLetter o _, FrenchLetter e _ => Lt
  | FrenchLetter u _, FrenchLetter e _ => Lt
  | FrenchLetter a _, FrenchLetter o _ => Gt
  | FrenchLetter e _, FrenchLetter o _ => Gt
  | FrenchLetter o _, FrenchLetter o _ => Eq
  | FrenchLetter u _, FrenchLetter o _ => Lt
  | FrenchLetter a _, FrenchLetter u _ => Gt
  | FrenchLetter e _, FrenchLetter u _ => Gt
  | FrenchLetter o _, FrenchLetter u _ => Gt
  | FrenchLetter u _, FrenchLetter u _ => Eq
  end.


Definition isgreater (c : comparison) : bool :=
  match c with
    Gt => true
  | Eq => false
  | Lt => false
  end.


Definition islesser (c : comparison) : bool :=
  match c with
    Lt => true
  | Gt => false
  | Eq => false
  end.


Definition isequal (c : comparison) : bool :=
  match c with
    Lt => false
  | Gt => false
  | Eq => true
  end.


(*
   help function of 'stratify_sub' 

   'highest' takes a list of letters and returns the maximal letters according to 'compare'
*)
Fixpoint highest (ll : list fletter) (result : list fletter) : list fletter :=
  match ll, result with
    nil, _            => result
  | h1 :: t1, nil     => highest t1 (h1 :: nil)
  | h1 :: t1, h2 :: _ => if (islesser (fl_compare h1 h2))
                           then highest t1 result
                           else if (isequal (fl_compare h1 h2))
                                   then highest t1 (h1 :: result)
                                   else highest t1 (h1 :: nil)
  end.


Definition à     : fletter := FrenchLetter a grave.
Definition á     : fletter := FrenchLetter a acute.
Definition è     : fletter := FrenchLetter e grave.
Definition é     : fletter := FrenchLetter e acute.
Definition ù     : fletter := FrenchLetter u grave.
Definition ú     : fletter := FrenchLetter u acute.
Definition ó     : fletter := FrenchLetter o acute.
Definition ò     : fletter := FrenchLetter o grave.


Eval compute in highest (à :: nil) nil. 
(* should be FrenchLetter a grave :: nil *)


Eval compute in highest (ù :: ú :: ó :: é :: ò :: à :: à :: nil) nil. 
(* should be FrenchLetter o acute :: FrenchLetter o grave :: nil *)

Definition highest' (ll : list fletter) (result : list fletter) : list fletter :=
  fold_right (fun c l =>  
    match l with 
    | nil => c :: nil
    | h :: t => if (islesser (fl_compare c h))
                then h :: t
                else if (isequal (fl_compare c h))
                     then c :: h :: t
                     else c :: nil
    end
  ) nil ll.



Eval compute in highest' (à :: nil) nil. 
Eval compute in highest' (á :: ù :: ú :: ó :: é :: ò :: à :: à :: nil) nil. 
  

Definition highest'' (ll : list fletter) : list fletter :=
  fold_right (fun c l =>  
    match l with 
    | nil => c :: nil
    | h :: _ => match fl_compare c h with
                | Lt => l
                | Eq => c :: l
                | Gt => c :: nil
    end end
  ) nil ll.


Eval compute in highest'' (à :: nil). 
Eval compute in highest'' (ù :: ú :: ó :: é :: ò :: à :: à :: nil). 
Eval compute in highest'' (á :: ù :: ú :: ó :: é :: ò :: à :: à :: nil). 


Lemma help1'':
forall r : list fletter,
  In à (highest'' (à :: r)).
Proof.
  intros.
  simpl. destruct (highest'' r) eqn:E. (* note that i don't actually
                                          use E, i just like to keep
                                          track of complex destructs
                                          explicitly *)
  simpl; tauto.
  destruct f as [c acc]. destruct c; simpl; tauto.
Qed.