Commit 99f907f1 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Start realizing theories list and option in Coq.

parent d6690d88
......@@ -828,13 +828,19 @@ COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_MAP_FILES = Map MapPermut
COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
COQLIBS_LIST_FILES = List Length Nth NthLength
COQLIBS_LIST = $(addprefix lib/coq/list/, $(COQLIBS_LIST_FILES))
COQLIBS_OPTION_FILES = Option
COQLIBS_OPTION = $(addprefix lib/coq/option/, $(COQLIBS_OPTION_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_BOOL) $(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_LIST) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
......@@ -864,6 +870,10 @@ drivers/coq-realizations.aux: Makefile
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_LIST_FILES); do \
echo 'theory list.'"$$f"' meta "realized_theory" "list.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_OPTION_FILES); do \
echo 'theory option.'"$$f"' meta "realized_theory" "option.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
......@@ -885,6 +895,10 @@ install_no_local::
cp $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/
mkdir -p $(LIBDIR)/why3/coq/map
cp $(addsuffix .vo, $(COQLIBS_MAP)) $(LIBDIR)/why3/coq/map/
mkdir -p $(LIBDIR)/why3/coq/list
cp $(addsuffix .vo, $(COQLIBS_LIST)) $(LIBDIR)/why3/coq/list/
mkdir -p $(LIBDIR)/why3/coq/option
cp $(addsuffix .vo, $(COQLIBS_OPTION)) $(LIBDIR)/why3/coq/option/
ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
......@@ -894,7 +908,7 @@ endif
install_local: $(COQVO) drivers/coq-realizations.aux
ifneq "$(MAKECMDGOALS)" "clean"
ifneq "$(MAKECMDGOALS)" "update-coq"
ifneq "$(MAKECMDGOALS:update-coq%=update-coq)" "update-coq"
include $(COQVD)
endif
endif
......@@ -904,7 +918,7 @@ depend: $(COQVD)
clean::
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
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: update-coq-int update-coq-bool update-coq-real update-coq-number update-coq-set update-coq-map update-coq-list update-coq-option 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
......@@ -924,6 +938,12 @@ update-coq-set: bin/why3 drivers/coq-realizations.aux theories/set.why
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-list: bin/why3 drivers/coq-realizations.aux theories/list.why
for f in $(COQLIBS_LIST_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T list.$$f -o lib/coq/list/; done
update-coq-option: bin/why3 drivers/coq-realizations.aux theories/option.why
for f in $(COQLIBS_OPTION_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T option.$$f -o lib/coq/option/; 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
......
......@@ -240,7 +240,6 @@ theory real.Square
end
theory real.ExpLog
prelude "Require Import Rtrigo_def."
......@@ -258,7 +257,6 @@ theory real.ExpLog
end
theory real.PowerInt
prelude "Require Import Rfunctions."
......@@ -273,5 +271,21 @@ theory real.PowerInt
end
theory list.List
syntax type list "list %1"
syntax function Nil "nil"
syntax function Cons "(cons %1 %2)"
end
theory option.Option
syntax type option "option %1"
syntax function None "None"
syntax function Some "(Some %1)"
end
(* this file has an extension .aux rather than .gen since it should not be distributed *)
import "coq-realizations.aux"
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* Why3 assumption *)
Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z :=
Fixpoint length {a:Type} {a_WT:WhyType a} (l:list a) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
| nil => 0%Z
| (cons _ r) => (1%Z + (length r))%Z
end.
(* Why3 goal *)
Lemma Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list
a)), (0%Z <= (length l))%Z.
Lemma Length_nonnegative : forall {a:Type} {a_WT:WhyType a},
forall (l:list a), (0%Z <= (length l))%Z.
Proof.
intros a a_WT l.
induction l as [|h t].
apply Zle_refl.
unfold length.
fold length.
omega.
Qed.
(* Why3 goal *)
Lemma Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
intros a a_WT l.
Lemma Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:list a),
((length l) = 0%Z) <-> (l = nil).
Proof.
intros a a_WT [|h t] ; split ; try easy.
unfold length. fold length.
intros H.
generalize (Length_nonnegative t).
omega.
Qed.
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
(* Why3 assumption *)
Inductive list (a:Type) {a_WT:WhyType a} :=
| Nil : list a
| Cons : a -> (list a) -> list a.
Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a).
Existing Instance list_WhyType.
Implicit Arguments Nil [[a] [a_WT]].
Implicit Arguments Cons [[a] [a_WT]].
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require option.Option.
(* Why3 goal *)
Definition nth: forall {a:Type} {a_WT:WhyType a}, Z -> list a -> option a.
intros a a_WT.
exact (fix nth n l := match l with nil => None | cons h t => if Zeq_bool n Z0 then Some h else nth (n - 1)%Z t end).
Defined.
(* Why3 goal *)
Lemma nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (l:list a),
match l with
| nil => ((nth n l) = None)
| (cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
end.
Proof.
intros a a_WT n l.
revert n.
induction l.
easy.
intros n.
split.
intros ->.
easy.
simpl.
generalize (Zeq_bool_if n 0).
now case Zeq_bool.
Qed.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require list.List.
Require list.Length.
Require list.Nth.
Require option.Option.
(* Why3 goal *)
Lemma nth_none_1 : forall {a:Type} {a_WT:WhyType a}, forall (l:list a) (i:Z),
(i < 0%Z)%Z -> ((list.Nth.nth i l) = None).
Proof.
intros a a_WT l.
induction l as [|h q].
easy.
intros i H.
simpl.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
intros H'.
now rewrite H' in H.
intros _.
apply IHq.
omega.
Qed.
(* Why3 goal *)
Lemma nth_none_2 : forall {a:Type} {a_WT:WhyType a}, forall (l:list a) (i:Z),
((list.Length.length l) <= i)%Z -> ((list.Nth.nth i l) = None).
Proof.
intros a a_WT l.
induction l as [|h q].
easy.
intros i H.
unfold Length.length in H.
fold Length.length in H.
simpl.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
intros H'.
rewrite H' in H.
generalize (Length.Length_nonnegative q).
omega.
intros _.
apply IHq.
omega.
Qed.
(* Why3 goal *)
Lemma nth_none_3 : forall {a:Type} {a_WT:WhyType a}, forall (l:list a) (i:Z),
((list.Nth.nth i l) = None) -> ((i < 0%Z)%Z \/
((list.Length.length l) <= i)%Z).
Proof.
intros a a_WT l.
induction l as [|h q].
intros i _.
simpl.
omega.
intros i.
simpl (Nth.nth i (h :: q)).
change (Length.length (h :: q)) with (1 + Length.length q)%Z.
generalize (Zeq_bool_if i 0).
case Zeq_bool.
easy.
intros Hi H.
specialize (IHq _ H).
omega.
Qed.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
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