### LCP: more proof attempts in Coq

parent 95d9e88f
 ... ... @@ -79,15 +79,24 @@ module LCP "longest common prefix" use import int.Int use map.Map use map.MapPermut use map.MapInjection use import array.Array predicate permutation (a:array int) = MapInjection.range a.elts a.length /\ MapInjection.injective a.elts a.length predicate map_permutation (m:Map.map int int) (u : int) = MapInjection.range m u /\ MapInjection.injective m u lemma map_permut_permutation : forall m1 m2:Map.map int int, u:int [MapPermut.permut_sub m1 m2 0 u]. MapPermut.permut_sub m1 m2 0 u -> map_permutation m1 u -> map_permutation m2 u use import array.Array use import array.ArrayPermut predicate permutation (a:array int) = map_permutation a.elts a.length lemma permut_permutation : forall a1 a2:array int. permut a1 a2 -> permutation a1 -> permutation a2 ... ...
 (* 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. Require map.MapPermut. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) Definition injective(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < n)%Z) -> ((~ (i = j)) -> ~ ((map.Map.get a i) = (map.Map.get a j)))). (* Why3 assumption *) Definition surjective(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> exists j:Z, ((0%Z <= j)%Z /\ (j < n)%Z) /\ ((map.Map.get a j) = i). (* Why3 assumption *) Definition range(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (map.Map.get a i))%Z /\ ((map.Map.get a i) < n)%Z). Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a n) -> ((range a n) -> (surjective a n)). (* Why3 assumption *) Definition map_permutation(m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ (injective m u). (* Why3 goal *) Theorem map_permut_permutation : forall (m1:(map.Map.map Z Z)) (m2:(map.Map.map Z Z)) (u:Z), (map.MapPermut.permut_sub m1 m2 0%Z u) -> ((map_permutation m1 u) -> (map_permutation m2 u)). intros m1 m2 u h1 h2. unfold permutation in *. simpl in *. subst l2. Print permut_sub. inversion h2. elim h2; auto. admit. unfold range, injective. intuition. destruct H1 as (h1 & h2 & h3). intros. assert (i0=i \/ i0 = j \/ (i0 <> i /\ i0 <> j)) by omega. destruct H1. subst i0. rewrite h2. Qed.
 ... ... @@ -4,6 +4,7 @@ Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. Require map.MapPermut. (* Why3 assumption *) Definition unit := unit. ... ... @@ -26,6 +27,14 @@ Definition range(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z), Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a n) -> ((range a n) -> (surjective a n)). (* Why3 assumption *) Definition map_permutation(m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ (injective m u). Axiom map_permut_permutation : forall (m1:(map.Map.map Z Z)) (m2:(map.Map.map Z Z)) (u:Z), (map.MapPermut.permut_sub m1 m2 0%Z u) -> ((map_permutation m1 u) -> (map_permutation m2 u)). (* Why3 assumption *) Inductive array (a:Type) {a_WT:WhyType a} := | mk_array : Z -> (map.Map.map Z a) -> array a. ... ... @@ -57,10 +66,6 @@ Definition set {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array 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 permutation(a:(array Z)): Prop := (range (elts a) (length a)) /\ (injective (elts a) (length a)). (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1 ... ... @@ -150,20 +155,22 @@ Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a}, Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2). (* Why3 assumption *) Definition permutation(a:(array Z)): Prop := (map_permutation (elts a) (length a)). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 a2) -> ((permutation a1) -> (permutation a2)). intros (l1,a1) (l2,a2) (h1,h2) h. intros (l1,a1) (l2,a2) (h1,h2). unfold permutation in *. simpl in *. subst l2. induction h2. ae. ae. apply IHh2_2; auto. ae. intro. apply map_permut_permutation with (m1:=a1); auto. Qed.
 ... ... @@ -3,44 +3,47 @@ Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. Require map.MapPermut. (* Why3 assumption *) Definition unit := unit. 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. Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b. (* Why3 assumption *) Definition injective(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < n)%Z) -> ((~ (i = j)) -> ~ ((map.Map.get a i) = (map.Map.get a j)))). Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b -> (map a b). (* Why3 assumption *) Definition surjective(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> exists j:Z, ((0%Z <= j)%Z /\ (j < n)%Z) /\ ((map.Map.get a j) = i). Axiom Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1). (* Why3 assumption *) Definition range(a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (map.Map.get a i))%Z /\ ((map.Map.get a i) < n)%Z). Axiom Select_neq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a n) -> ((range a n) -> (surjective a n)). Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, b -> (map a b). (* Why3 assumption *) Definition map_permutation(m:(map.Map.map Z Z)) (u:Z): Prop := (range m u) /\ (injective m u). Axiom Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). Axiom map_permut_permutation : forall (m1:(map.Map.map Z Z)) (m2:(map.Map.map Z Z)) (u:Z), (map.MapPermut.permut_sub m1 m2 0%Z u) -> ((map_permutation m1 u) -> (map_permutation m2 u)). (* Why3 assumption *) Inductive array (a:Type) {a_WT:WhyType a} := | mk_array : Z -> (map Z a) -> array a. | 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]]. (* Why3 assumption *) Definition elts {a:Type} {a_WT:WhyType a}(v:(array a)): (map Z a) := 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. ... ... @@ -52,64 +55,59 @@ Definition length {a:Type} {a_WT:WhyType a}(v:(array a)): Z := end. (* Why3 assumption *) Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := (get (elts a1) i). Definition get {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := (map.Map.get (elts a1) i). (* Why3 assumption *) Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array a) := (mk_array (length a1) (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) := (mk_array n (const v:(map Z a))). (mk_array n (map.Map.const v:(map.Map.map Z a))). (* Why3 assumption *) Definition array_bounded(a:(array Z)) (b:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\ (i < (length a))%Z) -> ((0%Z <= (get1 a i))%Z /\ ((get1 a i) < b)%Z). Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1 i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1 k) = (map.Map.get a2 k))). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((get a1 i) = (get a2 i)). (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map Z a)) (a2:(map Z a)) (i:Z) (j:Z): Prop := ((get a1 i) = (get a2 j)) /\ (((get a2 i) = (get a1 j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((get a1 k) = (get a2 k))). Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)), forall (i:Z) (j:Z), (exchange a1 (set (set a1 i (get a1 j)) j (get a1 i)) i Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z a)), forall (i:Z) (j:Z), (exchange a1 (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i j). (* Why3 assumption *) Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map Z a) -> (map Z a) -> Z -> Z -> Prop := | permut_refl : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), (map_eq_sub a1 a2 l u) -> (permut_sub a1 a2 l u) | permut_sym : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) | permut_trans : forall (a1:(map Z a)) (a2:(map Z a)) (a3:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u)) | permut_exchange : forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))). Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)) (a2:(map Z a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((get a2 i) = (get a1 i)). Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map Z a)) (a2:(map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((get a2 i) = (get a1 j)). Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a) -> (map.Map.map Z a) -> Z -> Z -> Prop := | permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a1 l u) | permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) | permut_trans : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) (a3:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u)) | permut_exchange : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))). Axiom permut_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). Axiom permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2 i) = (map.Map.get a1 i)). Axiom permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a2 i) = (map.Map.get a1 j)). (* Why3 assumption *) Definition exchange1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a)) ... ... @@ -136,6 +134,11 @@ Axiom permut_trans1 : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)) (a3:(array a)), (permut a1 a2) -> ((permut a2 a3) -> (permut a1 a3)). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)). (* Why3 assumption *) Definition array_eq_sub {a:Type} {a_WT:WhyType a}(a1:(array a)) (a2:(array a)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) l u). ... ... @@ -152,47 +155,55 @@ Axiom array_eq_sub_permut : forall {a:Type} {a_WT:WhyType a}, Axiom array_eq_permut : forall {a:Type} {a_WT:WhyType a}, forall (a1:(array a)) (a2:(array a)), (array_eq a1 a2) -> (permut a1 a2). Axiom permut_bounded : forall (a1:(array Z)) (a2:(array Z)) (n:Z), ((permut a1 a2) /\ (array_bounded a1 n)) -> (array_bounded a2 n). (* Why3 assumption *) Definition permutation(a:(array Z)): Prop := (map_permutation (elts a) (length a)). Axiom permut_permutation : forall (a1:(array Z)) (a2:(array Z)), (permut a1 a2) -> ((permutation a1) -> (permutation a2)). (* Why3 assumption *) Definition is_common_prefix(a:(array Z)) (x:Z) (y:Z) (l:Z): Prop := (0%Z <= l)%Z /\ (((x + l)%Z <= (length a))%Z /\ (((y + l)%Z <= (length a))%Z /\ forall (i:Z), ((0%Z <= i)%Z /\ (i < l)%Z) -> ((get1 a (x + i)%Z) = (get1 a (y + i)%Z)))). (i < l)%Z) -> ((get a (x + i)%Z) = (get a (y + i)%Z)))). Axiom common_prefix_eq : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ (x < (length a))%Z) -> (is_common_prefix a x x ((length a) - x)%Z). (x <= (length a))%Z) -> (is_common_prefix a x x ((length a) - x)%Z). Axiom common_prefix_eq2 : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ (x < (length a))%Z) -> ~ (is_common_prefix a x x (x <= (length a))%Z) -> ~ (is_common_prefix a x x (((length a) - x)%Z + 1%Z)%Z). Axiom not_common_prefix_if_last_different : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), ((0%Z < l)%Z /\ (((x + l)%Z < (length a))%Z /\ (((y + l)%Z < (length a))%Z /\ ~ ((get1 a (x + (l - 1%Z)%Z)%Z) = (get1 a (((y + l)%Z < (length a))%Z /\ ~ ((get a (x + (l - 1%Z)%Z)%Z) = (get a (y + (l - 1%Z)%Z)%Z))))) -> ~ (is_common_prefix a x y l). Parameter longest_common_prefix: (array Z) -> Z -> Z -> Z. Axiom lcp_spec : forall (a:(array Z)) (x:Z) (y:Z) (l:Z), (((0%Z <= x)%Z /\ (x < (length a))%Z) /\ ((0%Z <= y)%Z /\ (y < (length a))%Z)) -> (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> ((l = (longest_common_prefix a x y)) <-> ((is_common_prefix a x y l) /\ ~ (is_common_prefix a x y (l + 1%Z)%Z))). Axiom lcp_is_cp : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ (x < (length a))%Z) /\ ((0%Z <= y)%Z /\ (y < (length a))%Z)) -> (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> (is_common_prefix a x y (longest_common_prefix a x y)). Axiom lcp_eq : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ (x < (length a))%Z) /\ ((0%Z <= y)%Z /\ (y < (length a))%Z)) -> (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> forall (i:Z), ((0%Z <= i)%Z /\ (i < (longest_common_prefix a x y))%Z) -> ((get1 a (x + i)%Z) = (get1 a (y + i)%Z)). ((get a (x + i)%Z) = (get a (y + i)%Z)). Axiom lcp_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ (x < (length a))%Z) -> ((longest_common_prefix a x (x <= (length a))%Z) -> ((longest_common_prefix a x x) = ((length a) - x)%Z). Axiom lcp_sym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ (x <= (length a))%Z) /\ ((0%Z <= y)%Z /\ (y <= (length a))%Z)) -> ((longest_common_prefix a x y) = (longest_common_prefix a y x)). (* Why3 assumption *) Inductive ref (a:Type) {a_WT:WhyType a} := | mk_ref : a -> ref a. ... ... @@ -208,26 +219,26 @@ Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a := (* Why3 assumption *) Definition le(a:(array Z)) (x:Z) (y:Z): Prop := let n := (length a) in (((0%Z <= x)%Z /\ (x < n)%Z) /\ (((0%Z <= y)%Z /\ (y < n)%Z) /\ let l := (((0%Z <= x)%Z /\ (x <= n)%Z) /\ (((0%Z <= y)%Z /\ (y <= n)%Z) /\ let l := (longest_common_prefix a x y) in (((x + l)%Z = n) \/ (((x + l)%Z < n)%Z /\ (((y + l)%Z < n)%Z /\ ((get1 a (x + l)%Z) <= (get1 a (y + l)%Z))%Z))))). (((y + l)%Z < n)%Z /\ ((get a (x + l)%Z) <= (get a (y + l)%Z))%Z))))). Axiom le_refl : forall (a:(array Z)) (x:Z), ((0%Z <= x)%Z /\ (x < (length a))%Z) -> (le a x x). (x <= (length a))%Z) -> (le a x x). Axiom le_trans : forall (a:(array Z)) (x:Z) (y:Z) (z:Z), (((0%Z <= x)%Z /\ (x < (length a))%Z) /\ (((0%Z <= y)%Z /\ (y < (length a))%Z) /\ (((0%Z <= z)%Z /\ (z < (length a))%Z) /\ ((le a x y) /\ (le a y z))))) -> (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ (((0%Z <= z)%Z /\ (z <= (length a))%Z) /\ ((le a x y) /\ (le a y z))))) -> (le a x z). Axiom le_asym : forall (a:(array Z)) (x:Z) (y:Z), (((0%Z <= x)%Z /\ (x <= (length a))%Z) /\ (((0%Z <= y)%Z /\ (y <= (length a))%Z) /\ ~ (le a x y))) -> (le a y x). (* Why3 assumption *) Definition sorted_sub(a:(array Z)) (data:(array Z)) (l:Z) (u:Z): Prop := forall (i1:Z) (i2:Z), (((l <= i1)%Z /\ (i1 <= i2)%Z) /\ (i2 < u)%Z) -> (le a (get1 data i1) (get1 data i2)). Axiom sorted_bounded : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z), (((l <= i)%Z /\ (i < u)%Z) /\ (sorted_sub a data l u)) -> ((0%Z <= (get1 data i))%Z /\ ((get1 data i) < (length a))%Z). (le a (get data i1) (get data i2)). Require Import Why3. Ltac ae := why3 "alt-ergo" timelimit 3. ... ... @@ -235,9 +246,9 @@ Ltac ae := why3 "alt-ergo" timelimit 3. (* Why3 goal *) Theorem sorted_le : forall (a:(array Z)) (data:(array Z)) (l:Z) (u:Z) (i:Z) (x:Z), (((l <= i)%Z /\ (i < u)%Z) /\ ((sorted_sub a data l u) /\ (le a x (get1 data l)))) -> (le a x (get1 data i)). (get data l)))) -> (le a x (get data i)). intros a data l u i x ((h1,h2),(h3,h4)). apply le_trans with (get1 data l). apply le_trans with (get data l). ae. Qed. ... ...
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!