GCJ 2012 Qual A

A.v

Require Import Ascii String List Sorting Permutation PermutEq PermutSetoid.

Open Scope char_scope.

Definition trans := ascii -> ascii.

Definition chars : list ascii :=
  Eval compute in map ascii_of_nat (seq 0 256).

Definition smalls : list ascii :=
  Eval compute in map ascii_of_nat (seq (nat_of_ascii "a") (nat_of_ascii "z" - nat_of_ascii "a" + 1)).

Definition isSmallAlpha ch :=
  nat_of_ascii "a" <= nat_of_ascii ch <= nat_of_ascii "z".

Definition googlerese_prop_1 (t : trans) :=
  Permutation chars (map t chars).

Definition googlerese_prop_2 (t : trans) :=
  forall ch, ~isSmallAlpha ch -> t ch = ch.

Definition googlerese_prop_3 (t : trans) :=
  forall ch, isSmallAlpha ch -> isSmallAlpha (t ch).

Fixpoint strToList (s : string) : list ascii :=
  match s with
    | String ch s' => ch :: strToList s'
    | EmtptyString => nil
  end.

Definition hint_1g :=
  Eval compute in strToList "ejp mysljylc kd kxveddknmc re jsicpdrysi"%string.

Definition hint_1e :=
  Eval compute in strToList "our language is impossible to understand"%string.

Definition hint_2g :=
  Eval compute in strToList "rbcpc ypc rtcsra dkh wyfrepkym veddknkmkrkcd"%string.

Definition hint_2e :=
  Eval compute in strToList "there are twenty six factorial possibilities"%string.

Definition hint_3g :=
  Eval compute in strToList "de kr kd eoya kw aej tysr re ujdr lkgc jv"%string.

Definition hint_3e :=
  Eval compute in strToList "so it is okay if you want to just give up"%string.

Definition hint_4g :=
  Eval compute in strToList "y qee"%string.

Definition hint_4e :=
  Eval compute in strToList "a zoo"%string.

Definition hints (t : trans) :=
  map t hint_1e = hint_1g /\
  map t hint_2e = hint_2g /\
  map t hint_3e = hint_3g /\
  map t hint_4e = hint_4g.

Definition googlerese_t : { t : trans |
  hints t /\
  googlerese_prop_1 t}.
Proof.
eexists (fun ch =>
  match ch with
    | "a" => _  | "b" => _  | "c" => _  | "d" => _
    | "e" => _  | "f" => _  | "g" => _  | "h" => _
    | "i" => _  | "j" => _  | "k" => _  | "l" => _
    | "m" => _  | "n" => _  | "o" => _  | "p" => _
    | "q" => _  | "r" => _  | "s" => _  | "t" => _
    | "u" => _  | "v" => _  | "w" => _  | "x" => _
    | "y" => _  | "z" => _
    | _ => ch
  end).
split.
  compute.
  split; [reflexivity|].
  split; [reflexivity|].
  split; reflexivity.
Existential 1 := "z".
unfold googlerese_prop_1, chars.
simpl.
repeat constructor.
eapply Permutation_trans.
apply Permutation_rev.
apply Permutation_sym.
eapply Permutation_trans.
apply Permutation_rev.
simpl.
repeat constructor.
apply (Permutation_cons_app (strToList "zyxwvutsr") (strToList "ponmlkjihgfedcba") "q").
apply (Permutation_cons_app (strToList "zyxwvutsrponmlkjihgfedcb") (strToList "") "a").
apply (Permutation_cons_app (strToList "zyxwvutsrponmlkji") (strToList "gfedcb") "h").
apply (Permutation_cons_app (strToList "zyxwvu") (strToList "srponmlkjigfedcb") "t").
apply (Permutation_cons_app (strToList "zyxwvusrponmlkji") (strToList "fedcb") "g").
apply (Permutation_cons_app (strToList "zyxwvusrponmlk") (strToList "ifedcb") "j").
apply (Permutation_cons_app (strToList "zyxwvus") (strToList "ponmlkifedcb") "r").
apply (Permutation_cons_app (strToList "zyxwvusponmlkife") (strToList "cb") "d").
apply (Permutation_cons_app (strToList "zyxwvus") (strToList "onmlkifecb") "p").
apply (Permutation_cons_app (strToList "") (strToList "yxwvusonmlkifecb") "z").
apply (Permutation_cons_app (strToList "yxw") (strToList "usonmlkifecb") "v").
apply (Permutation_cons_app (strToList "yxwusonmlkif") (strToList "cb") "e").
apply (Permutation_cons_app (strToList "yxwu") (strToList "onmlkifcb") "s").
apply (Permutation_cons_app (strToList "y") (strToList "wuonmlkifcb") "x").
apply (Permutation_cons_app (strToList "ywuon") (strToList "lkifcb") "m").
apply (Permutation_cons_app (strToList "ywu") (strToList "nlkifcb") "o").
apply (Permutation_cons_app (strToList "yw") (strToList "nlkifcb") "u").
apply (Permutation_cons_app (strToList "ywnl") (strToList "ifcb") "k").
apply (Permutation_cons_app (strToList "ywnlifc") (strToList "") "b").
apply (Permutation_cons_app (strToList "ywn") (strToList "ifc") "l").
apply (Permutation_cons_app (strToList "y") (strToList "nifc") "w").
apply (Permutation_cons_app (strToList "ynif") (strToList "") "c").
apply (Permutation_cons_app (strToList "yn") (strToList "f") "i").
apply (Permutation_cons_app (strToList "yn") (strToList "") "f").
apply (Permutation_cons_app (strToList "y") (strToList "") "n").
auto.
Defined.

Definition tr_string :=
  Eval compute in map (proj1_sig googlerese_t) smalls.

Lemma tr_s : tr_string = strToList "ynficwlbkuomxsevzpdrjgthaq".
Proof.
  reflexivity.
Qed.

(*
 * exec this!
 *
tail -n +2 | tr ynficwlbkuomxsevzpdrjgthaq a-z | awk '{printf "Case #%d: %s\n", NR, $0}'
 *
 *)