 ### prove type invariant before pre-/post-

parent 05e8681c
 shape="ainfix =agetasetV4V0V3V2V1Iainfix =agetV4V2V1Iainfix =V2V0NFF">
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
 shape="ainfix =ainfix ++aNilareverseaNilaNilAainfix =alengthV0c0Aainfix >=c0alengthV0Aainfix =alengthaNilc0LaNil">
 ... ... @@ -25,11 +25,9 @@ Existing Instance option_WhyType. Implicit Arguments None [[a] [a_WT]]. Implicit Arguments Some [[a] [a_WT]]. Parameter nth: forall {a:Type} {a_WT:WhyType a}, BuiltIn.int -> (list a) -> (option a). Parameter nth: forall {a:Type} {a_WT:WhyType a}, Z -> (list a) -> (option a). Axiom nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:BuiltIn.int) (l:(list a)), Axiom nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z) (l:(list a)), match l with | Nil => ((nth n l) = (None :(option a))) | (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) -> ... ... @@ -37,8 +35,7 @@ Axiom nth_def : forall {a:Type} {a_WT:WhyType a}, forall (n:BuiltIn.int) end. (* Why3 assumption *) Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: BuiltIn.int := Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z ... ... @@ -51,13 +48,13 @@ Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). Axiom nth_none_1 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) (i:BuiltIn.int), (i < 0%Z)%Z -> ((nth i l) = (None :(option a))). (i:Z), (i < 0%Z)%Z -> ((nth i l) = (None :(option a))). Axiom nth_none_2 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) (i:BuiltIn.int), ((length l) <= i)%Z -> ((nth i l) = (None :(option a))). (i:Z), ((length l) <= i)%Z -> ((nth i l) = (None :(option a))). Axiom nth_none_3 : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)) (i:BuiltIn.int), ((nth i l) = (None :(option a))) -> ((i < 0%Z)%Z \/ (i:Z), ((nth i l) = (None :(option a))) -> ((i < 0%Z)%Z \/ ((length l) <= i)%Z). (* Why3 assumption *) ... ... @@ -95,16 +92,15 @@ Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list (l = (infix_plpl l1 (Cons x l2))). Axiom nth_append_1 : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (i:BuiltIn.int), (i < (length l1))%Z -> ((nth i (infix_plpl l1 l2)) = (nth i l1)). (l2:(list a)) (i:Z), (i < (length l1))%Z -> ((nth i (infix_plpl l1 l2)) = (nth i l1)). Axiom nth_append_2 : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (i:BuiltIn.int), ((length l1) <= i)%Z -> ((nth i (infix_plpl l1 l2)) = (nth (i - (length l1))%Z l2)). (l2:(list a)) (i:Z), ((length l1) <= i)%Z -> ((nth i (infix_plpl l1 l2)) = (nth (i - (length l1))%Z l2)). Parameter map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. Axiom map_WhyType : forall (a:Type) {a_WT:WhyType a} Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b). Existing Instance map_WhyType. ... ... @@ -130,35 +126,38 @@ Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (* Why3 assumption *) Inductive array (a:Type) {a_WT:WhyType a} := | mk_array : BuiltIn.int -> (map BuiltIn.int a) -> array a. | mk_array : Z -> (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]]. (* Why3 assumption *) Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map BuiltIn.int a) := match v with Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) := match v with | (mk_array x x1) => x1 end. (* Why3 assumption *) Definition length1 {a:Type} {a_WT:WhyType a}(v:(array a)): BuiltIn.int := Definition length1 {a:Type} {a_WT:WhyType a}(v:(array a)): Z := match v with | (mk_array x x1) => x end. (* Why3 assumption *) Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int): a := Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := (get (elts a1) i). (* Why3 assumption *) Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:BuiltIn.int) (v:a): (array a) := (mk_array (length1 a1) (set (elts a1) i v)). Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array a) := (mk_array (length1 a1) (set (elts a1) i v)). (* Why3 assumption *) Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) := (mk_array n (const v:(map Z a))). (* Why3 assumption *) Inductive buffer (a:Type) {a_WT:WhyType a} := | mk_buffer : BuiltIn.int -> BuiltIn.int -> (array a) -> (list a) -> buffer a. | mk_buffer : Z -> Z -> (array a) -> (list a) -> buffer a. Axiom buffer_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (buffer a). Existing Instance buffer_WhyType. Implicit Arguments mk_buffer [[a] [a_WT]]. ... ... @@ -176,39 +175,38 @@ Definition data {a:Type} {a_WT:WhyType a}(v:(buffer a)): (array a) := end. (* Why3 assumption *) Definition len {a:Type} {a_WT:WhyType a}(v:(buffer a)): BuiltIn.int := Definition len {a:Type} {a_WT:WhyType a}(v:(buffer a)): Z := match v with | (mk_buffer x x1 x2 x3) => x1 end. (* Why3 assumption *) Definition first {a:Type} {a_WT:WhyType a}(v:(buffer a)): BuiltIn.int := Definition first {a:Type} {a_WT:WhyType a}(v:(buffer a)): Z := match v with | (mk_buffer x x1 x2 x3) => x end. (* Why3 assumption *) Definition size {a:Type} {a_WT:WhyType a}(b:(buffer a)): BuiltIn.int := Definition size {a:Type} {a_WT:WhyType a}(b:(buffer a)): Z := (length1 (data b)). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem WP_parameter_head : forall {a:Type} {a_WT:WhyType a}, forall (b:BuiltIn.int), forall (rho:(list a)) (rho1:(map BuiltIn.int a)) (rho2:BuiltIn.int) (rho3:BuiltIn.int), ((0%Z < rho2)%Z /\ (((0%Z <= rho3)%Z /\ (rho3 < b)%Z) /\ (((0%Z <= rho2)%Z /\ (rho2 <= b)%Z) /\ ((rho2 = (length rho)) /\ forall (i:BuiltIn.int), ((0%Z <= i)%Z /\ (i < rho2)%Z) -> ((((rho3 + i)%Z < b)%Z -> ((nth i rho) = (Some (get rho1 (rho3 + i)%Z)))) /\ ((0%Z <= ((rho3 + i)%Z - b)%Z)%Z -> ((nth i rho) = (Some (get rho1 ((rho3 + i)%Z - b)%Z))))))))) -> (((0%Z <= rho3)%Z /\ (rho3 < b)%Z) -> Theorem WP_parameter_head : forall {a:Type} {a_WT:WhyType a}, forall (b:Z), forall (rho:(list a)) (rho1:(map Z a)) (rho2:Z) (rho3:Z), ((((0%Z <= rho3)%Z /\ (rho3 < b)%Z) /\ (((0%Z <= rho2)%Z /\ (rho2 <= b)%Z) /\ ((rho2 = (length rho)) /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < rho2)%Z) -> ((((rho3 + i)%Z < b)%Z -> ((nth i rho) = (Some (get rho1 (rho3 + i)%Z)))) /\ ((0%Z <= ((rho3 + i)%Z - b)%Z)%Z -> ((nth i rho) = (Some (get rho1 ((rho3 + i)%Z - b)%Z)))))))) /\ (0%Z < rho2)%Z) -> (((0%Z <= rho3)%Z /\ (rho3 < b)%Z) -> match rho with | Nil => False | (Cons x _) => ((get rho1 rho3) = x) end). intros a _a b rho rho1 rho2 rho3 (h1,(h2,(h2b,(h2c,h2d)))) (h3,h4). intros a _a b rho rho1 rho2 rho3 ((h2,(h2b,(h2c,h2d))),h1) (h3,h4). destruct rho. simpl in *. omega. ... ...
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. (* Why3 assumption *) Inductive option (a:Type) {a_WT:WhyType a} := | None : option a | Some : a -> option a. Axiom option_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (option a). Existing Instance option_WhyType. Implicit Arguments None [[a] [a_WT]]. Implicit Arguments Some [[a] [a_WT]]. Parameter nth: forall {a:Type} {a_WT:WhyType a}, BuiltIn.int -> (list a) -> (option a).