Commit 4943d021 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove unused Coq proofs.

parent 34810875
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.MinMax.
Require list.List.
Require list.Length.
Require list.Mem.
Require list.Append.
Axiom char : Type.
Parameter char_WhyType : WhyType char.
Existing Instance char_WhyType.
(* Why3 assumption *)
Definition word := (list char).
(* Why3 assumption *)
Inductive dist : (list char) -> (list char) -> Z -> Prop :=
| dist_eps : (dist nil nil 0%Z)
| dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (cons a w1) w2 (n + 1%Z)%Z)
| dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist w1 (cons a w2) (n + 1%Z)%Z)
| dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1
w2 n) -> forall (a:char), (dist (cons a w1) (cons a w2) n).
(* Why3 assumption *)
Definition min_dist (w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1
w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z.
(* Why3 assumption *)
Fixpoint last_char (a:char) (u:(list char)) {struct u}: char :=
match u with
| nil => a
| (cons c u') => (last_char c u')
end.
(* Why3 assumption *)
Fixpoint but_last (a:char) (u:(list char)) {struct u}: (list char) :=
match u with
| nil => nil
| (cons c u') => (cons a (but_last c u'))
end.
Axiom first_last_explicit : forall (u:(list char)) (a:char),
((List.app (but_last a u) (cons (last_char a u) nil)) = (cons a u)).
(* Why3 goal *)
Theorem first_last : forall (a:char) (u:(list char)), exists v:(list char),
exists b:char, ((List.app v (cons b nil)) = (cons a u)) /\
((list.Length.length v) = (list.Length.length u)).
intros a u.
exists (but_last a u).
exists (last_char a u).
split.
exact (first_last_explicit u a).
generalize a; induction u; intros.
simpl; omega.
unfold but_last; fold but_last.
unfold Length.length; fold @Length.length.
generalize (IHu a0); intros; omega.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
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) :=
| 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]].
(* Why3 assumption *)
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) :=
| 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]].
(* Why3 assumption *)
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)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
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)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
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,
((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 /\
(((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 -> 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_vu2
v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((map.Map.get a1
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 <= 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 o v v11.
intro h0; red in h0.
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
intuition.
apply (H4 v5); auto.
red; exists i0; intuition.
assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case.
auto.
subst i0.
unfold get in h01; simpl in h01.
omega.
exists j; intuition.
assert (case: (j < i \/ j = i)%Z) by omega. destruct case.
auto.
subst j.
unfold get in h04; simpl in h04.
omega.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
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) :=
| 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]].
(* Why3 assumption *)
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) :=
| 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]].
(* Why3 assumption *)
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)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
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)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
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,
((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 /\
(((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 -> 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_vu2
v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((map.Map.get a1
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 <= 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.
intros h0.
red in h0.
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
apply (h20 h30 v5); auto.
red.
exists i0; intuition.
assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case.
auto.
subst i0.
unfold get in h01; simpl in h01.
omega.
exists j; intuition.
assert (case: (j < i \/ j = i)%Z) by omega. destruct case.
auto.
subst j.
unfold get in h04; simpl in h04.
omega.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
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) :=
| 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]].
(* Why3 assumption *)
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) :=
| 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]].
(* Why3 assumption *)
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)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
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)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
(* Why3 assumption *)
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 /\
(((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 -> forall (deja_vu:Z) (deja_vu1:(map.Map.map Z bool)),
((0%Z <= deja_vu)%Z /\ ((deja_vu = n) /\ forall (i:Z), ((0%Z <= i)%Z /\
(i < n)%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_vu2 v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\
(j < i)%Z) /\ ((map.Map.get a1 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 <= 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)))))))))).
(* Why3 intros a a1 n a2 (h1,((h2,h3),(h4,(v1,(h5,(v2,(h6,h7))))))) h8
deja_vu deja_vu1 (h9,(h10,h11)) o h12 v21 v11 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 v3 (h32,h33). *)
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).
intro h0.
destruct (h18 (Map.get a1 i));
[auto with zarith | tauto | destruct H as (H1 & H2)].
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
assert (v5 <> Map.get a1 i).
assert (case: (i0 < i \/ j < i)%Z) by omega.
destruct case.
red; intro.
apply (H2 i0).
omega.
unfold get in h01; simpl in h01; omega.
red; intro; apply (H2 j).
omega.
unfold get in h04; simpl in h04; omega.
apply (h19 h31 v5); auto.
red; exists i0.
split.
split.
omega.
assert (case: (i0 < i \/ i0 = i)%Z) by omega.
destruct case.
auto.
subst i0.
unfold get in h01; simpl in h01.
omega.
split.
auto.
exists j.
split.
split.
omega.
assert (case: (j < i \/ j = i)%Z) by omega.
destruct case.
auto.
subst j.
unfold get in h04; simpl in h04.
omega.
auto.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
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) :=
| 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]].
(* Why3 assumption *)
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) :=
| 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]].
(* Why3 assumption *)
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)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
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)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
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,
((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 /\
(((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 -> 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_vu2
v) = true) /\ exists j:Z, ((0%Z <= j)%Z /\ (j < i)%Z) /\ ((map.Map.get a1
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 <= 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 (h18 (Map.get a1 i)); intuition.
subst v; omega.
red in h0.
destruct h0 as (i0,(h00,(h01,(j,(h02,(h03,h04)))))).
assert (v5 <> Map.get a1 i).
assert (case: (i0 < i \/ j < i)%Z) by omega. destruct case.
red; intro; apply (H1 i0). omega. unfold get in h01; simpl in h01. omega.
red; intro; apply (H1 j). omega. unfold get in h04; simpl in h04. omega.
apply (H v5); auto.
red; exists i0.