SubLists.v

Require Import Arith.
Require Import List.
Local Open Scope list_scope.

Inductive SubListsRel (n : nat) : forall (ns : list nat)
                      (mss : list (list nat)), Prop :=

  | base      : SubListsRel n nil (nil :: nil)

  | consEq    : forall ns m mss,
                n = m -> SubListsRel n ns mss ->
              (* ----------------------------- *)
                SubListsRel n (m :: ns) (nil :: mss)

  | consNotEq : forall ns m ms mss,
                (n <> m) -> SubListsRel n ns (ms :: mss) ->
              (* ------------------------------------------------- *)
                SubListsRel n (m :: ns) ((m :: ms) :: mss)
.

Definition SubLists (n : nat) (ns : list nat) : Set :=
  { mss | SubListsRel n ns mss }.

Example example1 : SubLists 0 (1 :: 2 :: 0 :: 3 :: 4 :: 0 :: 9 :: nil).
Proof.
eexists ; repeat econstructor ; intro Hf; inversion Hf.
Defined.

Check (eq_refl : proj1_sig example1
               = ((1 :: 2 :: nil) :: (3 :: 4 :: nil) :: (9 :: nil) :: nil)).

Ltac dismiss := intro Hf; inversion Hf.

Definition Strenghtened_SubLists (n : nat) (ns : list nat) : Set :=
   { mss | SubListsRel n ns mss /\ mss <> nil }.

Lemma subLists : forall n ns, SubLists n ns.
Proof.
intros n ns; cut (Strenghtened_SubLists n ns).
 - intros [mss [Hmss _]]; eexists; eassumption.
 - induction ns.
   + eexists; split; [econstructor | dismiss].
   + destruct IHns as [mss [Hmss mssNotNil]];
     destruct (eq_nat_dec n a).
     * eexists; split; [eapply consEq ; eassumption| dismiss].
     * destruct mss; [apply False_rect, mssNotNil; reflexivity |].
       eexists; split; [eapply consNotEq; eassumption| dismiss].
Defined.

Example example2 : SubLists 0 (1 :: 2 :: 0 :: 3 :: 4 :: 0 :: 9 :: nil) :=
  subLists _ _.

Check (eq_refl : proj1_sig example1 = proj1_sig example2).