simplifications and lemmas in theories MapPermut/ArrayPermut

parent e79e9a4f
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -88,11 +88,9 @@ Definition map_permut_sub {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT))
(* 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 := ((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) 0%Z l) /\
((map.MapPermut.permut_sub (elts a1) (elts a2) l u) /\ (map_eq_sub
(elts a2) (elts a2) u (length a1)))))).
(a2:(@array a a_WT)) (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2)
0%Z l) /\ ((map_permut_sub a1 a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u
(length a1))).
(* Why3 assumption *)
Definition permut {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (a2:(@array
......@@ -338,11 +336,9 @@ intuition.
red; simpl.
split. trivial.
apply permut_trans with a5.
apply permut_exchange with i1 j1; try omega.
red in H48; intuition.
red in H48; intuition.
red in H48; intuition.
red in H19; simpl in H19.
intuition.
assert (permut (mk_array a a8) (mk_array a a5)).
apply exchange_permut with i1 j1; auto.
destruct H54; intuition.
red in H19; intuition.
Qed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
......@@ -16,20 +16,30 @@ Inductive permut_sub {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) ->
| permut_refl : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _
a a_WT)), forall (l:Z) (u:Z), (map_eq_sub a1 a2 l u) ->
((@permut_sub _ _) a1 a2 l u)
| permut_sym : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _
a a_WT)), 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 a_WT)) (a2:(@map.Map.map
Z _ a a_WT)) (a3:(@map.Map.map Z _ a a_WT)), 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 a_WT)) (a2:(@map.Map.map
Z _ a a_WT)), forall (l:Z) (u:Z) (i:Z) (j:Z), ((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))))) ->
((@permut_sub _ _) a1 a2 l u))))).
(i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> ((~ (i = j)) ->
(((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))))) -> ((@permut_sub _ _) a1 a2 l u)))))).
(* Why3 goal *)
Lemma permut_sym : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@map.Map.map
Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z),
(permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u).
intros a a_WT a1 a2 l u h1.
induction h1; intuition.
apply permut_refl; unfold map_eq_sub in *; intuition.
rewrite <- H; auto.
apply permut_trans with a2; auto.
apply permut_exchange with j i; auto.
intros; rewrite <- H4; auto.
Qed.
(* Why3 goal *)
Lemma permut_exchange_set : forall {a:Type} {a_WT:WhyType a},
......@@ -38,13 +48,15 @@ Lemma permut_exchange_set : forall {a:Type} {a_WT:WhyType a},
(map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l
u)).
intros a a_WT a1 l u i j (h1,h2) (h3,h4).
apply permut_exchange with i j; auto.
assert (h: i=j \/ i<>j) by omega. destruct h.
subst.
rewrite Map.Select_eq; auto.
rewrite Map.Select_eq; auto.
assert (h: i=j \/ i<>j) by omega. destruct h.
subst.
subst. apply permut_refl.
red; intros.
assert (h: i=j \/ i<>j) by omega. destruct h.
subst. rewrite Map.Select_eq; auto.
rewrite Map.Select_neq.
rewrite Map.Select_neq; auto.
auto.
apply permut_exchange with i j; auto.
rewrite Map.Select_eq; auto.
rewrite Map.Select_neq; auto.
rewrite Map.Select_eq; auto.
......@@ -66,15 +78,12 @@ assert ((exists j, (l <= j < u)%Z /\ Map.get a2 i = Map.get a1 j) /\
2: easy.
revert i Hi.
induction h1.
(* refl *)
intros i Hi.
red in H.
split ; exists i ; intuition.
rewrite <- H; auto.
intros i Hi.
destruct (IHh1 i Hi) as ((j&H1&H2),(k&H3&H4)).
split.
now exists k ; split.
now exists j ; split.
(* trans *)
intros i Hi.
split.
destruct (IHh1_2 i Hi) as ((j&H1&H2),_).
......@@ -87,6 +96,7 @@ destruct (IHh1_2 j H1) as (_,(k&H3&H4)).
exists k.
split ; try easy.
now transitivity (Map.get a2 j).
(* exchange *)
intros k Hk.
destruct (Z_eq_dec k i) as [Hki|Hki].
split ;
......@@ -103,7 +113,13 @@ split ;
split ;
exists k ;
split ; try easy.
now apply sym_eq, H3 ; intuition.
now apply H3 ; intuition.
now apply sym_eq, H4 ; intuition.
now apply H4 ; intuition.
Qed.
(* Unused content named permut_sub_concat
intros a a_WT a1 a2 l m u h1 h2.
induction h1.
Qed.
*)
......@@ -167,10 +167,9 @@ module ArrayPermut
Values outside of the interval (l..u-1) are ignored. *)
predicate permut_sub (a1 a2: array 'a) (l u: int) =
a1.length = a2.length /\ 0 <= l <= a1.length /\ 0 <= u <= a1.length /\
map_eq_sub a1.elts a2.elts 0 l /\
M.permut_sub a1.elts a2.elts l u /\
map_eq_sub a2.elts a2.elts u (length a1)
map_permut_sub a1 a2 l u /\
map_eq_sub a1.elts a2.elts u (length a1)
(** [permut_sub a1 a2 l u] is true when the segment
[a1(l..u-1)] is a permutation of the segment [a2(l..u-1)]
and values outside of the interval (l..u-1) are equal. *)
......@@ -222,10 +221,8 @@ module ArraySwap
ensures { exchange (old a) a i j }
=
let v = a[i] in
begin
a[i] <- a[j];
a[j] <- v
end
a[i] <- a[j];
a[j] <- v
end
......
......@@ -103,15 +103,12 @@ theory MapPermut
| permut_refl : (* a1[l..u[ and a2[l..u[ are identical *)
forall a1 a2 : map int 'a. forall l u : int.
map_eq_sub a1 a2 l u -> permut_sub a1 a2 l u
| permut_sym : (* symmetry *)
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a1 l u
| permut_trans : (* transitivity *)
forall a1 a2 a3 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a3 l u -> permut_sub a1 a3 l u
| permut_exchange : (* elements at indices i and j have been swapped *)
forall a1 a2 : map int 'a. forall l u i j : int.
l <= i < u -> l <= j < u ->
l <= i < u -> l <= j < u -> i <> j ->
a1[i] = a2[j] -> a1[j] = a2[i] ->
(forall k:int. l <= k < u -> k <> i -> k <> j -> a1[k] = a2[k]) ->
permut_sub a1 a2 l u
......@@ -122,6 +119,11 @@ theory MapPermut
It is defined inductively as the smallest equivalence relation
that contains the exchanges *)
(* symmetry can be proved *)
lemma permut_sym:
forall a1 a2 : map int 'a. forall l u : int.
permut_sub a1 a2 l u -> permut_sub a2 a1 l u
lemma permut_exchange_set :
forall a: map int 'a. forall l u i j: int.
l <= i < u -> l <= j < u -> permut_sub a a[i <- a[j]][j <- a[i]] l u
......@@ -132,6 +134,12 @@ theory MapPermut
forall i: int. l <= i < u ->
exists j: int. l <= j < u /\ a2[i] = a1[j]
(*
lemma permut_sub_concat:
forall a1 a2: map int 'a, l m u: int.
permut_sub a1 a2 l m -> permut_sub a1 a2 m u -> permut_sub a1 a2 l u
*)
end
(** {2 Sum of elements of a map (indexed by integers)} *)
......
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