Library CoLoR.Util.List.ListDec

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2008-08-08
boolean functions on lists

Set Implicit Arguments.

Section S.

Variables (A : Type) (beq : A -> A -> bool)
(beq_ok : forall x y, beq x y = true <-> x = y).

Ltac case_beq := EqUtil.case_beq beq beq_ok.

boolean decidability of equality

Fixpoint beq_list (l m : list A) :=
match l, m with
| nil, nil => true
| x :: l', y :: m' => beq x y && beq_list l' m'
| _, _ => false
end.

Lemma beq_list_refl : forall l, beq_list l l = true.

Lemma beq_list_ok : forall l m, beq_list l m = true <-> l = m.

Lemma beq_list_ok_in : forall l,
forall hyp : forall x, In x l -> forall y, beq x y = true <-> x = y,
forall m, beq_list l m = true <-> l = m.

membership

Fixpoint mem (x : A) (l : list A) : bool :=
match l with
| nil => false
| y :: m => beq x y || mem x m
end.

Lemma mem_ok x : forall l, mem x l = true <-> In x l.

inclusion

Fixpoint incl (l l' : list A) : bool :=
match l with
| nil => true
| y :: m => mem y l' && incl m l'
end.

Lemma incl_ok : forall l l', incl l l' = true <-> l [= l'.

position of an element in a list

Fixpoint position_aux (i : nat) (x : A) (l : list A) : option nat :=
match l with
| nil => None
| y :: m => if beq x y then Some i else position_aux (S i) x m
end.

Definition position := position_aux 0.

Lemma position_ko : forall x l, position x l = None <-> ~In x l.

Lemma position_aux_plus x j k : forall l i,
position_aux i x l = Some k -> position_aux (i+j) x l = Some (k+j).

Lemma position_aux_S x k : forall l i,
position_aux i x l = Some k -> position_aux (S i) x l = Some (S k).

Lemma position_aux_ok1 k x : forall l i,
position_aux i x l = Some k -> k >= i /\ element_at l (k-i) = Some x.

Lemma position_aux_ok2 i x : forall l k, element_at l k = Some x ->
exists k', k' <= k /\ position_aux i x l = Some (i+k').

End S.

tactics

Ltac incl beq_ok :=
rewrite <- (incl_ok beq_ok); check_eq
|| fail 10 "list inclusion not satisfied".