Commit 5d77d51f authored by MARCHE Claude's avatar MARCHE Claude

make Coq proofs compatible with 8.4pl1

parent 0304fe4b
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
......@@ -9,7 +9,7 @@ Require int.ComputerDivision.
Require int.Power.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
......@@ -19,7 +19,7 @@ Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
......@@ -34,6 +34,7 @@ Theorem WP_parameter_fast_exp_imperative : forall (x:Z) (n:Z),
(((ZOmod e 2%Z) = 1%Z) -> forall (r1:Z), (r1 = (r * p)%Z) -> forall (p1:Z),
(p1 = (p * p)%Z) -> forall (e1:Z), (e1 = (ZOdiv e 2%Z)) ->
((r1 * (int.Power.power p1 e1))%Z = (int.Power.power x n)))).
(* Why3 intros x n h1 e p r (h2,h3) h4 h5 r1 h6 p1 h7 e1 h8. *)
intros x n h1 e p r (h2,h3) h4 h5 r1 h6 p1 h7 e1 h8.
subst.
assert (h: (2 <> 0)%Z) by omega.
......@@ -45,7 +46,7 @@ intros.
rewrite <- h3; clear h3.
rewrite H0 at 2. clear H0.
rewrite Power_sum by omega.
replace (2 * (e / 2))%Z with (e/2 + e/2)%Z by ring.
replace (2 * (ZOdiv e 2))%Z with (ZOdiv e 2 + ZOdiv e 2)%Z by ring.
rewrite Power_sum by apply H.
rewrite Power_mult2 by apply H.
rewrite Power_1.
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require Import ZOdiv.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
Require int.Power.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) :=
Inductive ref (a:Type) {a_WT:WhyType a} :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents (a:Type)(v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Implicit Arguments contents.
Import Power.
Open Scope Z_scope.
(* Why3 goal *)
Theorem WP_parameter_fast_exp_imperative : forall (x:Z) (n:Z),
......@@ -32,14 +34,15 @@ Theorem WP_parameter_fast_exp_imperative : forall (x:Z) (n:Z),
((~ ((ZOmod e 2%Z) = 1%Z)) -> forall (p1:Z), (p1 = (p * p)%Z) ->
forall (e1:Z), (e1 = (ZOdiv e 2%Z)) -> ((r * (int.Power.power p1
e1))%Z = (int.Power.power x n)))).
(* Why3 intros x n h1 e p r (h2,h3) h4 h5 p1 h6 e1 h7. *)
(* YOU MAY EDIT THE PROOF BELOW *)
intros x n Hn e0 p0 r0 (He0,Hind).
intros He0' Hmod p1 Hp e1 He.
rewrite <- Hind.
apply f_equal.
subst.
assert (h: (e0 = e0/2 + e0/2)%Z).
assert (e0 mod 2 = 0).
assert (h: (e0 = ZOdiv e0 2 + ZOdiv e0 2)).
assert (ZOmod e0 2 = 0).
generalize (ZOmod_lt_pos e0 2).
unfold Zabs; omega.
rewrite (ZO_div_mod_eq e0 2) at 1; omega.
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require Import ZOdiv.
......@@ -10,7 +10,7 @@ Require int.ComputerDivision.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
Axiom bag : forall (a:Type) {a_WT:WhyType a}, Type.
Parameter bag_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (bag a).
......@@ -22,11 +22,11 @@ Axiom occ_non_negative : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a))
(x:a), (0%Z <= (nb_occ x b))%Z.
(* Why3 assumption *)
Definition mem {a:Type} {a_WT:WhyType a}(x:a) (b:(bag a)): Prop :=
Definition mem {a:Type} {a_WT:WhyType a} (x:a) (b:(bag a)): Prop :=
(0%Z < (nb_occ x b))%Z.
(* Why3 assumption *)
Definition eq_bag {a:Type} {a_WT:WhyType a}(a1:(bag a)) (b:(bag a)): Prop :=
Definition eq_bag {a:Type} {a_WT:WhyType a} (a1:(bag a)) (b:(bag a)): Prop :=
forall (x:a), ((nb_occ x a1) = (nb_occ x b)).
Axiom bag_extensionality : forall {a:Type} {a_WT:WhyType a}, forall (a1:(bag
......@@ -74,7 +74,7 @@ Axiom bag_simpl_left : forall {a:Type} {a_WT:WhyType a}, forall (a1:(bag a))
(b:(bag a)) (c:(bag a)), ((union a1 b) = (union a1 c)) -> (b = c).
(* Why3 assumption *)
Definition add {a:Type} {a_WT:WhyType a}(x:a) (b:(bag a)): (bag a) :=
Definition add {a:Type} {a_WT:WhyType a} (x:a) (b:(bag a)): (bag a) :=
(union (singleton x) b).
Axiom occ_add_eq : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a)) (x:a)
......@@ -174,13 +174,13 @@ Axiom Elements_set_inside2 : forall {a:Type} {a_WT:WhyType a},
(diff (elements a1 i n) (singleton (map.Map.get a1 j))))).
(* Why3 assumption *)
Definition left1(i:Z): Z := ((2%Z * i)%Z + 1%Z)%Z.
Definition left1 (i:Z): Z := ((2%Z * i)%Z + 1%Z)%Z.
(* Why3 assumption *)
Definition right1(i:Z): Z := ((2%Z * i)%Z + 2%Z)%Z.
Definition right1 (i:Z): Z := ((2%Z * i)%Z + 2%Z)%Z.
(* Why3 assumption *)
Definition parent(i:Z): Z := (ZOdiv (i - 1%Z)%Z 2%Z).
Definition parent (i:Z): Z := (ZOdiv (i - 1%Z)%Z 2%Z).
Axiom Parent_inf : forall (i:Z), (0%Z < i)%Z -> ((parent i) < i)%Z.
......@@ -201,23 +201,23 @@ Axiom Child_parent : forall (i:Z), (0%Z < i)%Z ->
Axiom Parent_pos : forall (j:Z), (0%Z < j)%Z -> (0%Z <= (parent j))%Z.
(* Why3 assumption *)
Definition parentChild(i:Z) (j:Z): Prop := ((0%Z <= i)%Z /\ (i < j)%Z) ->
Definition parentChild (i:Z) (j:Z): Prop := ((0%Z <= i)%Z /\ (i < j)%Z) ->
((j = (left1 i)) \/ (j = (right1 i))).
(* Why3 assumption *)
Definition map := (map.Map.map Z Z).
Definition map := (map.Map.map Z Z).
(* Why3 assumption *)
Definition logic_heap := ((map.Map.map Z Z)* Z)%type.
Definition logic_heap := ((map.Map.map Z Z)* Z)%type.
(* Why3 assumption *)
Definition is_heap_array(a:(map.Map.map Z Z)) (idx:Z) (sz:Z): Prop :=
Definition is_heap_array (a:(map.Map.map Z Z)) (idx:Z) (sz:Z): Prop :=
(0%Z <= idx)%Z -> forall (i:Z) (j:Z), (((idx <= i)%Z /\ (i < j)%Z) /\
(j < sz)%Z) -> ((parentChild i j) -> ((map.Map.get a i) <= (map.Map.get a
j))%Z).
(* Why3 assumption *)
Definition is_heap(h:((map.Map.map Z Z)* Z)%type): Prop :=
Definition is_heap (h:((map.Map.map Z Z)* Z)%type): Prop :=
match h with
| (a, sz) => (0%Z <= sz)%Z /\ (is_heap_array a 0%Z sz)
end.
......@@ -225,9 +225,9 @@ Definition is_heap(h:((map.Map.map Z Z)* Z)%type): Prop :=
Axiom Is_heap_when_no_element : forall (a:(map.Map.map Z Z)) (idx:Z) (n:Z),
((0%Z <= n)%Z /\ (n <= idx)%Z) -> (is_heap_array a idx n).
Axiom Is_heap_sub : forall (a:(map.Map.map Z Z)) (i:Z) (n:Z),
(is_heap_array a i n) -> forall (j:Z), ((i <= j)%Z /\ (j <= n)%Z) ->
(is_heap_array a i j).
Axiom Is_heap_sub : forall (a:(map.Map.map Z Z)) (i:Z) (n:Z), (is_heap_array
a i n) -> forall (j:Z), ((i <= j)%Z /\ (j <= n)%Z) -> (is_heap_array a i
j).
Axiom Is_heap_sub2 : forall (a:(map.Map.map Z Z)) (n:Z), (is_heap_array a 0%Z
n) -> forall (j:Z), ((0%Z <= j)%Z /\ (j <= n)%Z) -> (is_heap_array a j n).
......@@ -261,7 +261,7 @@ Axiom Is_heap_relation : forall (a:(map.Map.map Z Z)) (n:Z), (0%Z < n)%Z ->
((map.Map.get a 0%Z) <= (map.Map.get a j))%Z)).
(* Why3 assumption *)
Definition model(h:((map.Map.map Z Z)* Z)%type): (bag Z) :=
Definition model (h:((map.Map.map Z Z)* Z)%type): (bag Z) :=
match h with
| (a, n) => (elements a 0%Z n)
end.
......@@ -292,12 +292,13 @@ Axiom Min_bag_union1 : forall (x:(bag Z)) (y:(bag Z)) (a:Z), (x = (add a
Axiom Min_bag_union2 : forall (x:(bag Z)) (a:Z), (a <= (min_bag x))%Z ->
(a <= (min_bag (add a x)))%Z.
Open Scope Z_scope.
(* Why3 goal *)
Theorem Is_heap_min : forall (a:(map.Map.map Z Z)) (n:Z), (0%Z < n)%Z ->
((is_heap_array a 0%Z n) -> ((map.Map.get a 0%Z) = (min_bag (model (a,
n))))).
(* Why3 intros a n h1 h2. *)
Proof.
intros a n H_n Heap.
unfold model.
......
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