From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude.
From Coq Require Import Sorting.
From VLSM.Lib Require Import Preamble ListExtras ListSetExtras.

Utility: Sorted List Functions and Results

Insert an element into a sorted list.

Fixpoint add_in_sorted_list_fn
  {A} (compare : A -> A -> comparison) (x : A) (l : list A) : list A :=
  match l with
  | [] => [x]
  | h :: t =>
    match compare x h with
    | Lt => x :: h :: t
    | Eq => h :: t
    | Gt => h :: @add_in_sorted_list_fn A compare x t
    end
  end.

Lemma add_in_sorted_list_no_empty {A} (compare : A -> A -> comparison) : forall msg sigma,
  add_in_sorted_list_fn compare msg sigma <> [].A: Type
compare: A → A → comparison
∀ (msg : A) (sigma : list A),
  add_in_sorted_list_fn compare msg sigma ≠ []
Proof.A: Type
compare: A → A → comparison
∀ (msg : A) (sigma : list A),
  add_in_sorted_list_fn compare msg sigma ≠ []
  unfold not.A: Type
compare: A → A → comparison
∀ (msg : A) (sigma : list A),
  add_in_sorted_list_fn compare msg sigma = [] → False intros.A: Type
compare: A → A → comparison
msg: A
sigma: list A
H: add_in_sorted_list_fn compare msg sigma = []
False destruct sigma; simpl in H.A: Type
compare: A → A → comparison
msg: A
H: [msg] = []
False
A: Type
compare: A → A → comparison
msg, a: A
sigma: list A
H: match compare msg a with
| Eq => a :: sigma
| Lt => msg :: a :: sigma
| Gt =>
    a :: add_in_sorted_list_fn compare msg sigma
end = []
False
  -A: Type
compare: A → A → comparison
msg: A
H: [msg] = []
False by inversion H.
  -A: Type
compare: A → A → comparison
msg, a: A
sigma: list A
H: match compare msg a with
| Eq => a :: sigma
| Lt => msg :: a :: sigma
| Gt =>
    a :: add_in_sorted_list_fn compare msg sigma
end = []
False by destruct (compare msg a); inversion H.
Qed.

Lemma add_in_sorted_list_in
  {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} :
  forall msg msg' sigma,
    msg' ∈ add_in_sorted_list_fn compare msg sigma ->
    msg = msg' \/ msg' ∈ sigma.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg msg' : A) (sigma : list A),
  msg' ∈ add_in_sorted_list_fn compare msg sigma
  → msg = msg' ∨ msg' ∈ sigma
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg msg' : A) (sigma : list A),
  msg' ∈ add_in_sorted_list_fn compare msg sigma
  → msg = msg' ∨ msg' ∈ sigma
  intros.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
sigma: list A
H0: msg' ∈ add_in_sorted_list_fn compare msg sigma
msg = msg' ∨ msg' ∈ sigma induction sigma; simpl in H0.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
H0: msg' ∈ [msg]
msg = msg' ∨ msg' ∈ []
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
H0: msg'
∈ match compare msg a with
  | Eq => a :: sigma
  | Lt => msg :: a :: sigma
  | Gt =>
      a
      :: add_in_sorted_list_fn compare msg sigma
  end
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
H0: msg' ∈ [msg]
msg = msg' ∨ msg' ∈ [] rewrite elem_of_cons in H0.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
H0: msg' = msg ∨ msg' ∈ []
msg = msg' ∨ msg' ∈ []
    by destruct H0 as [H0 | H0]; subst; try inversion H0; left.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
H0: msg'
∈ match compare msg a with
  | Eq => a :: sigma
  | Lt => msg :: a :: sigma
  | Gt =>
      a
      :: add_in_sorted_list_fn compare msg sigma
  end
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma destruct (compare msg a) eqn: Hcmp.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Eq
H0: msg' ∈ a :: sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Lt
H0: msg' ∈ msg :: a :: sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Gt
H0: msg'
∈ a :: add_in_sorted_list_fn compare msg sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Eq
H0: msg' ∈ a :: sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma by rewrite compare_eq in Hcmp; subst; right.
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Lt
H0: msg' ∈ msg :: a :: sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma rewrite elem_of_cons in H0.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Lt
H0: msg' = msg ∨ msg' ∈ a :: sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma
      by destruct H0 as [Heq | Hin]; subst; [left | right].
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Gt
H0: msg'
∈ a :: add_in_sorted_list_fn compare msg sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma rewrite elem_of_cons in H0.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Gt
H0: msg' = a
∨ msg' ∈ add_in_sorted_list_fn compare msg sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma
      destruct H0 as [Heq | Hin]; subst.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
Hcmp: compare msg a = Gt
IHsigma: a ∈ add_in_sorted_list_fn compare msg sigma
→ msg = a ∨ a ∈ sigma
msg = a ∨ a ∈ a :: sigma
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Gt
Hin: msg' ∈ add_in_sorted_list_fn compare msg sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma
      *A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
Hcmp: compare msg a = Gt
IHsigma: a ∈ add_in_sorted_list_fn compare msg sigma
→ msg = a ∨ a ∈ sigma
msg = a ∨ a ∈ a :: sigma by right; left.
      *A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Gt
Hin: msg' ∈ add_in_sorted_list_fn compare msg sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' ∈ a :: sigma rewrite elem_of_cons.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
Hcmp: compare msg a = Gt
Hin: msg' ∈ add_in_sorted_list_fn compare msg sigma
IHsigma: msg'
∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
msg = msg' ∨ msg' = a ∨ msg' ∈ sigma
        by apply IHsigma in Hin as []; itauto.
Qed.

Lemma add_in_sorted_list_in_rev
  {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} :
  forall msg msg' sigma,
    msg = msg' \/ msg' ∈ sigma ->
    msg' ∈ add_in_sorted_list_fn compare msg sigma.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg msg' : A) (sigma : list A),
  msg = msg' ∨ msg' ∈ sigma
  → msg' ∈ add_in_sorted_list_fn compare msg sigma
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg msg' : A) (sigma : list A),
  msg = msg' ∨ msg' ∈ sigma
  → msg' ∈ add_in_sorted_list_fn compare msg sigma
  intros.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
sigma: list A
H0: msg = msg' ∨ msg' ∈ sigma
msg' ∈ add_in_sorted_list_fn compare msg sigma induction sigma; simpl in H0.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
H0: msg = msg' ∨ msg' ∈ []
msg' ∈ add_in_sorted_list_fn compare msg []
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
H0: msg = msg' ∨ msg' ∈ a :: sigma
IHsigma: msg = msg' ∨ msg' ∈ sigma
→ msg'
  ∈ add_in_sorted_list_fn compare msg sigma
msg' ∈ add_in_sorted_list_fn compare msg (a :: sigma)
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
H0: msg = msg' ∨ msg' ∈ []
msg' ∈ add_in_sorted_list_fn compare msg [] by destruct H0 as [H0 | H0]; subst; [left | inversion H0].
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
H0: msg = msg' ∨ msg' ∈ a :: sigma
IHsigma: msg = msg' ∨ msg' ∈ sigma
→ msg'
  ∈ add_in_sorted_list_fn compare msg sigma
msg' ∈ add_in_sorted_list_fn compare msg (a :: sigma) rewrite elem_of_cons in H0; cbn.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg', a: A
sigma: list A
H0: msg = msg' ∨ msg' = a ∨ msg' ∈ sigma
IHsigma: msg = msg' ∨ msg' ∈ sigma
→ msg'
  ∈ add_in_sorted_list_fn compare msg sigma
msg'
∈ match compare msg a with
  | Eq => a :: sigma
  | Lt => msg :: a :: sigma
  | Gt => a :: add_in_sorted_list_fn compare msg sigma
  end
    by destruct H0 as [Heq | Heq], (compare msg a) eqn: Hcmp
    ; rewrite !elem_of_cons; rewrite ?compare_eq in Hcmp; subst; itauto.
Qed.

Lemma add_in_sorted_list_iff
  {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} :
  forall msg msg' sigma,
    msg' ∈ add_in_sorted_list_fn compare msg sigma <->
    msg = msg' \/ msg' ∈ sigma.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg msg' : A) (sigma : list A),
  msg' ∈ add_in_sorted_list_fn compare msg sigma
  ↔ msg = msg' ∨ msg' ∈ sigma
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg msg' : A) (sigma : list A),
  msg' ∈ add_in_sorted_list_fn compare msg sigma
  ↔ msg = msg' ∨ msg' ∈ sigma
  intros; split.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
sigma: list A
msg' ∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
sigma: list A
msg = msg' ∨ msg' ∈ sigma
→ msg' ∈ add_in_sorted_list_fn compare msg sigma
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
sigma: list A
msg' ∈ add_in_sorted_list_fn compare msg sigma
→ msg = msg' ∨ msg' ∈ sigma by apply add_in_sorted_list_in.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, msg': A
sigma: list A
msg = msg' ∨ msg' ∈ sigma
→ msg' ∈ add_in_sorted_list_fn compare msg sigma by apply add_in_sorted_list_in_rev.
Qed.

Lemma add_in_sorted_list_head
  {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} :
  forall msg sigma,
    msg ∈ add_in_sorted_list_fn compare msg sigma.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  msg ∈ add_in_sorted_list_fn compare msg sigma
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  msg ∈ add_in_sorted_list_fn compare msg sigma
  by intros; apply add_in_sorted_list_iff; left.
Qed.

Lemma add_in_sorted_list_tail
  {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} :
  forall msg sigma,
    sigma ⊆ add_in_sorted_list_fn compare msg sigma.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  sigma ⊆ add_in_sorted_list_fn compare msg sigma
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  sigma ⊆ add_in_sorted_list_fn compare msg sigma
  intros msg sigma x Hin.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg: A
sigma: list A
x: A
Hin: x ∈ sigma
x ∈ add_in_sorted_list_fn compare msg sigma
  by apply add_in_sorted_list_iff; right.
Qed.

Lemma LocallySorted_ForAll2 [A : Type] (R : A -> A -> Prop)
  : forall l, LocallySorted R l <-> ForAllSuffix2 R l.A: Type
R: A → A → Prop
∀ l : list A, LocallySorted R l ↔ ForAllSuffix2 R l
Proof.A: Type
R: A → A → Prop
∀ l : list A, LocallySorted R l ↔ ForAllSuffix2 R l
  induction l; split; intro Hl.A: Type
R: A → A → Prop
Hl: LocallySorted R []
ForAllSuffix2 R []
A: Type
R: A → A → Prop
Hl: ForAllSuffix2 R []
LocallySorted R []
A: Type
R: A → A → Prop
a: A
l: list A
IHl: LocallySorted R l ↔ ForAllSuffix2 R l
Hl: LocallySorted R (a :: l)
ForAllSuffix2 R (a :: l)
A: Type
R: A → A → Prop
a: A
l: list A
IHl: LocallySorted R l ↔ ForAllSuffix2 R l
Hl: ForAllSuffix2 R (a :: l)
LocallySorted R (a :: l)
  -A: Type
R: A → A → Prop
Hl: LocallySorted R []
ForAllSuffix2 R [] by constructor.
  -A: Type
R: A → A → Prop
Hl: ForAllSuffix2 R []
LocallySorted R [] by constructor.
  -A: Type
R: A → A → Prop
a: A
l: list A
IHl: LocallySorted R l ↔ ForAllSuffix2 R l
Hl: LocallySorted R (a :: l)
ForAllSuffix2 R (a :: l) inversion Hl; subst.A: Type
R: A → A → Prop
a: A
Hl: LocallySorted R [a]
IHl: LocallySorted R [] ↔ ForAllSuffix2 R []
ForAllSuffix2 R [a]
A: Type
R: A → A → Prop
a, b: A
l0: list A
Hl: LocallySorted R (a :: b :: l0)
IHl: LocallySorted R (b :: l0) ↔ ForAllSuffix2 R (b :: l0)
H1: LocallySorted R (b :: l0)
H2: R a b
ForAllSuffix2 R (a :: b :: l0)
    +A: Type
R: A → A → Prop
a: A
Hl: LocallySorted R [a]
IHl: LocallySorted R [] ↔ ForAllSuffix2 R []
ForAllSuffix2 R [a] by repeat constructor.
    +A: Type
R: A → A → Prop
a, b: A
l0: list A
Hl: LocallySorted R (a :: b :: l0)
IHl: LocallySorted R (b :: l0) ↔ ForAllSuffix2 R (b :: l0)
H1: LocallySorted R (b :: l0)
H2: R a b
ForAllSuffix2 R (a :: b :: l0) by apply IHl in H1; constructor.
  -A: Type
R: A → A → Prop
a: A
l: list A
IHl: LocallySorted R l ↔ ForAllSuffix2 R l
Hl: ForAllSuffix2 R (a :: l)
LocallySorted R (a :: l) apply proj2 in IHl; inversion Hl; subst.A: Type
R: A → A → Prop
a: A
l: list A
IHl: ForAllSuffix2 R l → LocallySorted R l
Hl: ForAllSuffix2 R (a :: l)
H1: match l with
| [] => True
| b :: _ => R a b
end
H2: ForAllSuffix
  (λ l : list A,
     match l with
     | [] => True
     | [a] => True
     | a :: b :: _ => R a b
     end) l
LocallySorted R (a :: l)
    by destruct l; constructor; auto.
Qed.

Lemma LocallySorted_filter [A : Type] (R : A -> A -> Prop) {HT : Transitive R}
  (P : A -> Prop) (Pdec : forall a, Decision (P a))
  : forall l, LocallySorted R l -> LocallySorted R (filter P l).A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ l : list A,
  LocallySorted R l → LocallySorted R (filter P l)
Proof.A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ l : list A,
  LocallySorted R l → LocallySorted R (filter P l)
  setoid_rewrite LocallySorted_ForAll2.A: Type
R: A → A → Prop
HT: Transitive R
P: A → Prop
Pdec: ∀ a : A, Decision (P a)
∀ l : list A,
  ForAllSuffix2 R l → ForAllSuffix2 R (filter P l)
  by apply ForAllSuffix2_filter.
