Commit 53872de5 authored by MARCHE Claude's avatar MARCHE Claude

update some sessions

parent 0eaac16c
......@@ -136,12 +136,13 @@ module Harness
use import Spec
use import InPlaceCountingSort
let harness () requires { k = 2 } =
(* a is [0;1;0] *)
let harness ()
requires { k = 2 }
= (* a is [0;1;0] *)
let a = make 3 0 in
a[1] <- 1;
in_place_counting_sort a;
(* b is now [0;0;1] *)
(* a is now [0;0;1] *)
assert { numeq a 0 0 3 = 2 };
assert { numeq a 1 0 3 = 1 };
assert { a[0] = 0 };
......
This diff is collapsed.
This diff is collapsed.
(* This file is generated by Why3's Coq 8.4 driver *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -8,89 +8,104 @@ Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
Implicit Arguments mk_ref [[a]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).
Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
((length (make n v)) = n).
Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
((get (make n v) i) = v).
(* Why3 assumption *)
Definition appear_twice (a:(@array Z _)) (v:Z) (u:Z): Prop := exists i:Z,
Definition appear_twice (a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z,
((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get a i) = v) /\ exists j:Z,
((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get a j) = v))).
(* Why3 goal *)
Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(@map.Map.map Z _
Z _)) (n:Z), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\
Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(map.Map.map Z Z))
(n:Z), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\
(((a = (n + 2%Z)%Z) /\ (2%Z <= n)%Z) /\ ((forall (i:Z), ((0%Z <= i)%Z /\
(i < a)%Z) -> ((0%Z <= (map.Map.get a1 i))%Z /\ ((map.Map.get a1
i) < n)%Z)) /\ exists v1:Z, (appear_twice a2 v1 (n + 2%Z)%Z) /\
exists v2:Z, (appear_twice a2 v2 (n + 2%Z)%Z) /\ ~ (v2 = v1)))) ->
((0%Z <= n)%Z -> ((0%Z <= n)%Z -> let o := (n + 1%Z)%Z in ((0%Z <= o)%Z ->
forall (v2:Z) (v1:Z) (deja_vu:(@map.Map.map Z _ bool _)), forall (i:Z),
((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) -> (v2 = (-1%Z)%Z)) /\
(((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
((0%Z <= n)%Z -> forall (deja_vu:Z) (deja_vu1:(map.Map.map Z bool)),
((0%Z <= deja_vu)%Z /\ ((deja_vu = n) /\ forall (i:Z),
((map.Map.get deja_vu1 i) = false))) -> let o := (n + 1%Z)%Z in
((0%Z <= o)%Z -> forall (v2:Z) (v1:Z) (deja_vu2:(map.Map.map Z bool)),
forall (i:Z), ((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) ->
(v2 = (-1%Z)%Z)) /\ (((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
(((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\
((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu
((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu2
v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((map.Map.get a1
j) = v)) \/ ((~ ((map.Map.get deja_vu v) = true)) /\ forall (j:Z),
j) = v)) \/ ((~ ((map.Map.get deja_vu2 v) = true)) /\ forall (j:Z),
((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((map.Map.get a1 j) = v)))) /\
(((v1 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) ->
~ (appear_twice a2 v i)) /\ ((v2 = (-1%Z)%Z) -> forall (v:Z),
((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v1)) -> ~ (appear_twice a2 v
i)))))))) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let v := (map.Map.get a1 i) in
(((0%Z <= n)%Z /\ ((0%Z <= v)%Z /\ (v < n)%Z)) -> (((map.Map.get deja_vu
v) = true) -> ((v1 = (-1%Z)%Z) -> forall (v11:Z), (v11 = v) ->
((v2 = (-1%Z)%Z) -> forall (v3:Z), ((0%Z <= v3)%Z /\ (v3 < n)%Z) ->
((~ (v3 = v11)) -> ~ (appear_twice a2 v3 (i + 1%Z)%Z)))))))))))).
(((0%Z <= deja_vu)%Z /\ ((0%Z <= v)%Z /\ (v < deja_vu)%Z)) ->
(((map.Map.get deja_vu2 v) = true) -> ((v1 = (-1%Z)%Z) -> forall (v11:Z),
(v11 = v) -> ((v2 = (-1%Z)%Z) -> forall (v3:Z), ((0%Z <= v3)%Z /\
(v3 < n)%Z) -> ((~ (v3 = v11)) -> ~ (appear_twice a2 v3
(i + 1%Z)%Z))))))))))).
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8
deja_vu deja_vu1 (h9,(h10,h11)) o h12 v3 v4 deja_vu2 i (h13,h14)
(h15,(h16,(h17,(h18,(h19,h20))))) (h21,h22) v (h23,(h24,h25)) h26 h27
v11 h28 h29 v5 (h30,h31) h32.
(*
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8 h9 o
h10 v22 v12 deja_vu i (h11,h12) (h13,(h14,(h15,(h16,(h17,h18)))))
(h19,h20) v (h21,(h22,h23)) h24 h25 v11 h26 h27 v3 (h28,h29) h30.
subst a2 a o v v11 v12 v22.
*)
subst a2 o v v11.
intro h0; red in h0.
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
intuition.
apply (H3 v3); auto.
apply (H4 v5); auto.
red; exists i0; intuition.
assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case.
auto.
......
(* This file is generated by Why3's Coq 8.4 driver *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -8,89 +8,104 @@ Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
Implicit Arguments mk_ref [[a]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).
Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
((length (make n v)) = n).
Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
((get (make n v) i) = v).
(* Why3 assumption *)
Definition appear_twice (a:(@array Z _)) (v:Z) (u:Z): Prop := exists i:Z,
Definition appear_twice (a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z,
((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get a i) = v) /\ exists j:Z,
((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get a j) = v))).
(* Why3 goal *)
Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(@map.Map.map Z _
Z _)) (n:Z), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\
Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(map.Map.map Z Z))
(n:Z), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\
(((a = (n + 2%Z)%Z) /\ (2%Z <= n)%Z) /\ ((forall (i:Z), ((0%Z <= i)%Z /\
(i < a)%Z) -> ((0%Z <= (map.Map.get a1 i))%Z /\ ((map.Map.get a1
i) < n)%Z)) /\ exists v1:Z, (appear_twice a2 v1 (n + 2%Z)%Z) /\
exists v2:Z, (appear_twice a2 v2 (n + 2%Z)%Z) /\ ~ (v2 = v1)))) ->
((0%Z <= n)%Z -> ((0%Z <= n)%Z -> let o := (n + 1%Z)%Z in ((0%Z <= o)%Z ->
forall (v2:Z) (v1:Z) (deja_vu:(@map.Map.map Z _ bool _)), forall (i:Z),
((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) -> (v2 = (-1%Z)%Z)) /\
(((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
((0%Z <= n)%Z -> forall (deja_vu:Z) (deja_vu1:(map.Map.map Z bool)),
((0%Z <= deja_vu)%Z /\ ((deja_vu = n) /\ forall (i:Z),
((map.Map.get deja_vu1 i) = false))) -> let o := (n + 1%Z)%Z in
((0%Z <= o)%Z -> forall (v2:Z) (v1:Z) (deja_vu2:(map.Map.map Z bool)),
forall (i:Z), ((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) ->
(v2 = (-1%Z)%Z)) /\ (((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
(((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\
((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu
((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu2
v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((map.Map.get a1
j) = v)) \/ ((~ ((map.Map.get deja_vu v) = true)) /\ forall (j:Z),
j) = v)) \/ ((~ ((map.Map.get deja_vu2 v) = true)) /\ forall (j:Z),
((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((map.Map.get a1 j) = v)))) /\
(((v1 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) ->
~ (appear_twice a2 v i)) /\ ((v2 = (-1%Z)%Z) -> forall (v:Z),
((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v1)) -> ~ (appear_twice a2 v
i)))))))) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let v := (map.Map.get a1 i) in
(((0%Z <= n)%Z /\ ((0%Z <= v)%Z /\ (v < n)%Z)) -> (((map.Map.get deja_vu
v) = true) -> ((~ (v1 = (-1%Z)%Z)) -> ((v2 = (-1%Z)%Z) -> ((v = v1) ->
((v2 = (-1%Z)%Z) -> forall (v3:Z), ((0%Z <= v3)%Z /\ (v3 < n)%Z) ->
((~ (v3 = v1)) -> ~ (appear_twice a2 v3 (i + 1%Z)%Z)))))))))))))).
(((0%Z <= deja_vu)%Z /\ ((0%Z <= v)%Z /\ (v < deja_vu)%Z)) ->
(((map.Map.get deja_vu2 v) = true) -> ((~ (v1 = (-1%Z)%Z)) ->
((v2 = (-1%Z)%Z) -> ((v = v1) -> ((v2 = (-1%Z)%Z) -> forall (v3:Z),
((0%Z <= v3)%Z /\ (v3 < n)%Z) -> ((~ (v3 = v1)) -> ~ (appear_twice a2 v3
(i + 1%Z)%Z))))))))))))).
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8
deja_vu deja_vu1 (h9,(h10,h11)) o h12 v3 v4 deja_vu2 i (h13,h14)
(h15,(h16,(h17,(h18,(h19,h20))))) (h21,h22) v (h23,(h24,h25)) h26 h27
h28 h29 h30 v5 (h31,h32) h33.
(*
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8 h9 o
h10 v22 v12 deja_vu i (h11,h12) (h13,(h14,(h15,(h16,(h17,h18)))))
(h19,h20) v (h21,(h22,h23)) h24 h25 h26 h27 h28 v3 (h29,h30) h31.
subst a2 a o v v12 v22.
*)
subst a2 a o v.
intros h0.
red in h0.
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
apply (h18 h28 v3); auto.
apply (h20 h30 v5); auto.
red.
exists i0; intuition.
assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case.
......
(* This file is generated by Why3's Coq 8.4 driver *)
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -8,97 +8,113 @@ Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Axiom qtmark : Type.
Parameter qtmark_WhyType : WhyType qtmark.
Existing Instance qtmark_WhyType.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
Implicit Arguments mk_ref [[a]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Inductive array (a:Type) :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
Implicit Arguments mk_array [[a]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).
Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
((length (make n v)) = n).
Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
((get (make n v) i) = v).
(* Why3 assumption *)
Definition appear_twice (a:(@array Z _)) (v:Z) (u:Z): Prop := exists i:Z,
Definition appear_twice (a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z,
((0%Z <= i)%Z /\ (i < u)%Z) /\ (((get a i) = v) /\ exists j:Z,
((0%Z <= j)%Z /\ (j < u)%Z) /\ ((~ (j = i)) /\ ((get a j) = v))).
(* Why3 goal *)
Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(@map.Map.map Z _
Z _)) (n:Z), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\
Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(map.Map.map Z Z))
(n:Z), let a2 := (mk_array a a1) in (((0%Z <= a)%Z /\
(((a = (n + 2%Z)%Z) /\ (2%Z <= n)%Z) /\ ((forall (i:Z), ((0%Z <= i)%Z /\
(i < a)%Z) -> ((0%Z <= (map.Map.get a1 i))%Z /\ ((map.Map.get a1
i) < n)%Z)) /\ exists v1:Z, (appear_twice a2 v1 (n + 2%Z)%Z) /\
exists v2:Z, (appear_twice a2 v2 (n + 2%Z)%Z) /\ ~ (v2 = v1)))) ->
((0%Z <= n)%Z -> ((0%Z <= n)%Z -> let o := (n + 1%Z)%Z in ((0%Z <= o)%Z ->
forall (v2:Z) (v1:Z) (deja_vu:(@map.Map.map Z _ bool _)), forall (i:Z),
((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) -> (v2 = (-1%Z)%Z)) /\
(((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
((0%Z <= n)%Z -> forall (deja_vu:Z) (deja_vu1:(map.Map.map Z bool)),
((0%Z <= deja_vu)%Z /\ ((deja_vu = n) /\ forall (i:Z),
((map.Map.get deja_vu1 i) = false))) -> let o := (n + 1%Z)%Z in
((0%Z <= o)%Z -> forall (v2:Z) (v1:Z) (deja_vu2:(map.Map.map Z bool)),
forall (i:Z), ((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) ->
(v2 = (-1%Z)%Z)) /\ (((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
(((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\
((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu
((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu2
v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((map.Map.get a1
j) = v)) \/ ((~ ((map.Map.get deja_vu v) = true)) /\ forall (j:Z),
j) = v)) \/ ((~ ((map.Map.get deja_vu2 v) = true)) /\ forall (j:Z),
((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((map.Map.get a1 j) = v)))) /\
(((v1 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) ->
~ (appear_twice a2 v i)) /\ ((v2 = (-1%Z)%Z) -> forall (v:Z),
((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v1)) -> ~ (appear_twice a2 v
i)))))))) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let v := (map.Map.get a1 i) in
(((0%Z <= n)%Z /\ ((0%Z <= v)%Z /\ (v < n)%Z)) -> ((~ ((map.Map.get deja_vu
v) = true)) -> (((0%Z <= v)%Z /\ (v < n)%Z) ->
forall (deja_vu1:(@map.Map.map Z _ bool _)), ((0%Z <= n)%Z /\
(deja_vu1 = (map.Map.set deja_vu v true))) -> ((v1 = (-1%Z)%Z) ->
forall (v3:Z), ((0%Z <= v3)%Z /\ (v3 < n)%Z) -> ~ (appear_twice a2 v3
(i + 1%Z)%Z))))))))))).
(((0%Z <= deja_vu)%Z /\ ((0%Z <= v)%Z /\ (v < deja_vu)%Z)) ->
((~ ((map.Map.get deja_vu2 v) = true)) -> (((0%Z <= v)%Z /\
(v < deja_vu)%Z) -> forall (deja_vu3:(map.Map.map Z bool)),
((0%Z <= deja_vu)%Z /\ (deja_vu3 = (map.Map.set deja_vu2 v true))) ->
((v1 = (-1%Z)%Z) -> forall (v3:Z), ((0%Z <= v3)%Z /\ (v3 < n)%Z) ->
~ (appear_twice a2 v3 (i + 1%Z)%Z)))))))))).
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8
deja_vu deja_vu1 (h9,(h10,h11)) o h12 v3 v4 deja_vu2 i (h13,h14)
(h15,(h16,(h17,(h18,(h19,h20))))) (h21,h22) v (h23,(h24,h25)) h26
(h27,h28) deja_vu3 (h29,h30) h31 v5 (h32,h33).
(*
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8 h9 o
h10 v22 v12 deja_vu i (h11,h12) (h13,(h14,(h15,(h16,(h17,h18)))))
(h19,h20) v (h21,(h22,h23)) h24 (h25,h26) deja_vu1 (h27,h28) h29 v3
(h30,h31).
*)
intro h0.
intuition.
destruct (h16 (Map.get a1 i)); intuition.
destruct (h18 (Map.get a1 i)); intuition.
subst v; auto with zarith.
red in h0.
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
assert (v3 <> Map.get a1 i).
assert (v5 <> Map.get a1 i).
assert (case: (i0 < i \/ j < i)%Z) by omega. destruct case.
red; intro; apply (H4 i0). omega. unfold get in h01; simpl in h01. omega.
red; intro.
apply (H4 i0). omega. unfold get in h01; simpl in h01. omega.
red; intro; apply (H4 j). omega. unfold get in h04; simpl in h04. omega.
apply (H0 v3); auto.
apply (H0 v5); auto.
red; exists i0; intuition.
assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case.
auto.
......
......@@ -52,9 +52,13 @@ Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v: (map.Map.map Z a))).
Parameter make: forall {a:Type} {a_WT:WhyType a}, Z -> a -> (array a).
Axiom make_length : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (v:a),
((length (make n v)) = n).
Axiom make_elts : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (i:Z) (v:a),
((get (make n v) i) = v).
(* Why3 assumption *)
Definition appear_twice (a:(array Z)) (v:Z) (u:Z): Prop := exists i:Z,
......@@ -68,47 +72,42 @@ Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(map.Map.map Z Z))
(i < a)%Z) -> ((0%Z <= (map.Map.get a1 i))%Z /\ ((map.Map.get a1
i) < n)%Z)) /\ exists v1:Z, (appear_twice a2 v1 (n + 2%Z)%Z) /\
exists v2:Z, (appear_twice a2 v2 (n + 2%Z)%Z) /\ ~ (v2 = v1)))) ->
((0%Z <= n)%Z -> ((0%Z <= n)%Z -> let o := (n + 1%Z)%Z in ((0%Z <= o)%Z ->
forall (v2:Z) (v1:Z) (deja_vu:(map.Map.map Z bool)), forall (i:Z),
((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) -> (v2 = (-1%Z)%Z)) /\
(((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
((0%Z <= n)%Z -> forall (deja_vu:Z) (deja_vu1:(map.Map.map Z bool)),
((0%Z <= deja_vu)%Z /\ ((deja_vu = n) /\ forall (i:Z),
((map.Map.get deja_vu1 i) = false))) -> let o := (n + 1%Z)%Z in
((0%Z <= o)%Z -> forall (v2:Z) (v1:Z) (deja_vu2:(map.Map.map Z bool)),
forall (i:Z), ((0%Z <= i)%Z /\ (i <= o)%Z) -> ((((v1 = (-1%Z)%Z) ->
(v2 = (-1%Z)%Z)) /\ (((~ (v1 = (-1%Z)%Z)) -> (appear_twice a2 v1 i)) /\
(((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\
((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu
((forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) -> ((((map.Map.get deja_vu2
v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((map.Map.get a1
j) = v)) \/ ((~ ((map.Map.get deja_vu v) = true)) /\ forall (j:Z),
j) = v)) \/ ((~ ((map.Map.get deja_vu2 v) = true)) /\ forall (j:Z),
((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((map.Map.get a1 j) = v)))) /\
(((v1 = (-1%Z)%Z) -> forall (v:Z), ((0%Z <= v)%Z /\ (v < n)%Z) ->
~ (appear_twice a2 v i)) /\ ((v2 = (-1%Z)%Z) -> forall (v:Z),
((0%Z <= v)%Z /\ (v < n)%Z) -> ((~ (v = v1)) -> ~ (appear_twice a2 v
i)))))))) -> (((0%Z <= i)%Z /\ (i < a)%Z) -> let v := (map.Map.get a1 i) in
(((0%Z <= n)%Z /\ ((0%Z <= v)%Z /\ (v < n)%Z)) -> ((~ ((map.Map.get deja_vu
v) = true)) -> (((0%Z <= v)%Z /\ (v < n)%Z) ->
forall (deja_vu1:(map.Map.map Z bool)), ((0%Z <= n)%Z /\
(deja_vu1 = (map.Map.set deja_vu v true))) -> ((v2 = (-1%Z)%Z) ->
forall (v3:Z), ((0%Z <= v3)%Z /\ (v3 < n)%Z) -> ((~ (v3 = v1)) ->
~ (appear_twice a2 v3 (i + 1%Z)%Z)))))))))))).
(* Why3 intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8 h9 o
h10 v2 v1 deja_vu i (h11,h12) (h13,(h14,(h15,(h16,(h17,h18)))))
(h19,h20) v (h21,(h22,h23)) h24 (h25,h26) deja_vu1 (h27,h28) h29 v3
(h30,h31) h32. *)
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8 h9 o
h10 v22 v12 deja_vu i (h11,h12) (h13,(h14,(h15,(h16,(h17,h18)))))
(h19,h20) v (h21,(h22,h23)) h24 (h25,h26) deja_vu1 (h27,h28) h29 v3
(h30,h31) h32.
(((0%Z <= deja_vu)%Z /\ ((0%Z <= v)%Z /\ (v < deja_vu)%Z)) ->
((~ ((map.Map.get deja_vu2 v) = true)) -> (((0%Z <= v)%Z /\
(v < deja_vu)%Z) -> forall (deja_vu3:(map.Map.map Z bool)),
((0%Z <= deja_vu)%Z /\ (deja_vu3 = (map.Map.set deja_vu2 v true))) ->
((v2 = (-1%Z)%Z) -> forall (v3:Z), ((0%Z <= v3)%Z /\ (v3 < n)%Z) ->
((~ (v3 = v1)) -> ~ (appear_twice a2 v3 (i + 1%Z)%Z))))))))))).
intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8
deja_vu deja_vu1 (h9,(h10,h11)) o h12 v3 v4 deja_vu2 i (h13,h14)
(h15,(h16,(h17,(h18,(h19,h20))))) (h21,h22) v (h23,(h24,h25)) h26
(h27,h28) deja_vu3 (h29,h30) h31 v5 (h32,h33) h34.
intros h0;
destruct (h16 (Map.get a1 i)); intuition.
destruct (h18 (Map.get a1 i)); intuition.
subst v; omega.
red in h0.
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
assert (v3 <> Map.get a1 i).
assert (v5 &