array_ArrayPermut_permut_sub_weakening_2.v 5.64 KB
 Jean-Christophe Filliâtre committed Feb 24, 2014 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 ``````(* This file is generated by Why3's Coq 8.4 driver *) (* Beware! Only edit allowed sections below *) Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. Require map.Occ. Require map.MapPermut. (* Why3 assumption *) Definition unit := unit. (* Why3 assumption *) 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 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 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 a_WT)) (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)). (* 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))). (* Why3 assumption *) Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (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 a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map_eq_sub (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub (elts a1) (elts a2) 0%Z (length a1)). (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z) (i:Z) (j:Z): Prop := ((l <= i)%Z /\ (i < u)%Z) /\ (((l <= j)%Z /\ (j < u)%Z) /\ (((map.Map.get a1 i) = (map.Map.get a2 j)) /\ (((map.Map.get a1 j) = (map.Map.get a2 i)) /\ forall (k:Z), ((l <= k)%Z /\ (k < u)%Z) -> ((~ (k = i)) -> ((~ (k = j)) -> ((map.Map.get a1 k) = (map.Map.get a2 k))))))). Axiom exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@map.Map.map Z _ a a_WT)) (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> (exchange a1 (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l u i j)). (* Why3 assumption *) Definition exchange1 {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\ (exchange (elts a1) (elts a2) 0%Z (length a1) i j). (* Why3 assumption *) Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\ (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\ (map.MapPermut.permut (elts a1) (elts a2) l u))). (* Why3 assumption *) Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((permut a1 a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u (length a1))). (* Why3 assumption *) Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array a a_WT)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut (elts a1) (elts a2) 0%Z (length a1)). `````` Jean-Christophe Filliâtre committed Feb 25, 2014 99 ``````Axiom exchange_permut_sub : forall {a:Type} {a_WT:WhyType a}, `````` Jean-Christophe Filliâtre committed Feb 24, 2014 100 101 102 103 `````` forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (i:Z) (j:Z) (l:Z) (u:Z), (exchange1 a1 a2 i j) -> (((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> ((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l u))))). `````` Jean-Christophe Filliâtre committed Feb 25, 2014 104 105 106 107 108 109 `````` (* Why3 goal *) Theorem permut_sub_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@array a a_WT)) (a2:(@array a a_WT)) (l1:Z) (u1:Z) (l2:Z) (u2:Z), (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) -> (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))). `````` Guillaume Melquiond committed Feb 01, 2018 110 111 ``````(* Why3 intros a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5). *) intros a1 a2 l1 u1 l2 u2 h1 (h2,h3) (h4,h5). `````` Jean-Christophe Filliâtre committed Feb 25, 2014 112 113 114 115 116 117 118 ``````unfold permut_sub in *. destruct h1 as (eql,(h1,eqr)). unfold map_eq_sub in *. split. (* eq left *) intros. apply eql; omega. split. `````` Jean-Christophe Filliâtre committed Feb 24, 2014 119 ``````(* permut *) `````` Jean-Christophe Filliâtre committed Feb 25, 2014 120 121 122 123 124 125 126 127 ``````unfold permut in *. destruct h1 as (h1,(h1a,(h1b,h1c))). repeat split; try assumption. omega. omega. unfold MapPermut.permut in *. intros v. assert (c: (l1 <= u1 \/ u1 < l1)%Z) by omega. destruct c. (* l1 <= u1 *) assert (Occ.occ v (elts a1) l2 u2 = Occ.occ v (elts a1) l2 l1 + Occ.occ v (elts a1) l1 u2)%Z. `````` Jean-Christophe Filliâtre committed Feb 24, 2014 128 `````` apply Occ.occ_append. omega. `````` Jean-Christophe Filliâtre committed Feb 25, 2014 129 ``````assert (Occ.occ v (elts a1) l1 u2 = Occ.occ v (elts a1) l1 u1 + Occ.occ v (elts a1) u1 u2)%Z. `````` Jean-Christophe Filliâtre committed Feb 24, 2014 130 `````` apply Occ.occ_append. omega. `````` Jean-Christophe Filliâtre committed Feb 25, 2014 131 ``````assert (Occ.occ v (elts a2) l2 u2 = Occ.occ v (elts a2) l2 l1 + Occ.occ v (elts a2) l1 u2)%Z. `````` Jean-Christophe Filliâtre committed Feb 24, 2014 132 `````` apply Occ.occ_append. omega. `````` Jean-Christophe Filliâtre committed Feb 25, 2014 133 ``````assert (Occ.occ v (elts a2) l1 u2 = Occ.occ v (elts a2) l1 u1 + Occ.occ v (elts a2) u1 u2)%Z. `````` Jean-Christophe Filliâtre committed Feb 24, 2014 134 `````` apply Occ.occ_append. omega. `````` Jean-Christophe Filliâtre committed Feb 25, 2014 135 136 137 138 139 140 ``````assert (Occ.occ v (elts a1) l2 l1 = Occ.occ v (elts a2) l2 l1). apply Occ.occ_eq. intros; apply eql; omega. assert (Occ.occ v (elts a1) u1 u2 = Occ.occ v (elts a2) u1 u2). apply Occ.occ_eq. intros; apply eqr; omega. generalize (h1c v); omega. (* u1 < l1 *) `````` Jean-Christophe Filliâtre committed Feb 24, 2014 141 ``````apply Occ.occ_eq. `````` Jean-Christophe Filliâtre committed Feb 25, 2014 142 143 144 145 146 147 ``````intros i hi. assert (c: (i < l1 \/ u1 <= i)%Z) by omega. destruct c. apply eql; omega. apply eqr; omega. (* eq right *) intros; apply eqr; omega. `````` Jean-Christophe Filliâtre committed Feb 24, 2014 148 149 ``````Qed. ``````