Qed.

Lemma LocallySorted_tl
  {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} :
  forall msg sigma,
    LocallySorted (compare_lt compare) (msg :: sigma) ->
    LocallySorted (compare_lt compare) sigma.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  LocallySorted (compare_lt compare) (msg :: sigma)
  → LocallySorted (compare_lt compare) sigma
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  LocallySorted (compare_lt compare) (msg :: sigma)
  → LocallySorted (compare_lt compare) sigma
  intros.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg: A
sigma: list A
H0: LocallySorted (compare_lt compare) (msg :: sigma)
LocallySorted (compare_lt compare) sigma apply Sorted_LocallySorted_iff in H0.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg: A
sigma: list A
H0: Sorted (compare_lt compare) (msg :: sigma)
LocallySorted (compare_lt compare) sigma
  inversion H0; subst; clear H0.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg: A
sigma: list A
H3: Sorted (compare_lt compare) sigma
H4: HdRel (compare_lt compare) msg sigma
LocallySorted (compare_lt compare) sigma
  by apply Sorted_LocallySorted_iff.
Qed.

Lemma add_in_sorted_list_sorted
  {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} :
  forall msg sigma,
    LocallySorted (compare_lt compare) sigma ->
    LocallySorted (compare_lt compare) (add_in_sorted_list_fn compare msg sigma).A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  LocallySorted (compare_lt compare) sigma
  → LocallySorted (compare_lt compare)
      (add_in_sorted_list_fn compare msg sigma)
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  LocallySorted (compare_lt compare) sigma
  → LocallySorted (compare_lt compare)
      (add_in_sorted_list_fn compare msg sigma)
  induction 1; cbn; try constructor; destruct (compare msg a) eqn: Hcmpa.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
Hcmpa: compare msg a = Eq
LocallySorted (compare_lt compare) [a]
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
Hcmpa: compare msg a = Lt
LocallySorted (compare_lt compare) [msg; a]
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare) [a; msg]
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
IHLocallySorted: LocallySorted (compare_lt compare)
  (add_in_sorted_list_fn compare msg
     (b :: l))
Hcmpa: compare msg a = Eq
LocallySorted (compare_lt compare) (a :: b :: l)
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
IHLocallySorted: LocallySorted (compare_lt compare)
  (add_in_sorted_list_fn compare msg
     (b :: l))
Hcmpa: compare msg a = Lt
LocallySorted (compare_lt compare)
  (msg :: a :: b :: l)
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
IHLocallySorted: LocallySorted (compare_lt compare)
  (add_in_sorted_list_fn compare msg
     (b :: l))
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare)
  (a
   :: match compare msg b with
      | Eq => b :: l
      | Lt => msg :: b :: l
      | Gt => b :: add_in_sorted_list_fn compare msg l
      end)
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
Hcmpa: compare msg a = Eq
LocallySorted (compare_lt compare) [a] by constructor.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
Hcmpa: compare msg a = Lt
LocallySorted (compare_lt compare) [msg; a] by constructor; [constructor |].
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare) [a; msg] constructor; [constructor |].A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
Hcmpa: compare msg a = Gt
compare_lt compare a msg
    by red; rewrite compare_asymmetric, Hcmpa.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
IHLocallySorted: LocallySorted (compare_lt compare)
  (add_in_sorted_list_fn compare msg
     (b :: l))
Hcmpa: compare msg a = Eq
LocallySorted (compare_lt compare) (a :: b :: l) by constructor.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
IHLocallySorted: LocallySorted (compare_lt compare)
  (add_in_sorted_list_fn compare msg
     (b :: l))
Hcmpa: compare msg a = Lt
LocallySorted (compare_lt compare)
  (msg :: a :: b :: l) by constructor; [constructor |].
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
IHLocallySorted: LocallySorted (compare_lt compare)
  (add_in_sorted_list_fn compare msg
     (b :: l))
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare)
  (a
   :: match compare msg b with
      | Eq => b :: l
      | Lt => msg :: b :: l
      | Gt => b :: add_in_sorted_list_fn compare msg l
      end) cbn in IHLocallySorted.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
IHLocallySorted: LocallySorted (compare_lt compare)
  match compare msg b with
  | Eq => b :: l
  | Lt => msg :: b :: l
  | Gt =>
      b
      :: add_in_sorted_list_fn
           compare msg l
  end
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare)
  (a
   :: match compare msg b with
      | Eq => b :: l
      | Lt => msg :: b :: l
      | Gt => b :: add_in_sorted_list_fn compare msg l
      end)
    destruct (compare msg b) eqn: Hcmpb.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
Hcmpb: compare msg b = Eq
IHLocallySorted: LocallySorted (compare_lt compare)
  (b :: l)
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare) (a :: b :: l)
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
Hcmpb: compare msg b = Lt
IHLocallySorted: LocallySorted (compare_lt compare)
  (msg :: b :: l)
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare)
  (a :: msg :: b :: l)
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
Hcmpb: compare msg b = Gt
IHLocallySorted: LocallySorted (compare_lt compare)
  (b
   :: add_in_sorted_list_fn compare
        msg l)
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare)
  (a :: b :: add_in_sorted_list_fn compare msg l)
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
Hcmpb: compare msg b = Eq
IHLocallySorted: LocallySorted (compare_lt compare)
  (b :: l)
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare) (a :: b :: l) by rewrite compare_eq in Hcmpb; constructor.
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
Hcmpb: compare msg b = Lt
IHLocallySorted: LocallySorted (compare_lt compare)
  (msg :: b :: l)
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare)
  (a :: msg :: b :: l) constructor; [done |].A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
Hcmpb: compare msg b = Lt
IHLocallySorted: LocallySorted (compare_lt compare)
  (msg :: b :: l)
Hcmpa: compare msg a = Gt
compare_lt compare a msg
      by red; rewrite compare_asymmetric, Hcmpa.
    +A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a, b: A
l: list A
H0: LocallySorted (compare_lt compare) (b :: l)
H1: compare_lt compare a b
Hcmpb: compare msg b = Gt
IHLocallySorted: LocallySorted (compare_lt compare)
  (b
   :: add_in_sorted_list_fn compare
        msg l)
Hcmpa: compare msg a = Gt
LocallySorted (compare_lt compare)
  (a :: b :: add_in_sorted_list_fn compare msg l) by constructor.
Qed.

Sorted lists as sets

