MapPermut.v 3.77 KB
 Guillaume Melquiond committed Dec 04, 2012 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 *) `````` Jean-Christophe Filliâtre committed Feb 05, 2014 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)). `````` Guillaume Melquiond committed Dec 04, 2012 12 `````` `````` Andrei Paskevich committed Feb 12, 2014 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))))))). `````` Guillaume Melquiond committed Dec 04, 2012 22 ``````(* Why3 assumption *) `````` 23 ``````Inductive permut {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) -> `````` Guillaume Melquiond committed Dec 10, 2013 24 `````` (@map.Map.map Z _ a a_WT) -> Z -> Z -> Prop := `````` Jean-Christophe Filliâtre committed Feb 05, 2014 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 committed Jul 11, 2013 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 committed Jul 11, 2013 32 `````` | permut_exchange : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map `````` Andrei Paskevich committed Feb 12, 2014 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). `````` Jean-Christophe Filliâtre committed Feb 06, 2014 35 36 `````` (* Why3 goal *) `````` Andrei Paskevich committed Feb 12, 2014 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 `````` Jean-Christophe Filliâtre committed Feb 05, 2014 40 `````` (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l `````` Andrei Paskevich committed Feb 12, 2014 41 `````` u i j)). `````` Jean-Christophe Filliâtre committed Feb 05, 2014 42 ``````intros a a_WT a1 l u i j (h1,h2) (h3,h4). `````` Andrei Paskevich committed Feb 12, 2014 43 44 ``````unfold exchange. intuition. `````` Jean-Christophe Filliâtre committed Feb 05, 2014 45 ``````rewrite Map.Select_eq; auto. `````` Andrei Paskevich committed Feb 12, 2014 46 47 48 ``````assert (H: i = j \/ i <> j) by omega. destruct H. rewrite H; rewrite Map.Select_eq; auto. `````` Jean-Christophe Filliâtre committed Feb 05, 2014 49 50 51 52 ``````rewrite Map.Select_neq; auto. rewrite Map.Select_eq; auto. rewrite Map.Select_neq; auto. rewrite Map.Select_neq; auto. `````` Guillaume Melquiond committed Dec 04, 2012 53 54 55 56 ``````Qed. (* Why3 goal *) Lemma permut_exists : forall {a:Type} {a_WT:WhyType a}, `````` Andrei Paskevich committed Feb 12, 2014 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))). `````` Guillaume Melquiond committed Dec 04, 2012 61 ``````Proof. `````` Andrei Paskevich committed Feb 12, 2014 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)). `````` Guillaume Melquiond committed Dec 04, 2012 65 66 67 ``````2: easy. revert i Hi. induction h1. `````` Jean-Christophe Filliâtre committed Feb 06, 2014 68 ``````(* refl *) `````` Guillaume Melquiond committed Dec 04, 2012 69 ``````intros i Hi. `````` Jean-Christophe Filliâtre committed Feb 05, 2014 70 71 72 ``````red in H. split ; exists i ; intuition. rewrite <- H; auto. `````` Jean-Christophe Filliâtre committed Feb 06, 2014 73 ``````(* trans *) `````` Guillaume Melquiond committed Dec 04, 2012 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). `````` Jean-Christophe Filliâtre committed Feb 06, 2014 86 ``````(* exchange *) `````` Andrei Paskevich committed Feb 12, 2014 87 88 89 ``````revert H. unfold exchange. intros [Hi [Hj [Ha1ia2j [Ha1ja2i H]]]] k Hk. `````` Guillaume Melquiond committed Dec 04, 2012 90 91 92 93 94 ``````destruct (Z_eq_dec k i) as [Hki|Hki]. split ; exists j ; split ; try easy ; rewrite Hki ; `````` Jean-Christophe Filliâtre committed Feb 05, 2014 95 `````` intuition. `````` Guillaume Melquiond committed Dec 04, 2012 96 97 98 99 100 ``````destruct (Z_eq_dec k j) as [Hkj|Hkj]. split ; exists i ; split ; try easy ; rewrite Hkj ; `````` Jean-Christophe Filliâtre committed Feb 05, 2014 101 `````` apply sym_eq; intuition. `````` Guillaume Melquiond committed Dec 04, 2012 102 103 104 ``````split ; exists k ; split ; try easy. `````` Andrei Paskevich committed Feb 12, 2014 105 106 ``````now apply H ; intuition. now apply sym_eq, H ; intuition. `````` Guillaume Melquiond committed Dec 04, 2012 107 108 ``````Qed. `````` Andrei Paskevich committed Feb 12, 2014 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. `````` Jean-Christophe Filliâtre committed Feb 06, 2014 117 ``````Qed. `````` Andrei Paskevich committed Feb 12, 2014 118 ``*)``