Realize map.MapPermut in Coq.

Makefile.in

@@ -815,7 +815,7 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
 COQLIBS_SET_FILES = Set
 COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
 
-COQLIBS_MAP_FILES = Map
+COQLIBS_MAP_FILES = Map MapPermut
 COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
 
 ifeq (@enable_coq_fp_libs@,yes)

lib/coq/map/MapPermut.v

+(* 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 *)
+Definition exchange {a:Type} {a_WT:WhyType a}(a1:(map.Map.map Z a))
+  (a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1
+  i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\
+  forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1
+  k) = (map.Map.get a2 k))).
+
+(* Why3 goal *)
+Lemma exchange_set : forall {a:Type} {a_WT:WhyType a},
+  forall (a1:(map.Map.map Z a)), forall (i:Z) (j:Z), (exchange a1
+  (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i
+  j).
+Proof.
+intros a a_WT a1 i j.
+split.
+now rewrite Map.Select_eq.
+split.
+destruct (Z_eq_dec i j) as [H|H].
+rewrite H.
+now rewrite Map.Select_eq.
+rewrite Map.Select_neq by now apply sym_not_eq.
+now rewrite Map.Select_eq.
+intros k (Hk1,Hk2).
+now rewrite 2!Map.Select_neq by now apply sym_not_eq.
+Qed.
+
+(* Why3 assumption *)
+Inductive permut_sub{a:Type} {a_WT:WhyType a}  : (map.Map.map Z a)
+  -> (map.Map.map Z a) -> Z -> Z -> Prop :=
+  | permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z),
+      (permut_sub a1 a1 l u)
+  | permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)),
+      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)) (a2:(map.Map.map Z a))
+      (a3:(map.Map.map Z a)), 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)) (a2:(map.Map.map Z a)),
+      forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) ->
+      (((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1
+      a2 l u))).
+
+(* Why3 goal *)
+Lemma permut_weakening : forall {a:Type} {a_WT:WhyType a},
+  forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l1:Z) (r1:Z)
+  (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) ->
+  ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)).
+Proof.
+intros a a_WT a1 a2 l1 r1 l2 r2 ((h1,h2),h3) h4.
+induction h4.
+constructor.
+constructor.
+now apply IHh4.
+constructor 3 with a2.
+now apply IHh4_1.
+now apply IHh4_2.
+constructor 4 with (3 := H1).
+omega.
+omega.
+Qed.
+
+(* Why3 goal *)
+Lemma permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z
+  a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) ->
+  forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2
+  i) = (map.Map.get a1 i)).
+Proof.
+intros a a_WT a1 a2 l u h1 i h2.
+induction h1.
+apply eq_refl.
+now apply sym_eq, IHh1.
+etransitivity.
+now apply IHh1_2.
+now apply IHh1_1.
+apply sym_eq.
+apply H1.
+omega.
+Qed.
+
+(* Why3 goal *)
+Lemma permut_exists : forall {a:Type} {a_WT:WhyType a},
+  forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z),
+  (permut_sub 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)).
+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)).
+2: easy.
+revert i Hi.
+induction h1.
+intros i Hi.
+now split ; exists i ; split.
+intros i Hi.
+destruct (IHh1 i Hi) as ((j&H1&H2),(k&H3&H4)).
+split.
+now exists k ; split.
+now exists j ; split.
+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).
+intros k Hk.
+destruct (Z_eq_dec k i) as [Hki|Hki].
+split ;
+  exists j ;
+  split ; try easy ;
+  rewrite Hki ;
+  apply H1.
+destruct (Z_eq_dec k j) as [Hkj|Hkj].
+split ;
+  exists i ;
+  split ; try easy ;
+  rewrite Hkj ;
+  apply sym_eq, H1.
+split ;
+  exists k ;
+  split ; try easy.
+now apply sym_eq, H1 ; split.
+now apply H1 ; split.
+Qed.
+
+