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 VLSM.Lib Require Import Preamble ListExtras ListSetExtras StdppListSet StdppExtras.

Utility: Topological Sorting

This module implements an algorithm producing a linear extension for a given partial order using an approach similar to that of Kahn's topological sorting algorithm.

The algorithm extracts an element with a minimal number of predecessors among the current elements, then recurses on the remaining elements.

To begin with, we assume an unconstrained precedes function to say whether an element precedes another. The proofs will show that if precedes determines a strict order on the set of elements in the list, then the top_sort algorithm produces a linear extension of that ordering (Lemmas top_sort_precedes and top_sort_precedes_before).

Section sec_min_predecessors.

Finding an element with a minimal number of predecessors

For this section we will fix a list l and count the predecessors occurring in that list.

Context
  {A : Type}
  (precedes : relation A)
  `{!RelDecision precedes}
  (l : list A)
  .

Definition count_predecessors
  (a : A)
  : nat
  := length (filter (fun b => precedes b a) l).

Lemma zero_predecessors
  (a : A)
  (Ha : count_predecessors a = 0)
  : Forall (fun b => ~ precedes b a) l.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
Ha: count_predecessors a = 0
Forall (λ b : A, ¬ precedes b a) l
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
Ha: count_predecessors a = 0
Forall (λ b : A, ¬ precedes b a) l
  apply length_zero_iff_nil in Ha.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
Ha: filter (λ b : A, precedes b a) l = []
Forall (λ b : A, ¬ precedes b a) l
  apply Forall_filter_nil in Ha.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
Ha: Forall (λ a0 : A, ¬ precedes a0 a) l
Forall (λ b : A, ¬ precedes b a) l
  by apply Ha.
Qed.

Finds an element minimizing count_predecessors in min :: remainder.

Fixpoint min_predecessors
  (remainder : list A)
  (min : A)
  : A
  :=
  match remainder with
  | [] => min
  | h :: t =>
    if decide (count_predecessors h < count_predecessors min)
    then min_predecessors t h
    else min_predecessors t min
  end.

Lemma min_predecessors_in
  (l' : list A)
  (a : A)
  (min := min_predecessors l' a)
  : min = a \/ min ∈ l'.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
a: A
min:= min_predecessors l' a: A
min = a ∨ min ∈ l'
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
a: A
min:= min_predecessors l' a: A
min = a ∨ min ∈ l'
  unfold min; clear min.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
a: A
min_predecessors l' a = a ∨ min_predecessors l' a ∈ l' revert a.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
∀ a : A,
  min_predecessors l' a = a
  ∨ min_predecessors l' a ∈ l'
  induction l'.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
∀ a : A,
  min_predecessors [] a = a
  ∨ min_predecessors [] a ∈ []
A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a : A,
  min_predecessors l' a = a
  ∨ min_predecessors l' a ∈ l'
∀ a0 : A,
  min_predecessors (a :: l') a0 = a0
  ∨ min_predecessors (a :: l') a0 ∈ a :: l'
  -A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
∀ a : A,
  min_predecessors [] a = a
  ∨ min_predecessors [] a ∈ [] by intros; left.
  -A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a : A,
  min_predecessors l' a = a
  ∨ min_predecessors l' a ∈ l'
∀ a0 : A,
  min_predecessors (a :: l') a0 = a0
  ∨ min_predecessors (a :: l') a0 ∈ a :: l' intro a0.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a : A,
  min_predecessors l' a = a
  ∨ min_predecessors l' a ∈ l'
a0: A
min_predecessors (a :: l') a0 = a0
∨ min_predecessors (a :: l') a0 ∈ a :: l' simpl.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a : A,
  min_predecessors l' a = a
  ∨ min_predecessors l' a ∈ l'
a0: A
(if
  decide
    (count_predecessors a < count_predecessors a0)
 then min_predecessors l' a
 else min_predecessors l' a0) = a0
∨ (if
    decide
      (count_predecessors a < count_predecessors a0)
   then min_predecessors l' a
   else min_predecessors l' a0) ∈ a :: l'
    by destruct (decide (count_predecessors a < count_predecessors a0));
      [destruct (IHl' a) | destruct (IHl' a0)]; rewrite elem_of_cons; itauto.
Qed.

Lemma min_predecessors_correct
  (l' : list A)
  (a : A)
  (min := min_predecessors l' a)
  (mins := count_predecessors min)
  : Forall (fun b => mins <= count_predecessors b) (a :: l').A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
a: A
min:= min_predecessors l' a: A
mins:= count_predecessors min: nat
Forall (λ b : A, mins ≤ count_predecessors b)
  (a :: l')
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
a: A
min:= min_predecessors l' a: A
mins:= count_predecessors min: nat
Forall (λ b : A, mins ≤ count_predecessors b)
  (a :: l')
  unfold mins, min; clear mins min.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
a: A
Forall
  (λ b : A,
     count_predecessors (min_predecessors l' a)
     ≤ count_predecessors b) (a :: l')
  rewrite Forall_forall.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
a: A
∀ x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
  revert a.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l, l': list A
∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
  induction l'; intros a0 x Hin; [by cbn; apply elem_of_list_singleton in Hin as -> |].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0, x: A
Hin: x ∈ a0 :: a :: l'
count_predecessors (min_predecessors (a :: l') a0)
≤ count_predecessors x
  apply elem_of_cons in Hin as [-> | Hin]; cbn.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
count_predecessors
  (if
    decide
      (count_predecessors a < count_predecessors a0)
   then min_predecessors l' a
   else min_predecessors l' a0)
≤ count_predecessors a0
A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0, x: A
Hin: x ∈ a :: l'
count_predecessors
  (if
    decide
      (count_predecessors a < count_predecessors a0)
   then min_predecessors l' a
   else min_predecessors l' a0) ≤ 
count_predecessors x
  -A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
count_predecessors
  (if
    decide
      (count_predecessors a < count_predecessors a0)
   then min_predecessors l' a
   else min_predecessors l' a0)
≤ count_predecessors a0 destruct (decide (count_predecessors a < count_predecessors a0)).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
l0: count_predecessors a < count_predecessors a0
count_predecessors (min_predecessors l' a)
≤ count_predecessors a0
A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
n: ¬ count_predecessors a < count_predecessors a0
count_predecessors (min_predecessors l' a0)
≤ count_predecessors a0
    +A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
l0: count_predecessors a < count_predecessors a0
count_predecessors (min_predecessors l' a)
≤ count_predecessors a0 transitivity (count_predecessors a); [| lia].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
l0: count_predecessors a < count_predecessors a0
count_predecessors (min_predecessors l' a)
≤ count_predecessors a
      by apply IHl'; left.
    +A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
n: ¬ count_predecessors a < count_predecessors a0
count_predecessors (min_predecessors l' a0)
≤ count_predecessors a0 by apply IHl'; left.
  -A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0, x: A
Hin: x ∈ a :: l'
count_predecessors
  (if
    decide
      (count_predecessors a < count_predecessors a0)
   then min_predecessors l' a
   else min_predecessors l' a0) ≤ count_predecessors x destruct (decide (count_predecessors a < count_predecessors a0)); [by apply IHl' |].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0, x: A
Hin: x ∈ a :: l'
n: ¬ count_predecessors a < count_predecessors a0
count_predecessors (min_predecessors l' a0)
≤ count_predecessors x
    apply not_lt in n; unfold ge in n.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0, x: A
Hin: x ∈ a :: l'
n: count_predecessors a0 ≤ count_predecessors a
count_predecessors (min_predecessors l' a0)
≤ count_predecessors x
    apply elem_of_cons in Hin as [-> | Hin].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
n: count_predecessors a0 ≤ count_predecessors a
count_predecessors (min_predecessors l' a0)
≤ count_predecessors a
A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0, x: A
Hin: x ∈ l'
n: count_predecessors a0 ≤ count_predecessors a
count_predecessors (min_predecessors l' a0)
≤ count_predecessors x
    +A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
n: count_predecessors a0 ≤ count_predecessors a
count_predecessors (min_predecessors l' a0)
≤ count_predecessors a transitivity (count_predecessors a0); [| lia].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0: A
n: count_predecessors a0 ≤ count_predecessors a
count_predecessors (min_predecessors l' a0)
≤ count_predecessors a0
      by apply IHl'; left.
    +A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
a: A
l': list A
IHl': ∀ a x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
a0, x: A
Hin: x ∈ l'
n: count_predecessors a0 ≤ count_predecessors a
count_predecessors (min_predecessors l' a0)
≤ count_predecessors x by apply IHl'; right.
Qed.

Given P a property on A, precedes_P is the relation induced by precedes on the subset of A determined by P.

Definition precedes_P
  (P : A -> Prop)
  (x y : sig P)
  : Prop
  := precedes (proj1_sig x) (proj1_sig y).

In what follows, let us fix a property P satisfied by all elements of l, such that precedes_P P is a StrictOrder.

Consequently, this means that precedes is a StrictOrder on the elements of l.

Context
  (P : A -> Prop)
  (HPl : Forall P l)
  {Hso : StrictOrder (precedes_P P)}
  .

Next we derive easier to work with formulations for the StrictOrder properties associated with precedes_P.

Lemma precedes_irreflexive
  (a : A)
  (Ha : P a)
  : ~ precedes a a.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a: A
Ha: P a
¬ precedes a a
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a: A
Ha: P a
¬ precedes a a
  specialize (StrictOrder_Irreflexive (exist P a Ha)).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a: A
Ha: P a
complement (precedes_P P) (a ↾ Ha) (a ↾ Ha)
→ ¬ precedes a a
  unfold complement; unfold precedes_P; simpl; intro Hirr.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a: A
Ha: P a
Hirr: precedes a a → False
¬ precedes a a
  by destruct (decide (precedes a a)).
Qed.

Lemma precedes_asymmetric
  (a b : A)
  (Ha : P a)
  (Hb : P b)
  (Hab : precedes a b)
  : ~ precedes b a.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a, b: A
Ha: P a
Hb: P b
Hab: precedes a b
¬ precedes b a
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a, b: A
Ha: P a
Hb: P b
Hab: precedes a b
¬ precedes b a
  intro Hba.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a, b: A
Ha: P a
Hb: P b
Hab: precedes a b
Hba: precedes b a
False
  exact
    (StrictOrder_Asymmetric Hso
      (exist P a Ha) (exist P b Hb)
      Hab Hba).
Qed.

Lemma precedes_transitive
  (a b c : A)
  (Ha : P a)
  (Hb : P b)
  (Hc : P c)
  (Hab : precedes a b)
  (Hbc : precedes b c)
  : precedes a c.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a, b, c: A
Ha: P a
Hb: P b
Hc: P c
Hab: precedes a b
Hbc: precedes b c
precedes a c
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
a, b, c: A
Ha: P a
Hb: P b
Hc: P c
Hab: precedes a b
Hbc: precedes b c
precedes a c
  exact
    (RelationClasses.StrictOrder_Transitive
      (exist P a Ha) (exist P b Hb) (exist P c Hc)
      Hab Hbc).
Qed.

If precedes is a StrictOrder on l, then there must exist an element of l with no predecessors in l.

Lemma count_predecessors_zero
  (Hl : l <> [])
  : Exists (fun a => count_predecessors a = 0) l.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
Hl: l ≠ []
Exists (λ a : A, count_predecessors a = 0) l
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
Hl: l ≠ []
Exists (λ a : A, count_predecessors a = 0) l
  unfold count_predecessors.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
Hl: l ≠ []
Exists
  (λ a : A,
     length (filter (λ b : A, precedes b a) l) = 0) l
  induction l; [done |].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
HPl: Forall P (a :: l0)
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: Forall P l0
→ l0 ≠ []
  → Exists
      (λ a : A,
         length
           (filter (λ b : A, precedes b a) l0) =
         0) l0
Exists
  (λ a0 : A,
     length
       (filter (λ b : A, precedes b a0) (a :: l0)) = 0)
  (a :: l0)
  inversion_clear HPl as [| ? ? HPa HPl0].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: Forall P l0
→ l0 ≠ []
  → Exists
      (λ a : A,
         length
           (filter (λ b : A, precedes b a) l0) =
         0) l0
HPa: P a
HPl0: Forall P l0
Exists
  (λ a0 : A,
     length
       (filter (λ b : A, precedes b a0) (a :: l0)) = 0)
  (a :: l0)
  specialize (IHl0 HPl0).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: l0 ≠ []
→ Exists
    (λ a : A,
       length
         (filter (λ b : A, precedes b a) l0) =
       0) l0
HPa: P a
HPl0: Forall P l0
Exists
  (λ a0 : A,
     length
       (filter (λ b : A, precedes b a0) (a :: l0)) = 0)
  (a :: l0)
  apply Exists_cons.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: l0 ≠ []
→ Exists
    (λ a : A,
       length
         (filter (λ b : A, precedes b a) l0) =
       0) l0
HPa: P a
HPl0: Forall P l0
length (filter (λ b : A, precedes b a) (a :: l0)) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  rewrite filter_cons.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: l0 ≠ []
→ Exists
    (λ a : A,
       length
         (filter (λ b : A, precedes b a) l0) =
       0) l0
HPa: P a
HPl0: Forall P l0
length
  (if decide (precedes a a)
   then a :: filter (λ b : A, precedes b a) l0
   else filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  destruct (decide (precedes a a)); [by contradict p; apply precedes_irreflexive |].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: l0 ≠ []
→ Exists
    (λ a : A,
       length
         (filter (λ b : A, precedes b a) l0) =
       0) l0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  assert ({ l0=[] }+{l0 <> [] }) by (destruct l0; clear; [left | right]; congruence).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: l0 ≠ []
→ Exists
    (λ a : A,
       length
         (filter (λ b : A, precedes b a) l0) =
       0) l0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
H: {l0 = []} + {l0 ≠ []}
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  destruct H as [? | Hl0]; [subst l0 |]; [by left |].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: l0 ≠ []
→ Exists
    (λ a : A,
       length
         (filter (λ b : A, precedes b a) l0) =
       0) l0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  specialize (IHl0 Hl0).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: Exists
  (λ a : A,
     length (filter (λ b : A, precedes b a) l0) =
     0) l0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  apply Exists_exists in IHl0.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
IHl0: ∃ x : A,
  x ∈ l0
  ∧ length (filter (λ b : A, precedes b x) l0) =
    0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  destruct IHl0 as [x [Hin Hlen]].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  destruct (decide (precedes a x)).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
n0: ¬ precedes a x
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0
  -A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0 left.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
length (filter (λ b : A, precedes b a) l0) = 0
    specialize (Forall_forall P l0); intros [Hall _].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: Forall P l0 → ∀ x : A, x ∈ l0 → P x
length (filter (λ b : A, precedes b a) l0) = 0
    specialize (Hall HPl0 x Hin).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: P x
length (filter (λ b : A, precedes b a) l0) = 0
    match goal with |- ?X = 0  => cut (X <= 0) end; [by lia |].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: P x
length (filter (λ b : A, precedes b a) l0) ≤ 0
    rewrite <- Hlen; clear Hlen.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: P x
length (filter (λ b : A, precedes b a) l0)
≤ length (filter (λ b : A, precedes b x) l0)
    apply filter_length_fn.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: P x
Forall (λ a0 : A, precedes a0 a → precedes a0 x) l0
    revert HPl0.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
HPa: P a
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: P x
Forall P l0
→ Forall (λ a0 : A, precedes a0 a → precedes a0 x) l0
    intro.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
HPa: P a
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: P x
HPl0: Forall P l0
Forall (λ a0 : A, precedes a0 a → precedes a0 x) l0
    apply (Forall_impl P); [done |].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
HPa: P a
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: P x
HPl0: Forall P l0
∀ x0 : A, P x0 → precedes x0 a → precedes x0 x
    intros.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
HPa: P a
n: ¬ precedes a a
Hl0: l0 ≠ []
p: precedes a x
Hall: P x
HPl0: Forall P l0
x0: A
H: P x0
H0: precedes x0 a
precedes x0 x
    by apply precedes_transitive with a.
  -A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
n0: ¬ precedes a x
length (filter (λ b : A, precedes b a) l0) = 0
∨ Exists
    (λ a0 : A,
       length
         (filter (λ b : A, precedes b a0) (a :: l0)) =
       0) l0 right.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
n0: ¬ precedes a x
Exists
  (λ a0 : A,
     length
       (filter (λ b : A, precedes b a0) (a :: l0)) = 0)
  l0 apply Exists_exists.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
n0: ¬ precedes a x
∃ x : A,
  x ∈ l0
  ∧ length (filter (λ b : A, precedes b x) (a :: l0)) =
    0 exists x.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
n0: ¬ precedes a x
x ∈ l0
∧ length (filter (λ b : A, precedes b x) (a :: l0)) =
  0
    rewrite filter_cons.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
a: A
l0: list A
Hso: StrictOrder (precedes_P P)
Hl: a :: l0 ≠ []
x: A
Hin: x ∈ l0
Hlen: length (filter (λ b : A, precedes b x) l0) = 0
HPa: P a
HPl0: Forall P l0
n: ¬ precedes a a
Hl0: l0 ≠ []
n0: ¬ precedes a x
x ∈ l0
∧ length
    (if decide (precedes a x)
     then a :: filter (λ b : A, precedes b x) l0
     else filter (λ b : A, precedes b x) l0) = 0
    by destruct (decide (precedes a x)).
Qed.

Hence, computing min_predecessors on l yields an element with no predecessors.

Lemma min_predecessors_zero
  (l' : list A)
  (a : A)
  (Hl : l = a :: l')
  (min := min_predecessors l' a)
  : count_predecessors min = 0.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
count_predecessors min = 0
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
count_predecessors min = 0
  assert (Hl' : l <> []) by (intro H; rewrite Hl in H; inversion H).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
Hl': l ≠ []
count_predecessors min = 0
  specialize (count_predecessors_zero Hl'); intro Hx.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
Hl': l ≠ []
Hx: Exists (λ a : A, count_predecessors a = 0) l
count_predecessors min = 0
  apply Exists_exists in Hx.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
Hl': l ≠ []
Hx: ∃ x : A, x ∈ l ∧ count_predecessors x = 0
count_predecessors min = 0 destruct Hx as [x [Hinx Hcountx]].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
Hl': l ≠ []
x: A
Hinx: x ∈ l
Hcountx: count_predecessors x = 0
count_predecessors min = 0
  specialize (min_predecessors_correct l' a); simpl; intro Hall.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
Hl': l ≠ []
x: A
Hinx: x ∈ l
Hcountx: count_predecessors x = 0
Hall: Forall
  (λ b : A,
     count_predecessors (min_predecessors l' a)
     ≤ count_predecessors b) 
  (a :: l')
count_predecessors min = 0
  rewrite Forall_forall in Hall.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
Hl': l ≠ []
x: A
Hinx: x ∈ l
Hcountx: count_predecessors x = 0
Hall: ∀ x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
count_predecessors min = 0
  rewrite Hl in Hinx.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
HPl: Forall P l
Hso: StrictOrder (precedes_P P)
l': list A
a: A
Hl: l = a :: l'
min:= min_predecessors l' a: A
Hl': l ≠ []
x: A
Hinx: x ∈ a :: l'
Hcountx: count_predecessors x = 0
Hall: ∀ x : A,
  x ∈ a :: l'
  → count_predecessors (min_predecessors l' a)
    ≤ count_predecessors x
count_predecessors min = 0
  by specialize (Hall x Hinx); unfold min; lia.
Qed.

End sec_min_predecessors.

#[export] Instance precedes_P_transitive
  `{Transitive A preceeds} (P : A -> Prop)
  : Transitive (precedes_P preceeds P).A: Type
preceeds: relation A
H: Transitive preceeds
P: A → Prop
Transitive (precedes_P preceeds P)
Proof.A: Type
preceeds: relation A
H: Transitive preceeds
P: A → Prop
Transitive (precedes_P preceeds P)
  intros [x Hx] [y Hy] [z Hz]; unfold precedes_P.A: Type
preceeds: relation A
H: Transitive preceeds
P: A → Prop
x: A
Hx: P x
y: A
Hy: P y
z: A
Hz: P z
preceeds (`(x ↾ Hx)) (`(y ↾ Hy))
→ preceeds (`(y ↾ Hy)) (`(z ↾ Hz))
  → preceeds (`(x ↾ Hx)) (`(z ↾ Hz))
  by etransitivity.
Qed.

#[export] Instance precedes_P_irreflexive
  `{Irreflexive A preceeds} (P : A -> Prop)
  : Irreflexive (precedes_P preceeds P).A: Type
preceeds: relation A
H: Irreflexive preceeds
P: A → Prop
Irreflexive (precedes_P preceeds P)
Proof.A: Type
preceeds: relation A
H: Irreflexive preceeds
P: A → Prop
Irreflexive (precedes_P preceeds P)
  intros [x Hx]; unfold precedes_P, complement; cbn.A: Type
preceeds: relation A
H: Irreflexive preceeds
P: A → Prop
x: A
Hx: P x
preceeds x x → False
  by apply irreflexivity.
Qed.

#[export] Instance precedes_P_strict
  `{StrictOrder A preceeds} (P : A -> Prop)
  : StrictOrder (precedes_P preceeds P).A: Type
preceeds: relation A
H: StrictOrder preceeds
P: A → Prop
StrictOrder (precedes_P preceeds P)
Proof.A: Type
preceeds: relation A
H: StrictOrder preceeds
P: A → Prop
StrictOrder (precedes_P preceeds P)
  by split; typeclasses eauto.
Qed.

Section sec_topologically_sorted.

Definition and properties of topologically sorted lists

