Commit c2674ad6 authored by Clement Fumex's avatar Clement Fumex

update Coq realisations

Fix Bool.v
Add TODO to Seq.v and BV_Gen.v
update queens_bv session
parent 311905a8
......@@ -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 update-coq-seq 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 update-coq-bv 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
......
This diff is collapsed.
......@@ -36,19 +36,6 @@ intros x y.
apply refl_equal.
Qed.
(* Why3 goal *)
Lemma xorb_def : forall (x:bool) (y:bool),
((Init.Datatypes.xorb x y) = match (x,
y) with
| (true, false) => true
| (false, true) => true
| (_, _) => false
end).
Proof.
intros x y.
apply refl_equal.
Qed.
(* Why3 goal *)
Lemma notb_def : forall (x:bool),
((Init.Datatypes.negb x) = match x with
......@@ -60,12 +47,22 @@ intros x.
apply refl_equal.
Qed.
(* Why3 goal *)
Lemma xorb_def : forall (x:bool) (y:bool),
((Init.Datatypes.xorb x y) = match x with
| false => y
| true => (Init.Datatypes.negb y)
end).
Proof.
intros x y.
destruct x; destruct y; auto.
Qed.
(* Why3 goal *)
Lemma implb_def : forall (x:bool) (y:bool),
((Init.Datatypes.implb x y) = match (x,
y) with
| (true, false) => false
| (_, _) => true
((Init.Datatypes.implb x y) = match x with
| false => true
| true => y
end).
Proof.
now intros [|] [|].
......
(********************************************************************)
(* *)
(* 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.
Require BuiltIn.
Require bool.Bool.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require bv.Pow2int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......@@ -194,6 +193,32 @@ Definition nth: t -> Z -> bool.
exact nth_aux.
Defined.
Lemma nth_aux_out_of_bound : forall {l} (v : Vector.t bool l) (n : Z), ((n < 0%Z)%Z \/
(Z.of_nat l <= n)%Z) -> ((nth_aux v n) = false).
induction v.
simpl; auto.
simpl.
intros.
case Z.eq_dec.
intros; elimtype False; destruct H.
omega.
subst n0.
auto with zarith.
intro; rewrite IHv;auto.
intuition; auto with zarith.
right.
rewrite Zpos_P_of_succ_nat in H0.
omega.
Qed.
(* Why3 goal *)
Lemma nth_out_of_bound : forall (x:t) (n:Z), ((n < 0%Z)%Z \/
(size_int <= n)%Z) -> ((nth x n) = false).
intros.
unfold nth.
rewrite nth_aux_out_of_bound; auto with zarith.
Qed.
Definition zero_aux {l} : Vector.t bool l.
exact (Vector.const false l).
Defined.
......@@ -211,9 +236,8 @@ Lemma Nth_zero_aux : forall {l} (n:Z), ((@nth_aux l zero_aux n) = false).
Qed.
(* Why3 goal *)
Lemma Nth_zero : forall (n:Z), ((0%Z <= n)%Z /\ (n < size_int)%Z) ->
((nth zero n) = false).
intros n (h1,h2); apply Nth_zero_aux.
Lemma Nth_zero : forall (n:Z), ((nth zero n) = false).
intros n; apply Nth_zero_aux.
Qed.
Definition ones_aux l : Vector.t bool l.
......@@ -231,49 +255,6 @@ Lemma Nth_ones : forall (n:Z), ((0%Z <= n)%Z /\ (n < size_int)%Z) ->
intros; apply nth_const; easy.
Qed.
Definition eq_aux {l} (v1 v2 : Vector.t bool l): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < (Z.of_nat l))%Z) -> ((nth_aux v1 n) = (nth_aux v2 n)).
(* Why3 assumption *)
Definition eq (v1:t) (v2:t): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < size_int)%Z) -> ((nth v1 n) = (nth v2 n)).
Lemma eq_is_aux : forall v1 v2, eq_aux v1 v2 <-> eq v1 v2.
unfold eq_aux, eq; easy.
Qed.
Lemma eq_aux_cons : forall {l} v1 v2 b b', b = b' /\ @eq_aux l v1 v2 <-> eq_aux (b :: v1) (b' :: v2).
intros; unfold eq_aux.
rewrite Nat2Z.inj_succ.
split; intros.
simpl; case Z.eq_dec; intro.
easy.
apply H; omega.
split.
apply (H 0%Z); omega.
intros.
rewrite <- (nth_cons v1 n b) by omega.
rewrite <- (nth_cons v2 n b') by omega.
apply H; omega.
Qed.
Lemma Extensionality_aux : forall {l} (x y : Vector.t bool l), eq_aux x y -> x = y.
intros l x y; pattern l, x, y.
apply Vector.rect2.
easy.
intros.
apply (eq_aux_cons v1 v2 a b) in H0; destruct H0.
apply H in H1.
rewrite H0, H1; trivial.
Qed.
(* Why3 goal *)
Lemma Extensionality : forall (x:t) (y:t), (eq x y) -> (x = y).
intros x y.
rewrite <- eq_is_aux.
apply Extensionality_aux.
Qed.
(* Why3 goal *)
Definition bw_and: t -> t -> t.
exact (Vector.map2 (fun x y => x && y)).
......@@ -386,6 +367,34 @@ Definition asr: t -> Z -> t.
exact (fun v m => BshiftRa_iter last_bit v (Z.to_nat m)).
Defined.
Definition eq_aux {l} (v1 v2 : Vector.t bool l): Prop := forall (n:Z), ((0%Z <= n)%Z /\
(n < (Z.of_nat l))%Z) -> ((nth_aux v1 n) = (nth_aux v2 n)).
Lemma eq_aux_cons : forall {l} v1 v2 b b', b = b' /\ @eq_aux l v1 v2 <-> eq_aux (b :: v1) (b' :: v2).
intros; unfold eq_aux.
rewrite Nat2Z.inj_succ.
split; intros.
simpl; case Z.eq_dec; intro.
easy.
apply H; omega.
split.
apply (H 0%Z); omega.
intros.
rewrite <- (nth_cons v1 n b) by omega.
rewrite <- (nth_cons v2 n b') by omega.
apply H; omega.
Qed.
Lemma Extensionality_aux : forall {l} (x y : Vector.t bool l), eq_aux x y -> x = y.
intros l x y; pattern l, x, y.
apply Vector.rect2.
easy.
intros.
apply (eq_aux_cons v1 v2 a b) in H0; destruct H0.
apply H in H1.
rewrite H0, H1; trivial.
Qed.
(* Vector helper lemmas *)
Lemma singleton_is_singl : forall b : Vector.t bool 1, b = [ Vector.hd b ].
......@@ -1500,3 +1509,27 @@ Lemma two_power_size_val : ((max_int + 1%Z)%Z = (bv.Pow2int.pow2 size_int)).
unfold max_int.
omega.
Qed.
(* Why3 assumption *)
Definition eq_sub_bv (a:t) (b:t) (i:t) (n:t): Prop := let mask :=
(lsl_bv (sub (lsl_bv (of_int 1%Z) n) (of_int 1%Z)) i) in ((bw_and b
mask) = (bw_and a mask)).
(* Why3 assumption *)
Definition eq_sub (a:t) (b:t) (i:Z) (n:Z): Prop := forall (j:Z),
((i <= j)%Z /\ (j < (i + n)%Z)%Z) -> ((nth a j) = (nth b j)).
(* Why3 goal *)
Lemma eq_sub_equiv : forall (a:t) (b:t) (i:t) (n:t), (eq_sub a b (to_uint i)
(to_uint n)) <-> (eq_sub_bv a b i n).
intros a b i n.
admit.
Qed.
(* Why3 goal *)
Lemma Extensionality : forall (x:t) (y:t), (eq_sub x y 0%Z size_int) ->
(x = y).
intros x y.
apply Extensionality_aux.
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.
Require BuiltIn.
Require int.Int.
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
......@@ -377,3 +372,4 @@ Qed.
Lemma pow2_64 : ((pow2 64%Z) = 18446744073709551616%Z).
easy.
Qed.
......@@ -245,6 +245,12 @@ rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
*)
Qed.
(* Why3 goal *)
Lemma snoc_last : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (x:a),
((get (snoc s x) (length s)) = x).
intros a a_WT s x.
Admitted. (* TODO *)
(* Why3 goal *)
Definition mixfix_lb_dtdt_rb: forall {a:Type} {a_WT:WhyType a}, (seq a) ->
Z -> Z -> (seq a).
......
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