Commit 07132f83 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Implicitly introduce type arguments in Coq printer.

parent 486766c4
......@@ -123,10 +123,10 @@ Theorem WP_parameter_add : forall {a:Type} {a_WT:WhyType a}, forall (h:Z)
forall (rho6:(map.Map.map key (option a))), (rho6 = (map.Map.set rho2 k
(Init.Datatypes.Some v))) -> forall (i1:Z), ((0%Z <= i1)%Z /\
(i1 < rho)%Z) -> (good_hash (mk_array rho o) i1))).
(* Why3 intros a a_WT h h1 h2 k v ((h1,(h2,h3)),h4) rho rho1
(* Why3 intros h h1 h2 k v ((h1,(h2,h3)),h4) rho rho1
((h5,(h6,h7)),h8) rho2 rho3 rho4 (((h9,(h10,h11)),h12),(h13,h14)) i
(h15,h16) (h17,h18) o (h19,h20) rho5 h21 rho6 h22 i1 (h23,h24). *)
intros a a_WT rho rho1 rho2 k v ((h1,(h2,h3)),h4) rho3 rho4 ((h5,(h6,h7)),h8)
intros rho rho1 rho2 k v ((h1,(h2,h3)),h4) rho3 rho4 ((h5,(h6,h7)),h8)
rho5 rho6 rho7 (((h9,(h10,h11)),h12),(h13,h14)) i1 (h15,h16) (h17,h18) o
(h19,h20) rho8 h21 rho9 h22 i (h23,h24).
subst i1.
......
......@@ -99,7 +99,7 @@ Theorem VC_find : forall {a:Type} {a_WT:WhyType a}, forall (h:(t a))
| (Init.Datatypes.Some v) => (list.Mem.mem (k, v) o1)
end -> (result = ((view h) k))).
Proof.
intros a a_WT h h_view h_data h_size k (h1,(h2,h3)) o i (h4,h5) o1 result h6.
intros h h_view h_data h_size k (h1,(h2,h3)) o i (h4,h5) o1 result h6.
subst i.
destruct result.
symmetry.
......
......@@ -99,10 +99,10 @@ Theorem VC_remove : forall {a:Type} {a_WT:WhyType a}, forall (h:(t a))
| (Init.Datatypes.Some v) => (list.Mem.mem (k, v) l)
end -> ((o1 = Init.Datatypes.None) -> (((view h)
k) = Init.Datatypes.None))).
(* Why3 intros a a_WT h h_view h_data h_size k (h1,(h2,h3)) o i (h4,h5) l o1
(* Why3 intros h h_view h_data h_size k (h1,(h2,h3)) o i (h4,h5) l o1
h6 h7. *)
Proof.
intros a a_WT h h_view h_data h_size k (h1,(h2,h3)) o i (h4,h5) l o1 h6 h7.
intros h h_view h_data h_size k (h1,(h2,h3)) o i (h4,h5) l o1 h6 h7.
subst i.
rewrite h7 in h6.
subst l.
......
......@@ -462,9 +462,9 @@ Theorem WP_parameter_infix_tl : forall {a:Type} {a_WT:WhyType a},
| (VMC p2 s m _) => exists ms:machine_state, (transition c_glob (VMS p2 s
m) ms)
end)))))))).
(* Why3 intros a a_WT s1 s11 s2 s21 (h1,h2) code2 x p mc p1 x1 y z h3 (h4,h5)
(* Why3 intros s1 s11 s2 s21 (h1,h2) code2 x p mc p1 x1 y z h3 (h4,h5)
c_glob post2 mc' mc'' h6 h7 h8 h9 h10 h11 post21 h12 h13. *)
intros a a_WT s1 s11 s2 s21 (h1,h2) code2 x p mc p1 x1 y z h3 (h4,h5) c_glob
intros s1 s11 s2 s21 (h1,h2) code2 x p mc p1 x1 y z h3 (h4,h5) c_glob
post2 mc' mc'' h6 h7 h8 h9 h10 h11 post21 h12 h13.
Require Import Why3.
Ltac cvc := why3 "CVC4,1.4," timelimit 10.
......
......@@ -541,9 +541,9 @@ Theorem WP_parameter_make_loop_hl : forall {a:Type} {a_WT:WhyType a},
| (VMC p2 s m _) => exists ms:machine_state, (transition c_glob (VMS p2 s
m) ms)
end)))))))).
(* Why3 intros a a_WT c c1 c2 inv p x y z h1 (h2,h3) post2 x1 c_glob p1 mc'
(* Why3 intros c c1 c2 inv p x y z h1 (h2,h3) post2 x1 c_glob p1 mc'
mc'' h4 h5 h6 (h7,(h8,h9)) mc h10 h11 h12 post21 h13 h14. *)
intros a a_WT c c1 c2 inv p x y z h1 (h2,h3) post2 x1 c_glob p1 mc' mc'' h4
intros c c1 c2 inv p x y z h1 (h2,h3) post2 x1 c_glob p1 mc' mc'' h4
h5 h6 (h7,(h8,h9)) mc h10 h11 h12 post21 h13 h14.
Require Import Why3.
Ltac cvc := why3 "CVC4,1.4,".
......
......@@ -537,9 +537,9 @@ Theorem WP_parameter_ifunf : forall {a:Type} {a_WT:WhyType a},
(x2:(list Z)) (x3:(map id Z)) (x4:Z), (mc' = (VMC x1 x2 x3 x4)) ->
((mc = mc') -> (transition c_glob (VMS x1 x2 x3) (infix_at f (VMS x1 x2
x3)))))).
(* Why3 intros a a_WT pre2 code_f f h1 x c_glob p mc mc' h2 h3 post2 (h4,h5)
(* Why3 intros pre2 code_f f h1 x c_glob p mc mc' h2 h3 post2 (h4,h5)
x1 x2 x3 x4 h6 h7. *)
intros a a_WT pre2 code_f f h1 x c_glob p mc mc' h2 h3 post2 (h4,h5) x1 x2 x3
intros pre2 code_f f h1 x c_glob p mc mc' h2 h3 post2 (h4,h5) x1 x2 x3
x4 h6 h7.
unfold post2 in *;clear post2.
subst.
......
......@@ -536,7 +536,7 @@ Theorem WP_parameter_ifunf : forall {a:Type} {a_WT:WhyType a},
c_glob, post2) mc mc') /\ ~ ((infix_at post2 mc') = true)) -> forall (x1:Z)
(x2:(list Z)) (x3:(map id Z)) (x4:Z), (mc' = (VMC x1 x2 x3 x4)) ->
(mc = mc'))).
intros a a_WT pre2 code_f f h1 x c_glob p mc mc' h2 h3 post2 (h4,h5) x1 x2 x3
intros pre2 code_f f h1 x c_glob p mc mc' h2 h3 post2 (h4,h5) x1 x2 x3
x4 h6.
remember post2 as post;unfold post2 in *;clear post2.
inversion h4;subst. trivial.
......
......@@ -175,10 +175,10 @@ Theorem WP_parameter_enqueue : forall {a:Type} {a_WT:WhyType a},
(rho5 = (rho1 + 1%Z)%Z) -> forall (rho6:(@list a a_WT)),
(rho6 = (infix_plpl rho (Cons x (Nil :(@list a a_WT))))) ->
(rho6 = (to_list (mk_array rho3 o) rho2 rho5))).
(* Why3 intros a a_WT x rho rho1 rho2 rho3 rho4
(* Why3 intros x rho rho1 rho2 rho3 rho4
((((h1,((h2,h3),h4)),h5),h6),h7) (h8,h9) o (h10,h11) rho5 h12 rho6
h13. *)
intros a a_WT x rho rho1 rho2 rho3 rho4 ((((h1,((h2,h3),h4)),h5),h6),h7)
intros x rho rho1 rho2 rho3 rho4 ((((h1,((h2,h3),h4)),h5),h6),h7)
(h8,h9) o (h10,h11) rho5 h12 rho6 h13.
subst rho6.
symmetry.
......
......@@ -86,8 +86,8 @@ Theorem exchange_permut_sub : forall {a:Type} {a_WT:WhyType a},
forall (a1:(array a)) (a2:(array a)) (i:Z) (j:Z) (l:Z) (u:Z), (exchange1 a1
a2 i j) -> (((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) ->
((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l u))))).
(* Why3 intros a a_WT a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7. *)
intros a a_WT a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7.
(* Why3 intros a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7. *)
intros a1 a2 i j l u h1 (h2,h3) (h4,h5) h6 h7.
destruct h1 as (h11,h12).
destruct h12 as (ha,(hb,(hc,(hd,he)))).
red. repeat split.
......
......@@ -107,8 +107,8 @@ Theorem permut_sub_weakening : forall {a:Type} {a_WT:WhyType a},
forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z)
(u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) ->
(((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))).
(* Why3 intros a a_WT a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5). *)
intros a a_WT a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5).
(* Why3 intros a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5). *)
intros a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5).
unfold permut_sub in *.
destruct h1 as (eql,(h1,eqr)).
unfold map_eq_sub in *.
......
......@@ -156,8 +156,8 @@ Ltac cvc := why3 "CVC4,1.4,"; admit.
(* Why3 goal *)
Theorem Permut_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list
a)) (l2:(list a)), (permut l1 l2) -> ((length l1) = (length l2)).
(* Why3 intros a a_WT l1 l2 h1. *)
intros a a_WT l1 l2 h1.
(* Why3 intros l1 l2 h1. *)
intros l1 l2 h1.
generalize dependent l2.
induction l1; intros.
destruct l2.
......
......@@ -32,9 +32,7 @@ Axiom ax : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ((id x) = x).
(* Why3 goal *)
Theorem g1 : forall {a:Type} {a_WT:WhyType a}, exists x:a, ((id x) = x).
(* Why3 intros a a_WT. *)
Proof.
intros a a_WT.
exists why_inhabitant.
apply ax.
Qed.
......
......@@ -42,7 +42,7 @@ Fixpoint flatten {a:Type} {a_WT:WhyType a} (l:(list (a*
Theorem length_flatten : forall {a:Type} {a_WT:WhyType a},
forall (l:(list (a* a)%type)),
((list.Length.length (flatten l)) = (2%Z * (list.Length.length l))%Z).
intros a a_WT l.
intros l.
induction l.
auto.
simpl (flatten (a0::l)).
......
......@@ -2,181 +2,201 @@
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require int.MinMax.
Require map.Map.
Parameter bag : forall (a:Type) {a_WT:WhyType a}, Type.
Axiom bag_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (bag a).
Axiom bag : forall (a:Type), Type.
Parameter bag_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (bag a).
Existing Instance bag_WhyType.
Parameter nb_occ: forall {a:Type} {a_WT:WhyType a}, a -> (bag a) ->
BuiltIn.int.
Parameter nb_occ: forall {a:Type} {a_WT:WhyType a}, a -> (bag a) -> Z.
Axiom occ_non_negative : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a))
(x:a), (0%Z <= (nb_occ x b))%Z.
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
a)) (b:(bag a)), (eq_bag a1 b) -> (a1 = b).
Axiom bag_extensionality :
forall {a:Type} {a_WT:WhyType a},
forall (a1:bag a) (b:bag a), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall {a:Type} {a_WT:WhyType a}, (bag a).
Parameter empty_bag: forall {a:Type} {a_WT:WhyType a}, bag a.
Axiom occ_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ((nb_occ x
(empty_bag :(bag a))) = 0%Z).
Axiom occ_empty :
forall {a:Type} {a_WT:WhyType a},
forall (x:a), ((nb_occ x (empty_bag : bag a)) = 0%Z).
Axiom is_empty : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a)),
(forall (x:a), ((nb_occ x b) = 0%Z)) -> (b = (empty_bag :(bag a))).
Axiom is_empty :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a), (forall (x:a), ((nb_occ x b) = 0%Z)) ->
(b = (empty_bag : bag a)).
Parameter singleton: forall {a:Type} {a_WT:WhyType a}, a -> (bag a).
Parameter singleton: forall {a:Type} {a_WT:WhyType a}, a -> bag a.
Axiom occ_singleton : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a),
((x = y) /\ ((nb_occ y (singleton x)) = 1%Z)) \/ ((~ (x = y)) /\ ((nb_occ y
(singleton x)) = 0%Z)).
Axiom occ_singleton :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (y:a),
((x = y) /\ ((nb_occ y (singleton x)) = 1%Z)) \/
(~ (x = y) /\ ((nb_occ y (singleton x)) = 0%Z)).
Axiom occ_singleton_eq : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a), (x = y) -> ((nb_occ y (singleton x)) = 1%Z).
Axiom occ_singleton_eq :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (y:a), (x = y) -> ((nb_occ y (singleton x)) = 1%Z).
Axiom occ_singleton_neq : forall {a:Type} {a_WT:WhyType a}, forall (x:a)
(y:a), (~ (x = y)) -> ((nb_occ y (singleton x)) = 0%Z).
Axiom occ_singleton_neq :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (y:a), ~ (x = y) -> ((nb_occ y (singleton x)) = 0%Z).
Parameter union: forall {a:Type} {a_WT:WhyType a}, (bag a) -> (bag a) -> (bag
a).
Parameter union:
forall {a:Type} {a_WT:WhyType a}, (bag a) -> (bag a) -> bag a.
Axiom occ_union : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (a1:(bag a))
(b:(bag a)), ((nb_occ x (union a1 b)) = ((nb_occ x a1) + (nb_occ x b))%Z).
Axiom occ_union :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (a1:bag a) (b:bag a),
((nb_occ x (union a1 b)) = ((nb_occ x a1) + (nb_occ x b))%Z).
Axiom Union_comm : forall {a:Type} {a_WT:WhyType a}, forall (a1:(bag a))
(b:(bag a)), ((union a1 b) = (union b a1)).
Axiom Union_comm :
forall {a:Type} {a_WT:WhyType a},
forall (a1:bag a) (b:bag a), ((union a1 b) = (union b a1)).
Axiom Union_identity : forall {a:Type} {a_WT:WhyType a}, forall (a1:(bag a)),
((union a1 (empty_bag :(bag a))) = a1).
Axiom Union_identity :
forall {a:Type} {a_WT:WhyType a},
forall (a1:bag a), ((union a1 (empty_bag : bag a)) = a1).
Axiom Union_assoc : forall {a:Type} {a_WT:WhyType a}, forall (a1:(bag a))
(b:(bag a)) (c:(bag a)), ((union a1 (union b c)) = (union (union a1 b) c)).
Axiom Union_assoc :
forall {a:Type} {a_WT:WhyType a},
forall (a1:bag a) (b:bag a) (c:bag a),
((union a1 (union b c)) = (union (union a1 b) c)).
Axiom bag_simpl : forall {a:Type} {a_WT:WhyType a}, forall (a1:(bag a))
(b:(bag a)) (c:(bag a)), ((union a1 b) = (union c b)) -> (a1 = c).
Axiom bag_simpl_right :
forall {a:Type} {a_WT:WhyType a},
forall (a1:bag a) (b:bag a) (c:bag a), ((union a1 b) = (union c b)) ->
(a1 = c).
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).
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) :=
(union (singleton x) b).
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)
(y:a), (x = y) -> ((nb_occ x (add x b)) = ((nb_occ x b) + 1%Z)%Z).
Axiom occ_add_eq :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a) (x:a) (y:a), (x = y) ->
((nb_occ y (add x b)) = ((nb_occ y b) + 1%Z)%Z).
Axiom occ_add_neq : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a))
(x:a) (y:a), (~ (x = y)) -> ((nb_occ y (add x b)) = (nb_occ y b)).
Axiom occ_add_neq :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a) (x:a) (y:a), ~ (x = y) ->
((nb_occ y (add x b)) = (nb_occ y b)).
Parameter card: forall {a:Type} {a_WT:WhyType a}, (bag a) -> BuiltIn.int.
Parameter card: forall {a:Type} {a_WT:WhyType a}, (bag a) -> Z.
Axiom Card_empty : forall {a:Type} {a_WT:WhyType a}, ((card (empty_bag :(bag
a))) = 0%Z).
Axiom Card_nonneg :
forall {a:Type} {a_WT:WhyType a}, forall (x:bag a), (0%Z <= (card x))%Z.
Axiom Card_zero_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:(bag a)),
((card x) = 0%Z) -> (x = (empty_bag :(bag a))).
Axiom Card_empty :
forall {a:Type} {a_WT:WhyType a}, ((card (empty_bag : bag a)) = 0%Z).
Axiom Card_singleton : forall {a:Type} {a_WT:WhyType a}, forall (x:a),
((card (singleton x)) = 1%Z).
Axiom Card_zero_empty :
forall {a:Type} {a_WT:WhyType a},
forall (x:bag a), ((card x) = 0%Z) -> (x = (empty_bag : bag a)).
Axiom Card_union : forall {a:Type} {a_WT:WhyType a}, forall (x:(bag a))
(y:(bag a)), ((card (union x y)) = ((card x) + (card y))%Z).
Axiom Card_singleton :
forall {a:Type} {a_WT:WhyType a},
forall (x:a), ((card (singleton x)) = 1%Z).
Axiom Card_add : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (b:(bag a)),
((card (add x b)) = (1%Z + (card b))%Z).
Axiom Card_union :
forall {a:Type} {a_WT:WhyType a},
forall (x:bag a) (y:bag a), ((card (union x y)) = ((card x) + (card y))%Z).
Parameter diff: forall {a:Type} {a_WT:WhyType a}, (bag a) -> (bag a) -> (bag
a).
Axiom Card_add :
forall {a:Type} {a_WT:WhyType a},
forall (x:a) (b:bag a), ((card (add x b)) = (1%Z + (card b))%Z).
Axiom Diff_occ : forall {a:Type} {a_WT:WhyType a}, forall (b1:(bag a))
(b2:(bag a)) (x:a), ((nb_occ x (diff b1 b2)) = (Zmax 0%Z ((nb_occ x
b1) - (nb_occ x b2))%Z)).
Parameter diff:
forall {a:Type} {a_WT:WhyType a}, (bag a) -> (bag a) -> bag a.
Axiom Diff_empty_right : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag
a)), ((diff b (empty_bag :(bag a))) = b).
Axiom Diff_occ :
forall {a:Type} {a_WT:WhyType a},
forall (b1:bag a) (b2:bag a) (x:a),
((nb_occ x (diff b1 b2)) =
(ZArith.BinInt.Z.max 0%Z ((nb_occ x b1) - (nb_occ x b2))%Z)).
Axiom Diff_empty_left : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a)),
((diff (empty_bag :(bag a)) b) = (empty_bag :(bag a))).
Axiom Diff_empty_right :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a), ((diff b (empty_bag : bag a)) = b).
Axiom Diff_add : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a)) (x:a),
((diff (add x b) (singleton x)) = b).
Axiom Diff_empty_left :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a), ((diff (empty_bag : bag a) b) = (empty_bag : bag a)).
Axiom Diff_comm : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a))
(b1:(bag a)) (b2:(bag a)), ((diff (diff b b1) b2) = (diff (diff b b2) b1)).
Axiom Diff_add :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a) (x:a), ((diff (add x b) (singleton x)) = b).
Axiom Add_diff : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a)) (x:a),
(mem x b) -> ((add x (diff b (singleton x))) = b).
Axiom Diff_comm :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a) (b1:bag a) (b2:bag a),
((diff (diff b b1) b2) = (diff (diff b b2) b1)).
Parameter map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b},
Type.
Axiom map_WhyType : forall (a:Type) {a_WT:WhyType a}
(b:Type) {b_WT:WhyType b}, WhyType (map a b).
Existing Instance map_WhyType.
Axiom Add_diff :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a) (x:a), (mem x b) -> ((add x (diff b (singleton x))) = b).
Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b.
Parameter choose: forall {a:Type} {a_WT:WhyType a}, (bag a) -> a.
Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(map a b) -> a -> b -> (map a b).
Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) ->
((get (set m a1 b1) a2) = b1).
Axiom Select_neq : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a),
forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)).
Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1).
Axiom choose_mem :
forall {a:Type} {a_WT:WhyType a},
forall (b:bag a), ~ ((empty_bag : bag a) = b) -> mem (choose b) b.
(* Why3 assumption *)
Definition array (a:Type) {a_WT:WhyType a} := (map BuiltIn.int a).
Parameter elements: forall {a:Type} {a_WT:WhyType a}, (map BuiltIn.int a)
-> BuiltIn.int -> BuiltIn.int -> (bag a).
Definition array (a:Type) := Z -> a.
Axiom Elements_empty : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map
BuiltIn.int a)) (i:BuiltIn.int) (j:BuiltIn.int), (j <= i)%Z ->
((elements a1 i j) = (empty_bag :(bag a))).
Parameter elements:
forall {a:Type} {a_WT:WhyType a}, (Z -> a) -> Z -> Z -> bag a.
Axiom Elements_add : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map
BuiltIn.int a)) (i:BuiltIn.int) (j:BuiltIn.int), (i < j)%Z -> ((elements a1
i j) = (add (get a1 (j - 1%Z)%Z) (elements a1 i (j - 1%Z)%Z))).
Axiom Elements_empty :
forall {a:Type} {a_WT:WhyType a},
forall (a1:Z -> a) (i:Z) (j:Z), (j <= i)%Z ->
((elements a1 i j) = (empty_bag : bag a)).
Axiom Elements_singleton : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map
BuiltIn.int a)) (i:BuiltIn.int) (j:BuiltIn.int), (j = (i + 1%Z)%Z) ->
((elements a1 i j) = (singleton (get a1 i))).
Axiom Elements_add :
forall {a:Type} {a_WT:WhyType a},
forall (a1:Z -> a) (i:Z) (j:Z), (i < j)%Z ->
((elements a1 i j) = (add (a1 (j - 1%Z)%Z) (elements a1 i (j - 1%Z)%Z))).
Axiom Elements_union : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map
BuiltIn.int a)) (i:BuiltIn.int) (j:BuiltIn.int) (k:BuiltIn.int),
((i <= j)%Z /\ (j <= k)%Z) -> ((elements a1 i k) = (union (elements a1 i j)
(elements a1 j k))).
Axiom Elements_singleton :
forall {a:Type} {a_WT:WhyType a},
forall (a1:Z -> a) (i:Z) (j:Z), (j = (i + 1%Z)%Z) ->
((elements a1 i j) = (singleton (a1 i))).
Axiom Elements_union :
forall {a:Type} {a_WT:WhyType a},
forall (a1:Z -> a) (i:Z) (j:Z) (k:Z), ((i <= j)%Z /\ (j <= k)%Z) ->
((elements a1 i k) = (union (elements a1 i j) (elements a1 j k))).
(* Why3 goal *)
Theorem Elements_add1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map
BuiltIn.int a)) (i:BuiltIn.int) (j:BuiltIn.int), (i < j)%Z -> ((elements a1
i j) = (add (get a1 i) (elements a1 (i + 1%Z)%Z j))).
(* YOU MAY EDIT THE PROOF BELOW *)
intros X _X a i j Hij.
Theorem Elements_add1 {a:Type} {a_WT:WhyType a} :
forall (a1:Z -> a) (i:Z) (j:Z), (i < j)%Z ->
((elements a1 i j) = (add (a1 i) (elements a1 (i + 1%Z)%Z j))).
Proof.
intros a1 i j h1.
unfold add.
pattern (elements a i j);
rewrite (Elements_union _ _ (i+1)%Z);
pattern (elements a1 i j);
rewrite (Elements_union _ _ (i+1)%Z);
auto with zarith.
rewrite Elements_singleton; auto with zarith.
Qed.
......@@ -13,164 +13,211 @@ Existing Instance bag_WhyType.
Parameter nb_occ: forall {a:Type} {a_WT:WhyType a}, a -> (bag a) -> Z.
Axiom occ_non_negative : forall {a:Type} {a_WT:WhyType a}, forall (b:(bag a))
(x:a), (0%Z <= (nb_occ x b))%Z.
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
a)) (b:(bag a)), (eq_bag a1 b) -> (a1 = b).
Axiom bag_extensionality :
forall {a:Type} {a_WT:WhyType a},
forall (a1:bag a) (b:bag a), (eq_bag a1 b) -> (a1 = b).
Parameter empty_bag: forall {a:Type} {a_WT:WhyType a}, (bag a).
Parameter empty_bag: forall {a:Type} {a_WT:WhyType a}, bag a.
Axiom occ_empty : forall {a:Type} {a_WT:WhyType a}, forall (x:a), ((nb_occ x
(empty_bag : (bag a))) = 0%Z).