Library dfs_DfsRandomSearch_list_suffix_fst_not_twice_1

Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.

Definition unit := unit.

Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.

Axiom set : forall (a:Type), Type.
Parameter set_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (set a).
Existing Instance set_WhyType.

Parameter mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.

Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
  a)): Prop := forall (x:a), (mem x s1) <-> (mem x s2).

Axiom extensionality : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
  (s2:(set a)), (infix_eqeq s1 s2) -> (s1 = s2).

Definition subset {a:Type} {a_WT:WhyType a} (s1:(set a)) (s2:(set
  a)): Prop := forall (x:a), (mem x s1) -> (mem x s2).

Axiom subset_refl : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
  (subset s s).

Axiom subset_trans : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
  (s2:(set a)) (s3:(set a)), (subset s1 s2) -> ((subset s2 s3) -> (subset s1
  s3)).

Parameter empty: forall {a:Type} {a_WT:WhyType a}, (set a).

Definition is_empty {a:Type} {a_WT:WhyType a} (s:(set a)): Prop :=
  forall (x:a), ~ (mem x s).

Axiom empty_def1 : forall {a:Type} {a_WT:WhyType a}, (is_empty (empty : (set
  a))).

Axiom mem_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ~ (mem x
  (empty : (set a))).

Parameter add: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).

Axiom add_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
  forall (s:(set a)), (mem x (add y s)) <-> ((x = y) \/ (mem x s)).

Parameter remove: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> (set a).

Axiom remove_def1 : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
  (s:(set a)), (mem x (remove y s)) <-> ((~ (x = y)) /\ (mem x s)).

Axiom add_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
  a)), (mem x s) -> ((add x (remove x s)) = s).

Axiom remove_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
  a)), ((remove x (add x s)) = (remove x s)).

Axiom subset_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(set
  a)), (subset (remove x s) s).

Parameter union: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
  a).

Axiom union_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
  (s2:(set a)) (x:a), (mem x (union s1 s2)) <-> ((mem x s1) \/ (mem x s2)).

Parameter inter: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
  a).

Axiom inter_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
  (s2:(set a)) (x:a), (mem x (inter s1 s2)) <-> ((mem x s1) /\ (mem x s2)).

Parameter diff: forall {a:Type} {a_WT:WhyType a}, (set a) -> (set a) -> (set
  a).

Axiom diff_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
  (s2:(set a)) (x:a), (mem x (diff s1 s2)) <-> ((mem x s1) /\ ~ (mem x s2)).

Axiom subset_diff : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
  (s2:(set a)), (subset (diff s1 s2) s1).

Parameter choose: forall {a:Type} {a_WT:WhyType a}, (set a) -> a.

Axiom choose_def : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
  (~ (is_empty s)) -> (mem (choose s) s).

Parameter cardinal: forall {a:Type} {a_WT:WhyType a}, (set a) -> Z.

Axiom cardinal_nonneg : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
  (0%Z <= (cardinal s))%Z.

Axiom cardinal_empty : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
  ((cardinal s) = 0%Z) <-> (is_empty s).

Axiom cardinal_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
  forall (s:(set a)), (~ (mem x s)) -> ((cardinal (add x
  s)) = (1%Z + (cardinal s))%Z).

Axiom cardinal_remove : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
  forall (s:(set a)), (mem x s) -> ((cardinal s) = (1%Z + (cardinal (remove x
  s)))%Z).

Axiom cardinal_subset : forall {a:Type} {a_WT:WhyType a}, forall (s1:(set a))
  (s2:(set a)), (subset s1 s2) -> ((cardinal s1) <= (cardinal s2))%Z.

Axiom cardinal1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(set a)),
  ((cardinal s) = 1%Z) -> forall (x:a), (mem x s) -> (x = (choose s)).

Parameter elements: forall {a:Type} {a_WT:WhyType a}, (list a) -> (set a).

