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".