MapPermut.v 1.96 KB
Newer Older
1 2 3 4 5 6 7 8
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
9
(*                                                                  *)
10 11
(********************************************************************)

12 13 14 15 16 17
(* 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.
18
Require map.Occ.
19

20
(* Why3 assumption *)
21 22 23
Definition permut {a:Type} {a_WT:WhyType a} (m1:(map.Map.map Z a))
  (m2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (v:a), ((map.Occ.occ v
  m1 l u) = (map.Occ.occ v m2 l u)).
24

25
(* Why3 goal *)
26
Lemma permut_trans : forall {a:Type} {a_WT:WhyType a},
27 28 29
  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 a1 a2 l u) -> ((permut a2 a3 l u) ->
  (permut a1 a3 l u)).
30 31 32
intros a a_WT a1 a2 a3 l u h1 h2.
unfold permut in *.
intros. transitivity (Occ.occ v a2 l u); auto.
33 34 35 36
Qed.

(* Why3 goal *)
Lemma permut_exists : forall {a:Type} {a_WT:WhyType a},
37 38 39
  forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) (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))).
40
Proof.
41
intros a a_WT a1 a2 l u i h1 Hi.
42 43 44 45 46 47 48
pose (v := Map.get a2 i).
assert (0 < map.Occ.occ v a2 l u)%Z.
  apply map.Occ.occ_pos. assumption.
rewrite <- h1 in H.
generalize (map.Occ.occ_exists v a1 l u H).
intros (j, (hj1,hj2)).
exists j; intuition. 
49 50
Qed.