MapPermut.v 3.77 KB
Newer Older
1 2 3 4 5 6 7 8
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.

(* Why3 assumption *)
9 10 11
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)).
12

13 14 15 16 17 18 19 20 21
(* 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))))))).

22
(* Why3 assumption *)
23
Inductive permut {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) ->
24
  (@map.Map.map Z _ a a_WT) -> Z -> Z -> Prop :=
25
  | permut_refl : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _
26 27
      a a_WT)), forall (l:Z) (u:Z), (map_eq_sub a1 a2 l u) -> ((@permut _ _)
      a1 a2 l u)
MARCHE Claude's avatar
MARCHE Claude committed
28 29
  | 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),
30 31
      ((@permut _ _) a1 a2 l u) -> (((@permut _ _) a2 a3 l u) ->
      ((@permut _ _) a1 a3 l u))
MARCHE Claude's avatar
MARCHE Claude committed
32
  | permut_exchange : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map
33 34
      Z _ a a_WT)), forall (l:Z) (u:Z) (i:Z) (j:Z), (exchange a1 a2 l u i
      j) -> ((@permut _ _) a1 a2 l u).
35 36

(* Why3 goal *)
37 38 39
Lemma 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
40
  (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l
41
  u i j)).
42
intros a a_WT a1 l u i j (h1,h2) (h3,h4).
43 44
unfold exchange.
intuition.
45
rewrite Map.Select_eq; auto.
46 47 48
assert (H: i = j \/ i <> j) by omega.
destruct H.
rewrite H; rewrite Map.Select_eq; auto.
49 50 51 52
rewrite Map.Select_neq; auto.
rewrite Map.Select_eq; auto.
rewrite Map.Select_neq; auto.
rewrite Map.Select_neq; auto.
53 54 55 56
Qed.

(* Why3 goal *)
Lemma permut_exists : forall {a:Type} {a_WT:WhyType a},
57 58 59 60
  forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (l:Z)
  (u:Z) (i:Z), (permut a1 a2 l u) -> (((l <= i)%Z /\ (i < u)%Z) ->
  exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a1
  j) = (map.Map.get a2 i))).
61
Proof.
62 63 64
intros a a_WT a1 a2 l u i h1 Hi.
assert ((exists j, (l <= j < u)%Z /\ Map.get a1 j = Map.get a2 i) /\
  (exists j, (l <= j < u)%Z /\ Map.get a2 j = Map.get a1 i)).
65 66 67
2: easy.
revert i Hi.
induction h1.
68
(* refl *)
69
intros i Hi.
70 71 72
red in H.
split ; exists i ; intuition.
  rewrite <- H; auto.
73
(* trans *)
74 75 76 77 78 79 80 81 82 83 84 85
intros i Hi.
split.
destruct (IHh1_2 i Hi) as ((j&H1&H2),_).
destruct (IHh1_1 j H1) as ((k&H3&H4),_).
exists k.
split ; try easy.
now transitivity (Map.get a2 j).
destruct (IHh1_1 i Hi) as (_,(j&H1&H2)).
destruct (IHh1_2 j H1) as (_,(k&H3&H4)).
exists k.
split ; try easy.
now transitivity (Map.get a2 j).
86
(* exchange *)
87 88 89
revert H.
unfold exchange.
intros [Hi [Hj [Ha1ia2j [Ha1ja2i H]]]] k Hk.
90 91 92 93 94
destruct (Z_eq_dec k i) as [Hki|Hki].
split ;
  exists j ;
  split ; try easy ;
  rewrite Hki ;
95
  intuition.
96 97 98 99 100
destruct (Z_eq_dec k j) as [Hkj|Hkj].
split ;
  exists i ;
  split ; try easy ;
  rewrite Hkj ;
101
  apply sym_eq; intuition.
102 103 104
split ;
  exists k ;
  split ; try easy.
105 106
now apply H ; intuition.
now apply sym_eq, H ; intuition.
107 108
Qed.

109 110 111 112 113 114 115 116
(* Unused content named permut_sym
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.
117
Qed.
118
*)