Commit 4fb332a6 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Fix regeneration of Coq realizations and add set.Set to realizaed theories.

parent 0e28a82a
......@@ -881,13 +881,16 @@ COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
COQLIBS_NUMBER_FILES = Divisibility Gcd Parity Prime
COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET_FILES = Set
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
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_FP)
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
......@@ -911,6 +914,8 @@ drivers/coq-realizations.aux: Makefile
echo 'theory real.'"$$f"' meta "realized" "real.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_NUMBER_FILES); do \
echo 'theory number.'"$$f"' meta "realized" "number.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_SET_FILES); do \
echo 'theory set.'"$$f"' meta "realized" "set.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized" "floating_point.'"$$f"'", "" end'; done; \
) > $@
......@@ -926,6 +931,8 @@ install_no_local::
cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
mkdir -p $(LIBDIR)/why3/coq/number
cp $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
mkdir -p $(LIBDIR)/why3/coq/set
cp $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/
ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
......@@ -949,6 +956,7 @@ update-coq: bin/why3 drivers/coq-realizations.aux
for f in $(COQLIBS_INT_ALL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
for f in $(COQLIBS_REAL_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T real.$$f -o lib/coq/real/; done
for f in $(COQLIBS_NUMBER_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T number.$$f -o lib/coq/number/; done
for f in $(COQLIBS_SET_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
for f in $(COQLIBS_FP_FILES); do bin/why3 --realize -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
else
......
......@@ -102,3 +102,4 @@ replace 1%R with (1*1)%R by auto with real.
apply Rmult_le_compat; auto with real.
Qed.
......@@ -7,12 +7,11 @@ Require Import ClassicalEpsilon.
Require Import FunctionalExtensionality.
(* "it is folklore that the two are consistent" *)
Parameter eq : forall {a:Type} {a_WT:WhyType a}, a -> a -> bool.
Axiom eq_dec:
forall {a:Type} {a_WT:WhyType a} (x y:a),
if eq x y then x=y else x<>y.
Variable eq : forall {a:Type} {a_WT:WhyType a}, a -> a -> bool.
Hypothesis eq_dec:
forall {a:Type} {a_WT:WhyType a} (x y:a),
if eq x y then x=y else x<>y.
(* Why3 goal *)
Definition set : forall (a:Type) {a_WT:WhyType a}, Type.
......@@ -20,6 +19,12 @@ intros.
exact (a -> bool).
Defined.
Global Instance set_WhyType : forall a {a_WT:WhyType a}, WhyType (set a).
Proof.
intros.
exact (fun _ => true).
Qed.
(* Why3 goal *)
Definition mem: forall {a:Type} {a_WT:WhyType a}, a -> (set a) -> Prop.
intros a a_WT x s.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment