updated Coq realization

parent 3ee891f7
......@@ -946,7 +946,7 @@ ifeq (@enable_coq_fp_libs@,yes)
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
endif
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: 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 update-coq-seq 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
......
......@@ -280,3 +280,4 @@ intros p1 p2 a b h1.
apply le_ge_eq.
split; apply numof_change_any; apply h1.
Qed.
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
......@@ -63,7 +52,7 @@ auto with *.
Qed.
(* Why3 goal *)
Definition mixfix_lbrb: forall {a:Type} {a_WT:WhyType a}, (seq a) -> Z -> a.
Definition get: forall {a:Type} {a_WT:WhyType a}, (seq a) -> Z -> a.
intros a (default, _) s i.
exact ((fix nth n l := match l with
| nil => default
......@@ -73,7 +62,7 @@ Defined.
(* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(seq a)) (s2:(seq
a)): Prop := ((length s1) = (length s2)) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < (length s1))%Z) -> ((mixfix_lbrb s1 i) = (mixfix_lbrb s2 i)).
(i < (length s1))%Z) -> ((get s1 i) = (get s2 i)).
Notation "x == y" := (infix_eqeq x y) (at level 70, no associativity).
......@@ -103,7 +92,7 @@ assert (h: (0 <= 0 < length (a0 :: s1)%list)%Z).
unfold length. fold length.
generalize (length_nonneg s1); omega.
generalize (H1 0%Z h); clear H1.
unfold mixfix_lbrb. destruct a_WT. auto.
unfold get. destruct a_WT. auto.
apply IHs1.
split.
unfold length in H0. fold length in H0. omega.
......@@ -111,7 +100,7 @@ intros i hi.
assert (h: (0 <= i+1 < length (a0 :: s1)%list)%Z).
unfold length. fold length. omega.
generalize (H1 (i+1)%Z h); clear H1.
unfold mixfix_lbrb. destruct a_WT.
unfold get. destruct a_WT.
assert (Zeq_bool (i+1) 0 = false).
generalize (Zeq_is_eq_bool (i+1) 0).
case (Zeq_bool (i+1) 0); intuition.
......@@ -138,8 +127,8 @@ Qed.
(* Why3 goal *)
Lemma cons_get : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (s:(seq a))
(i:Z), ((0%Z <= i)%Z /\ (i <= (length s))%Z) -> (((i = 0%Z) ->
((mixfix_lbrb (cons x s) i) = x)) /\ ((~ (i = 0%Z)) ->
((mixfix_lbrb (cons x s) i) = (mixfix_lbrb s (i - 1%Z)%Z)))).
((get (cons x s) i) = x)) /\ ((~ (i = 0%Z)) -> ((get (cons x s) i) = (get s
(i - 1%Z)%Z)))).
intros a (d,eq) x s i hi.
split.
intro; subst i; now auto.
......@@ -147,7 +136,7 @@ intro; subst i; now auto.
destruct s.
simpl in hi. intro. absurd (i=0)%Z; omega.
intro h.
unfold mixfix_lbrb at 1.
unfold get at 1.
simpl ((fix nth (n : int) (l : list a) {struct l} : a :=
match l with
| nil => d
......@@ -188,8 +177,8 @@ Qed.
(* Why3 goal *)
Lemma snoc_get : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (x:a)
(i:Z), ((0%Z <= i)%Z /\ (i <= (length s))%Z) -> (((i < (length s))%Z ->
((mixfix_lbrb (snoc s x) i) = (mixfix_lbrb s i))) /\
((~ (i < (length s))%Z) -> ((mixfix_lbrb (snoc s x) i) = x))).
((get (snoc s x) i) = (get s i))) /\ ((~ (i < (length s))%Z) ->
((get (snoc s x) i) = x))).
(*
intros a a_WT (l, d) x i (h1,h2).
split; intros.
......@@ -233,7 +222,7 @@ Admitted. (* TODO *)
Lemma sub_get : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
(j:Z), ((0%Z <= i)%Z /\ ((i <= j)%Z /\ (j <= (length s))%Z)) ->
forall (k:Z), ((0%Z <= k)%Z /\ (k < (j - i)%Z)%Z) ->
((mixfix_lbrb (mixfix_lb_dtdt_rb s i j) k) = (mixfix_lbrb s (i + k)%Z)).
((get (mixfix_lb_dtdt_rb s i j) k) = (get s (i + k)%Z)).
intros a a_WT s i j (h1,(h2,h3)) k (h4,h5).
Admitted. (* TODO *)
......@@ -254,19 +243,18 @@ Lemma concat_length : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
(s2:(seq a)), ((length (infix_plpl s1
s2)) = ((length s1) + (length s2))%Z).
(*
intros a a_WT (l1,d1) (l2,d2).
unfold length; simpl.
intros a a_WT s1 s2.
unfold length, infix_plpl.
rewrite List.app_length.
rewrite Nat2Z.inj_add. auto.
Qed.
*)
Admitted. (* TODO *)
(* Why3 goal *)
Lemma concat_get1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
(s2:(seq a)) (i:Z), ((0%Z <= i)%Z /\ (i < (length s1))%Z) ->
((mixfix_lbrb (infix_plpl s1 s2) i) = (mixfix_lbrb s1 i)).
((get (infix_plpl s1 s2) i) = (get s1 i)).
intros a a_WT s1 s2 i (h1,h2).
Admitted. (* TODO *)
......@@ -274,8 +262,8 @@ Admitted. (* TODO *)
(* Why3 goal *)
Lemma concat_get2 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
(s2:(seq a)) (i:Z), (((length s1) <= i)%Z /\
(i < ((length s1) + (length s2))%Z)%Z) -> ((mixfix_lbrb (infix_plpl s1 s2)
i) = (mixfix_lbrb s2 (i - (length s1))%Z)).
(i < ((length s1) + (length s2))%Z)%Z) -> ((get (infix_plpl s1 s2)
i) = (get s2 (i - (length s1))%Z)).
intros a a_WT s1 s2 i (h1,h2).
Admitted. (* TODO *)
......@@ -320,9 +308,16 @@ Qed.
(* Why3 goal *)
Lemma create_get : forall {a:Type} {a_WT:WhyType a}, forall (len:Z) (f:(Z ->
a)) (i:Z), ((0%Z <= i)%Z /\ (i < len)%Z) -> ((mixfix_lbrb (create len f)
i) = (f i)).
a)) (i:Z), ((0%Z <= i)%Z /\ (i < len)%Z) -> ((get (create len f) i) = (f
i)).
intros a a_WT len f i (h1,h2).
Admitted. (* TODO *)
(* Unused content named mixfix_lbrb
intros a (default, _) s i.
exact ((fix nth n l := match l with
| nil => default
| cons h t => if Zeq_bool n 0%Z then h else nth (n - 1)%Z t end) i s).
Defined.
*)
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