Commit 20cdf859 authored by MARCHE Claude's avatar MARCHE Claude

simplified Coq proof

parent 6592b788
(* 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,66 +8,68 @@ 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))).
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))).
(* 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),
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)) /\
(((~ (v2 = (-1%Z)%Z)) -> ((appear_twice a2 v2 i) /\ ~ (v2 = v1))) /\
......@@ -81,10 +83,14 @@ Theorem WP_parameter_two_equal_elements : forall (a:Z) (a1:(@map.Map.map Z _
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 /\
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
......@@ -98,15 +104,21 @@ 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 v3); auto.
red; exists i0; intuition.
red; exists i0.
(*
Require Import Why3.
why3 "alt-ergo" timelimit 2.
*)
split.
assert (case: (i0 < i \/ i0 = i)%Z) by omega. destruct case.
auto.
auto with zarith.
subst i0.
unfold get in h01; simpl in h01.
omega.
exists j; intuition.
split; auto.
exists j.
assert (case: (j < i \/ j = i)%Z) by omega. destruct case.
auto.
auto with zarith.
subst j.
unfold get in h04; simpl in h04.
omega.
......
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