Commit 4c401f16 authored by MARCHE Claude's avatar MARCHE Claude

fix generation of Coq headers for realizations

parent 868901e2
......@@ -929,7 +929,7 @@ ifeq (@enable_coq_fp_libs@,yes)
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
endif
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 headers-coq
update-coq: remove-coq-headers 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 headers-coq
update-coq-int: bin/why3realize.@OCAMLBEST@ drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3realize.@OCAMLBEST@ -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
......@@ -1841,6 +1841,9 @@ headers-coq:
headache -c misc/headache_config.txt -h misc/header.txt \
lib/coq/*/*.v
remove-coq-headers:
headache -r -c misc/headache_config.txt lib/coq/*/*.v
#########
# myself
#########
......
......@@ -14,11 +14,6 @@
Require Import BuiltIn.
Require BuiltIn.
(* 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),
((Init.Datatypes.andb x y) = match x with
......
......@@ -21,18 +21,6 @@ Require real.FromInt.
Require floating_point.Rounding.
Require floating_point.DoubleFormat.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Reals.Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require floating_point.DoubleFormat.
Require Import floating_point.GenFloat.
(* Why3 goal *)
......
......@@ -14,11 +14,6 @@
Require Import BuiltIn.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require Import floating_point.GenFloat.
(* Why3 goal *)
......
......@@ -14,11 +14,6 @@
Require Import BuiltIn.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
(* Why3 assumption *)
Inductive mode :=
| NearestTiesToEven : mode
......
......@@ -21,18 +21,6 @@ Require real.FromInt.
Require floating_point.Rounding.
Require floating_point.SingleFormat.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Reals.Rbasic_fun.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.Abs.
Require real.FromInt.
Require floating_point.Rounding.
Require floating_point.SingleFormat.
Require Import floating_point.GenFloat.
(* Why3 goal *)
......
......@@ -14,11 +14,6 @@
Require Import BuiltIn.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require Import floating_point.GenFloat.
(* Why3 goal *)
......
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 comment *)
(* abs is replaced with (ZArith.BinInt.Z.abs x) by the coq driver *)
......
......@@ -16,13 +16,6 @@ Require BuiltIn.
Require int.Int.
Require int.Abs.
(* 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 int.Abs.
Require Import Zquot.
(* Why3 comment *)
......
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* 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 Import int.EuclideanDivision.
(* Why3 goal *)
......
......@@ -16,13 +16,6 @@ Require BuiltIn.
Require int.Int.
Require int.Abs.
(* 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 int.Abs.
(* Why3 goal *)
Definition div: Z -> Z -> Z.
intros x y.
......
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Section Exponentiation.
(* Why3 goal *)
......
......@@ -14,11 +14,6 @@
Require Import BuiltIn.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
(* Why3 comment *)
(* infix_ls is replaced with (x < x1)%Z by the coq driver *)
......
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* Why3 comment *)
(* min is replaced with (ZArith.BinInt.Z.min x x1) by the coq driver *)
......
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
(* 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 Import Exponentiation.
(* Why3 goal *)
......
......@@ -18,15 +18,6 @@ Require list.List.
Require list.Length.
Require list.Mem.
(* 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.Mem.
(* Why3 goal *)
Lemma infix_plpl_def : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)),
......
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require list.List.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
(* Why3 comment *)
(* combine is replaced with (Lists.List.combine x x1) by the coq driver *)
......
......@@ -19,16 +19,6 @@ Require list.Length.
Require list.Mem.
Require list.Append.
(* 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.Mem.
Require list.Append.
(* Why3 assumption *)
Inductive distinct {a:Type} {a_WT:WhyType a}: (list a) -> Prop :=
| distinct_zero : (distinct Init.Datatypes.nil)
......
......@@ -16,13 +16,6 @@ Require BuiltIn.
Require list.List.
Require option.Option.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
Require option.Option.
(* Why3 assumption *)
Definition hd {a:Type} {a_WT:WhyType a} (l:(list a)): (option a) :=
match l with
......
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require list.List.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
(* Why3 goal *)
Definition hd: forall {a:Type} {a_WT:WhyType a}, (list a) -> a.
intros a a_WT [|h _].
......
......@@ -16,13 +16,6 @@ Require BuiltIn.
Require int.Int.
Require list.List.
(* 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 *)
Fixpoint length {a:Type} {a_WT:WhyType a} (l:(list a)) {struct l}: Z :=
match l with
......
......@@ -14,11 +14,6 @@
Require Import BuiltIn.
Require BuiltIn.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Global Instance list_WhyType : forall T {T_WT : WhyType T}, WhyType (list T).
split.
apply nil.
......
......@@ -15,12 +15,6 @@ Require Import BuiltIn.
Require BuiltIn.
Require list.List.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require list.List.
(* Why3 assumption *)
Fixpoint mem {a:Type} {a_WT:WhyType a} (x:a) (l:(list a)) {struct l}: Prop :=
match l with
......
......@@ -17,14 +17,6 @@ Require int.Int.
Require list.List.
Require option.Option.
(* 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).
......
......@@ -19,16 +19,6 @@ Require list.Nth.
Require option.Option.
Require list.HdTl.
(* 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.Nth.
Require option.Option.
Require list.HdTl.
(* Why3 goal *)
Lemma Nth_tl : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)), ((list.HdTl.tl l1) = (Init.Datatypes.Some l2)) ->
......
......@@ -19,16 +19,6 @@ Require list.Length.
Require list.Nth.
Require option.Option.
(* 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) = Init.Datatypes.None).
......
......@@ -22,19 +22,6 @@ Require option.Option.
Require list.NthLength.
Require list.Append.
(* 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.Mem.
Require list.Nth.
Require option.Option.
Require list.NthLength.
Require list.Append.
(* Why3 goal *)
Lemma nth_append_1 : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a))
(l2:(list a)) (i:Z), (i < (list.Length.length l1))%Z -> ((list.Nth.nth i
......
......@@ -16,13 +16,6 @@ Require BuiltIn.
Require int.Int.
Require list.List.
(* 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 goal *)
Definition nth: forall {a:Type} {a_WT:WhyType a}, Z -> (list a) -> a.
intros a a_WT.
......
......@@ -20,17 +20,6 @@ Require list.Mem.
Require list.Append.
Require list.Reverse.
(* 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.Mem.
Require list.Append.
Require list.Reverse.
(* Why3 goal *)
Definition num_occ: forall {a:Type} {a_WT:WhyType a}, a -> (list a) -> Z.
intros a a_WT x.
......
......@@ -21,18 +21,6 @@ Require list.Append.
Require list.Reverse.
Require list.NumOcc.
(* 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.Mem.
Require list.Append.
Require list.Reverse.
Require list.NumOcc.
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (l1:(list a))
(l2:(list a)): Prop := forall (x:a), ((list.NumOcc.num_occ x
......
......@@ -20,17 +20,6 @@ Require list.Mem.
Require list.Append.
Require list.Reverse.
(* 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.Mem.
Require list.Append.
Require list.Reverse.
(* Why3 goal *)
Lemma rev_append_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(list a))
(t:(list a)),
......
......@@ -19,16 +19,6 @@ Require list.Length.
Require list.Mem.
Require list.Append.
(* 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.Mem.
Require list.Append.
(* Why3 goal *)
Lemma reverse_def : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)),
((Lists.List.rev l) = match l with
......@@ -98,4 +88,3 @@ intros a a_WT l.
rewrite 2!Length.length_std.
now rewrite List.rev_length.
Qed.
......@@ -17,14 +17,6 @@ Require int.Int.
Require map.Map.
Require map.Occ.
(* 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 map.Map.
Require map.Occ.
(* preliminaries *)
Definition into (n:nat) (f:nat -> nat) :=
......@@ -91,11 +83,11 @@ assert (trans_inj: injection (S n) trans).
(* i = n *)
destruct (eq_nat_dec j n); auto with *.
(* i = n and j <> n *)
destruct (eq_nat_dec j k); omega.
destruct (eq_nat_dec j k); omega.
(* i <> n *)
destruct (eq_nat_dec i k); auto with *.
destruct (eq_nat_dec j n); auto with *.
destruct (eq_nat_dec j k); omega.
destruct (eq_nat_dec j k); omega.
(* i <> n and i <> k *)
destruct (eq_nat_dec j n); auto with *.
destruct (eq_nat_dec j k); omega.
......@@ -164,7 +156,7 @@ Qed.
Require Import ZArith.
Open Scope Z_scope.
Theorem lifting:
Theorem lifting:
forall n:Z,
forall f:Z -> Z,
(forall x:Z, 0 <= x < n -> 0 <= f x < n) ->
......@@ -217,7 +209,7 @@ elim (Hsurj_g j); auto with *.
intros x (inter_x, eq_x).
exists (Z_of_nat x).
split; auto with *.
rewrite <- Heq_g_f; omega.
rewrite <- Heq_g_f; omega.
Qed.
......@@ -334,4 +326,3 @@ assert (occ v m (i+1) n >= 1)%Z.
omega.
generalize (Hocc v); omega.
Qed.
......@@ -17,14 +17,6 @@ Require int.Int.
Require map.Map.
Require map.Occ.
(* 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 map.Map.
Require map.Occ.
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (m1:(map.Map.map Z a))
(m2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (v:a), ((map.Occ.occ v
......@@ -53,6 +45,5 @@ assert (0 < map.Occ.occ v a2 l u)%Z.
rewrite <- h1 in H.
generalize (map.Occ.occ_exists v a1 l u H).
intros (j, (hj1,hj2)).
exists j; intuition.
exists j; intuition.
Qed.
......@@ -16,13 +16,6 @@ Require BuiltIn.
Require int.Int.
Require map.Map.
(* 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 map.Map.
(* Why3 goal *)
Definition occ: forall {a:Type} {a_WT:WhyType a}, a -> (map.Map.map Z a) ->
Z -> Z -> Z.
......@@ -118,7 +111,7 @@ omega.
omega.
replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
trivial.
replace (l + (u-l))%Z with u by ring. trivial.
replace (l + (u-l))%Z with u by ring. trivial.
Qed.
(* Why3 goal *)
......@@ -161,8 +154,8 @@ replace (mid + x - 1)%Z with (mid+(x-1))%Z by ring. trivial.
omega.
replace (mid + x - 1)%Z with (mid+(x-1))%Z by ring. trivial.
replace (mid + (u-mid))%Z with u by ring. trivial.
replace (mid + (u-mid))%Z with u by ring. trivial.
replace (mid + (u-mid))%Z with u by ring. trivial.
replace (mid + (u-mid))%Z with u by ring. trivial.
Qed.
(* Why3 goal *)
......@@ -274,4 +267,3 @@ replace (l + x - 1)%Z with (l+(x-1))%Z by ring.
rewrite <- h0. trivial. omega. omega.
replace (l + x - 1)%Z with (l+(x-1))%Z by ring. assumption.
Qed.
......@@ -22,19 +22,6 @@ Require number.Divisibility.
Require number.Gcd.
Require number.Prime.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *