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 {_} {_} _ _ _.
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 {_} {_} _ _ _.