(* 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.