The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

Require Import List.

(* To adapt your specification a bit it makes sense to use
 *   'sumbool' from Coq standard library:
 *)
Definition Decide (P : Prop) := { P } + { ~ P }.
(* P is a Proposition, so it will be erased on extraction,
 *   the remaining information (in ocaml) will simple be
 *   which branch (i.e. if P was contructed or shown
 *   contradictory)
 *)

Section Sublist.
  
  Variable A : Type.
  (* The program(s) are parametrized over some type of elements *)
  
  Variable eq_A_dec : forall x y : A, Decide (x = y).
  (* And we have to be able to see if they are equal or not *)
  
  Section Specification.
    
    (* what does it mean to be a sublist? *)
    Definition Sublist (sub list : list A) :=
      exists begin, exists tail, begin ++ sub ++ tail = list.

    (* The type of programs which decide if one list is a
     *   sublist of another:
     *)
    Definition Sublist_spec (sub list : list A) :=
      Decide (Sublist sub list).
  
  End Specification.
  
  (* Now we can attempt to realize the specification by giving an
   * implementation inside Coq with this type
   *)
  
  Section Implementation.
    
    Section Subproblem.
      
      (* As usual in programming (and proofs), diving into subproblems
       * will make things much easier:
       *)
      
      Definition Prefix (pre list : list A) :=
        exists tail, pre ++ tail = list.
 
      Definition Prefix_spec (pre list : list A) :=
        Decide (Prefix pre list).
      
      Definition Prefix_dec (pre list : list A) : Prefix_spec pre list.
      refine (
        fix Prefix_dec (pre list : list A) : Prefix_spec pre list := _
      ).
      refine (
        match pre as pre return Prefix_spec pre list with
          | nil => left _ _
          | p :: ps => _
        end
      ).
      
      unfold Prefix.
      exists list.
      reflexivity.
      
      refine (
        match list as list return Prefix_spec (p :: ps) list with
          | nil => right _ _
          | x :: xs => _
        end
      ).
      
      intros [x H].
      simpl in H.
      discriminate H.
      
      refine (
        match eq_A_dec p x with
          | left eqPrf => (* the first two elements of both lists are equal
*)
            match Prefix_dec ps xs with
              | left prePrf => left _ _
              | right nprePrf => right _ _
            end
          | right nqPrf => (* they are not equal *)
            right _ _
        end
      ).
      
      subst.
      destruct prePrf as [tail tailPrf].
      exists tail; rewrite <- tailPrf.
      reflexivity.
      
      subst.
      intros [tail tailPrf]; apply nprePrf.
      exists tail; injection tailPrf; congruence.
      
      intros [tail tailPrf]; apply nqPrf.
      injection tailPrf; congruence.
      Defined.
    
    End Subproblem.
  
    (* and then define the Sublist function in a similar way .. *)
  
  End Implementation.

End Sublist.

Extraction Prefix_dec.

And then extraction gives:

(** val prefix_dec :
    ('a1 -> 'a1 -> decide) -> 'a1 list -> 'a1 list -> 'a1 prefix_spec **)

let rec prefix_dec eq_A_dec pre list0 =
  match pre with
    | Nil -> Left
    | Cons (p, ps) ->
        (match list0 with
           | Nil -> Right
           | Cons (x, xs) ->
               (match eq_A_dec p x with
                  | Left -> prefix_dec eq_A_dec ps xs
                  | Right -> Right))

-- 
View this message in context: 
http://www.nabble.com/Simple-example-tp22106715p22109277.html
Sent from the Coq mailing list archive at Nabble.com.