Commit 918f1945 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add Coq realization for map.Map.

parent d21fa51e
......@@ -815,13 +815,16 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET_FILES = Set
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_MAP_FILES = Map
COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_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_SET) $(COQLIBS_FP)
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_MAP) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
......@@ -847,6 +850,8 @@ drivers/coq-realizations.aux: Makefile
echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_SET_FILES); do \
echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_MAP_FILES); do \
echo 'theory map.'"$$f"' meta "realized_theory" "map.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
......@@ -855,8 +860,8 @@ opt byte: $(COQVO)
install_no_local::
mkdir -p $(LIBDIR)/why3/coq
mkdir -p $(LIBDIR)/why3/coq/int
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/real
cp $(addsuffix .vo, $(COQLIBS_REAL)) $(LIBDIR)/why3/coq/real/
......@@ -864,6 +869,8 @@ install_no_local::
cp $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
mkdir -p $(LIBDIR)/why3/coq/set
cp $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/
mkdir -p $(LIBDIR)/why3/coq/map
cp $(addsuffix .vo, $(COQLIBS_MAP)) $(LIBDIR)/why3/coq/map/
ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
......@@ -883,7 +890,7 @@ 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-fp
update-coq: update-coq-int 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
......@@ -897,6 +904,9 @@ update-coq-number: bin/why3 drivers/coq-realizations.aux theories/number.why
update-coq-set: bin/why3 drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
update-coq-map: bin/why3 drivers/coq-realizations.aux theories/map.why
for f in $(COQLIBS_MAP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T map.$$f -o lib/coq/map/; done
update-coq-fp: bin/why3 drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
......
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require Import ClassicalEpsilon.
Inductive _map (a b:Type) :=
| _map_constr : (a -> b) -> _map a b.
(* Why3 goal *)
Definition map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b},
Type.
intros.
exact (_map a b).
Defined.
Global Instance map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b).
Proof.
intros.
repeat split.
exact (fun _ => why_inhabitant).
intros x y.
apply excluded_middle_informative.
Qed.
(* Why3 goal *)
Definition get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
intros a a_WT b b_WT (m) x.
exact (m x).
Defined.
(* Why3 goal *)
Definition set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
intros a a_WT b b_WT (m) x y.
split.
intros x'.
destruct (why_decidable_eq x x') as [H|H].
exact y.
exact (m x').
Defined.
(* Why3 goal *)
Lemma Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Proof.
intros a a_WT b b_WT (m) a1 a2 b1 h1.
unfold get, set.
now case why_decidable_eq.
Qed.
(* Why3 goal *)
Lemma Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Proof.
intros a a_WT b b_WT (m) a1 a2 b1 h1.
unfold get, set.
now case why_decidable_eq.
Qed.
(* Why3 goal *)
Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
intros a a_WT b b_WT y.
exact (_map_constr _ _ (fun _ => y)).
Defined.
(* Why3 goal *)
Lemma Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
Proof.
easy.
Qed.
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