Context
  {A : Type}
  (precedes : relation A)
  `{!RelDecision precedes}
  (l : list A)
  .

We say that a list l is topologically_sorted w.r.t a precedes relation iff a precedes b implies that a cannot occur after b in l.

Definition topologically_sorted
  :=
  forall
    (a b : A)
    (Hab : precedes a b)
    (l1 l2 : list A)
    (Heq : l = l1 ++ [b] ++ l2)
    , a ∉ l2.

The following properties assume that precedes determines a StrictOrder on the list.

Context
  (P : A -> Prop)
  {Hso : StrictOrder (precedes_P precedes P)}
  .

Section sec_topologically_sorted_fixed_list.

Context
  (Hl : Forall P l)
  (Hts : topologically_sorted)
  .

If l is topologically_sorted, then for any occurrences of a and b in l such that a precedes b it must be that the occurrence of a is before that of b.

Hence all occurrences of a must be before all occurrences of b in a topologically_sorted list.

Lemma topologically_sorted_occurrences_ordering
  (a b : A)
  (Hab : precedes a b)
  (la1 la2 : list A)
  (Heqa : l = la1 ++ [a] ++ la2)
  (lb1 lb2 : list A)
  (Heqb : l = lb1 ++ [b] ++ lb2)
  : exists (lab : list A), lb1 = la1 ++ a :: lab.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
∃ lab : list A, lb1 = la1 ++ a :: lab
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
∃ lab : list A, lb1 = la1 ++ a :: lab
  assert (Hpa : P a).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
P a
A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
Hpa: P a
∃ lab : list A, lb1 = la1 ++ a :: lab
  {A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
P a rewrite Forall_forall in Hl.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: ∀ x : A, x ∈ l → P x
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
P a apply Hl.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: ∀ x : A, x ∈ l → P x
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
a ∈ l rewrite Heqa, !elem_of_app, elem_of_list_singleton.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: ∀ x : A, x ∈ l → P x
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
a ∈ la1 ∨ a = a ∨ a ∈ la2 auto. }A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1, lb2: list A
Heqb: l = lb1 ++ [b] ++ lb2
Hpa: P a
∃ lab : list A, lb1 = la1 ++ a :: lab
  specialize (Hts a b Hab lb1 lb2 Heqb).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: l = lb1 ++ [b] ++ lb2
Hpa: P a
∃ lab : list A, lb1 = la1 ++ a :: lab
  rewrite Heqa in Heqb.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: la1 ++ [a] ++ la2 = lb1 ++ [b] ++ lb2
Hpa: P a
∃ lab : list A, lb1 = la1 ++ a :: lab
  assert (Ha : a ∉ b :: lb2).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: la1 ++ [a] ++ la2 = lb1 ++ [b] ++ lb2
Hpa: P a
a ∉ b :: lb2
A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: la1 ++ [a] ++ la2 = lb1 ++ [b] ++ lb2
Hpa: P a
Ha: a ∉ b :: lb2
∃ lab : list A, lb1 = la1 ++ a :: lab
  {A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: la1 ++ [a] ++ la2 = lb1 ++ [b] ++ lb2
Hpa: P a
a ∉ b :: lb2 intro Ha.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: la1 ++ [a] ++ la2 = lb1 ++ [b] ++ lb2
Hpa: P a
Ha: a ∈ b :: lb2
False apply Hts.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: la1 ++ [a] ++ la2 = lb1 ++ [b] ++ lb2
Hpa: P a
Ha: a ∈ b :: lb2
a ∈ lb2
    rewrite elem_of_cons in Ha.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: la1 ++ [a] ++ la2 = lb1 ++ [b] ++ lb2
Hpa: P a
Ha: a = b ∨ a ∈ lb2
a ∈ lb2
    destruct Ha; subst; [| done].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
la1, la2: list A
b: A
Hab: precedes b b
Hl: Forall P (la1 ++ [b] ++ la2)
lb2: list A
Hts: b ∉ lb2
lb1: list A
Hpa: P b
Heqb: la1 ++ [b] ++ la2 = lb1 ++ [b] ++ lb2
b ∈ lb2
    by apply (precedes_irreflexive precedes P b Hpa) in Hab.
  }A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
a: A
lb2: list A
Hts: a ∉ lb2
b: A
Hab: precedes a b
la1, la2: list A
Heqa: l = la1 ++ [a] ++ la2
lb1: list A
Heqb: la1 ++ [a] ++ la2 = lb1 ++ [b] ++ lb2
Hpa: P a
Ha: a ∉ b :: lb2
∃ lab : list A, lb1 = la1 ++ a :: lab
  by apply (occurrences_ordering a b la1 la2 lb1 lb2 Heqb Ha).
Qed.

If a and b are in a topologically_sorted list lts and a precedes b then there is an a before any occurrence of b in lts.

Corollary top_sort_before
  (a b : A)
  (Hab : precedes a b)
  (Ha : a ∈ l)
  (l1 l2 : list A)
  (Heq : l = l1 ++ [b] ++ l2)
  : a ∈ l1.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
l1, l2: list A
Heq: l = l1 ++ [b] ++ l2
a ∈ l1
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
l1, l2: list A
Heq: l = l1 ++ [b] ++ l2
a ∈ l1
  apply elem_of_list_split in Ha.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: ∃ l1 l2 : list A, l = l1 ++ a :: l2
l1, l2: list A
Heq: l = l1 ++ [b] ++ l2
a ∈ l1
  destruct Ha as [la1 [la2 Ha]].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Ha: l = la1 ++ a :: la2
l1, l2: list A
Heq: l = l1 ++ [b] ++ l2
a ∈ l1
  specialize (topologically_sorted_occurrences_ordering a b Hab la1 la2 Ha l1 l2 Heq).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Ha: l = la1 ++ a :: la2
l1, l2: list A
Heq: l = l1 ++ [b] ++ l2
(∃ lab : list A, l1 = la1 ++ a :: lab) → a ∈ l1
  intros [lab ->].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
la1, la2: list A
Ha: l = la1 ++ a :: la2
l2, lab: list A
Heq: l = (la1 ++ a :: lab) ++ [b] ++ l2
a ∈ la1 ++ a :: lab
  by rewrite elem_of_app; right; left.
Qed.

As a corollary of the above, if a precedes b then a can be found before b in l.

Corollary top_sort_precedes
  (a b : A)
  (Hab : precedes a b)
  (Ha : a ∈ l)
  (Hb : b ∈ l)
  : exists l1 l2 l3, l = l1 ++ [a] ++ l2 ++ [b] ++ l3.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
Hb: b ∈ l
∃ l1 l2 l3 : list A, l = l1 ++ [a] ++ l2 ++ [b] ++ l3
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
Hb: b ∈ l
∃ l1 l2 l3 : list A, l = l1 ++ [a] ++ l2 ++ [b] ++ l3
  apply elem_of_list_split in Hb.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
Hb: ∃ l1 l2 : list A, l = l1 ++ b :: l2
∃ l1 l2 l3 : list A, l = l1 ++ [a] ++ l2 ++ [b] ++ l3
  destruct Hb as [l12 [l3 Hb']].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
l12, l3: list A
Hb': l = l12 ++ b :: l3
∃ l1 l2 l3 : list A, l = l1 ++ [a] ++ l2 ++ [b] ++ l3
  specialize (top_sort_before a b Hab Ha l12 l3 Hb').A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
l12, l3: list A
Hb': l = l12 ++ b :: l3
a ∈ l12
→ ∃ l1 l2 l3 : list A,
    l = l1 ++ [a] ++ l2 ++ [b] ++ l3
  intros Ha12.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
l12, l3: list A
Hb': l = l12 ++ b :: l3
Ha12: a ∈ l12
∃ l1 l2 l3 : list A, l = l1 ++ [a] ++ l2 ++ [b] ++ l3 apply elem_of_list_split in Ha12.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
l12, l3: list A
Hb': l = l12 ++ b :: l3
Ha12: ∃ l1 l2 : list A, l12 = l1 ++ a :: l2
∃ l1 l2 l3 : list A, l = l1 ++ [a] ++ l2 ++ [b] ++ l3
  destruct Ha12 as [l1 [l2 ->]].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
l3, l1, l2: list A
Hb': l = (l1 ++ a :: l2) ++ b :: l3
∃ l1 l2 l3 : list A, l = l1 ++ [a] ++ l2 ++ [b] ++ l3
  exists l1, l2, l3.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
Hl: Forall P l
Hts: topologically_sorted
a, b: A
Hab: precedes a b
Ha: a ∈ l
l3, l1, l2: list A
Hb': l = (l1 ++ a :: l2) ++ b :: l3
l = l1 ++ [a] ++ l2 ++ [b] ++ l3
  by rewrite Hb', <- app_assoc.
Qed.

End sec_topologically_sorted_fixed_list.
End sec_topologically_sorted.

Lemma toplogically_sorted_remove_last
  {A : Type}
  (precedes : relation A)
  `{!RelDecision precedes}
  (l : list A)
  (Hts : topologically_sorted precedes l)
  (init : list A)
  (final : A)
  (Hinit : l = init ++ [final])
  : topologically_sorted precedes init.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
topologically_sorted precedes init
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
topologically_sorted precedes init
  subst l.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
init: list A
final: A
Hts: topologically_sorted precedes (init ++ [final])
topologically_sorted precedes init
  intros a b Hab l1 l2 Hinit.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
init: list A
final: A
Hts: topologically_sorted precedes (init ++ [final])
a, b: A
Hab: precedes a b
l1, l2: list A
Hinit: init = l1 ++ [b] ++ l2
a ∉ l2
  specialize (Hts a b Hab l1 (l2 ++ [final])).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
init: list A
final, a, b: A
l1, l2: list A
Hts: init ++ [final] = l1 ++ [b] ++ l2 ++ [final]
→ a ∉ l2 ++ [final]
Hab: precedes a b
Hinit: init = l1 ++ [b] ++ l2
a ∉ l2
  rewrite Hinit in Hts.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
init: list A
final, a, b: A
l1, l2: list A
Hts: (l1 ++ [b] ++ l2) ++ [final] =
l1 ++ [b] ++ l2 ++ [final] → 
a ∉ l2 ++ [final]
Hab: precedes a b
Hinit: init = l1 ++ [b] ++ l2
a ∉ l2 repeat rewrite <- app_assoc in Hts.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
init: list A
final, a, b: A
l1, l2: list A
Hts: l1 ++ [b] ++ l2 ++ [final] =
l1 ++ [b] ++ l2 ++ [final] → 
a ∉ l2 ++ [final]
Hab: precedes a b
Hinit: init = l1 ++ [b] ++ l2
a ∉ l2
  specialize (Hts eq_refl).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
init: list A
final, a, b: A
l1, l2: list A
Hts: a ∉ l2 ++ [final]
Hab: precedes a b
Hinit: init = l1 ++ [b] ++ l2
a ∉ l2 intro Hnin.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
init: list A
final, a, b: A
l1, l2: list A
Hts: a ∉ l2 ++ [final]
Hab: precedes a b
Hinit: init = l1 ++ [b] ++ l2
Hnin: a ∈ l2
False apply Hts.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
init: list A
final, a, b: A
l1, l2: list A
Hts: a ∉ l2 ++ [final]
Hab: precedes a b
Hinit: init = l1 ++ [b] ++ l2
Hnin: a ∈ l2
a ∈ l2 ++ [final]
  by apply elem_of_app; left.
Qed.

Definition precedes_closed
  {A : Type}
  (precedes : relation A)
  `{!RelDecision precedes}
  (s : set A)
  : Prop
  :=
  Forall (fun (b : A) => forall (a : A) (Hmj : precedes a b), a ∈ s) s.

Lemma precedes_closed_set_eq
  {A : Type}
  (precedes : relation A)
  `{!RelDecision precedes}
  (s1 s2 : set A)
  (Heq : set_eq s1 s2)
  : precedes_closed precedes s1 <-> precedes_closed precedes s2.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
s1, s2: set A
Heq: set_eq s1 s2
precedes_closed precedes s1
↔ precedes_closed precedes s2
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
s1, s2: set A
Heq: set_eq s1 s2
precedes_closed precedes s1
↔ precedes_closed precedes s2
  unfold precedes_closed; repeat rewrite Forall_forall; firstorder.
Qed.

