(*B  {section 2|The {t|sumbool} Type} B*)
(*B

It is defined in the
{link http://coq.inria.fr/stdlib/Coq.Init.Specif.html#
|Specif} module.
{t|sumbool}
{i|{q '|is a boolean type equipped with the justification of their value}:}
[coq[
Inductive sumbool (A B:Prop) : Set :=
  | left : A -> {A} + {B}
  | right : B -> {A} + {B}
 where "{ A } + { B }" := (sumbool A B) : type_scope.

Add Printing If sumbool.
]coq]
Indeed, like {t|bool} and 
{link http://coq.inria.fr/refman/Reference-Manual004.html#toc15
|many other 2-constructors}
types it can use
the {q|{t|if ... then ... else ...}} construct; with the
{link http://coq.inria.fr/refman/Reference-Manual004.html#@command42
|Add Printing If} it is also printed this way.
{p}

It is used everywhere in Coq's standard library.
Just by {i|importing} standard lists, we get quite a bunch of decision
procedures:
B*)
Set Implicit Arguments.
Require Import List.
SearchAbout sumbool.
(*B The search gives about 100 lines of output. B*)
(*B Let's have a closer look at one of them: B*)
Check Compare_dec.zerop.
(*B {code}
Compare_dec.zerop
     : forall n : nat, {n = 0} + {0 < n}
{end}
We can use it in programs:
B*)
Eval compute in (if Compare_dec.zerop 42 then 51 else 69).
(*B {code}
= 69
: nat
{end}
and extraction works as expected:
B*)
Extraction Compare_dec.zerop.
(*B [caml[
(** val zerop : nat -> sumbool **)

let zerop = function
| O -> Left
| S n0 -> Right
]caml] {p}
Note that it can be made more practical:
B*)
Extract Inductive sumbool => "bool" ["true" "false"].
Extraction Compare_dec.zerop.
(*B [caml[
(** val zerop : nat -> bool **)

let zerop = function
| O -> true
| S n0 -> false
]caml] {p}
 B*)

(*B In proofs, {t|sumbool} gives us something {i|more}: the {q|justifications}.
 Let's compare it with this classical {t|bool} version: B*)
Definition bool_zerop (n : nat) :=
  match n with
    | O => true
    | S _ => false
  end.
(*B If we are proving something (even stupid): B*)
Goal  (if (Compare_dec.zerop 42) then 51 else 69) = 69.
Proof.
  destruct (Compare_dec.zerop 42).
  (*B There, we have a {i|hypothesis} in the context (i.e. as
     a Prop with Coq's default {q|{t|=}}):
{code}
  e : 42 = 0
  ============================
   51 = 69
{end} So, that's easy. B*)
  inversion e. 
  reflexivity.
  (* Proof completed. *)
Qed.
(*B Whereas with {t|bool_zerop}: B*)
Goal  (if (bool_zerop 42) then 51 else 69) = 69.
Proof.
 destruct (bool_zerop 42).
 (*B  we don't have {i|the knowledge}:
{code}  
  ============================
   51 = 69
{end} It is not impossible (requires a {t|remember}, and then a few
theorems) but much more tedious. B*)
Abort.

(*B 
{p}
Before going further, let's add a few notations: B*)
Notation "'Decide_left'" := (left _ _).
Notation "'Decide_right'" := (right _ _).
Notation "'Decide_with' x" :=
  (if x then Decide_left else Decide_right) (at level 42).

(*B   

{section 2|A Schoolbook Example}

The common example is the decision about equality of natural numbers
{t|eq_nat_dec} (also explained in
{link http://adam.chlipala.net/cpdt/html/Subset.html |CPDT}).
The {i|fixpoint} just compares the numbers like {i|anyone} would do.
All the goals generated by {t|refine} are equalities and non-equalities,
they can be solved by the
{link http://coq.inria.fr/refman/Reference-Manual011.html#@tactic164
|congruence} tactic which {i|{q '|is a decision procedure for ground
equalities with uninterpreted symbols}}.
 B*)
Definition eq_nat_dec : forall n m : nat, {n = m} + {n <> m}.
  refine (fix f (n m : nat) : {n = m} + {n <> m} :=
    match n, m with
      | O, O => Decide_left
      | S n', S m' => Decide_with (f n' m')
      | _, _ => Decide_right
    end); congruence. 
Defined.
(*B  {p}
Let's make a few tests: B*)
Eval compute in eq_nat_dec 42 42.
(*B {code}
= Decide_left
: {42 = 42} + {42 <> 42}
{end} B*)
Eval compute in eq_nat_dec 42 51.
(*B {code}
= Decide_right
: {42 = 51} + {42 <> 51}
{end} B*)
(*B and have a look at some OCaml code: B*)
Extract Inductive sumbool => "bool" ["true" "false"].
Extraction eq_nat_dec.
(*B [caml[
(** val eq_nat_dec : nat -> nat -> bool **)

let rec eq_nat_dec n m =
  match n with
  | O ->
    (match m with
     | O -> true
     | S n0 -> false)
  | S n' ->
    (match m with
     | O -> false
     | S m' -> eq_nat_dec n' m')
]caml] {p}
 B*)

(*B  {p}
For automatically dealing with this kind of functions,
there is a tactic called
{t|{link http://coq.inria.fr/refman/Reference-Manual011.html#@tactic119
|decide equality}}. It solves
{i|{q '|a goal of the form {t|{text}forall x y:R, {x=y}+{~x=y}{end}},
where {t|R} is an inductive type such that its constructors do not
take proofs or functions as arguments, nor objects in dependent
types}}: B*)
Definition eq_nat_autodec (n m : nat) : {n = m} + {n <> m}.
  decide equality.
Defined.
(*B In this case, the code is as beautiful as before: B*)
Extraction eq_nat_autodec.
(*B [caml[
(** val eq_nat_autodec : nat -> nat -> bool **)

let rec eq_nat_autodec n m0 =
  match n with
  | O ->
    (match m0 with
     | O -> true
     | S n0 -> false)
  | S n0 ->
    (match m0 with
     | O -> false
     | S n1 -> eq_nat_autodec n0 n1)
]caml]
 B*)

(*B  {section 2|Decisions on Character Strings} B*)

(*B Let's try to do something with the {t|sumbool} type{~}{...}
 In the same time, we start exploring some stuff from the
 standard library:
{link http://coq.inria.fr/stdlib/Coq.Strings.Ascii.html |Ascii} and
{link http://coq.inria.fr/stdlib/Coq.Strings.String.html |String}.
 B*)
Require Import Ascii String.
(*B It gives us [coq[
Inductive string : Set :=
  | EmptyString : string
  | String : ascii -> string -> string.
]coq]
where B*)
(*B [coq[
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
Definition zero := 
  Ascii false false false false false false false false.
Definition one :=
  Ascii true false false false false false false false.
]coq]
So, strings here are lists of 8-bits integers, lower bits on the left.
B*)

(*B
{section 3|The String Equality}

Let's write {t|string_eq_dec}, the equality between strings,
 using the lower-lever {t|ascii_dec}:
 B*)
Check ascii_dec.
(*B {code}
ascii_dec
     : forall a b : ascii, {a = b} + {a <> b}
{end}
 B*)
Definition string_eq_dec: 
  forall sa sb : string, { sa = sb } + { sa <> sb }.
refine (fix frec (sa sb : string): 
              { sa = sb } + { sa <> sb } :=
  match sa with
    | EmptyString =>
      match sb with
        | EmptyString => Decide_left
        | String _ _ => Decide_right
      end
    | String ch_a tl_a => 
      match sb with
        | EmptyString => Decide_right
        | String ch_b tl_b => 
          if ascii_dec ch_a ch_b 
          then Decide_with (frec tl_a tl_b)
          else Decide_right         
      end
  end); congruence.
Defined.
(*B {p}
 Here one single {t|decide equality} does not seem to be enough, but
repeating it gives {i|something}: B*)
Definition string_eq_autodec:
  forall sa sb : string, { sa = sb } + { sa <> sb }.
repeat decide equality.
Defined.
(*B The problem is that the {t|repeat} goes too far {i|inside} the
Ascii characters.
 B*)
Extraction string_eq_autodec.
(*B It gives an ugly piece of code comparing every single bit of Ascii
character:
[caml[
(** val string_eq_autodec : string -> string -> bool **)

let rec string_eq_autodec s sb0 =
  match s with
  | EmptyString ->
    (match sb0 with
     | EmptyString -> true
     | String (a, s0) -> false)
  | String (a, s0) ->
    (match sb0 with
     | EmptyString -> false
     | String (a0, s1) ->
       let Ascii (x, x0, x1, x2, x3, x4, x5, x6) = a in
       let Ascii (b7, b8, b9, b10, b11, b12, b13, b14) = a0 in
       (match x with
        | True ->
          (match b7 with
           | True ->
             (match x0 with
              | True ->
              
                  (* ... hundreds of lines ... *)
]caml] {p}

The {i|hand-written} one looks much better: B*)
Extraction string_eq_dec.
(*B [caml[
(** val string_eq_dec : string -> string -> bool **)

let rec string_eq_dec sa sb =
  match sa with
  | EmptyString ->
    (match sb with
     | EmptyString -> true
     | String (a, s) -> false)
  | String (ch_a, tl_a) ->
    (match sb with
     | EmptyString -> false
     | String (ch_b, tl_b) ->
       if ascii_dec ch_a ch_b then
         string_eq_dec tl_a tl_b
       else
         false)
]caml]
 B*)

(*B {section 3|Lexicographic Order} B*)

(*B We now try to specify and implement the lexicographic order
on strings. {p}

{section 4|Specification}
For the order  on Ascii characters, 
we will use {t|nat_of_ascii} and then the order on naturals.
There are a few theorems on that embedding: B*)
Check ascii_nat_embedding.
(*B {code}
ascii_nat_embedding
     : forall a : ascii, ascii_of_nat (nat_of_ascii a) = a
{end}
 B*)
Check nat_ascii_embedding.
(*B {code}
nat_ascii_embedding
     : forall n : nat,
         n < 256 -> nat_of_ascii (ascii_of_nat n) = n
{end}
 B*)

(*B  {p}
We first specify what it {i|means} for 2 strings to be in
lexicographic order. B*)
Inductive in_lex_order: string -> string -> Prop :=
| lexord_empty_strings:   (* "" <= "" *)
  in_lex_order EmptyString EmptyString
| lexord_chars_different:  (* "A..." <= "B..." *)
  forall (c1 c2: ascii) (s1 s2: string),
    nat_of_ascii c1 < nat_of_ascii c2 ->
    in_lex_order (String c1 s1) (String c2 s2)
| lexord_chars_equal:     (* s1 <= s2  ->   As1 <= As2 *)
  forall (c: ascii) (s1 s2: string),
    in_lex_order s1 s2 ->
    in_lex_order (String c s1) (String c s2)
| lexord_string_shorter: (* "aaa" <= "aaaaa" *)
  forall s, in_lex_order EmptyString s.
(*B  {p}
We add the 4 constructors to {t|auto}'s database. B*)
Hint Constructors in_lex_order.
(*B  {p}
Let's check it with a few examples{note|Of course, it is by doing the
examples that I got the inductive definition right little by
little{~};)}{~}{...}
 B*)
Example ex_lex_01: in_lex_order "AAA" "AAB".
Proof. auto. Qed.
Example ex_lex_02: in_lex_order "AAA" "AAA".
Proof. auto. Qed.
(*B {t|ex_lex_03} made me fight a bit. Here is the first version: B*)
Example ex_lex_03: ~ in_lex_order "AAB" "AAA".
Proof. unfold not. intros.
  Time repeat match goal with
                H: in_lex_order _ _ |- _ => 
                  inversion H; clear H
              end;
  repeat match goal with
           H: nat_of_ascii _ < nat_of_ascii _ |- _ =>
             compute in H 
         end;
  repeat match goal with
           H: S _ <=  _ |- _ => 
             inversion H; clear H; subst
         end.
  (* Proof Completed. *)
(*B After forcing the unfolding of {t|not},
   {begin list}
   {*} we invert all the hypotheses using our inductive proposition;
   {*} we force the computation of the {t|nat_of_ascii} functions;
   {*} we invert the ({i|false}) inequalities.
   {end}
We use
{link http://coq.inria.fr/refman/Reference-Manual009.html#@command156 |Time}
to see that this makes {i|a lot} of steps:  
{code}
Proof completed.
Finished transaction in 1. secs (0.u,1.71174s)
{end}
The type-checking of the proof gets even worse:
 B*)
Time Qed.
(*B {code}
ex_lex_03 is defined
Finished transaction in 8. secs (6.997937u,0.046993s)
{end}
B*)
(*B  {p}
The problem is the last repeated step, on the inequalities.
Just remember, when we play with naturals, {t|omega} is our friend. B*)
Require Import Omega.
Example ex_lex_03': ~ in_lex_order "AAB" "AAA".
Proof.
  unfold not; intros.
  repeat match goal with
           H: in_lex_order _ _ |- _ => 
             inversion H; clear H
         end;
  repeat match goal with
           H: nat_of_ascii _ < nat_of_ascii _ |- _ => 
             compute in H
         end;
  match goal with H: S _ <=  _ |- _ => omega end.
Time Qed.
(*B {code}
ex_lex_03' is defined
Finished transaction in 0. secs (0.040994u,0.s)
{end}
 B*)
Example ex_lex_04: in_lex_order "AAA" "AAAA".
Proof. auto. Qed.
(*B {t|ex_lex_05} works like {t|ex_lex_03}: B*)
Example ex_lex_05: ~ in_lex_order "AAAA" "AAA".
Proof. unfold not. intros. 
  repeat match goal with
           H: in_lex_order _ _ |- _ => 
             inversion H; clear H
         end;
  repeat match goal with
           H: nat_of_ascii _ < nat_of_ascii _ |- _ => 
             compute in H
         end;
  match goal with H: S _ <=  _ |- _ => omega end.
Qed.

(*B  
{section 4|Implementation}

That was the specification; now the implementation.
We just give a name to the intended return type:
 B*)
Definition lexicographic_decision (a b : string) := 
  { in_lex_order a b } + { ~ (in_lex_order a b) }.

(*B  {p}
First, we will need this lemma about {t|nat_of_ascii}.
 B*)
Lemma nat_of_ascii_injective: 
  forall c1 c2, nat_of_ascii c1 = nat_of_ascii c2 -> c1 = c2.
Proof.
  intros; simpl. 
  assert (ascii_of_nat (nat_of_ascii c1) = 
              ascii_of_nat (nat_of_ascii c2))
      as Hinvol. auto.
  repeat rewrite ascii_nat_embedding in Hinvol.
  trivial.
Qed.

(*B  {p}
{t|nat_of_ascii_injective} is used to prove the following one, which
will allow {i|intuition auto} to finish its job {i|nicely}:
 B*)
Lemma tricky_step_in_decide_lex_order:
  forall c1 c2 s1 s2,
    ~ nat_of_ascii c1 < nat_of_ascii c2 ->
    ~ nat_of_ascii c2 < nat_of_ascii c1 ->
    in_lex_order s1 s2 ->
    in_lex_order (String c1 s1) (String c2 s2).
Proof.
  intros.
  assert (nat_of_ascii c1 = nat_of_ascii c2) as c1_c2_nat_eq. 
    omega.
  apply nat_of_ascii_injective in c1_c2_nat_eq; subst; auto.
Qed.

(*B  {p}

And now is the definition of {b|{t|decide_lex_order}}.
We use {t|Compare_dec.lt_dec}
to compare naturals, it has a {t|sumbool} type too{note
|Note that 
there is also {t|lt_eq_lt_dec} but 
we are not ready to use it for now
(it is a {t|sumbool} embedded in a {t|sumor}, so, maybe another time
{t|:)}).}:
{code}forall n m : nat, {n < m} + {~ n < m}{end}
{p}


 B*)
Require Import Compare_dec.

Definition decide_lex_order:
  forall a b : string, lexicographic_decision a b.

refine (fix fcontinue a b: lexicographic_decision a b := 
  match a, b with
    | EmptyString, EmptyString => Decide_left
    | EmptyString, _ => Decide_left
    | _, EmptyString => Decide_right
    | String c1 s1, String c2 s2 => 
      match lt_dec (nat_of_ascii c1) (nat_of_ascii c2) with 
        | Decide_left => Decide_left
        | Decide_right =>
          match lt_dec (nat_of_ascii c2) (nat_of_ascii c1) with
            | Decide_left => Decide_right
            | Decide_right => Decide_with (fcontinue s1 s2)
          end
      end
  end);
  solve [
    intuition auto using tricky_step_in_decide_lex_order 
    | match goal with
        |- ~ in_lex_order _ _ => 
          unfold not; intro H; inversion H;
            subst; intuition auto
      end   ].
Defined.

(*B Just for the record, the following is how looked my first {q|Proof
Complete}
on that one. The idea is to explore with wild ugly tactics or
inline lemmas, and
then do the {i|factorisation}, {i|cleaning}, and {i|optimisations}.
[coq[
unfold not in *; intros; auto.

inversion H.

inversion H. intuition.
subst. intuition.

assert (nat_of_ascii c1 = nat_of_ascii c2). omega.

Lemma nat_of_ascii_injective: forall c1 c2, 
  nat_of_ascii c1 = nat_of_ascii c2 -> c1 = c2.
  intros; simpl. 
  assert (ascii_of_nat (nat_of_ascii c1) =
         ascii_of_nat (nat_of_ascii c2)).
      auto.
  repeat rewrite ascii_nat_embedding in H0.
  trivial.
Qed.

apply nat_of_ascii_injective in H.
subst.
auto.

inversion H; subst.

intuition auto.
intuition auto.
Defined.
]coq]
 B*)

(*B We can give it a try: B*)
Eval compute in (decide_lex_order "AAA" "BBB").
(*B {code}
     = Decide_left
     : lexicographic_decision "AAA" "BBB"
{end}
 B*)
Time Eval compute in (decide_lex_order "AAA" "ABB").
(*B {code}
     = Decide_left
     : lexicographic_decision "AAA" "ABB"
Finished transaction in 4. secs (0.u,3.544461s)
{end}
 B*)
Time Eval compute in (decide_lex_order "AAA" "AAB").
(*B {code}
     = Decide_left
     : lexicographic_decision "AAA" "AAB"
Finished transaction in 9. secs (0.u,8.202753s)
{end}
 B*)
Time Eval compute in (decide_lex_order "AA" "A").
(*B {code}
     = Decide_right
     : lexicographic_decision "AA" "A"
Finished transaction in 13. secs (0.u,12.995024s)
{end} {p}
 B*)
(*B The tactic
{link http://coq.inria.fr/refman/Reference-Manual011.html#@tactic61
|vm_compute} does not seem to improve the speed there.
But anyway, the important performance-wise is the OCaml code,
and it looks pretty good: B*)
Extraction decide_lex_order.
(*B [caml[
(** val decide_lex_order : 
      string -> string -> lexicographic_decision **)

let rec decide_lex_order a b =
  match a with
  | EmptyString -> true
  | String (c1, s1) ->
    (match b with
     | EmptyString -> false
     | String (c2, s2) ->
       if lt_dec (nat_of_ascii c1) (nat_of_ascii c2)
       then true
       else if lt_dec (nat_of_ascii c2) (nat_of_ascii c1)
            then false
            else decide_lex_order s1 s2)
]caml]
 B*)


(*B {ignore end_ignored_bonus} B*)
(* ********************************************************************** *)
Inductive char_in_string: ascii -> string -> Prop :=
| char_in_string_there:
  forall (c: ascii) (s : string),
    char_in_string c (String c s)
| char_in_string_later:
  forall (ca c: ascii) (s : string),
    char_in_string c s -> char_in_string c (String ca s).

Definition contains_char:
  forall (s : string) (c : ascii), { char_in_string c s } + { ~ char_in_string c s }.
refine (fix frec (s : string) (c : ascii):
  { char_in_string c s } + { ~ char_in_string c s } :=
  match s with
    | EmptyString => Decide_right
    | String x tl_s =>
      if ascii_dec x c then Decide_left else Decide_with (frec tl_s c)
  end);
  intuition (
    try match goal with H: char_in_string _ _ |- _ =>  inversion H; auto end;
    subst; auto using char_in_string_there, char_in_string_later).
Defined.

Eval compute in (contains_char "Bouh" "o").
(*B {code}
= Decide_left
: {char_in_string "o" "Bouh"} + {~ char_in_string "o" "Bouh"}
{end}
 B*)
Eval compute in (contains_char "Bouh" "n").
(*B {code}
= Decide_right
: {char_in_string "n" "Bouh"} + {~ char_in_string "n" "Bouh"}
{end}
 B*)
Extraction contains_char.
(*B [caml[
(** val contains_char : string -> ascii -> bool **)

let rec contains_char s c =
  match s with
  | EmptyString -> false
  | String (x, tl_s) -> if ascii_dec x c then true else contains_char tl_s c
]caml]
 B*)

(*B {end_ignored_bonus} B*)