From 86c3b64cac0a5ae8e6eb410f1d258dae93abcf23 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Wed, 12 Feb 2014 20:43:37 +0100 Subject: [PATCH] update Coq realization for Map.Permut --- lib/coq/map/MapPermut.v | 89 +++++++++++++++++++---------------------- 1 file changed, 41 insertions(+), 48 deletions(-) diff --git a/lib/coq/map/MapPermut.v b/lib/coq/map/MapPermut.v index 72f09d514..306073b59 100644 --- a/lib/coq/map/MapPermut.v +++ b/lib/coq/map/MapPermut.v @@ -10,6 +10,15 @@ 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 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))))))). + (* Why3 assumption *) Inductive permut {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) -> (@map.Map.map Z _ a a_WT) -> Z -> Z -> Prop := @@ -21,60 +30,38 @@ Inductive permut {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) -> ((@permut _ _) a1 a2 l u) -> (((@permut _ _) a2 a3 l u) -> ((@permut _ _) 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) -> ((~ (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 _ _) a1 a2 l u)))))). + 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). (* 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 a1 - a2 l u) -> (permut 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}, - forall (a1:(@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) -> (permut a1 +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 (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l - u)). + u i j)). intros a a_WT a1 l u i j (h1,h2) (h3,h4). -assert (h: i=j \/ i<>j) by omega. destruct h. -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. +unfold exchange. +intuition. rewrite Map.Select_eq; auto. +assert (H: i = j \/ i <> j) by omega. +destruct H. +rewrite H; rewrite Map.Select_eq; auto. rewrite Map.Select_neq; auto. rewrite Map.Select_eq; auto. -intros. rewrite Map.Select_neq; auto. rewrite Map.Select_neq; auto. Qed. (* Why3 goal *) Lemma permut_exists : 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 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)). + 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))). Proof. -intros a a_WT a1 a2 l u h1 i Hi. -assert ((exists j, (l <= j < u)%Z /\ Map.get a2 i = Map.get a1 j) /\ - (exists j, (l <= j < u)%Z /\ Map.get a1 i = Map.get a2 j)). +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)). 2: easy. revert i Hi. induction h1. @@ -97,7 +84,9 @@ exists k. split ; try easy. now transitivity (Map.get a2 j). (* exchange *) -intros k Hk. +revert H. +unfold exchange. +intros [Hi [Hj [Ha1ia2j [Ha1ja2i H]]]] k Hk. destruct (Z_eq_dec k i) as [Hki|Hki]. split ; exists j ; @@ -113,13 +102,17 @@ split ; split ; exists k ; split ; try easy. -now apply sym_eq, H4 ; intuition. -now apply H4 ; intuition. +now apply H ; intuition. +now apply sym_eq, H ; intuition. Qed. -(* Unused content named permut_sub_concat -intros a a_WT a1 a2 l m u h1 h2. -induction h1. - +(* 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. Qed. - *) +*) -- GitLab