Lemma topologically_sorted_precedes_closed_remove_last
  {A : Type}
  (precedes : relation A)
  `{!RelDecision precedes}
  (P : A -> Prop)
  {Hso : StrictOrder (precedes_P precedes P)}
  (l : list A)
  (Hl : Forall P l)
  (Hts : topologically_sorted precedes l)
  (init : list A)
  (final : A)
  (Hinit : l = init ++ [final])
  (Hpc : precedes_closed precedes l)
  : precedes_closed precedes init.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
Hpc: precedes_closed precedes l
precedes_closed precedes init
Proof.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
Hpc: precedes_closed precedes l
precedes_closed precedes init
  unfold precedes_closed in *.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
Hpc: Forall (λ b : A, ∀ a : A, precedes a b → a ∈ l)
  l
Forall (λ b : A, ∀ a : A, precedes a b → a ∈ init)
  init
  rewrite Forall_forall in Hpc.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
Hpc: ∀ x : A, x ∈ l → ∀ a : A, precedes a x → a ∈ l
Forall (λ b : A, ∀ a : A, precedes a b → a ∈ init)
  init rewrite Forall_forall.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
Hpc: ∀ x : A, x ∈ l → ∀ a : A, precedes a x → a ∈ l
∀ x : A, x ∈ init → ∀ a : A, precedes a x → a ∈ init
  subst l.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
final: A
Hts: topologically_sorted precedes (init ++ [final])
Hl: Forall P (init ++ [final])
Hpc: ∀ x : A,
  x ∈ init ++ [final]
  → ∀ a : A, precedes a x → a ∈ init ++ [final]
∀ x : A, x ∈ init → ∀ a : A, precedes a x → a ∈ init
  intros b Hb a Hab.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
final: A
Hts: topologically_sorted precedes (init ++ [final])
Hl: Forall P (init ++ [final])
Hpc: ∀ x : A,
  x ∈ init ++ [final]
  → ∀ a : A, precedes a x → a ∈ init ++ [final]
b: A
Hb: b ∈ init
a: A
Hab: precedes a b
a ∈ init
  assert (Hb' : b ∈ init ++ [final]) by (apply elem_of_app; left; done).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
final: A
Hts: topologically_sorted precedes (init ++ [final])
Hl: Forall P (init ++ [final])
Hpc: ∀ x : A,
  x ∈ init ++ [final]
  → ∀ a : A, precedes a x → a ∈ init ++ [final]
b: A
Hb: b ∈ init
a: A
Hab: precedes a b
Hb': b ∈ init ++ [final]
a ∈ init
  specialize (Hpc b Hb' a Hab).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
final: A
Hts: topologically_sorted precedes (init ++ [final])
Hl: Forall P (init ++ [final])
a: A
Hpc: a ∈ init ++ [final]
b: A
Hb: b ∈ init
Hab: precedes a b
Hb': b ∈ init ++ [final]
a ∈ init
  apply elem_of_app in Hpc.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
final: A
Hts: topologically_sorted precedes (init ++ [final])
Hl: Forall P (init ++ [final])
a: A
Hpc: a ∈ init ∨ a ∈ [final]
b: A
Hb: b ∈ init
Hab: precedes a b
Hb': b ∈ init ++ [final]
a ∈ init
  destruct Hpc as [Ha | Ha]; [done |].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
final: A
Hts: topologically_sorted precedes (init ++ [final])
Hl: Forall P (init ++ [final])
a: A
Ha: a ∈ [final]
b: A
Hb: b ∈ init
Hab: precedes a b
Hb': b ∈ init ++ [final]
a ∈ init
  rewrite elem_of_list_singleton in Ha; subst final.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
a: A
Hl: Forall P (init ++ [a])
Hts: topologically_sorted precedes (init ++ [a])
b: A
Hb: b ∈ init
Hab: precedes a b
Hb': b ∈ init ++ [a]
a ∈ init
  apply elem_of_list_split in Hb' as  (l1 & l2 & Heq).A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
a: A
Hl: Forall P (init ++ [a])
Hts: topologically_sorted precedes (init ++ [a])
b: A
Hb: b ∈ init
Hab: precedes a b
l1, l2: list A
Heq: init ++ [a] = l1 ++ b :: l2
a ∈ init
  destruct (topologically_sorted_occurrences_ordering precedes
             (init ++ [a]) P Hl Hts a b Hab init [] eq_refl l1 l2 Heq)
        as [lab Hlab].A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
a: A
Hl: Forall P (init ++ [a])
Hts: topologically_sorted precedes (init ++ [a])
b: A
Hb: b ∈ init
Hab: precedes a b
l1, l2: list A
Heq: init ++ [a] = l1 ++ b :: l2
lab: list A
Hlab: l1 = init ++ a :: lab
a ∈ init
  rewrite Hlab in Heq.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
a: A
Hl: Forall P (init ++ [a])
Hts: topologically_sorted precedes (init ++ [a])
b: A
Hb: b ∈ init
Hab: precedes a b
l1, l2, lab: list A
Heq: init ++ [a] = (init ++ a :: lab) ++ b :: l2
Hlab: l1 = init ++ a :: lab
a ∈ init apply (f_equal length) in Heq.A: Type
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
init: list A
a: A
Hl: Forall P (init ++ [a])
Hts: topologically_sorted precedes (init ++ [a])
b: A
Hb: b ∈ init
Hab: precedes a b
l1, l2, lab: list A
Heq: length (init ++ [a]) =
length ((init ++ a :: lab) ++ b :: l2)
Hlab: l1 = init ++ a :: lab
a ∈ init
  by rewrite !app_length in Heq; cbn in Heq; lia.
Qed.

Section sec_top_sort.

The topological sorting algorithm

Context
  `{EqDecision A}
  (precedes : relation A)
  `{!RelDecision precedes}
  .

Iteratively extracts n elements with minimal number of predecessors from a given list.

Fixpoint top_sort_n
  (n : nat)
  (l : list A)
  : list A
  :=
  match n, l with
  | 0, _ => []
  | _, [] => []
  | S n', a :: l' =>
    let min := min_predecessors precedes l l' a in
    let l'' := set_remove min l in
    min :: top_sort_n n' l''
  end.

Repeats the procedure above to order all elements from the input list.

Definition top_sort
  (l : list A)
  : list A
  := top_sort_n (length l) l.

The result of top_sort and its input are equal as sets.

Lemma top_sort_set_eq
  (l : list A)
  : set_eq l (top_sort l).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
set_eq l (top_sort l)
Proof.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
set_eq l (top_sort l)
  unfold top_sort.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
set_eq l (top_sort_n (length l) l)
  remember (length l) as n.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
n: nat
Heqn: n = length l
set_eq l (top_sort_n n l) generalize dependent l.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
∀ l : list A, n = length l → set_eq l (top_sort_n n l)
  induction n; intros; destruct l; [done.. |]; inversion Heqn.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
set_eq (a :: l) (top_sort_n (S (length l)) (a :: l))
  simpl.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
set_eq (a :: l)
  (min_predecessors precedes (a :: l) l a
   :: top_sort_n (length l)
        (if
          decide
            (min_predecessors precedes (a :: l) l a =
             a)
         then l
         else
          a
          :: set_remove
               (min_predecessors precedes (a :: l) l a)
               l))
  remember (min_predecessors precedes (a :: l) l a) as min.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
set_eq (a :: l)
  (min
   :: top_sort_n (length l)
        (if decide (min = a)
         then l
         else a :: set_remove min l))
  remember (set_remove min l) as l'.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
l': set A
Heql': l' = set_remove min l
set_eq (a :: l)
  (min
   :: top_sort_n (length l)
        (if decide (min = a) then l else a :: l'))
  destruct (decide (min = a)); [by subst a; subst; apply set_eq_cons, IHn |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
l': set A
Heql': l' = set_remove min l
n0: min ≠ a
set_eq (a :: l)
  (min :: top_sort_n (length l) (a :: l'))
  specialize (min_predecessors_in precedes (a :: l) l a).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
l': set A
Heql': l' = set_remove min l
n0: min ≠ a
(let min := min_predecessors precedes (a :: l) l a in
 min = a ∨ min ∈ l)
→ set_eq (a :: l)
    (min :: top_sort_n (length l) (a :: l'))
  rewrite <- Heqmin.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
l': set A
Heql': l' = set_remove min l
n0: min ≠ a
(let min := min in min = a ∨ min ∈ l)
→ set_eq (a :: l)
    (min :: top_sort_n (length l) (a :: l')) simpl.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
l': set A
Heql': l' = set_remove min l
n0: min ≠ a
min = a ∨ min ∈ l
→ set_eq (a :: l)
    (min :: top_sort_n (length l) (a :: l')) intros [Heq | Hin]; [done |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
IHn: ∀ l : list A,
  n = length l → set_eq l (top_sort_n n l)
a: A
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
l': set A
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
set_eq (a :: l)
  (min :: top_sort_n (length l) (a :: l'))
  specialize (IHn (a :: l')).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: n = length (a :: l')
→ set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
set_eq (a :: l)
  (min :: top_sort_n (length l) (a :: l'))
  specialize (set_remove_length min l Hin).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: n = length (a :: l')
→ set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
length l = S (length (set_remove min l))
→ set_eq (a :: l)
    (min :: top_sort_n (length l) (a :: l'))
  rewrite <- Heql'.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: n = length (a :: l')
→ set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
length l = S (length l')
→ set_eq (a :: l)
    (min :: top_sort_n (length l) (a :: l')) rewrite <- H0.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: n = length (a :: l')
→ set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
n = S (length l')
→ set_eq (a :: l) (min :: top_sort_n n (a :: l')) intro Hlen.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: n = length (a :: l')
→ set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
set_eq (a :: l) (min :: top_sort_n n (a :: l'))
  specialize (IHn Hlen).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
set_eq (a :: l) (min :: top_sort_n n (a :: l'))
  split; intros x Hx; rewrite elem_of_cons in Hx;
    destruct Hx as [Heq | Hinx]; try (subst x).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
a ∈ min :: top_sort_n n (a :: l')
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ l
x ∈ min :: top_sort_n n (a :: l')
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
min ∈ a :: l
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ top_sort_n n (a :: l')
x ∈ a :: l
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
a ∈ min :: top_sort_n n (a :: l') by right; apply IHn; left.
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ l
x ∈ min :: top_sort_n n (a :: l') destruct (decide (x = min)); [by subst; left |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ l
n1: x ≠ min
x ∈ min :: top_sort_n n (a :: l')
    specialize (set_remove_3 _ _ l Hinx n1).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ l
n1: x ≠ min
x ∈ set_remove min l
→ x ∈ min :: top_sort_n n (a :: l')
    rewrite <- Heql'.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ l
n1: x ≠ min
x ∈ l' → x ∈ min :: top_sort_n n (a :: l') intro Hinx'.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ l
n1: x ≠ min
Hinx': x ∈ l'
x ∈ min :: top_sort_n n (a :: l')
    by right; apply IHn; right.
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
min ∈ a :: l by right.
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ top_sort_n n (a :: l')
x ∈ a :: l apply IHn in Hinx.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x ∈ a :: l'
x ∈ a :: l
    rewrite elem_of_cons in Hinx.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
n: nat
a: A
l': set A
IHn: set_eq (a :: l') (top_sort_n n (a :: l'))
l: list A
Heqn: S n = length (a :: l)
H0: n = length l
min: A
Heqmin: min = min_predecessors precedes (a :: l) l a
Heql': l' = set_remove min l
n0: min ≠ a
Hin: min ∈ l
Hlen: n = S (length l')
x: A
Hinx: x = a ∨ x ∈ l'
x ∈ a :: l
    destruct Hinx as [-> | Hinx]; [left | right]; subst.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
a: A
l: list A
Heqn: S (length l) = length (a :: l)
IHn: set_eq
  (a
   :: set_remove
        (min_predecessors precedes (a :: l) l a)
        l)
  (top_sort_n (length l)
     (a
      :: set_remove
           (min_predecessors precedes 
              (a :: l) l a) l))
Hin: min_predecessors precedes (a :: l) l a ∈ l
n0: min_predecessors precedes (a :: l) l a ≠ a
Hlen: length l =
S
  (length
     (set_remove
        (min_predecessors precedes (a :: l) l a)
        l))
x: A
Hinx: x
∈ set_remove
    (min_predecessors precedes (a :: l) l a) l
x ∈ l
    by apply set_remove_1 in Hinx.
Qed.

Lemma top_sort_nodup
  (l : list A)
  (Hl : NoDup l)
  : NoDup (top_sort l).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
Hl: NoDup l
NoDup (top_sort l)
Proof.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
Hl: NoDup l
NoDup (top_sort l)
  unfold top_sort.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
Hl: NoDup l
NoDup (top_sort_n (length l) l)
  remember (length l) as len.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
Hl: NoDup l
len: nat
Heqlen: len = length l
NoDup (top_sort_n len l)
  generalize dependent l.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
∀ l : list A,
  NoDup l → len = length l → NoDup (top_sort_n len l)
  induction len; intros; [by cbn; constructor |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
l: list A
Hl: NoDup l
Heqlen: S len = length l
NoDup (top_sort_n (S len) l)
  destruct l as [| a l]; [by constructor |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
NoDup (top_sort_n (S len) (a :: l))
  simpl.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
NoDup
  (min_predecessors precedes (a :: l) l a
   :: top_sort_n len
        (if
          decide
            (min_predecessors precedes (a :: l) l a =
             a)
         then l
         else
          a
          :: set_remove
               (min_predecessors precedes (a :: l) l a)
               l))
  assert (Hl' : NoDup l) by (inversion Hl; done).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
NoDup
  (min_predecessors precedes (a :: l) l a
   :: top_sort_n len
        (if
          decide
            (min_predecessors precedes (a :: l) l a =
             a)
         then l
         else
          a
          :: set_remove
               (min_predecessors precedes (a :: l) l a)
               l))
  assert (Hlen : len = length l) by (inversion Heqlen; done).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
NoDup
  (min_predecessors precedes (a :: l) l a
   :: top_sort_n len
        (if
          decide
            (min_predecessors precedes (a :: l) l a =
             a)
         then l
         else
          a
          :: set_remove
               (min_predecessors precedes (a :: l) l a)
               l))
  assert (Hl'' : NoDup (set_remove (min_predecessors precedes (a :: l) l a) l))
    by (apply set_remove_nodup; done).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
NoDup
  (min_predecessors precedes (a :: l) l a
   :: top_sort_n len
        (if
          decide
            (min_predecessors precedes (a :: l) l a =
             a)
         then l
         else
          a
          :: set_remove
               (min_predecessors precedes (a :: l) l a)
               l))
  destruct (decide (min_predecessors precedes (a :: l) l a = a)); constructor.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
e: min_predecessors precedes (a :: l) l a = a
min_predecessors precedes (a :: l) l a
∉ top_sort_n len l
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
e: min_predecessors precedes (a :: l) l a = a
NoDup (top_sort_n len l)
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
min_predecessors precedes (a :: l) l a
∉ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes (a :: l) l a) l)
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
NoDup
  (top_sort_n len
     (a
      :: set_remove
           (min_predecessors precedes (a :: l) l a) l))
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
e: min_predecessors precedes (a :: l) l a = a
min_predecessors precedes (a :: l) l a
∉ top_sort_n len l specialize (IHlen l Hl'  Hlen).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
l: list A
IHlen: NoDup (top_sort_n len l)
a: A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
e: min_predecessors precedes (a :: l) l a = a
min_predecessors precedes (a :: l) l a
∉ top_sort_n len l
    rewrite e in *.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
l: list A
IHlen: NoDup (top_sort_n len l)
a: A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup (set_remove a l)
e: min_predecessors precedes (a :: l) l a = a
a ∉ top_sort_n len l
    inversion Hl; subst.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
IHlen: NoDup (top_sort_n (length l) l)
a: A
Hl: NoDup (a :: l)
Heqlen: S (length l) = length (a :: l)
Hl': NoDup l
Hl'': NoDup (set_remove a l)
e: min_predecessors precedes (a :: l) l a = a
H1: a ∉ l
H2: NoDup l
a ∉ top_sort_n (length l) l intro Ha; elim H1.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
l: list A
IHlen: NoDup (top_sort_n (length l) l)
a: A
Hl: NoDup (a :: l)
Heqlen: S (length l) = length (a :: l)
Hl': NoDup l
Hl'': NoDup (set_remove a l)
e: min_predecessors precedes (a :: l) l a = a
H1: a ∉ l
H2: NoDup l
Ha: a ∈ top_sort_n (length l) l
a ∈ l
    by apply top_sort_set_eq in Ha.
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
e: min_predecessors precedes (a :: l) l a = a
NoDup (top_sort_n len l) by apply IHlen.
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
min_predecessors precedes (a :: l) l a
∉ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes (a :: l) l a) l) intro Hmin.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes 
             (a :: l) l a) l)
False
    assert (Hlen' : len = length (a :: set_remove (min_predecessors precedes (a :: l) l a) l)).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes 
             (a :: l) l a) l)
len =
length
  (a
   :: set_remove
        (min_predecessors precedes (a :: l) l a) l)
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes 
             (a :: l) l a) l)
Hlen': len =
length
  (a
   :: set_remove
        (min_predecessors precedes 
           (a :: l) l a) l)
False
    {A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes 
             (a :: l) l a) l)
len =
length
  (a
   :: set_remove
        (min_predecessors precedes (a :: l) l a) l)
      simpl.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes 
             (a :: l) l a) l)
len =
S
  (length
     (set_remove
        (min_predecessors precedes (a :: l) l a) l))
      rewrite <- set_remove_length; [done |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes 
             (a :: l) l a) l)
min_predecessors precedes (a :: l) l a ∈ l
      by destruct (@min_predecessors_in _ precedes _ (a :: l) l a).
    }A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ top_sort_n len
    (a
     :: set_remove
          (min_predecessors precedes 
             (a :: l) l a) l)
Hlen': len =
length
  (a
   :: set_remove
        (min_predecessors precedes 
           (a :: l) l a) l)
False
    rewrite Hlen' in Hmin.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ top_sort_n
    (length
       (a
        :: set_remove
             (min_predecessors precedes
                (a :: l) l a) l))
    (a
     :: set_remove
          (min_predecessors precedes 
             (a :: l) l a) l)
Hlen': len =
length
  (a
   :: set_remove
        (min_predecessors precedes 
           (a :: l) l a) l)
False
    apply (proj2 (top_sort_set_eq (a :: set_remove (min_predecessors precedes (a :: l) l a) l)))
      in Hmin.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a
∈ a
  :: set_remove
       (min_predecessors precedes (a :: l) l a)
       l
Hlen': len =
length
  (a
   :: set_remove
        (min_predecessors precedes 
           (a :: l) l a) l)
False
    rewrite elem_of_cons in Hmin.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Hmin: min_predecessors precedes (a :: l) l a = a
∨ min_predecessors precedes (a :: l) l a
  ∈ set_remove
      (min_predecessors precedes (a :: l) l a)
      l
Hlen': len =
length
  (a
   :: set_remove
        (min_predecessors precedes 
           (a :: l) l a) l)
False
    destruct Hmin; [done |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
H: min_predecessors precedes (a :: l) l a
∈ set_remove
    (min_predecessors precedes (a :: l) l a) l
Hlen': len =
length
  (a
   :: set_remove
        (min_predecessors precedes 
           (a :: l) l a) l)
False
    by apply set_remove_2 in H.
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
NoDup
  (top_sort_n len
     (a
      :: set_remove
           (min_predecessors precedes (a :: l) l a) l)) apply IHlen.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
NoDup
  (a
   :: set_remove
        (min_predecessors precedes (a :: l) l a) l)
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
len =
length
  (a
   :: set_remove
        (min_predecessors precedes (a :: l) l a) l)
    +A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
NoDup
  (a
   :: set_remove
        (min_predecessors precedes (a :: l) l a) l) constructor; [| done].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
a
∉ set_remove (min_predecessors precedes (a :: l) l a)
    l
      intro Ha.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Ha: a
∈ set_remove
    (min_predecessors precedes (a :: l) l a) l
False apply set_remove_iff in Ha; [| done].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Ha: a ∈ l
∧ a ≠ min_predecessors precedes (a :: l) l a
False
      destruct Ha as [Ha _].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
Ha: a ∈ l
False
      by inversion Hl.
    +A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
len =
length
  (a
   :: set_remove
        (min_predecessors precedes (a :: l) l a) l) simpl.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
len =
S
  (length
     (set_remove
        (min_predecessors precedes (a :: l) l a) l))
      rewrite <- set_remove_length; [done |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
len: nat
IHlen: ∀ l : list A,
  NoDup l
  → len = length l → NoDup (top_sort_n len l)
a: A
l: list A
Hl: NoDup (a :: l)
Heqlen: S len = length (a :: l)
Hl': NoDup l
Hlen: len = length l
Hl'': NoDup
  (set_remove
     (min_predecessors precedes (a :: l) l a) l)
n: min_predecessors precedes (a :: l) l a ≠ a
min_predecessors precedes (a :: l) l a ∈ l
      by destruct (@min_predecessors_in _ precedes _ (a :: l) l a).
Qed.

Context
  (P : A -> Prop)
  {Hso : StrictOrder (precedes_P precedes P)}
  (l : list A)
  (Hl : Forall P l)
  .

Under the assumption that precedes induces a StrictOrder on the elements of l, top_sort l is topologically_sorted.

Lemma top_sort_sorted : topologically_sorted precedes (top_sort l).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
topologically_sorted precedes (top_sort l)
Proof.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
topologically_sorted precedes (top_sort l)
  intros a b Hab l1 l2 Heq Ha2.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, b: A
Hab: precedes a b
l1, l2: list A
Heq: top_sort l = l1 ++ [b] ++ l2
Ha2: a ∈ l2
False
  assert (Ha : a ∈ l).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, b: A
Hab: precedes a b
l1, l2: list A
Heq: top_sort l = l1 ++ [b] ++ l2
Ha2: a ∈ l2
a ∈ l
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, b: A
Hab: precedes a b
l1, l2: list A
Heq: top_sort l = l1 ++ [b] ++ l2
Ha2: a ∈ l2
Ha: a ∈ l
False
  {A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, b: A
Hab: precedes a b
l1, l2: list A
Heq: top_sort l = l1 ++ [b] ++ l2
Ha2: a ∈ l2
a ∈ l
    apply top_sort_set_eq.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, b: A
Hab: precedes a b
l1, l2: list A
Heq: top_sort l = l1 ++ [b] ++ l2
Ha2: a ∈ l2
a ∈ top_sort l
    by cbn in Heq; rewrite Heq, elem_of_app, elem_of_cons; auto.
  }A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, b: A
Hab: precedes a b
l1, l2: list A
Heq: top_sort l = l1 ++ [b] ++ l2
Ha2: a ∈ l2
Ha: a ∈ l
False
  unfold top_sort in Heq.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, b: A
Hab: precedes a b
l1, l2: list A
Heq: top_sort_n (length l) l = l1 ++ [b] ++ l2
Ha2: a ∈ l2
Ha: a ∈ l
False
  remember (length l) as n.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, b: A
Hab: precedes a b
l1, l2: list A
n: nat
Heqn: n = length l
Heq: top_sort_n n l = l1 ++ [b] ++ l2
Ha2: a ∈ l2
Ha: a ∈ l
False
  revert l Hl Heqn a b Hab l1 Ha l2 Ha2 Heq.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l = l1 ++ [b] ++ l2
                  → False
  induction n; intros
  ; try (symmetry in Heqn;  apply length_zero_iff_nil in Heqn; subst l; inversion Ha).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
Hl: Forall P l
Heqn: S n = length l
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ l
l2: list A
Ha2: a ∈ l2
Heq: top_sort_n (S n) l = l1 ++ [b] ++ l2
False
  destruct l as [| a0 l0]; inversion Hl; subst; simpl in Heq; [by inversion Ha |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n n
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
l1 ++ b :: l2
H1: P a0
H2: Forall P l0
False
  remember (min_predecessors precedes (a0 :: l0) l0 a0) as min.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heq: min
:: top_sort_n n
     (if decide (min = a0)
      then l0
      else a0 :: set_remove min l0) =
l1 ++ b :: l2
H1: P a0
H2: Forall P l0
False
  remember
    (match decide (min = a0) return (set A) with
    | left _ => l0
    | right _ => @cons A a0 (set_remove min l0)
    end) as l'.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
False
  inversion Heqn.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
False
  assert (Hall' : Forall P l').A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Forall P l'
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
False
  {A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Forall P l'
    rewrite Forall_forall.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
∀ x : A, x ∈ l' → P x intros x Hx.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
x: A
Hx: x ∈ l'
P x
    rewrite Forall_forall in H2.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: ∀ x : A, x ∈ l0 → P x
H0: n = length l0
x: A
Hx: x ∈ l'
P x
    destruct (decide (min = a0)); subst; [by apply H2 |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l0: list A
IHn: ∀ l : list A,
  Forall P l
  → length l0 = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n (length l0) l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0) =
l1 ++ b :: l2
n0: min_predecessors precedes (a0 :: l0) l0 a0 ≠ a0
H1: P a0
H2: ∀ x : A, x ∈ l0 → P x
x: A
Hx: x
∈ a0
  :: set_remove
       (min_predecessors precedes 
          (a0 :: l0) l0 a0) l0
P x
    apply elem_of_cons in Hx.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l0: list A
IHn: ∀ l : list A,
  Forall P l
  → length l0 = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n (length l0) l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0) =
l1 ++ b :: l2
n0: min_predecessors precedes (a0 :: l0) l0 a0 ≠ a0
H1: P a0
H2: ∀ x : A, x ∈ l0 → P x
x: A
Hx: x = a0
∨ x
  ∈ set_remove
      (min_predecessors precedes (a0 :: l0) l0 a0)
      l0
P x
    destruct Hx as [-> | Hx]; [done |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l0: list A
IHn: ∀ l : list A,
  Forall P l
  → length l0 = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n (length l0) l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0) =
l1 ++ b :: l2
n0: min_predecessors precedes (a0 :: l0) l0 a0 ≠ a0
H1: P a0
H2: ∀ x : A, x ∈ l0 → P x
x: A
Hx: x
∈ set_remove
    (min_predecessors precedes (a0 :: l0) l0 a0)
    l0
P x
    apply set_remove_1 in Hx.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l0: list A
IHn: ∀ l : list A,
  Forall P l
  → length l0 = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n (length l0) l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0) =
l1 ++ b :: l2
n0: min_predecessors precedes (a0 :: l0) l0 a0 ≠ a0
H1: P a0
H2: ∀ x : A, x ∈ l0 → P x
x: A
Hx: x ∈ l0
P x
    by apply H2.
  }A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
False
  assert (Hlenl' : n = length l').A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
n = length l'
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
False
  {A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
n = length l'
    destruct (decide (min = a0)); subst; cbn; [done |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l0: list A
IHn: ∀ l : list A,
  Forall P l
  → length l0 = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n (length l0) l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0) =
l1 ++ b :: l2
n0: min_predecessors precedes (a0 :: l0) l0 a0 ≠ a0
H1: P a0
H2: Forall P l0
Hall': Forall P
  (a0
   :: set_remove
        (min_predecessors precedes 
           (a0 :: l0) l0 a0) l0)
length l0 =
S
  (length
     (set_remove
        (min_predecessors precedes (a0 :: l0) l0 a0)
        l0))
    rewrite <- set_remove_length; [done |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l0: list A
IHn: ∀ l : list A,
  Forall P l
  → length l0 = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n (length l0) l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0) =
l1 ++ b :: l2
n0: min_predecessors precedes (a0 :: l0) l0 a0 ≠ a0
H1: P a0
H2: Forall P l0
Hall': Forall P
  (a0
   :: set_remove
        (min_predecessors precedes 
           (a0 :: l0) l0 a0) l0)
min_predecessors precedes (a0 :: l0) l0 a0 ∈ l0
    specialize (min_predecessors_in precedes (a0 :: l0) l0 a0).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l0: list A
IHn: ∀ l : list A,
  Forall P l
  → length l0 = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n (length l0) l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0) =
l1 ++ b :: l2
n0: min_predecessors precedes (a0 :: l0) l0 a0 ≠ a0
H1: P a0
H2: Forall P l0
Hall': Forall P
  (a0
   :: set_remove
        (min_predecessors precedes 
           (a0 :: l0) l0 a0) l0)
(let min := min_predecessors precedes (a0 :: l0) l0 a0
   in
 min = a0 ∨ min ∈ l0)
→ min_predecessors precedes (a0 :: l0) l0 a0 ∈ l0
    by cbn; intros [Heq' | Hin].
  }A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
IHn: ∀ l : list A,
  Forall P l
  → n = length l
    → ∀ a b : A,
        precedes a b
        → ∀ l1 : list A,
            a ∈ l
            → ∀ l2 : list A,
                a ∈ l2
                → top_sort_n n l =
                  l1 ++ [b] ++ l2 → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
a, b: A
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
l': set A
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
False
  specialize (IHn l' Hall' Hlenl' a b Hab).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
a, b: A
l': set A
IHn: ∀ l1 : list A,
  a ∈ l'
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n n l' = l1 ++ [b] ++ l2
        → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
False
  assert (Hminb : b <> min).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
a, b: A
l': set A
IHn: ∀ l1 : list A,
  a ∈ l'
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n n l' = l1 ++ [b] ++ l2
        → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
b ≠ min
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
a, b: A
l': set A
IHn: ∀ l1 : list A,
  a ∈ l'
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n n l' = l1 ++ [b] ++ l2
        → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
Hminb: b ≠ min
False
  {A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
a, b: A
l': set A
IHn: ∀ l1 : list A,
  a ∈ l'
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n n l' = l1 ++ [b] ++ l2
        → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
b ≠ min
    destruct (decide (b = min)); subst; [| done].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++
        [min_predecessors precedes 
           (a0 :: l0) l0 a0] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a
  (min_predecessors precedes (a0 :: l0) l0 a0)
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
l1 ++
min_predecessors precedes (a0 :: l0) l0 a0 :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
min_predecessors precedes (a0 :: l0) l0 a0
≠ min_predecessors precedes (a0 :: l0) l0 a0
    specialize (min_predecessors_zero precedes (a0 :: l0) P Hl l0 a0 eq_refl).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++
        [min_predecessors precedes 
           (a0 :: l0) l0 a0] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a
  (min_predecessors precedes (a0 :: l0) l0 a0)
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
l1 ++
min_predecessors precedes (a0 :: l0) l0 a0 :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
(let min := min_predecessors precedes (a0 :: l0) l0 a0
   in
 count_predecessors precedes (a0 :: l0) min = 0)
→ min_predecessors precedes (a0 :: l0) l0 a0
  ≠ min_predecessors precedes (a0 :: l0) l0 a0
    simpl.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++
        [min_predecessors precedes 
           (a0 :: l0) l0 a0] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a
  (min_predecessors precedes (a0 :: l0) l0 a0)
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
l1 ++
min_predecessors precedes (a0 :: l0) l0 a0 :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
count_predecessors precedes (a0 :: l0)
  (min_predecessors precedes (a0 :: l0) l0 a0) = 0
→ min_predecessors precedes (a0 :: l0) l0 a0
  ≠ min_predecessors precedes (a0 :: l0) l0 a0 intro Hmin.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++
        [min_predecessors precedes 
           (a0 :: l0) l0 a0] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a
  (min_predecessors precedes (a0 :: l0) l0 a0)
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
l1 ++
min_predecessors precedes (a0 :: l0) l0 a0 :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
Hmin: count_predecessors precedes 
  (a0 :: l0)
  (min_predecessors precedes (a0 :: l0) l0 a0) =
0
min_predecessors precedes (a0 :: l0) l0 a0
≠ min_predecessors precedes (a0 :: l0) l0 a0
    apply zero_predecessors in Hmin.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++
        [min_predecessors precedes 
           (a0 :: l0) l0 a0] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a
  (min_predecessors precedes (a0 :: l0) l0 a0)
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
l1 ++
min_predecessors precedes (a0 :: l0) l0 a0 :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
Hmin: Forall
  (λ b : A,
     ¬ precedes b
         (min_predecessors precedes 
            (a0 :: l0) l0 a0)) 
  (a0 :: l0)
min_predecessors precedes (a0 :: l0) l0 a0
≠ min_predecessors precedes (a0 :: l0) l0 a0
    rewrite Forall_forall in Hmin.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++
        [min_predecessors precedes 
           (a0 :: l0) l0 a0] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a
  (min_predecessors precedes (a0 :: l0) l0 a0)
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
l1 ++
min_predecessors precedes (a0 :: l0) l0 a0 :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
Hmin: ∀ x : A,
  x ∈ a0 :: l0
  → ¬ precedes x
        (min_predecessors precedes 
           (a0 :: l0) l0 a0)
min_predecessors precedes (a0 :: l0) l0 a0
≠ min_predecessors precedes (a0 :: l0) l0 a0
    apply Hmin in Ha.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++
        [min_predecessors precedes 
           (a0 :: l0) l0 a0] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a
  (min_predecessors precedes (a0 :: l0) l0 a0)
l1: list A
Ha: ¬ precedes a
    (min_predecessors precedes (a0 :: l0) l0 a0)
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
l1 ++
min_predecessors precedes (a0 :: l0) l0 a0 :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
Hmin: ∀ x : A,
  x ∈ a0 :: l0
  → ¬ precedes x
        (min_predecessors precedes 
           (a0 :: l0) l0 a0)
min_predecessors precedes (a0 :: l0) l0 a0
≠ min_predecessors precedes (a0 :: l0) l0 a0
    by congruence.
  }A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
a, b: A
l': set A
IHn: ∀ l1 : list A,
  a ∈ l'
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n n l' = l1 ++ [b] ++ l2
        → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = l1 ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
Hminb: b ≠ min
False
  destruct l1 as [| _min l1]; inversion Heq; [by subst |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
a, b: A
l': set A
IHn: ∀ l1 : list A,
  a ∈ l'
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n n l' = l1 ++ [b] ++ l2
        → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
Hab: precedes a b
_min: A
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = (_min :: l1) ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
Hminb: b ≠ min
H3: min = _min
H4: top_sort_n n l' = l1 ++ b :: l2
False
  subst _min.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
a, b: A
l': set A
IHn: ∀ l1 : list A,
  a ∈ l'
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n n l' = l1 ++ [b] ++ l2
        → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = (min :: l1) ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
Hminb: b ≠ min
H4: top_sort_n n l' = l1 ++ b :: l2
False
  destruct (decide (a ∈ l')) as [i | i]; [by apply (IHn l1 i l2 Ha2 H4) |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
n: nat
a, b: A
l': set A
IHn: ∀ l1 : list A,
  a ∈ l'
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n n l' = l1 ++ [b] ++ l2
        → False
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
Heqn: S n = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
min: A
Heqmin: min =
min_predecessors precedes (a0 :: l0) l0 a0
Heql': l' =
(if decide (min = a0)
 then l0
 else a0 :: set_remove min l0)
Heq: min :: top_sort_n n l' = (min :: l1) ++ b :: l2
H1: P a0
H2: Forall P l0
H0: n = length l0
Hall': Forall P l'
Hlenl': n = length l'
Hminb: b ≠ min
H4: top_sort_n n l' = l1 ++ b :: l2
i: a ∉ l'
False
  subst.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, b, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++ [b] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
(min_predecessors precedes (a0 :: l0) l0 a0
 :: l1) ++ b :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
Hminb: b ≠ min_predecessors precedes (a0 :: l0) l0 a0
i: a
∉ (if
    decide
      (min_predecessors precedes (a0 :: l0) l0 a0 =
       a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
H4: top_sort_n (length l0)
  (if
    decide
      (min_predecessors precedes (a0 :: l0) l0 a0 =
       a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0) = 
l1 ++ b :: l2
False apply i, top_sort_set_eq.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, b, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++ [b] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
(min_predecessors precedes (a0 :: l0) l0 a0
 :: l1) ++ b :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
Hminb: b ≠ min_predecessors precedes (a0 :: l0) l0 a0
i: a
∉ (if
    decide
      (min_predecessors precedes (a0 :: l0) l0 a0 =
       a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
H4: top_sort_n (length l0)
  (if
    decide
      (min_predecessors precedes (a0 :: l0) l0 a0 =
       a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0) = 
l1 ++ b :: l2
a
∈ top_sort
    (if
      decide
        (min_predecessors precedes (a0 :: l0) l0 a0 =
         a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes (a0 :: l0) l0 a0)
           l0) unfold top_sort.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, b, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++ [b] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
(min_predecessors precedes (a0 :: l0) l0 a0
 :: l1) ++ b :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
Hminb: b ≠ min_predecessors precedes (a0 :: l0) l0 a0
i: a
∉ (if
    decide
      (min_predecessors precedes (a0 :: l0) l0 a0 =
       a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
H4: top_sort_n (length l0)
  (if
    decide
      (min_predecessors precedes (a0 :: l0) l0 a0 =
       a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0) = 
l1 ++ b :: l2
a
∈ top_sort_n
    (length
       (if
         decide
           (min_predecessors precedes (a0 :: l0) l0 a0 =
            a0)
        then l0
        else
         a0
         :: set_remove
              (min_predecessors precedes (a0 :: l0) l0
                 a0) l0))
    (if
      decide
        (min_predecessors precedes (a0 :: l0) l0 a0 =
         a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes (a0 :: l0) l0 a0)
           l0)
  rewrite <- Hlenl', H4, elem_of_app, !elem_of_cons.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
a, b, a0: A
l0: list A
IHn: ∀ l1 : list A,
  a
  ∈ (if
      decide
        (min_predecessors precedes 
           (a0 :: l0) l0 a0 = a0)
     then l0
     else
      a0
      :: set_remove
           (min_predecessors precedes 
              (a0 :: l0) l0 a0) l0)
  → ∀ l2 : list A,
      a ∈ l2
      → top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes
                 (a0 :: l0) l0 a0 = a0)
           then l0
           else
            a0
            :: set_remove
                 (min_predecessors precedes
                    (a0 :: l0) l0 a0) l0) =
        l1 ++ [b] ++ l2 → False
l: list A
Hl: Forall P (a0 :: l0)
Heqn: S (length l0) = length (a0 :: l0)
Hab: precedes a b
l1: list A
Ha: a ∈ a0 :: l0
l2: list A
Ha2: a ∈ l2
Heq: min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes 
            (a0 :: l0) l0 a0 = a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes
               (a0 :: l0) l0 a0) l0) =
(min_predecessors precedes (a0 :: l0) l0 a0
 :: l1) ++ b :: l2
H1: P a0
H2: Forall P l0
Hlenl': length l0 =
length
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes
            (a0 :: l0) l0 a0) l0)
Hall': Forall P
  (if
    decide
      (min_predecessors precedes 
         (a0 :: l0) l0 a0 = a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
Hminb: b ≠ min_predecessors precedes (a0 :: l0) l0 a0
i: a
∉ (if
    decide
      (min_predecessors precedes (a0 :: l0) l0 a0 =
       a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0)
H4: top_sort_n (length l0)
  (if
    decide
      (min_predecessors precedes (a0 :: l0) l0 a0 =
       a0)
   then l0
   else
    a0
    :: set_remove
         (min_predecessors precedes 
            (a0 :: l0) l0 a0) l0) = 
l1 ++ b :: l2
a ∈ l1 ∨ a = b ∨ a ∈ l2
  by itauto.
Qed.

lts is a topological_sorting of l if it has the same elements as l and is topologically_sorted.

Definition topological_sorting
  (l lts : list A)
  :=
  set_eq l lts /\ topologically_sorted precedes lts.

Corollary top_sort_correct : topological_sorting l (top_sort l).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
topological_sorting l (top_sort l)
Proof.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
topological_sorting l (top_sort l)
  split.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
set_eq l (top_sort l)
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
topologically_sorted precedes (top_sort l)
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
set_eq l (top_sort l) by apply top_sort_set_eq.
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
topologically_sorted precedes (top_sort l) by apply top_sort_sorted.
Qed.

Maximal elements

Definition get_maximal_element := ListExtras.last_error (top_sort l).

Lemma maximal_element_in
  (a : A)
  (Hmax : get_maximal_element = Some a) :
  a ∈ l.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: get_maximal_element = Some a
a ∈ l
Proof.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: get_maximal_element = Some a
a ∈ l
  unfold get_maximal_element in Hmax.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
a ∈ l
  assert (exists l', l' ++ [a] = top_sort l).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
∃ l' : list A, l' ++ [a] = top_sort l
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
H: ∃ l' : list A, l' ++ [a] = top_sort l
a ∈ l
  {A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
∃ l' : list A, l' ++ [a] = top_sort l
    destruct l; [by simpl in Hmax; itauto congruence |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
∃ l' : list A, l' ++ [a] = top_sort (a0 :: l0)
    specialize (@exists_last _ (top_sort (a0 :: l0))) as Hlast.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
Hlast: top_sort (a0 :: l0) ≠ []
→ {l' : list A &
  {a : A | top_sort (a0 :: l0) = l' ++ [a]}}
∃ l' : list A, l' ++ [a] = top_sort (a0 :: l0)
    spec Hlast.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
Hlast: top_sort (a0 :: l0) ≠ []
→ {l' : list A &
  {a : A | top_sort (a0 :: l0) = l' ++ [a]}}
top_sort (a0 :: l0) ≠ []
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
Hlast: {l' : list A &
{a : A | top_sort (a0 :: l0) = l' ++ [a]}}
∃ l' : list A, l' ++ [a] = top_sort (a0 :: l0) unfold top_sort.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
Hlast: top_sort (a0 :: l0) ≠ []
→ {l' : list A &
  {a : A | top_sort (a0 :: l0) = l' ++ [a]}}
top_sort_n (length (a0 :: l0)) (a0 :: l0) ≠ []
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
Hlast: {l' : list A &
{a : A | top_sort (a0 :: l0) = l' ++ [a]}}
∃ l' : list A, l' ++ [a] = top_sort (a0 :: l0) simpl.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
Hlast: top_sort (a0 :: l0) ≠ []
→ {l' : list A &
  {a : A | top_sort (a0 :: l0) = l' ++ [a]}}
min_predecessors precedes (a0 :: l0) l0 a0
:: top_sort_n (length l0)
     (if
       decide
         (min_predecessors precedes (a0 :: l0) l0 a0 =
          a0)
      then l0
      else
       a0
       :: set_remove
            (min_predecessors precedes (a0 :: l0) l0
               a0) l0) ≠ []
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
Hlast: {l' : list A &
{a : A | top_sort (a0 :: l0) = l' ++ [a]}}
∃ l' : list A, l' ++ [a] = top_sort (a0 :: l0) itauto congruence.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
Hlast: {l' : list A &
{a : A | top_sort (a0 :: l0) = l' ++ [a]}}
∃ l' : list A, l' ++ [a] = top_sort (a0 :: l0)
    destruct Hlast as [l' [a' Heq]].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
Hmax: last_error (top_sort (a0 :: l0)) = Some a
l': list A
a': A
Heq: top_sort (a0 :: l0) = l' ++ [a']
∃ l' : list A, l' ++ [a] = top_sort (a0 :: l0)
    rewrite Heq in Hmax.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
l': list A
a': A
Hmax: last_error (l' ++ [a']) = Some a
Heq: top_sort (a0 :: l0) = l' ++ [a']
∃ l' : list A, l' ++ [a] = top_sort (a0 :: l0)
    rewrite Heq.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
l': list A
a': A
Hmax: last_error (l' ++ [a']) = Some a
Heq: top_sort (a0 :: l0) = l' ++ [a']
∃ l'0 : list A, l'0 ++ [a] = l' ++ [a']
    exists l'.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
l': list A
a': A
Hmax: last_error (l' ++ [a']) = Some a
Heq: top_sort (a0 :: l0) = l' ++ [a']
l' ++ [a] = l' ++ [a']
    specialize (last_error_is_last l' a') as Hlast.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a0: A
l0: list A
Hl: Forall P (a0 :: l0)
a: A
l': list A
a': A
Hmax: last_error (l' ++ [a']) = Some a
Heq: top_sort (a0 :: l0) = l' ++ [a']
Hlast: last_error (l' ++ [a']) = Some a'
l' ++ [a] = l' ++ [a']
    by itauto congruence.
  }A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
H: ∃ l' : list A, l' ++ [a] = top_sort l
a ∈ l
  assert (a ∈ top_sort l).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
H: ∃ l' : list A, l' ++ [a] = top_sort l
a ∈ top_sort l
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
H: ∃ l' : list A, l' ++ [a] = top_sort l
H0: a ∈ top_sort l
a ∈ l
  {A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
H: ∃ l' : list A, l' ++ [a] = top_sort l
a ∈ top_sort l
    destruct H as [l' <-].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
l': list A
a ∈ l' ++ [a]
    by apply elem_of_app; right; left.
  }A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
H: ∃ l' : list A, l' ++ [a] = top_sort l
H0: a ∈ top_sort l
a ∈ l
  specialize (top_sort_correct) as [Htop _].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
H: ∃ l' : list A, l' ++ [a] = top_sort l
H0: a ∈ top_sort l
Htop: set_eq l (top_sort l)
a ∈ l
  destruct Htop as [_ Htop].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a: A
Hmax: last_error (top_sort l) = Some a
H: ∃ l' : list A, l' ++ [a] = top_sort l
H0: a ∈ top_sort l
Htop: top_sort l ⊆ l
a ∈ l
  by specialize (Htop a H0); itauto.
Qed.

Lemma get_maximal_element_correct
  (a max : A)
  (Hina : a ∈ l)
  (Hmax : get_maximal_element = Some max) :
  ~ precedes max a.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
¬ precedes max a
Proof.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
¬ precedes max a
  specialize top_sort_correct as [Hseteq Htop].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
Hseteq: set_eq l (top_sort l)
Htop: topologically_sorted precedes (top_sort l)
¬ precedes max a
  unfold topologically_sorted in Htop.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ a b : A,
  precedes a b
  → ∀ l1 l2 : list A,
      top_sort l = l1 ++ [b] ++ l2 → a ∉ l2
¬ precedes max a
  intros contra.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ a b : A,
  precedes a b
  → ∀ l1 l2 : list A,
      top_sort l = l1 ++ [b] ++ l2 → a ∉ l2
contra: precedes max a
False
  specialize (Htop max a contra).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
False
  assert (Hinmax : max ∈ l) by (apply maximal_element_in; itauto).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
False
  assert (Hinatop : a ∈ top_sort l) by (apply Hseteq; itauto).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
Hinatop: a ∈ top_sort l
False
  apply elem_of_list_split in Hinatop.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
Hinatop: ∃ l1 l2 : list A, top_sort l = l1 ++ a :: l2
False
  destruct Hinatop as [prefA [sufA HeqA]].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
prefA, sufA: list A
HeqA: top_sort l = prefA ++ a :: sufA
False
  unfold get_maximal_element in Hmax.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: last_error (top_sort l) = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
prefA, sufA: list A
HeqA: top_sort l = prefA ++ a :: sufA
False
  destruct sufA.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: last_error (top_sort l) = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
prefA: list A
HeqA: top_sort l = prefA ++ [a]
False
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: last_error (top_sort l) = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
prefA: list A
a0: A
sufA: list A
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
False
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: last_error (top_sort l) = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
prefA: list A
HeqA: top_sort l = prefA ++ [a]
False rewrite HeqA in Hmax.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
Hmax: last_error (prefA ++ [a]) = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ [a]
False
    specialize (last_error_is_last prefA a) as Hlast.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
Hmax: last_error (prefA ++ [a]) = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ [a]
Hlast: last_error (prefA ++ [a]) = Some a
False
    assert (a = max) by itauto congruence.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
Hmax: last_error (prefA ++ [a]) = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ [a]
Hlast: last_error (prefA ++ [a]) = Some a
H: a = max
False
    subst a.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
max: A
Hina: max ∈ l
prefA: list A
Hmax: last_error (prefA ++ [max]) = Some max
Hseteq: set_eq l (top_sort l)
contra: precedes max max
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [max] ++ l2 → max ∉ l2
Hinmax: max ∈ l
Hlast: last_error (prefA ++ [max]) = Some max
HeqA: top_sort l = prefA ++ [max]
False
    specialize StrictOrder_Irreflexive as Hirr.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
max: A
Hina: max ∈ l
prefA: list A
Hmax: last_error (prefA ++ [max]) = Some max
Hseteq: set_eq l (top_sort l)
contra: precedes max max
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [max] ++ l2 → max ∉ l2
Hinmax: max ∈ l
Hlast: last_error (prefA ++ [max]) = Some max
HeqA: top_sort l = prefA ++ [max]
Hirr: Irreflexive (precedes_P precedes P)
False
    unfold Irreflexive in Hirr.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
max: A
Hina: max ∈ l
prefA: list A
Hmax: last_error (prefA ++ [max]) = Some max
Hseteq: set_eq l (top_sort l)
contra: precedes max max
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [max] ++ l2 → max ∉ l2
Hinmax: max ∈ l
Hlast: last_error (prefA ++ [max]) = Some max
HeqA: top_sort l = prefA ++ [max]
Hirr: Reflexive (complement (precedes_P precedes P))
False unfold complement in Hirr.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
max: A
Hina: max ∈ l
prefA: list A
Hmax: last_error (prefA ++ [max]) = Some max
Hseteq: set_eq l (top_sort l)
contra: precedes max max
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [max] ++ l2 → max ∉ l2
Hinmax: max ∈ l
Hlast: last_error (prefA ++ [max]) = Some max
HeqA: top_sort l = prefA ++ [max]
Hirr: Reflexive
  (λ (x : {x : A | P x}) (y : {x : A | P x}),
     precedes_P precedes P x y → False)
False
    unfold Reflexive in Hirr.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
max: A
Hina: max ∈ l
prefA: list A
Hmax: last_error (prefA ++ [max]) = Some max
Hseteq: set_eq l (top_sort l)
contra: precedes max max
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [max] ++ l2 → max ∉ l2
Hinmax: max ∈ l
Hlast: last_error (prefA ++ [max]) = Some max
HeqA: top_sort l = prefA ++ [max]
Hirr: ∀ x : {x : A | P x},
  precedes_P precedes P x x → False
False
    assert (P max) by (eapply Forall_forall; done).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
max: A
Hina: max ∈ l
prefA: list A
Hmax: last_error (prefA ++ [max]) = Some max
Hseteq: set_eq l (top_sort l)
contra: precedes max max
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [max] ++ l2 → max ∉ l2
Hinmax: max ∈ l
Hlast: last_error (prefA ++ [max]) = Some max
HeqA: top_sort l = prefA ++ [max]
Hirr: ∀ x : {x : A | P x},
  precedes_P precedes P x x → False
H: P max
False
    by specialize (Hirr (exist _ max H)); itauto.
  -A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
Hmax: last_error (top_sort l) = Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
prefA: list A
a0: A
sufA: list A
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
False rewrite HeqA in Hmax.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA: list A
Hmax: last_error (prefA ++ a :: a0 :: sufA) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
False
    specialize (@exists_last _ (a0 :: sufA)) as Hex.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA: list A
Hmax: last_error (prefA ++ a :: a0 :: sufA) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Hex: a0 :: sufA ≠ []
→ {l' : list A &
  {a : A | a0 :: sufA = l' ++ [a]}}
False
    spec Hex.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA: list A
Hmax: last_error (prefA ++ a :: a0 :: sufA) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Hex: a0 :: sufA ≠ []
→ {l' : list A &
  {a : A | a0 :: sufA = l' ++ [a]}}
a0 :: sufA ≠ []
A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA: list A
Hmax: last_error (prefA ++ a :: a0 :: sufA) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Hex: {l' : list A & {a : A | a0 :: sufA = l' ++ [a]}}
False itauto congruence.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA: list A
Hmax: last_error (prefA ++ a :: a0 :: sufA) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Hex: {l' : list A & {a : A | a0 :: sufA = l' ++ [a]}}
False
    destruct Hex as [l' [a' Heq]].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA: list A
Hmax: last_error (prefA ++ a :: a0 :: sufA) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
l': list A
a': A
Heq: a0 :: sufA = l' ++ [a']
False
    rewrite Heq in Hmax.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
a': A
Hmax: last_error (prefA ++ a :: l' ++ [a']) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Heq: a0 :: sufA = l' ++ [a']
False
    specialize (last_error_is_last (prefA ++ a :: l') a') as Hlast.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
a': A
Hmax: last_error (prefA ++ a :: l' ++ [a']) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Heq: a0 :: sufA = l' ++ [a']
Hlast: last_error ((prefA ++ a :: l') ++ [a']) =
Some a'
False
    rewrite <- app_assoc in Hlast.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
a': A
Hmax: last_error (prefA ++ a :: l' ++ [a']) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Heq: a0 :: sufA = l' ++ [a']
Hlast: last_error (prefA ++ (a :: l') ++ [a']) =
Some a'
False
    simpl in Hlast.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
a': A
Hmax: last_error (prefA ++ a :: l' ++ [a']) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Heq: a0 :: sufA = l' ++ [a']
Hlast: last_error (prefA ++ a :: l' ++ [a']) =
Some a'
False
    assert (a' = max) by itauto congruence.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
a': A
Hmax: last_error (prefA ++ a :: l' ++ [a']) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: ∀ l1 l2 : list A,
  top_sort l = l1 ++ [a] ++ l2 → max ∉ l2
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Heq: a0 :: sufA = l' ++ [a']
Hlast: last_error (prefA ++ a :: l' ++ [a']) =
Some a'
H: a' = max
False
    specialize (Htop prefA (l' ++ [a'])).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
a': A
Hmax: last_error (prefA ++ a :: l' ++ [a']) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: top_sort l = prefA ++ [a] ++ l' ++ [a']
→ max ∉ l' ++ [a']
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: a0 :: sufA
Heq: a0 :: sufA = l' ++ [a']
Hlast: last_error (prefA ++ a :: l' ++ [a']) =
Some a'
H: a' = max
False
    rewrite Heq in HeqA.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
a': A
Hmax: last_error (prefA ++ a :: l' ++ [a']) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: top_sort l = prefA ++ [a] ++ l' ++ [a']
→ max ∉ l' ++ [a']
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: l' ++ [a']
Heq: a0 :: sufA = l' ++ [a']
Hlast: last_error (prefA ++ a :: l' ++ [a']) =
Some a'
H: a' = max
False
    specialize (Htop HeqA).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
a': A
Hmax: last_error (prefA ++ a :: l' ++ [a']) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: max ∉ l' ++ [a']
contra: precedes max a
Hinmax: max ∈ l
HeqA: top_sort l = prefA ++ a :: l' ++ [a']
Heq: a0 :: sufA = l' ++ [a']
Hlast: last_error (prefA ++ a :: l' ++ [a']) =
Some a'
H: a' = max
False
    subst a'.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
a, max: A
Hina: a ∈ l
prefA: list A
a0: A
sufA, l': list A
Hmax: last_error (prefA ++ a :: l' ++ [max]) =
Some max
Hseteq: set_eq l (top_sort l)
Htop: max ∉ l' ++ [max]
contra: precedes max a
Hinmax: max ∈ l
Hlast: last_error (prefA ++ a :: l' ++ [max]) =
Some max
Heq: a0 :: sufA = l' ++ [max]
HeqA: top_sort l = prefA ++ a :: l' ++ [max]
False
    by contradict Htop; apply elem_of_app; right; left.
Qed.

Lemma get_maximal_element_some
  (Hne : l <> []) :
  exists a, get_maximal_element = Some a.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
Hne: l ≠ []
∃ a : A, get_maximal_element = Some a
Proof.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
Hne: l ≠ []
∃ a : A, get_maximal_element = Some a
  unfold get_maximal_element.A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
Hl: Forall P l
Hne: l ≠ []
∃ a : A, last_error (top_sort l) = Some a
  destruct l; cbn; [by congruence |].A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a: A
l0: list A
Hl: Forall P (a :: l0)
Hne: a :: l0 ≠ []
∃ a0 : A,
  Some
    (List.last
       (top_sort_n (length l0)
          (if
            decide
              (min_predecessors precedes (a :: l0) l0
                 a = a)
           then l0
           else
            a
            :: set_remove
                 (min_predecessors precedes (a :: l0)
                    l0 a) l0))
       (min_predecessors precedes (a :: l0) l0 a)) =
  Some a0
  exists (List.last
     (top_sort_n (length l0)
        (if decide (min_predecessors precedes (a :: l0) l0 a = a)
         then l0
         else a :: set_remove (min_predecessors precedes (a :: l0) l0 a) l0))
     (min_predecessors precedes (a :: l0) l0 a)).A: Type
EqDecision0: EqDecision A
precedes: relation A
RelDecision0: RelDecision precedes
P: A → Prop
Hso: StrictOrder (precedes_P precedes P)
l: list A
a: A
l0: list A
Hl: Forall P (a :: l0)
Hne: a :: l0 ≠ []
Some
  (List.last
     (top_sort_n (length l0)
        (if
          decide
            (min_predecessors precedes (a :: l0) l0 a =
             a)
         then l0
         else
          a
          :: set_remove
               (min_predecessors precedes (a :: l0) l0
                  a) l0))
     (min_predecessors precedes (a :: l0) l0 a)) =
Some
  (List.last
     (top_sort_n (length l0)
        (if
          decide
            (min_predecessors precedes (a :: l0) l0 a =
             a)
         then l0
         else
          a
          :: set_remove
               (min_predecessors precedes (a :: l0) l0
                  a) l0))
     (min_predecessors precedes (a :: l0) l0 a))
  by itauto.
Qed.

End sec_top_sort.

Some of the results above depend on the precedes relation being a StrictOrder for a property-defined sig type. However, when the relation is strict to begin with, we can obtain simpler statements for these results.

Section sec_simple_top_sort.

Context
  `{EqDecision A}
  (precedes : A -> A -> Prop)
  `{!RelDecision precedes}
  `{!StrictOrder precedes}
  .

