decrease1: updated proof

parent c4da6ea2
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| (mk_ref contents1) => contents1
end.
Implicit Arguments contents.
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), 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) (b:Type), 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 (b:Type) (a:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Inductive array (a:Type) :=
| mk_array : Z -> (map Z a) -> array a.
Implicit Arguments mk_array.
Definition elts (a:Type)(u:(array a)): (map Z a) :=
match u with
| (mk_array _ elts1) => elts1
end.
Implicit Arguments elts.
Definition length (a:Type)(u:(array a)): Z :=
match u with
| (mk_array length1 _) => length1
end.
Implicit Arguments length.
Definition get1 (a:Type)(a1:(array a)) (i:Z): a := (get (elts a1) i).
Implicit Arguments get1.
Definition set1 (a:Type)(a1:(array a)) (i:Z) (v:a): (array a) :=
match a1 with
| (mk_array xcl0 _) => (mk_array xcl0 (set (elts a1) i v))
end.
Implicit Arguments set1.
Definition decrease1(a:(array Z)): Prop := forall (i:Z), ((0%Z <= i)%Z /\
(i < ((length a) - 1%Z)%Z)%Z) -> (((get1 a i) - 1%Z)%Z <= (get1 a
(i + 1%Z)%Z))%Z.
Axiom decrease1_induction : forall (a:(array Z)), (decrease1 a) ->
forall (i:Z) (j:Z), (((0%Z <= i)%Z /\ (i <= j)%Z) /\
(j < (length a))%Z) -> ((((get1 a i) + i)%Z - j)%Z <= (get1 a j))%Z.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_search_rec : forall (a:Z), forall (i:Z), forall (a1:(map
Z Z)), let a2 := (mk_array a a1) in (((decrease1 a2) /\ (0%Z <= i)%Z) ->
((i < a)%Z -> (((0%Z <= i)%Z /\ (i < a)%Z) -> ((~ ((get a1 i) = 0%Z)) ->
(((0%Z <= i)%Z /\ (i < a)%Z) -> ((0%Z < (get a1 i))%Z ->
(((0%Z <= i)%Z /\ (i < a)%Z) -> let result := (get a1 i) in
(((decrease1 a2) /\ (0%Z <= (i + result)%Z)%Z) -> forall (result1:Z),
(((result1 = (-1%Z)%Z) /\ forall (j:Z), (((i + result)%Z <= j)%Z /\
(j < a)%Z) -> ~ ((get a1 j) = 0%Z)) \/ ((((i + result)%Z <= result1)%Z /\
(result1 < a)%Z) /\ (((get a1 result1) = 0%Z) /\ forall (j:Z),
(((i + result)%Z <= j)%Z /\ (j < result1)%Z) -> ~ ((get a1 j) = 0%Z)))) ->
(((result1 = (-1%Z)%Z) /\ forall (j:Z), ((i <= j)%Z /\ (j < a)%Z) ->
~ ((get a1 j) = 0%Z)) \/ (((i <= result1)%Z /\ (result1 < a)%Z) /\
(((get a1 result1) = 0%Z) /\ forall (j:Z), ((i <= j)%Z /\
(j < result1)%Z) -> ~ ((get a1 j) = 0%Z)))))))))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
intuition.
left; intuition.
assert (case: (j < i+get a1 i \/ i+get a1 i <= j)%Z) by omega. destruct case.
generalize (decrease1_induction (mk_array a a1) H5 i j); unfold get1; simpl; intuition.
apply H14 with j; auto.
right; intuition.
assert (case: (j < i+get a1 i \/ i+get a1 i <= j)%Z) by omega. destruct case.
generalize (decrease1_induction (mk_array a a1) H5 i j); unfold get1; simpl; intuition.
apply H16 with j; auto.
Qed.
(* DO NOT EDIT BELOW *)
This diff is collapsed.
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