# BaseLists

Require Import Base LTactics.

Ltac fstep N := unfold N; fold N.

Ltac have E := let X := fresh "E" in decide E as [X|X]; subst; try congruence; try omega; clear X.

Section Fix_X.

Variable X : Type.

Hypothesis eq_dec_X : eq_dec X.

Lemma pos_None (x : X) l l' : pos x l = None-> pos x l' = None -> pos x (l ++ l') = None.

Proof.

revert x l'; induction l; simpl; intros; eauto.

have (x = a).

destruct (pos x l) eqn:E; try congruence.

rewrite IHl; eauto.

Qed.

Lemma pos_first_S (x : X) l l' i : pos x l = Some i -> pos x (l ++ l') = Some i.

Proof.

revert x i; induction l; intros; simpl in *.

- inv H.

- decide (x = a); eauto.

destruct (pos x l) eqn:E.

+ eapply IHl in E.
now rewrite E.
+ inv H.

Qed.

Lemma pos_second_S x l l' i : pos x l = None ->
pos x l' = Some i ->
pos x (l ++ l') = Some ( i + |l| ).

Proof.

revert i l'; induction l; simpl; intros.

- rewrite plus_comm.
eauto.
- dec; subst; try congruence.

destruct (pos x l) eqn:EE.
congruence.
erewrite IHl; eauto.

Qed.

Lemma pos_length (e : X) n E : pos e E = Some n -> n < |E|.

Proof.

revert e n; induction E; simpl; intros.

- inv H.

- decide (e = a).

+ inv H.
simpl. omega.
+ destruct (pos e E) eqn:EE.

* inv H.
assert (n1 < |E|) by eauto. omega.
* inv H.

Qed.

Fixpoint replace (xs : list X) (y y' : X) :=
match xs with
| nil => nil
| x :: xs' => (if decision (x = y) then y' else x) :: replace xs' y y'
end.

Lemma replace_same xs x : replace xs x x = xs.

Proof.

revert x; induction xs; intros; simpl; [ | dec; subst ]; congruence.

Qed.

Lemma replace_diff xs x y : x <> y -> ~ x el replace xs x y.

Proof.

revert x y; induction xs; intros; simpl; try dec; firstorder.

Qed.

Lemma replace_pos xs x y y' : x <> y -> x <> y' -> pos x xs = pos x (replace xs y y').

Proof.

induction xs; intros; simpl.

- reflexivity.

- repeat dec; try congruence; try omega; subst; decide (a = y); try now congruence; subst.

+ rewrite IHxs; eauto. + rewrite IHxs; eauto.

Qed.

End Fix_X.

Arguments replace {_} {_} _ _ _.