The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Cedric Auger wrote:
> Here is an awful way to do it using tactics.

Well, here's a non-awful way, with no documentation.  See my in-progress 
textbook for more pointers on writing this kind of code:
   http://adam.chlipala.net/cpdt/


Require Import List.

Parameter A : Set.
Parameter A_dec : forall a b : A, {a = b} + {a <> b}.

Notation "'Yes' x" := (inleft _ (exist _ x _)) (at level 60).
Notation "'No'" := (inright _ _) (at level 60).

Notation "x <- c1 ; c2" := (match c1 with
                             | inleft (exist x _) => c2
                             | inright _ => No
                           end) (right associativity, at level 61).

Ltac t' := simpl in *; subst; intuition eauto; try congruence.
Ltac t := t'; repeat progress (match goal with
                                | [ H : _ :: _ = _ :: _ |- _ ] => 
injection H; clear H; intros
                                | [ _ : _ :: _ = ?ls ++ _ |- _ ] => 
destruct ls
                              end; t').

Definition prefix (ls1 ls2 : list A) : {ls3 : list A | ls2 = ls1 ++ ls3} 
+ {forall ls3, ls2 <> ls1 ++ ls3}.
 refine (fix prefix (ls1 ls2 : list A) {struct ls1}
   : {ls3 : list A | ls2 = ls1 ++ ls3} + {forall ls3, ls2 <> ls1 ++ ls3} :=
   match ls1, ls2 return {ls3 : list A | ls2 = ls1 ++ ls3} + {forall 
ls3, ls2 <> ls1 ++ ls3} with
     | nil, _ => Yes ls2
     | _ :: _, nil => No
     | x1 :: ls1', x2 :: ls2' =>
       if A_dec x1 x2
         then ls3 <- prefix ls1' ls2';
              Yes ls3
         else No
   end); t.
Qed.

Notation "'Yes2' x && y" := (inleft _ (existT _ x (exist _ y _))) (at 
level 60).
Notation "x &&& y <-- c1 ; c2" := (match c1 with
                                   | inleft (existT x (exist y _)) => c2
                                   | inright _ => No
                                 end) (right associativity, at level 61).
Notation "x <--- c1 ; c2 || c3" := (match c1 with
                                     | inleft (exist x _) => c2
                                     | inright _ => c3
                                   end) (right associativity, at level 61).

Theorem app_cons_not_nil : forall (x y:list A) (a:A), nil = x ++ a :: y 
-> False.
 apply app_cons_not_nil.
Qed.

Hint Resolve app_cons_not_nil.

Definition sublist (ls1 ls2 : list A)
 : {ls3 : list A & {ls4 : list A | ls2 = ls3 ++ ls1 ++ ls4}}
 + {forall ls3 ls4, ls2 <> ls3 ++ ls1 ++ ls4}.
 refine (fix sublist (ls1 ls2 : list A) {struct ls2}
   : {ls3 : list A & {ls4 : list A | ls2 = ls3 ++ ls1 ++ ls4}}
   + {forall ls3 ls4, ls2 <> ls3 ++ ls1 ++ ls4} :=
   match ls1, ls2 return {ls3 : list A & {ls4 : list A | ls2 = ls3 ++ 
ls1 ++ ls4}}
     + {forall ls3 ls4, ls2 <> ls3 ++ ls1 ++ ls4} with
     | nil, ls2 => Yes2 nil && ls2
     | _, nil => No
     | x1 :: ls1', x2 :: ls2' =>
       ls3 <--- prefix (x1 :: ls1') (x2 :: ls2');
       Yes2 nil && ls3
       ||
       ls3 &&& ls4 <-- sublist (x1 :: ls1') ls2';
       Yes2 (x2 :: ls3) && ls4
   end); t.
Qed.