Subseq

Subseq.v

Inductive subseq {X : Type} : (list X) -> (list X) -> Prop :=
  | s_nil : forall (xs : list X),
              subseq nil xs
  | s_diff : forall (y : X) (xs ys : list X),
              subseq xs ys -> subseq xs (y::ys)
  | s_same : forall (x : X) (xs ys : list X),
              subseq xs ys -> subseq (x::xs) (x::ys).

(*
subseq [1,2,3] [1,2,3]:

------------ (s_nil)
subseq [] []
-------------- (s_same)
subseq [3] [3]
------------------ (s_same)
subseq [2,3] [2,3]
---------------------- (s_same)
subseq [1,2,3] [1,2,3]


subseq [1,2,3] [1,1,1,2,2,3]:

  ------------ (s_nil)
  subseq [] []
  -------------- (s_same)
  subseq [3] [3]
  ---------------- (s_diff)
  subseq [3] [2,3]
  -------------------- (s_same)
  subseq [2,3] [2,2,3]
  ---------------------- (s_diff)
  subseq [2,3] [1,2,2,3]
  ------------------------ (s_diff)
  subseq [2,3] [1,1,2,2,3]
---------------------------- (s_same)
subseq [1,2,3] [1,1,1,2,2,3]


subseq [1,2,3] [1,2,7,3]:

      ------------ (s_nil)
      subseq [] []
     -------------- (s_same)
     subseq [3] [3]
    ---------------- (s_diff)
    subseq [3] [7,3]
  -------------------- (s_same)
  subseq [2,3] [2,7,3]
------------------------ (s_same)
subseq [1,2,3] [1,2,7,3]


subseq [1,2,3] [5,6,1,9,9,2,7,3,8]:

         ------------- (s_nil)
         subseq [] [8]
        ---------------- (s_same)
        subseq [3] [3,8]
       ------------------ (s_diff)
       subseq [3] [7,3,8]
     ---------------------- (s_same)
     subseq [2,3] [2,7,3,8]
    ------------------------ (s_diff)
    subseq [2,3] [9,2,7,3,8]
   -------------------------- (s_diff)
   subseq [2,3] [9,9,2,7,3,8]
  ------------------------------ (s_same)
  subseq [1,2,3] [1,9,9,2,7,3,8]
 -------------------------------- (s_diff)
 subseq [1,2,3] [6,1,9,9,2,7,3,8]
---------------------------------- (s_diff)
subseq [1,2,3] [5,6,1,9,9,2,7,3,8]


!subseq [1,2,3] [1,2]:

    ------------- (no rule)
    subseq [3] []
  ---------------- (s_same)
  subseq [2,3] [2]
-------------------- (s_same)
subseq [1,2,3] [1,2]


!subseq [1,2,3] [1,3]:

   ------------- (no rule)
   subseq [2] []
 ---------------- (s_diff)
 subseq [2,3] [3]
-------------------- (s_same)
subseq [1,2,3] [1,3]


!subseq [1,2,3] [5,6,2,1,7,3,8]:

       --------------- (no rule)
       subseq [2,3] []
       ---------------- (s_diff)
       subseq [2,3] [8]
      ------------------ (s_diff)
      subseq [2,3] [3,8]
     -------------------- (s_diff)
     subseq [2,3] [7,3,8]
   ------------------------ (s_same)
   subseq [1,2,3] [1,7,3,8]
  -------------------------- (s_diff)
  subseq [1,2,3] [2,1,7,3,8]
 ---------------------------- (s_diff)
 subseq [1,2,3] [6,2,1,7,3,8]
------------------------------ (s_diff)
subseq [1,2,3] [5,6,2,1,7,3,8]
*)