Lemma LocallySorted_elem_of_lt {A} {lt : relation A} `{StrictOrder A lt} :
  forall x y s,
  LocallySorted lt (y :: s) ->
  x ∈ s ->
  lt y x.A: Type
lt: relation A
H: StrictOrder lt
∀ (x y : A) (s : list A),
  LocallySorted lt (y :: s) → x ∈ s → lt y x
Proof.A: Type
lt: relation A
H: StrictOrder lt
∀ (x y : A) (s : list A),
  LocallySorted lt (y :: s) → x ∈ s → lt y x
  intros x y s LS IN.A: Type
lt: relation A
H: StrictOrder lt
x, y: A
s: list A
LS: LocallySorted lt (y :: s)
IN: x ∈ s
lt y x revert y x LS IN.A: Type
lt: relation A
H: StrictOrder lt
s: list A
∀ y x : A, LocallySorted lt (y :: s) → x ∈ s → lt y x
  induction s.A: Type
lt: relation A
H: StrictOrder lt
∀ y x : A, LocallySorted lt [y] → x ∈ [] → lt y x
A: Type
lt: relation A
H: StrictOrder lt
a: A
s: list A
IHs: ∀ y x : A, LocallySorted lt (y :: s) → x ∈ s → lt y x
∀ y x : A,
  LocallySorted lt (y :: a :: s) → x ∈ a :: s → lt y x
  -A: Type
lt: relation A
H: StrictOrder lt
∀ y x : A, LocallySorted lt [y] → x ∈ [] → lt y x by inversion 2.
  -A: Type
lt: relation A
H: StrictOrder lt
a: A
s: list A
IHs: ∀ y x : A, LocallySorted lt (y :: s) → x ∈ s → lt y x
∀ y x : A,
  LocallySorted lt (y :: a :: s) → x ∈ a :: s → lt y x by do 2 inversion 1; subst; firstorder.
Qed.

Lemma add_in_sorted_list_existing
  {A} {compare : A -> A -> comparison} `{CompareStrictOrder A compare} :
  forall msg sigma,
    LocallySorted (compare_lt compare) sigma ->
    msg ∈ sigma ->
    add_in_sorted_list_fn compare msg sigma = sigma.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  LocallySorted (compare_lt compare) sigma
  → msg ∈ sigma
    → add_in_sorted_list_fn compare msg sigma = sigma
Proof.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
∀ (msg : A) (sigma : list A),
  LocallySorted (compare_lt compare) sigma
  → msg ∈ sigma
    → add_in_sorted_list_fn compare msg sigma = sigma
  induction sigma; intros; [by inversion H1 |].A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: LocallySorted (compare_lt compare) sigma
→ msg ∈ sigma
  → add_in_sorted_list_fn compare msg sigma =
    sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
H1: msg ∈ a :: sigma
add_in_sorted_list_fn compare msg (a :: sigma) =
a :: sigma
  rewrite elem_of_cons in H1.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: LocallySorted (compare_lt compare) sigma
→ msg ∈ sigma
  → add_in_sorted_list_fn compare msg sigma =
    sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
H1: msg = a ∨ msg ∈ sigma
add_in_sorted_list_fn compare msg (a :: sigma) =
a :: sigma
  destruct H1 as [Heq | Hin].A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: LocallySorted (compare_lt compare) sigma
→ msg ∈ sigma
  → add_in_sorted_list_fn compare msg sigma =
    sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Heq: msg = a
add_in_sorted_list_fn compare msg (a :: sigma) =
a :: sigma
A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: LocallySorted (compare_lt compare) sigma
→ msg ∈ sigma
  → add_in_sorted_list_fn compare msg sigma =
    sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Hin: msg ∈ sigma
add_in_sorted_list_fn compare msg (a :: sigma) =
a :: sigma
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: LocallySorted (compare_lt compare) sigma
→ msg ∈ sigma
  → add_in_sorted_list_fn compare msg sigma =
    sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Heq: msg = a
add_in_sorted_list_fn compare msg (a :: sigma) =
a :: sigma by subst; simpl; rewrite compare_eq_refl.
  -A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: LocallySorted (compare_lt compare) sigma
→ msg ∈ sigma
  → add_in_sorted_list_fn compare msg sigma =
    sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Hin: msg ∈ sigma
add_in_sorted_list_fn compare msg (a :: sigma) =
a :: sigma apply LocallySorted_tl in H0 as LS.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: LocallySorted (compare_lt compare) sigma
→ msg ∈ sigma
  → add_in_sorted_list_fn compare msg sigma =
    sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Hin: msg ∈ sigma
LS: LocallySorted (compare_lt compare) sigma
add_in_sorted_list_fn compare msg (a :: sigma) =
a :: sigma
    specialize (IHsigma LS Hin).A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: add_in_sorted_list_fn compare msg sigma =
sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Hin: msg ∈ sigma
LS: LocallySorted (compare_lt compare) sigma
add_in_sorted_list_fn compare msg (a :: sigma) =
a :: sigma simpl.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: add_in_sorted_list_fn compare msg sigma =
sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Hin: msg ∈ sigma
LS: LocallySorted (compare_lt compare) sigma
match compare msg a with
| Eq => a :: sigma
| Lt => msg :: a :: sigma
| Gt => a :: add_in_sorted_list_fn compare msg sigma
end = a :: sigma
    destruct (compare msg a) eqn: Hcmp; try rewrite IHsigma; [done | | done].A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: add_in_sorted_list_fn compare msg sigma =
sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Hin: msg ∈ sigma
LS: LocallySorted (compare_lt compare) sigma
Hcmp: compare msg a = Lt
msg :: a :: sigma = a :: sigma
    apply (@LocallySorted_elem_of_lt _ _ compare_lt_strict_order msg a sigma H0) in Hin.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: add_in_sorted_list_fn compare msg sigma =
sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Hin: compare_lt compare a msg
LS: LocallySorted (compare_lt compare) sigma
Hcmp: compare msg a = Lt
msg :: a :: sigma = a :: sigma
    unfold compare_lt in Hin.A: Type
compare: A → A → comparison
H: CompareStrictOrder compare
msg, a: A
sigma: list A
IHsigma: add_in_sorted_list_fn compare msg sigma =
sigma
H0: LocallySorted (compare_lt compare) (a :: sigma)
Hin: compare a msg = Lt
LS: LocallySorted (compare_lt compare) sigma
Hcmp: compare msg a = Lt
msg :: a :: sigma = a :: sigma
    by rewrite compare_asymmetric, Hcmp in Hin; inversion Hin.
Qed.