Axiom elements_mem : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a))
  (x:a), (list.Mem.mem x l) <-> (mem x (elements l)).

Axiom elements_Nil : forall {a:Type} {a_WT:WhyType a},
  ((elements Init.Datatypes.nil) = (empty : (set a))).

Axiom vertex : Type.
Parameter vertex_WhyType : WhyType vertex.
Existing Instance vertex_WhyType.

Parameter vertices: (set vertex).

Parameter successors: vertex -> (set vertex).

Axiom successors_vertices : forall (x:vertex), (mem x vertices) -> (subset
  (successors x) vertices).

Definition edge (x:vertex) (y:vertex): Prop := (mem x vertices) /\ (mem y
  (successors x)).

Inductive path: vertex -> (list vertex) -> vertex -> Prop :=
  | Path_empty : forall (x:vertex), (path x Init.Datatypes.nil x)
  | Path_cons : forall (x:vertex) (y:vertex) (z:vertex) (l:(list vertex)),
      (edge x y) -> ((path y l z) -> (path x (Init.Datatypes.cons x l) z)).

Axiom path_right_extension : forall (x:vertex) (y:vertex) (z:vertex)
  (l:(list vertex)), (path x l y) -> ((edge y z) -> (path x
  (Init.Datatypes.app l (Init.Datatypes.cons y Init.Datatypes.nil)) z)).

Axiom path_right_inversion : forall (x:vertex) (z:vertex) (l:(list vertex)),
  (path x l z) -> (((x = z) /\ (l = Init.Datatypes.nil)) \/ exists y:vertex,
  exists l´:(list vertex), (path x l´ y) /\ ((edge y z) /\
  (l = (Init.Datatypes.app l´ (Init.Datatypes.cons y Init.Datatypes.nil))))).

Axiom path_trans : forall (x:vertex) (y:vertex) (z:vertex) (l1:(list vertex))
  (l2:(list vertex)), (path x l1 y) -> ((path y l2 z) -> (path x
  (Init.Datatypes.app l1 l2) z)).

Axiom empty_path : forall (x:vertex) (y:vertex), (path x Init.Datatypes.nil
  y) -> (x = y).

Axiom path_decomposition : forall (x:vertex) (y:vertex) (z:vertex)
  (l1:(list vertex)) (l2:(list vertex)), (path x
  (Init.Datatypes.app l1 (Init.Datatypes.cons y l2)) z) -> ((path x l1 y) /\
  (path y (Init.Datatypes.cons y l2) z)).

Axiom mem_decidable : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
  (l:(list a)), (list.Mem.mem x l) \/ ~ (list.Mem.mem x l).

Require Import ssreflect.
Ltac compress :=
  repeat (match goal with [H1: ?A, H2: ?A |- _] => clear H2 end).

Theorem list_suffix_fst_not_twice : forall (x:vertex) (l:(list vertex)),
  (list.Mem.mem x l) -> exists l1:(list vertex), exists l2:(list vertex),
  (l = (Init.Datatypes.app l1 (Init.Datatypes.cons x l2))) /\ ~ (list.Mem.mem
  x l2).
Proof.
move=> x l.
elim: l => [ hNil | y l HI hxinyl].
- by simpl in hNil.
- have Hxinl_Notxinl: (Mem.mem x l) \/ ~ (Mem.mem x l).
   + by apply mem_decidable.
   move: Hxinl_Notxinl => [Hxinl | HNotxinl].
   - apply HI in Hxinl. move: Hxinl => [l1 [l2 [eqll1xl2 hNotxinl2]]].
     exists (y :: l1)%list. exists l2.
     simpl. split.
     by rewrite eqll1xl2.
     by [].
   - exists nil. exists l.
     simpl; split.
     + have Exy: x = y.
       - simpl in hxinyl.
         move: hxinyl => [eqxy | hxinl].
         + by [ ].
         + by apply HNotxinl in hxinl.
       by rewrite Exy.
     + exact HNotxinl.
Qed.