Lvc.Infra.Pos

Require Import CSet Map OrderedTypeEx Util List Get Computable DecSolve AllInRel.

Set Implicit Arguments.

Fixpoint pos X `{OrderedType X} (l:list X) (x:X) (n:nat) : option nat :=
  match l with
    | nil ⇒ None
    | y::l ⇒ if [ x === y ] then Some n else pos l x (S n)
  end.

Lemma pos_add X `{OrderedType X} k´ symb (f:X) k i
: pos symb f k = Some i → pos symb f (k´ + k) = Some (k´ + i).

Lemma pos_sub X `{OrderedType X} k´ symb (f:X) k i
: pos symb f (k´ + k) = Some (k´ + i) → pos symb f k = Some i.

Lemma pos_ge X `{OrderedType X} symb (l:X) i k
: pos symb l k = Some i
  → k ≤ i.

Lemma pos_sub´ X `{OrderedType X} k´ symb (f:X) k i
: pos symb f k = Some i → k´ ≤ k → pos symb f (k - k´) = Some (i - k´).

Lemma update_with_list_lookup_in_list_first X `{OrderedType X} B E n
      (Z:list X) (Y:list B) z
: length Z = length Y
  → get Z n z
  → (∀ n´ z´, n´ < n → get Z n´ z´ → z´ =/= z)
  → ∃ y, get Y n y ∧ E [Z <-- Y] z === y.

Lemma list_lookup_in_list_first X `{OrderedType X} B E
      (Z:list X) (Y:list B) x y
: length Z = length Y
  → (E [Z <-- Y]) x = y
  → x ∈ of_list Z
  → ∃ n y´, get Y n y´ ∧ y === y´ ∧ (∀ n´ x´, n´ < n → get Z n´ x´ → x´ =/= x).

Lemma of_list_get_first X `{OrderedType X} (Z:list X) z
: z ∈ of_list Z
  → ∃ n z´, get Z n z´ ∧ z === z´ ∧ (∀ n´ z´, n´ < n → get Z n´ z´ → z´ =/= z).

Lemma get_first_pos X `{OrderedType X} n
      (Z:list X) z
: get Z n z
  → (∀ n´ z´, n´ < n → get Z n´ z´ → z´ =/= z)
  → pos Z z 0 = Some n.

Lemma pos_get X `{OrderedType X} (symb:list X) v x i
: pos symb v i = ⎣x ⎦
   → ∃ v´, get symb (x-i) v´ ∧ v === v´ ∧ x ≥ i.

Lemma pos_none X `{OrderedType X} symb (x:X) k k´
: pos symb x k = None
  → pos symb x k´ = None.

Lemma pos_eq X `{OrderedType X} symb y k
: pos symb y k = Some k
  → hd_error symb === Some y.

Lemma pos_indep X `{OrderedType X} symb symb´ x y k k´
: pos symb x k = pos symb´ y k
  → pos symb x k´ = pos symb´ y k´.

Lemma pos_inc X `{OrderedType X} symb symb´ x y k k´
: pos symb x k = pos symb´ y k
  → pos symb x (k´ + k) = pos symb´ y (k´ + k).

Lemma pos_dec X `{OrderedType X} symb symb´ x y k k´
: pos symb x k = pos symb´ y k
  → pos symb x (k - k´) = pos symb´ y (k - k´).

Lemma pos_app_in X `{OrderedType X} x k L L´
: x ∈ of_list L
  → pos (L ++ L´) x k = pos L x k.

Lemma pos_app_not_in X `{OrderedType X} x k L L´
: x ∉ of_list L
  → pos (L ++ L´) x k = pos L´ x (length L + k).