Lemma set_eq_first_equal {A}  {lt : relation A} `{StrictOrder A lt} :
  forall x1 x2 s1 s2,
  LocallySorted lt (x1 :: s1) ->
  LocallySorted lt (x2 :: s2) ->
  set_eq (x1 :: s1) (x2 :: s2) ->
  x1 = x2 /\ set_eq s1 s2.A: Type
lt: relation A
H: StrictOrder lt
∀ (x1 x2 : A) (s1 s2 : list A),
  LocallySorted lt (x1 :: s1)
  → LocallySorted lt (x2 :: s2)
    → set_eq (x1 :: s1) (x2 :: s2)
      → x1 = x2 ∧ set_eq s1 s2
Proof.A: Type
lt: relation A
H: StrictOrder lt
∀ (x1 x2 : A) (s1 s2 : list A),
  LocallySorted lt (x1 :: s1)
  → LocallySorted lt (x2 :: s2)
    → set_eq (x1 :: s1) (x2 :: s2)
      → x1 = x2 ∧ set_eq s1 s2
  intros x1 x2 s1 s2 LS1 LS2 [IN1 IN2].A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x1 :: s1 ⊆ x2 :: s2
IN2: x2 :: s2 ⊆ x1 :: s1
x1 = x2 ∧ set_eq s1 s2
  assert (x12 : x1 = x2).A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x1 :: s1 ⊆ x2 :: s2
IN2: x2 :: s2 ⊆ x1 :: s1
x1 = x2
A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x1 :: s1 ⊆ x2 :: s2
IN2: x2 :: s2 ⊆ x1 :: s1
x12: x1 = x2
x1 = x2 ∧ set_eq s1 s2
  {A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x1 :: s1 ⊆ x2 :: s2
IN2: x2 :: s2 ⊆ x1 :: s1
x1 = x2
    specialize (IN1 x1).A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x1 ∈ x1 :: s1 → x1 ∈ x2 :: s2
IN2: x2 :: s2 ⊆ x1 :: s1
x1 = x2
    rewrite 2 elem_of_cons in IN1.A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x1 = x1 ∨ x1 ∈ s1 → x1 = x2 ∨ x1 ∈ s2
IN2: x2 :: s2 ⊆ x1 :: s1
x1 = x2
    specialize (IN1 (or_introl (eq_refl x1))).A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x1 = x2 ∨ x1 ∈ s2
IN2: x2 :: s2 ⊆ x1 :: s1
x1 = x2
    destruct IN1; [done |].A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
IN2: x2 :: s2 ⊆ x1 :: s1
x1 = x2
    specialize (IN2 x2).A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
IN2: x2 ∈ x2 :: s2 → x2 ∈ x1 :: s1
x1 = x2
    rewrite 2 elem_of_cons in IN2.A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
IN2: x2 = x2 ∨ x2 ∈ s2 → x2 = x1 ∨ x2 ∈ s1
x1 = x2
    specialize (IN2 (or_introl (eq_refl x2))).A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
IN2: x2 = x1 ∨ x2 ∈ s1
x1 = x2
    destruct IN2; [by subst |].A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
H1: x2 ∈ s1
x1 = x2
    pose proof (LocallySorted_elem_of_lt x2 x1 s1 LS1 H1).A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
H1: x2 ∈ s1
H2: lt x1 x2
x1 = x2
    pose proof (LocallySorted_elem_of_lt x1 x2 s2 LS2 H0).A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
H1: x2 ∈ s1
H2: lt x1 x2
H3: lt x2 x1
x1 = x2
    pose proof (StrictOrder_Irreflexive x1) as ltIrr.A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
H1: x2 ∈ s1
H2: lt x1 x2
H3: lt x2 x1
ltIrr: complement lt x1 x1
x1 = x2
    destruct H as [Hirr Htr].A: Type
lt: relation A
Hirr: Irreflexive lt
Htr: Transitive lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
H0: x1 ∈ s2
H1: x2 ∈ s1
H2: lt x1 x2
H3: lt x2 x1
ltIrr: complement lt x1 x1
x1 = x2
    by pose proof (Htr x1 x2 x1 H2 H3) as Hlt.
  }A: Type
lt: relation A
H: StrictOrder lt
x1, x2: A
s1, s2: list A
LS1: LocallySorted lt (x1 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x1 :: s1 ⊆ x2 :: s2
IN2: x2 :: s2 ⊆ x1 :: s1
x12: x1 = x2
x1 = x2 ∧ set_eq s1 s2
  subst.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
x2 = x2 ∧ set_eq s1 s2
  split; [done |].A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
set_eq s1 s2
  split.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
s1 ⊆ s2
A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
s2 ⊆ s1
  -A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
s1 ⊆ s2 intros x Hx.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
x: A
Hx: x ∈ s1
x ∈ s2
    pose proof (LocallySorted_elem_of_lt x _ _ LS1 Hx).A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
x: A
Hx: x ∈ s1
H0: lt x2 x
x ∈ s2
    specialize (IN1 x).A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
x: A
IN1: x ∈ x2 :: s1 → x ∈ x2 :: s2
Hx: x ∈ s1
H0: lt x2 x
x ∈ s2
    rewrite elem_of_cons in IN1.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
x: A
IN1: x = x2 ∨ x ∈ s1 → x ∈ x2 :: s2
Hx: x ∈ s1
H0: lt x2 x
x ∈ s2
    specialize (IN1 (or_intror Hx)).A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
x: A
IN1: x ∈ x2 :: s2
Hx: x ∈ s1
H0: lt x2 x
x ∈ s2
    rewrite elem_of_cons in IN1.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
x: A
IN1: x = x2 ∨ x ∈ s2
Hx: x ∈ s1
H0: lt x2 x
x ∈ s2
    destruct IN1; [| done].A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
x: A
H1: x = x2
Hx: x ∈ s1
H0: lt x2 x
x ∈ s2
    subst.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
H0: lt x2 x2
Hx: x2 ∈ s1
x2 ∈ s2
    by apply StrictOrder_Irreflexive in H0.
  -A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
s2 ⊆ s1 intros x Hx.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
x: A
Hx: x ∈ s2
x ∈ s1
    pose proof (LocallySorted_elem_of_lt x _ _ LS2 Hx).A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN2: x2 :: s2 ⊆ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
x: A
Hx: x ∈ s2
H0: lt x2 x
x ∈ s1
    specialize (IN2 x).A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
x: A
IN2: x ∈ x2 :: s2 → x ∈ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
Hx: x ∈ s2
H0: lt x2 x
x ∈ s1
    rewrite elem_of_cons in IN2.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
x: A
IN2: x = x2 ∨ x ∈ s2 → x ∈ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
Hx: x ∈ s2
H0: lt x2 x
x ∈ s1
    specialize (IN2 (or_intror Hx)).A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
x: A
IN2: x ∈ x2 :: s1
IN1: x2 :: s1 ⊆ x2 :: s2
Hx: x ∈ s2
H0: lt x2 x
x ∈ s1
    rewrite elem_of_cons in IN2.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
x: A
IN2: x = x2 ∨ x ∈ s1
IN1: x2 :: s1 ⊆ x2 :: s2
Hx: x ∈ s2
H0: lt x2 x
x ∈ s1
    destruct IN2; [| done].A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
x: A
H1: x = x2
IN1: x2 :: s1 ⊆ x2 :: s2
Hx: x ∈ s2
H0: lt x2 x
x ∈ s1
    subst.A: Type
lt: relation A
H: StrictOrder lt
x2: A
s1, s2: list A
LS1: LocallySorted lt (x2 :: s1)
LS2: LocallySorted lt (x2 :: s2)
IN1: x2 :: s1 ⊆ x2 :: s2
H0: lt x2 x2
Hx: x2 ∈ s2
x2 ∈ s1
    by apply StrictOrder_Irreflexive in H0.
Qed.

Lemma set_equality_predicate {A}  {lt : relation A} `{StrictOrder A lt} :
  forall s1 s2,
  LocallySorted lt s1 ->
  LocallySorted lt s2 ->
  set_eq s1 s2 <-> s1 = s2.A: Type
lt: relation A
H: StrictOrder lt
∀ s1 s2 : list A,
  LocallySorted lt s1
  → LocallySorted lt s2 → set_eq s1 s2 ↔ s1 = s2
