(* Une théorie pour représenter les tableaux contenant des booléens *)

Require Import Omega.
Section BitArrays.
Variables T : Type.

(* length of arrays *)
Variable length : T -> nat.
(* access *)
Variable get : T -> nat -> bool.
(* update *)
Variable update : T -> nat -> bool -> T.
(* initialisation *)
Variable make : nat -> bool -> T.

(* Axioms *)
Hypothesis get_make : forall n k b, get (make n b) k = b.
Hypothesis length_make : forall n b, length (make n b) = n.

Hypothesis get_upd_eq : forall t n b, n < length t -> get (update t n b) n = b.
Hypothesis get_upd_diff : forall t n m b, n < length t -> m <> n 
           -> get (update t n b) m = get t m.
Hypothesis length_upd : forall t n b, length (update t n b) = length t.

Hypothesis ext : forall t1 t2, 
       length t1 = length t2 -> (forall n, n < length t1 -> get t1 n = get t2 n) 
       -> t1 = t2.

Goal False.




End BitArrays.