diff --git a/Makefile.in b/Makefile.in index 9a2a26c7abd5306a6e17c29ed89006bb4fd7716b..b989f18248a2dbaffc3613d22ee14bb10ade5a38 100644 --- a/Makefile.in +++ b/Makefile.in @@ -806,6 +806,9 @@ COQLIBS_INT_FILES = Abs ComputerDivision Div2 EuclideanDivision Int MinMax Power COQLIBS_INT_ALL_FILES = Exponentiation $(COQLIBS_INT_FILES) COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_ALL_FILES)) +COQLIBS_BOOL_FILES = Bool +COQLIBS_BOOL = $(addprefix lib/coq/bool/, $(COQLIBS_BOOL_FILES)) + COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax PowerInt Real Square RealInfix COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES)) @@ -824,7 +827,7 @@ COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES) COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES)) endif -COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_FP) +COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_BOOL) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_FP) COQV = $(addsuffix .v, $(COQLIBS_FILES)) COQVO = $(addsuffix .vo, $(COQLIBS_FILES)) @@ -844,6 +847,8 @@ drivers/coq-realizations.aux: Makefile echo 'theory BuiltIn meta "realized_theory" "BuiltIn", "" end'; \ for f in $(COQLIBS_INT_FILES); do \ echo 'theory int.'"$$f"' meta "realized_theory" "int.'"$$f"'", "" end'; done; \ + for f in $(COQLIBS_BOOL_FILES); do \ + echo 'theory bool.'"$$f"' meta "realized_theory" "bool.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_REAL_FILES); do \ echo 'theory real.'"$$f"' meta "realized_theory" "real.'"$$f"'", "" end'; done; \ for f in $(COQLIBS_NUMBER_FILES); do \ @@ -863,6 +868,8 @@ install_no_local:: cp lib/coq/BuiltIn.vo $(LIBDIR)/why3/coq/ mkdir -p $(LIBDIR)/why3/coq/int cp $(addsuffix .vo, $(COQLIBS_INT)) $(LIBDIR)/why3/coq/int/ + mkdir -p $(LIBDIR)/why3/coq/bool + cp $(addsuffix .vo, $(COQLIBS_BOOL)) $(LIBDIR)/why3/coq/bool/ mkdir -p $(LIBDIR)/why3/coq/real cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/ mkdir -p $(LIBDIR)/why3/coq/number @@ -890,11 +897,14 @@ depend: $(COQVD) clean:: rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES)) -update-coq: update-coq-int update-coq-real update-coq-number update-coq-set update-coq-map update-coq-fp +update-coq: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-fp update-coq-int: bin/why3 drivers/coq-realizations.aux theories/int.why for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done +update-coq-bool: bin/why3 drivers/coq-realizations.aux theories/bool.why + for f in $(COQLIBS_BOOL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T bool.$$f -o lib/coq/bool/; done + update-coq-real: bin/why3 drivers/coq-realizations.aux theories/real.why for f in $(COQLIBS_REAL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done diff --git a/drivers/coq-common.gen b/drivers/coq-common.gen index 66f17933ac3077ec282e49685827a4c3a5bdeba1..43def460c13df8552de1e288c37bbb069c4c6879 100644 --- a/drivers/coq-common.gen +++ b/drivers/coq-common.gen @@ -39,7 +39,7 @@ theory bool.Bool syntax function orb "(orb %1 %2)" syntax function xorb "(xorb %1 %2)" syntax function notb "(negb %1)" - syntax function implb "(implb %1)" + syntax function implb "(implb %1 %2)" end diff --git a/lib/coq/bool/Bool.v b/lib/coq/bool/Bool.v new file mode 100644 index 0000000000000000000000000000000000000000..d10e0231c33845558caa91af2367ff070c9a3bc9 --- /dev/null +++ b/lib/coq/bool/Bool.v @@ -0,0 +1,61 @@ +(* This file is generated by Why3's Coq-realize driver *) +(* Beware! Only edit allowed sections below *) +Require Import BuiltIn. +Require BuiltIn. + +(* Why3 goal *) +Lemma andb_def : forall (x:bool) (y:bool), + ((andb x y) = match x with + | true => y + | false => false + end). +Proof. +intros x y. +apply refl_equal. +Qed. + +(* Why3 goal *) +Lemma orb_def : forall (x:bool) (y:bool), + ((orb x y) = match x with + | false => y + | true => true + end). +Proof. +intros x y. +apply refl_equal. +Qed. + +(* Why3 goal *) +Lemma xorb_def : forall (x:bool) (y:bool), ((xorb x y) = match (x, + y) with + | (true, false) => true + | (false, true) => true + | (_, _) => false + end). +Proof. +intros x y. +apply refl_equal. +Qed. + +(* Why3 goal *) +Lemma notb_def : forall (x:bool), + ((negb x) = match x with + | false => true + | true => false + end). +Proof. +intros x. +apply refl_equal. +Qed. + +(* Why3 goal *) +Lemma implb_def : forall (x:bool) (y:bool), ((implb x y) = match (x, + y) with + | (true, false) => false + | (_, _) => true + end). +Proof. +now intros [|] [|]. +Qed. + +