#[local] Lemma Forall_True : forall l : list A, Forall (fun _ => True) l.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
∀ l : list A, Forall (λ _ : A, True) l
Proof.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
∀ l : list A, Forall (λ _ : A, True) l
  by intro; apply Forall_forall.
Qed.

Corollary simple_topologically_sorted_precedes_closed_remove_last
  (l : list A)
  (Hts : topologically_sorted precedes l)
  (init : list A)
  (final : A)
  (Hinit : l = init ++ [final])
  (Hpc : precedes_closed precedes l)
  : precedes_closed precedes init.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
l: list A
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
Hpc: precedes_closed precedes l
precedes_closed precedes init
Proof.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
l: list A
Hts: topologically_sorted precedes l
init: list A
final: A
Hinit: l = init ++ [final]
Hpc: precedes_closed precedes l
precedes_closed precedes init
  by eapply topologically_sorted_precedes_closed_remove_last;
    [typeclasses eauto | apply Forall_True | ..].
Qed.

Corollary simple_top_sort_correct : forall l,
  topological_sorting precedes l (top_sort precedes l).A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
∀ l : list A,
  topological_sorting precedes l (top_sort precedes l)
Proof.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
∀ l : list A,
  topological_sorting precedes l (top_sort precedes l)
  by intro; eapply top_sort_correct; [typeclasses eauto | apply Forall_True].
