ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity

update sessions

Browse Source
This commit is contained in:
Andrei Paskevich
2014-01-19 23:14:51 +01:00
parent 61127a1939
commit b67fb7c087
104 changed files with 10898 additions and 10894 deletions
Download Patch File Download Diff File Expand all files Collapse all files

43
examples/decrease1/decrease1_Decrease1_decrease1_induction_2.v
View File

@@ -1,4 +1,4 @@
(* 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 BuiltIn.
@@ -6,7 +6,7 @@ Require int.Int.
Require map.Map.
(* Why3 assumption *)
Definition unit := unit.
Definition unit := unit.
(* Why3 assumption *)
Inductive ref (a:Type) {a_WT:WhyType a} :=
@@ -16,52 +16,54 @@ 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_WT)): 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) -> array a.
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> 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]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map.Map.map Z a) :=
match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): 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 :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (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)).
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)).
(* 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))).
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))).
(* Why3 assumption *)
Definition decrease1(a:(array Z)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
Definition decrease1 (a:(@array Z _)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < ((length a) - 1%Z)%Z)%Z) -> (((get a i) - 1%Z)%Z <= (get a
(i + 1%Z)%Z))%Z.
(* Why3 goal *)
Theorem decrease1_induction : forall (a:(array Z)), (decrease1 a) ->
forall (i:Z) (j:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\ (j < (length a))%Z) ->
Theorem decrease1_induction : forall (a:(@array Z _)), (decrease1 a) ->
forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ ((i <= j)%Z /\ (j < (length a))%Z)) ->
((((get a i) + i)%Z - j)%Z <= (get a j))%Z.
(* Why3 intros a h1 i j (h2,(h3,h4)). *)
(* YOU MAY EDIT THE PROOF BELOW *)
unfold decrease1.
intros a Ha i j Hij.
@@ -70,18 +72,17 @@ apply (Zlt_lower_bound_ind _ i).
2: omega.
intuition.
assert (x = i \/ i < x)%Z by omega.
destruct H4.
destruct H5.
subst x.
ring_simplify.
omega.
apply Zle_trans with (get a (x-1) - 1)%Z.
assert (i <= x-1 < x)%Z by omega.
assert (0 <= i <= x-1 /\ x-1 < length a)%Z by omega.
generalize (H (x-1)%Z H8 H9); clear H; intuition.
assert (0 <= i /\ i <= x-1 < length a)%Z by omega.
generalize (H0 (x-1)%Z H8 H9); clear H0; intuition.
apply Zle_trans with (get a (x-1+1))%Z.
apply (Ha (x-1)%Z); omega.
ring_simplify (x-1+1)%Z.
omega.
Qed.