Proof.A: Type
lt: relation A
H: StrictOrder lt
∀ s1 s2 : list A,
  LocallySorted lt s1
  → LocallySorted lt s2 → set_eq s1 s2 ↔ s1 = s2
  intros s1 s2 LS1 LS2 .A: Type
lt: relation A
H: StrictOrder lt
s1, s2: list A
LS1: LocallySorted lt s1
LS2: LocallySorted lt s2
set_eq s1 s2 ↔ s1 = s2 rename H into SO.A: Type
lt: relation A
SO: StrictOrder lt
s1, s2: list A
LS1: LocallySorted lt s1
LS2: LocallySorted lt s2
set_eq s1 s2 ↔ s1 = s2
  assert (SO' := SO).A: Type
lt: relation A
SO: StrictOrder lt
s1, s2: list A
LS1: LocallySorted lt s1
LS2: LocallySorted lt s2
SO': StrictOrder lt
set_eq s1 s2 ↔ s1 = s2 destruct SO' as [IR TR].A: Type
lt: relation A
SO: StrictOrder lt
s1, s2: list A
LS1: LocallySorted lt s1
LS2: LocallySorted lt s2
IR: Irreflexive lt
TR: Transitive lt
set_eq s1 s2 ↔ s1 = s2
  split; [| by intros ->].A: Type
lt: relation A
SO: StrictOrder lt
s1, s2: list A
LS1: LocallySorted lt s1
LS2: LocallySorted lt s2
IR: Irreflexive lt
TR: Transitive lt
set_eq s1 s2 → s1 = s2
  generalize dependent s2.A: Type
lt: relation A
SO: StrictOrder lt
s1: list A
LS1: LocallySorted lt s1
IR: Irreflexive lt
TR: Transitive lt
∀ s2 : list A,
  LocallySorted lt s2 → set_eq s1 s2 → s1 = s2
  induction s1; destruct s2; intros; [done | | |].A: Type
lt: relation A
SO: StrictOrder lt
LS1: LocallySorted lt []
IR: Irreflexive lt
TR: Transitive lt
a: A
s2: list A
LS2: LocallySorted lt (a :: s2)
H: set_eq [] (a :: s2)
[] = a :: s2
A: Type
lt: relation A
SO: StrictOrder lt
a: A
s1: list A
LS1: LocallySorted lt (a :: s1)
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
LS2: LocallySorted lt []
H: set_eq (a :: s1) []
a :: s1 = []
A: Type
lt: relation A
SO: StrictOrder lt
a: A
s1: list A
LS1: LocallySorted lt (a :: s1)
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
a0: A
s2: list A
LS2: LocallySorted lt (a0 :: s2)
H: set_eq (a :: s1) (a0 :: s2)
a :: s1 = a0 :: s2
  -A: Type
lt: relation A
SO: StrictOrder lt
LS1: LocallySorted lt []
IR: Irreflexive lt
TR: Transitive lt
a: A
s2: list A
LS2: LocallySorted lt (a :: s2)
H: set_eq [] (a :: s2)
[] = a :: s2 by destruct H as [_ H]; apply list_nil_subseteq in H.
  -A: Type
lt: relation A
SO: StrictOrder lt
a: A
s1: list A
LS1: LocallySorted lt (a :: s1)
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
LS2: LocallySorted lt []
H: set_eq (a :: s1) []
a :: s1 = [] by destruct H as [H _]; apply list_nil_subseteq in H.
  -A: Type
lt: relation A
SO: StrictOrder lt
a: A
s1: list A
LS1: LocallySorted lt (a :: s1)
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
a0: A
s2: list A
LS2: LocallySorted lt (a0 :: s2)
H: set_eq (a :: s1) (a0 :: s2)
a :: s1 = a0 :: s2 apply (set_eq_first_equal a a0 s1 s2 LS1 LS2) in H.A: Type
lt: relation A
SO: StrictOrder lt
a: A
s1: list A
LS1: LocallySorted lt (a :: s1)
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
a0: A
s2: list A
LS2: LocallySorted lt (a0 :: s2)
H: a = a0 ∧ set_eq s1 s2
a :: s1 = a0 :: s2 destruct H; subst.A: Type
lt: relation A
SO: StrictOrder lt
s1: list A
a0: A
LS1: LocallySorted lt (a0 :: s1)
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
s2: list A
LS2: LocallySorted lt (a0 :: s2)
H0: set_eq s1 s2
a0 :: s1 = a0 :: s2
    apply Sorted_LocallySorted_iff, Sorted_inv in LS1 as [LS1 _].A: Type
lt: relation A
SO: StrictOrder lt
s1: list A
a0: A
LS1: Sorted lt s1
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
s2: list A
LS2: LocallySorted lt (a0 :: s2)
H0: set_eq s1 s2
a0 :: s1 = a0 :: s2
    apply Sorted_LocallySorted_iff in LS1.A: Type
lt: relation A
SO: StrictOrder lt
s1: list A
a0: A
LS1: LocallySorted lt s1
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
s2: list A
LS2: LocallySorted lt (a0 :: s2)
H0: set_eq s1 s2
a0 :: s1 = a0 :: s2
    apply Sorted_LocallySorted_iff, Sorted_inv in LS2 as [LS2 _].A: Type
lt: relation A
SO: StrictOrder lt
s1: list A
a0: A
LS1: LocallySorted lt s1
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
s2: list A
LS2: Sorted lt s2
H0: set_eq s1 s2
a0 :: s1 = a0 :: s2
    apply Sorted_LocallySorted_iff in LS2.A: Type
lt: relation A
SO: StrictOrder lt
s1: list A
a0: A
LS1: LocallySorted lt s1
IR: Irreflexive lt
TR: Transitive lt
IHs1: LocallySorted lt s1
→ ∀ s2 : list A,
    LocallySorted lt s2
    → set_eq s1 s2 → s1 = s2
s2: list A
LS2: LocallySorted lt s2
H0: set_eq s1 s2
a0 :: s1 = a0 :: s2
    by apply (IHs1 LS1 s2 LS2) in H0; subst.
Qed.

(* [Transitive] isn't necessary but makes the proof simpler. *)

Lemma lsorted_app
  {A : Type}
  (l : list A)
  (R : A -> A -> Prop)
  (Hsorted : LocallySorted R l)
  (Htransitive : Transitive R)
  (alfa beta : list A)
  (Hconcat : l = alfa ++ beta) :
  LocallySorted R alfa /\ LocallySorted R beta.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
alfa, beta: list A
Hconcat: l = alfa ++ beta
LocallySorted R alfa ∧ LocallySorted R beta
Proof.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
alfa, beta: list A
Hconcat: l = alfa ++ beta
LocallySorted R alfa ∧ LocallySorted R beta
  generalize dependent l.A: Type
R: A → A → Prop
Htransitive: Transitive R
alfa, beta: list A
∀ l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa ∧ LocallySorted R beta
  generalize dependent beta.A: Type
R: A → A → Prop
Htransitive: Transitive R
alfa: list A
∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa ∧ LocallySorted R beta
  induction alfa.A: Type
R: A → A → Prop
Htransitive: Transitive R
∀ beta l : list A,
  LocallySorted R l
  → l = [] ++ beta
    → LocallySorted R [] ∧ LocallySorted R beta
A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
∀ beta l : list A,
  LocallySorted R l
  → l = (a :: alfa) ++ beta
    → LocallySorted R (a :: alfa)
      ∧ LocallySorted R beta
  -A: Type
R: A → A → Prop
Htransitive: Transitive R
∀ beta l : list A,
  LocallySorted R l
  → l = [] ++ beta
    → LocallySorted R [] ∧ LocallySorted R beta intros.A: Type
R: A → A → Prop
Htransitive: Transitive R
beta, l: list A
Hsorted: LocallySorted R l
Hconcat: l = [] ++ beta
LocallySorted R [] ∧ LocallySorted R beta
    split.A: Type
R: A → A → Prop
Htransitive: Transitive R
beta, l: list A
Hsorted: LocallySorted R l
Hconcat: l = [] ++ beta
LocallySorted R []
A: Type
R: A → A → Prop
Htransitive: Transitive R
beta, l: list A
Hsorted: LocallySorted R l
Hconcat: l = [] ++ beta
LocallySorted R beta
    +A: Type
R: A → A → Prop
Htransitive: Transitive R
beta, l: list A
Hsorted: LocallySorted R l
Hconcat: l = [] ++ beta
LocallySorted R [] by apply LSorted_nil.
    +A: Type
R: A → A → Prop
Htransitive: Transitive R
beta, l: list A
Hsorted: LocallySorted R l
Hconcat: l = [] ++ beta
LocallySorted R beta by simpl in *; rewrite Hconcat in Hsorted.
  -A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
∀ beta l : list A,
  LocallySorted R l
  → l = (a :: alfa) ++ beta
    → LocallySorted R (a :: alfa)
      ∧ LocallySorted R beta intros.A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
beta, l: list A
Hsorted: LocallySorted R l
Hconcat: l = (a :: alfa) ++ beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    apply Sorted_LocallySorted_iff in Hsorted.A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
beta, l: list A
Hsorted: Sorted R l
Hconcat: l = (a :: alfa) ++ beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    apply Sorted_StronglySorted in Hsorted; [| done].A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
beta, l: list A
Hsorted: StronglySorted R l
Hconcat: l = (a :: alfa) ++ beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    rewrite Hconcat in Hsorted.A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
beta, l: list A
Hsorted: StronglySorted R ((a :: alfa) ++ beta)
Hconcat: l = (a :: alfa) ++ beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    simpl in Hsorted.A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
beta, l: list A
Hsorted: StronglySorted R (a :: alfa ++ beta)
Hconcat: l = (a :: alfa) ++ beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    apply StronglySorted_inv in Hsorted.A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
beta, l: list A
Hsorted: StronglySorted R (alfa ++ beta)
∧ Forall (R a) (alfa ++ beta)
Hconcat: l = (a :: alfa) ++ beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    destruct Hsorted.A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa: list A
IHalfa: ∀ beta l : list A,
  LocallySorted R l
  → l = alfa ++ beta
    → LocallySorted R alfa
      ∧ LocallySorted R beta
beta, l: list A
H: StronglySorted R (alfa ++ beta)
H0: Forall (R a) (alfa ++ beta)
Hconcat: l = (a :: alfa) ++ beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    specialize (IHalfa beta (alfa ++ beta)).A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa, beta: list A
IHalfa: LocallySorted R (alfa ++ beta)
→ alfa ++ beta = alfa ++ beta
  → LocallySorted R alfa
    ∧ LocallySorted R beta
l: list A
H: StronglySorted R (alfa ++ beta)
H0: Forall (R a) (alfa ++ beta)
Hconcat: l = (a :: alfa) ++ beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    spec IHalfa; [by apply Sorted_LocallySorted_iff, StronglySorted_Sorted |].A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa, beta, l: list A
H: StronglySorted R (alfa ++ beta)
H0: Forall (R a) (alfa ++ beta)
Hconcat: l = (a :: alfa) ++ beta
IHalfa: alfa ++ beta = alfa ++ beta
→ LocallySorted R alfa ∧ LocallySorted R beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    destruct (IHalfa eq_refl).A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa, beta, l: list A
H: StronglySorted R (alfa ++ beta)
H0: Forall (R a) (alfa ++ beta)
Hconcat: l = (a :: alfa) ++ beta
IHalfa: alfa ++ beta = alfa ++ beta
→ LocallySorted R alfa ∧ LocallySorted R beta
H1: LocallySorted R alfa
H2: LocallySorted R beta
LocallySorted R (a :: alfa) ∧ LocallySorted R beta
    split; [| done].A: Type
R: A → A → Prop
Htransitive: Transitive R
a: A
alfa, beta, l: list A
H: StronglySorted R (alfa ++ beta)
H0: Forall (R a) (alfa ++ beta)
Hconcat: l = (a :: alfa) ++ beta
IHalfa: alfa ++ beta = alfa ++ beta
→ LocallySorted R alfa ∧ LocallySorted R beta
H1: LocallySorted R alfa
H2: LocallySorted R beta
LocallySorted R (a :: alfa)
    destruct alfa; constructor; [done |].A: Type
R: A → A → Prop
Htransitive: Transitive R
a, a0: A
alfa, beta, l: list A
H: StronglySorted R ((a0 :: alfa) ++ beta)
H0: Forall (R a) ((a0 :: alfa) ++ beta)
Hconcat: l = (a :: a0 :: alfa) ++ beta
IHalfa: (a0 :: alfa) ++ beta = (a0 :: alfa) ++ beta
→ LocallySorted R (a0 :: alfa)
  ∧ LocallySorted R beta
H1: LocallySorted R (a0 :: alfa)
H2: LocallySorted R beta
R a a0
    rewrite Forall_forall in H0.A: Type
R: A → A → Prop
Htransitive: Transitive R
a, a0: A
alfa, beta, l: list A
H: StronglySorted R ((a0 :: alfa) ++ beta)
H0: ∀ x : A, x ∈ (a0 :: alfa) ++ beta → R a x
Hconcat: l = (a :: a0 :: alfa) ++ beta
IHalfa: (a0 :: alfa) ++ beta = (a0 :: alfa) ++ beta
→ LocallySorted R (a0 :: alfa)
  ∧ LocallySorted R beta
H1: LocallySorted R (a0 :: alfa)
H2: LocallySorted R beta
R a a0
    apply H0; left.
Qed.

Lemma lsorted_pairwise_ordered
  {A : Type}
  (l : list A)
  (R : A -> A -> Prop)
  (Hsorted : LocallySorted R l)
  (Htransitive : Transitive R)
  (x y : A)
  (alfa beta gamma : list A)
  (Hconcat : l = alfa ++ [x] ++ beta ++ [y] ++ gamma) :
  R x y.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hconcat: l = alfa ++ [x] ++ beta ++ [y] ++ gamma
R x y
Proof.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hconcat: l = alfa ++ [x] ++ beta ++ [y] ++ gamma
R x y
  apply (lsorted_app _ _ Hsorted _ alfa) in Hconcat.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hconcat: LocallySorted R alfa
∧ LocallySorted R
    ([x] ++ beta ++ [y] ++ gamma)
R x y
  destruct Hconcat as [_ Hneed].A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hneed: LocallySorted R ([x] ++ beta ++ [y] ++ gamma)
R x y
  simpl in Hneed.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hneed: LocallySorted R (x :: beta ++ y :: gamma)
R x y
  rewrite <- Sorted_LocallySorted_iff in Hneed.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hneed: Sorted R (x :: beta ++ y :: gamma)
R x y
  apply Sorted_extends in Hneed; [| done].A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hneed: Forall (R x) (beta ++ y :: gamma)
R x y
  rewrite Forall_forall in Hneed.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hneed: ∀ x0 : A, x0 ∈ beta ++ y :: gamma → R x x0
R x y
  specialize (Hneed y).A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hneed: y ∈ beta ++ y :: gamma → R x y
R x y
  spec Hneed; [| done].A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
alfa, beta, gamma: list A
Hneed: y ∈ beta ++ y :: gamma → R x y
y ∈ beta ++ y :: gamma
  by apply elem_of_app; right; left.
Qed.

Lemma lsorted_pair_wise_unordered
  {A : Type}
  (l : list A)
  (R : A -> A -> Prop)
  (Hsorted : LocallySorted R l)
  (Htransitive : Transitive R)
  (x y : A)
  (Hin_x : x ∈ l)
  (Hin_y : y ∈ l) :
  x = y \/ R x y \/ R y x.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
Hin_x: x ∈ l
Hin_y: y ∈ l
x = y ∨ R x y ∨ R y x
Proof.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
Hin_x: x ∈ l
Hin_y: y ∈ l
x = y ∨ R x y ∨ R y x
  apply elem_of_list_split in Hin_x.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
Hin_x: ∃ l1 l2 : list A, l = l1 ++ x :: l2
Hin_y: y ∈ l
x = y ∨ R x y ∨ R y x
  destruct Hin_x as [pref1 [suf1 Hconcat1]].A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ l
x = y ∨ R x y ∨ R y x
  rewrite Hconcat1 in Hin_y.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1 ++ x :: suf1
x = y ∨ R x y ∨ R y x
  apply elem_of_app in Hin_y.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1 ∨ y ∈ x :: suf1
x = y ∨ R x y ∨ R y x
  rewrite elem_of_cons in Hin_y.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1 ∨ y = x ∨ y ∈ suf1
x = y ∨ R x y ∨ R y x
  assert (y =x \/ y ∈ pref1 ++ suf1).A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1 ∨ y = x ∨ y ∈ suf1
y = x ∨ y ∈ pref1 ++ suf1
A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1 ∨ y = x ∨ y ∈ suf1
H: y = x ∨ y ∈ pref1 ++ suf1
x = y ∨ R x y ∨ R y x {A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1 ∨ y = x ∨ y ∈ suf1
y = x ∨ y ∈ pref1 ++ suf1
    destruct Hin_y as [Hin_y | Hin_y]; [| destruct Hin_y].A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1
y = x ∨ y ∈ pref1 ++ suf1
A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y = x
y = x ∨ y ∈ pref1 ++ suf1
A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y ∈ suf1
y = x ∨ y ∈ pref1 ++ suf1
    -A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1
y = x ∨ y ∈ pref1 ++ suf1 by right; apply elem_of_app; left.
    -A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y = x
y = x ∨ y ∈ pref1 ++ suf1 by left.
    -A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y ∈ suf1
y = x ∨ y ∈ pref1 ++ suf1 by right; apply elem_of_app; right.
  }A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1 ∨ y = x ∨ y ∈ suf1
H: y = x ∨ y ∈ pref1 ++ suf1
x = y ∨ R x y ∨ R y x
  clear Hin_y.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y = x ∨ y ∈ pref1 ++ suf1
x = y ∨ R x y ∨ R y x
  rename H into Hin_y.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y = x ∨ y ∈ pref1 ++ suf1
x = y ∨ R x y ∨ R y x
  destruct Hin_y as [Hin_y | Hin_y]; [by left |].A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
Hin_y: y ∈ pref1 ++ suf1
x = y ∨ R x y ∨ R y x
  apply elem_of_app in Hin_y; destruct Hin_y.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y ∈ pref1
x = y ∨ R x y ∨ R y x
A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y ∈ suf1
x = y ∨ R x y ∨ R y x
  -A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y ∈ pref1
x = y ∨ R x y ∨ R y x apply elem_of_list_split in H.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: ∃ l1 l2 : list A, pref1 = l1 ++ y :: l2
x = y ∨ R x y ∨ R y x
    destruct H as [pref2 [suf2 Hconcat2]].A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
pref2, suf2: list A
Hconcat2: pref1 = pref2 ++ y :: suf2
x = y ∨ R x y ∨ R y x
    rewrite Hconcat2 in Hconcat1.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1, pref2, suf2: list A
Hconcat1: l = (pref2 ++ y :: suf2) ++ x :: suf1
Hconcat2: pref1 = pref2 ++ y :: suf2
x = y ∨ R x y ∨ R y x
    rewrite <- app_assoc in Hconcat1.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1, pref2, suf2: list A
Hconcat1: l = pref2 ++ (y :: suf2) ++ x :: suf1
Hconcat2: pref1 = pref2 ++ y :: suf2
x = y ∨ R x y ∨ R y x
    specialize (lsorted_pairwise_ordered l R Hsorted Htransitive y x pref2 suf2 suf1 Hconcat1).A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1, pref2, suf2: list A
Hconcat1: l = pref2 ++ (y :: suf2) ++ x :: suf1
Hconcat2: pref1 = pref2 ++ y :: suf2
R y x → x = y ∨ R x y ∨ R y x
    by intros; right; right.
  -A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: y ∈ suf1
x = y ∨ R x y ∨ R y x apply elem_of_list_split in H.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
H: ∃ l1 l2 : list A, suf1 = l1 ++ y :: l2
x = y ∨ R x y ∨ R y x
    destruct H as [pref2 [suf2 Hconcat2]].A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1: list A
Hconcat1: l = pref1 ++ x :: suf1
pref2, suf2: list A
Hconcat2: suf1 = pref2 ++ y :: suf2
x = y ∨ R x y ∨ R y x
    rewrite Hconcat2 in Hconcat1.A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1, pref2, suf2: list A
Hconcat1: l = pref1 ++ x :: pref2 ++ y :: suf2
Hconcat2: suf1 = pref2 ++ y :: suf2
x = y ∨ R x y ∨ R y x
    specialize (lsorted_pairwise_ordered l R Hsorted Htransitive x y pref1 pref2 suf2 Hconcat1).A: Type
l: list A
R: A → A → Prop
Hsorted: LocallySorted R l
Htransitive: Transitive R
x, y: A
pref1, suf1, pref2, suf2: list A
Hconcat1: l = pref1 ++ x :: pref2 ++ y :: suf2
Hconcat2: suf1 = pref2 ++ y :: suf2
R x y → x = y ∨ R x y ∨ R y x
    by intros; right; left.
Qed.