Qed.

Corollary simple_maximal_element_in l
  (a : A)
  (Hmax : get_maximal_element precedes l = Some a) :
  a ∈ l.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
l: list A
a: A
Hmax: get_maximal_element precedes l = Some a
a ∈ l
Proof.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
l: list A
a: A
Hmax: get_maximal_element precedes l = Some a
a ∈ l
  by eapply maximal_element_in; [typeclasses eauto | apply Forall_True |].
Qed.

Corollary simple_get_maximal_element_correct l
  (a max : A)
  (Hina : a ∈ l)
  (Hmax : get_maximal_element precedes l = Some max) :
  ~ precedes max a.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
l: list A
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element precedes l = Some max
¬ precedes max a
Proof.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
l: list A
a, max: A
Hina: a ∈ l
Hmax: get_maximal_element precedes l = Some max
¬ precedes max a
  by eapply get_maximal_element_correct; [typeclasses eauto | apply Forall_True | ..].
Qed.

Corollary simple_get_maximal_element_some
  l (Hne : l <> []) :
  exists a, get_maximal_element precedes l = Some a.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
l: list A
Hne: l ≠ []
∃ a : A, get_maximal_element precedes l = Some a
Proof.A: Type
EqDecision0: EqDecision A
precedes: A → A → Prop
RelDecision0: RelDecision precedes
StrictOrder0: StrictOrder precedes
l: list A
Hne: l ≠ []
∃ a : A, get_maximal_element precedes l = Some a
  by eapply get_maximal_element_some; [apply Forall_True |].
Qed.

End sec_simple_top_sort.