Fix some Coq realizations.

lib/coq/map/MapInjection.v

@@ -13,6 +13,7 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
+Require HighOrd.
 Require int.Int.
 Require map.Map.
 Require map.Occ.
@@ -39,6 +40,7 @@ Theorem injective_implies_surjective:
   into n f ->
   injection n f ->
   surjection n f.
+Proof.
 induction n.
 (* case n = 0 *)
 unfold surjection; intros.
@@ -162,6 +164,7 @@ Theorem lifting:
     (forall x:Z, 0 <= x < n -> 0 <= f x < n) ->
     exists g:nat -> nat,
       forall i:nat, Z_of_nat i < n -> Z_of_nat (g i) = f (Z_of_nat i).
+Proof.
 intros n f Hpos.
 exists (fun n => Zabs_nat (f (Z_of_nat n))).
 intros i Hi_inf_n.
@@ -176,6 +179,7 @@ Theorem Zinjective_implies_surjective:
   (forall i:Z, 0 <= i < n -> 0 <= f i < n) ->
   (forall i j:Z, 0 <= i < n -> 0 <= j < n -> f i = f j -> i = j) ->
   forall i:Z, 0 <= i < n -> exists k:Z, 0 <= k < n /\ f k = i.
+Proof.
 intros n f Hinto.
 elim (lifting n f Hinto).
 intros g Heq_g_f Hinj i Hi_inf_n.
@@ -216,23 +220,23 @@ Qed.
 
 
 (* Why3 assumption *)
-Definition injective (a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z) (j:Z),
+Definition injective (a:(Z -> Z)) (n:Z): Prop := forall (i:Z) (j:Z),
   ((0%Z <= i)%Z /\ (i < n)%Z) -> (((0%Z <= j)%Z /\ (j < n)%Z) ->
-  ((~ (i = j)) -> ~ ((map.Map.get a i) = (map.Map.get a j)))).
+  ((~ (i = j)) -> ~ ((a i) = (a j)))).
 
 (* Why3 assumption *)
-Definition surjective (a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z),
+Definition surjective (a:(Z -> Z)) (n:Z): Prop := forall (i:Z),
   ((0%Z <= i)%Z /\ (i < n)%Z) -> exists j:Z, ((0%Z <= j)%Z /\ (j < n)%Z) /\
-  ((map.Map.get a j) = i).
+  ((a j) = i).
 
 (* Why3 assumption *)
-Definition range (a:(map.Map.map Z Z)) (n:Z): Prop := forall (i:Z),
-  ((0%Z <= i)%Z /\ (i < n)%Z) -> ((0%Z <= (map.Map.get a i))%Z /\
-  ((map.Map.get a i) < n)%Z).
+Definition range (a:(Z -> Z)) (n:Z): Prop := forall (i:Z), ((0%Z <= i)%Z /\
+  (i < n)%Z) -> ((0%Z <= (a i))%Z /\ ((a i) < n)%Z).
 
 (* Why3 goal *)
-Lemma injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a
-  n) -> ((range a n) -> (surjective a n)).
+Lemma injective_surjective : forall (a:(Z -> Z)) (n:Z), (injective a n) ->
+  ((range a n) -> (surjective a n)).
+Proof.
 unfold injective, range, surjective.
 intros a n h1 h2.
 intros.
@@ -247,8 +251,9 @@ Qed.
 Import Occ.
 
 (* Why3 goal *)
-Lemma injection_occ : forall (m:(map.Map.map Z Z)) (n:Z), (injective m n) <->
+Lemma injection_occ : forall (m:(Z -> Z)) (n:Z), (injective m n) <->
   forall (v:Z), ((map.Occ.occ v m 0%Z n) <= 1%Z)%Z.
+Proof.
 intros m n; split.
 (* -> *)
 intros inj v.
@@ -277,7 +282,7 @@ elim (inj i j); omega.
 
 (* <- *)
 intros Hocc i j hi hj neq eq.
-pose (v := (Map.get m i)).
+pose (v := m i).
 assert (occ v m 0 n >= 2)%Z.
 assert (occ v m 0 n = occ v m 0 i + occ v m i n)%Z.
   apply occ_append; omega.

lib/coq/map/MapPermut.v

@@ -13,33 +13,33 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
+Require HighOrd.
 Require int.Int.
 Require map.Map.
 Require map.Occ.
 
 (* Why3 assumption *)
-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)).
+Definition permut {a:Type} {a_WT:WhyType a} (m1:(Z -> a)) (m2:(Z -> a)) (l:Z)
+  (u:Z): Prop := forall (v:a), ((map.Occ.occ v m1 l u) = (map.Occ.occ v m2 l
+  u)).
 
 (* Why3 goal *)
-Lemma permut_trans : forall {a:Type} {a_WT:WhyType a},
-  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)).
+Lemma permut_trans : forall {a:Type} {a_WT:WhyType a}, forall (a1:(Z -> a))
+  (a2:(Z -> a)) (a3:(Z -> a)), forall (l:Z) (u:Z), (permut a1 a2 l u) ->
+  ((permut a2 a3 l u) -> (permut a1 a3 l u)).
+Proof.
 intros a a_WT a1 a2 a3 l u h1 h2.
 unfold permut in *.
 intros. transitivity (Occ.occ v a2 l u); auto.
 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)) (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))).
+Lemma permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(Z -> a))
+  (a2:(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) /\ ((a1 j) = (a2 i))).
 Proof.
 intros a a_WT a1 a2 l u i h1 Hi.
-pose (v := Map.get a2 i).
+pose (v := a2 i).
 assert (0 < map.Occ.occ v a2 l u)%Z.
   apply map.Occ.occ_pos. assumption.
 rewrite <- h1 in H.

lib/coq/map/Occ.v

@@ -13,24 +13,25 @@
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
+Require HighOrd.
 Require int.Int.
 Require map.Map.
 
 (* Why3 goal *)
-Definition occ: forall {a:Type} {a_WT:WhyType a}, a -> (map.Map.map Z a) ->
-  Z -> Z -> Z.
+Definition occ: forall {a:Type} {a_WT:WhyType a}, a -> (Z -> a) -> Z -> Z ->
+  Z.
 Proof.
 intros a a_WT v m l u.
 induction (Z.to_nat (u-l)) as [|delta occ_].
 exact Z0.
-exact ((if why_decidable_eq (map.Map.get m (l + Z_of_nat delta)%Z) v then 1 else 0) + occ_)%Z.
+exact ((if why_decidable_eq (m (l + Z_of_nat delta)%Z) v then 1 else 0) + occ_)%Z.
 Defined.
 
 Lemma occ_equation :
   forall {a:Type} {a_WT:WhyType a} v m l u,
   (l < u)%Z ->
   occ v m l u =
-  ((if why_decidable_eq (map.Map.get m (u - 1)%Z) v then 1 else 0) + occ v m l (u - 1))%Z.
+  ((if why_decidable_eq (m (u - 1)%Z) v then 1 else 0) + occ v m l (u - 1))%Z.
 Proof.
 intros a a_WT v m l u Hlu.
 assert (0 < u - l)%Z as h1' by omega.
@@ -50,9 +51,38 @@ simpl.
 now rewrite <- minus_n_O, Nat2Z.id.
 Qed.
 
+Require Import Zwf.
+
+Lemma occ_equation' :
+  forall {a:Type} {a_WT:WhyType a} v m l u,
+  (l < u)%Z ->
+  occ v m l u =
+  ((if why_decidable_eq (m l) v then 1 else 0) + occ v m (l + 1) u)%Z.
+Proof.
+intros a a_WT v m l u Hlu.
+induction u using (well_founded_induction (Zwf_well_founded l)).
+destruct (Z_lt_le_dec (l + 1) u) as [Hlu'|Hlu'].
+rewrite Zplus_comm.
+rewrite occ_equation with (1 := Hlu).
+rewrite occ_equation with (1 := Hlu').
+rewrite <- Zplus_assoc.
+apply f_equal.
+rewrite Zplus_comm.
+apply H.
+clear -Hlu' ; unfold Zwf ; omega.
+clear -Hlu' ; omega.
+replace u with (l + 1)%Z.
+unfold occ.
+rewrite Z.add_simpl_l.
+rewrite <- Zminus_diag_reverse.
+simpl.
+now rewrite (Zplus_0_r l).
+clear -Hlu Hlu' ; omega.
+Qed.
+
 (* Why3 goal *)
-Lemma occ_empty : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
-  (m:(map.Map.map Z a)) (l:Z) (u:Z), (u <= l)%Z -> ((occ v m l u) = 0%Z).
+Lemma occ_empty : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m:(Z -> a))
+  (l:Z) (u:Z), (u <= l)%Z -> ((occ v m l u) = 0%Z).
 Proof.
 intros a a_WT v m l u h1.
 assert (u - l <= 0)%Z as h1' by omega.
@@ -63,8 +93,8 @@ Qed.
 
 (* Why3 goal *)
 Lemma occ_right_no_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
-  (m:(map.Map.map Z a)) (l:Z) (u:Z), (l < u)%Z -> ((~ ((map.Map.get m
-  (u - 1%Z)%Z) = v)) -> ((occ v m l u) = (occ v m l (u - 1%Z)%Z))).
+  (m:(Z -> a)) (l:Z) (u:Z), (l < u)%Z -> ((~ ((m (u - 1%Z)%Z) = v)) ->
+  ((occ v m l u) = (occ v m l (u - 1%Z)%Z))).
 Proof.
 intros a a_WT v m l u h1 h2.
 rewrite occ_equation with (1 := h1).
@@ -72,9 +102,9 @@ now destruct why_decidable_eq as [H|H].
 Qed.
 
 (* Why3 goal *)
-Lemma occ_right_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
-  (m:(map.Map.map Z a)) (l:Z) (u:Z), (l < u)%Z -> (((map.Map.get m
-  (u - 1%Z)%Z) = v) -> ((occ v m l u) = (1%Z + (occ v m l (u - 1%Z)%Z))%Z)).
+Lemma occ_right_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m:(Z ->
+  a)) (l:Z) (u:Z), (l < u)%Z -> (((m (u - 1%Z)%Z) = v) -> ((occ v m l
+  u) = (1%Z + (occ v m l (u - 1%Z)%Z))%Z)).
 Proof.
 intros a a_WT v m l u h1 h2.
 rewrite occ_equation with (1 := h1).
@@ -82,9 +112,29 @@ now destruct why_decidable_eq as [H|H].
 Qed.
 
 (* Why3 goal *)
-Lemma occ_bounds : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
-  (m:(map.Map.map Z a)) (l:Z) (u:Z), (l <= u)%Z -> ((0%Z <= (occ v m l
-  u))%Z /\ ((occ v m l u) <= (u - l)%Z)%Z).
+Lemma occ_left_no_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
+  (m:(Z -> a)) (l:Z) (u:Z), (l < u)%Z -> ((~ ((m l) = v)) -> ((occ v m l
+  u) = (occ v m (l + 1%Z)%Z u))).
+Proof.
+intros a a_WT v m l u h1 h2.
+rewrite occ_equation' with (1 := h1).
+now destruct why_decidable_eq as [H|H].
+Qed.
+
+(* Why3 goal *)
+Lemma occ_left_add : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m:(Z ->
+  a)) (l:Z) (u:Z), (l < u)%Z -> (((m l) = v) -> ((occ v m l
+  u) = (1%Z + (occ v m (l + 1%Z)%Z u))%Z)).
+Proof.
+intros a a_WT v m l u h1 h2.
+rewrite occ_equation' with (1 := h1).
+now destruct why_decidable_eq as [H|H].
+Qed.
+
+(* Why3 goal *)
+Lemma occ_bounds : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m:(Z ->
+  a)) (l:Z) (u:Z), (l <= u)%Z -> ((0%Z <= (occ v m l u))%Z /\ ((occ v m l
+  u) <= (u - l)%Z)%Z).
 Proof.
 intros a a_WT v m l u h1.
 cut (0 <= u - l)%Z. 2: omega.
@@ -93,7 +143,7 @@ pattern (u - l)%Z; apply Z_lt_induction. 2: omega.
 intros.
 assert (h: (x = 0 \/ x <> 0)%Z) by omega. destruct h.
 now rewrite occ_empty; omega.
-destruct (why_decidable_eq (Map.get m (l + (x-1))%Z) v).
+destruct (why_decidable_eq (m (l + (x-1))%Z) v).
 rewrite occ_right_add.
 generalize (H (x-1)%Z); clear H; intros.
 assert (0 <= occ v m l (l + (x - 1)) <= x-1)%Z.
@@ -115,9 +165,9 @@ replace (l + (u-l))%Z with u by ring. trivial.
 Qed.
 
 (* Why3 goal *)
-Lemma occ_append : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
-  (m:(map.Map.map Z a)) (l:Z) (mid:Z) (u:Z), ((l <= mid)%Z /\
-  (mid <= u)%Z) -> ((occ v m l u) = ((occ v m l mid) + (occ v m mid u))%Z).
+Lemma occ_append : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m:(Z ->
+  a)) (l:Z) (mid:Z) (u:Z), ((l <= mid)%Z /\ (mid <= u)%Z) -> ((occ v m l
+  u) = ((occ v m l mid) + (occ v m mid u))%Z).
 Proof.
 intros a a_WT v m l mid u (h1,h2).
 cut (0 <= u - mid)%Z. 2: omega.
@@ -129,7 +179,7 @@ assert (h: (x = 0 \/ x <> 0)%Z) by omega. destruct h.
 rewrite (occ_empty _ _ mid (mid+x)%Z).
 subst x. ring_simplify ((mid+0)%Z). ring.
 omega.
-destruct (why_decidable_eq (Map.get m (mid + (x-1))%Z) v).
+destruct (why_decidable_eq (m (mid + (x-1))%Z) v).
 rewrite (occ_right_add _ _ l (mid+x))%Z.
 rewrite (occ_right_add _ _ mid (mid+x))%Z.
 generalize (H (x-1)%Z); clear H; intros.
@@ -159,9 +209,9 @@ replace (mid + (u-mid))%Z with u by ring. trivial.
 Qed.
 
 (* Why3 goal *)
-Lemma occ_neq : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
-  (m:(map.Map.map Z a)) (l:Z) (u:Z), (forall (i:Z), ((l <= i)%Z /\
-  (i < u)%Z) -> ~ ((map.Map.get m i) = v)) -> ((occ v m l u) = 0%Z).
+Lemma occ_neq : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m:(Z -> a))
+  (l:Z) (u:Z), (forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ~ ((m i) = v)) ->
+  ((occ v m l u) = 0%Z).
 Proof.
 intros a a_WT v m l u.
 assert (h: (u < l \/ 0 <= u - l)%Z) by omega. destruct h.
@@ -172,8 +222,8 @@ pattern (u - l)%Z; apply Z_lt_induction. 2: omega.
 clear H; intros.
 assert (h: (x = 0 \/ x <> 0)%Z) by omega. destruct h.
 now rewrite occ_empty; omega.
-destruct (why_decidable_eq (Map.get m (l + (x-1))%Z) v).
-assert (Map.get m (l + (x - 1)) <> v)%Z.
+destruct (why_decidable_eq (m (l + (x-1))%Z) v).
+assert (m (l + (x - 1)) <> v)%Z.
   apply H1; omega.
 intuition.
 rewrite occ_right_no_add.
@@ -186,9 +236,9 @@ trivial.
 Qed.
 
 (* Why3 goal *)
-Lemma occ_exists : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
-  (m:(map.Map.map Z a)) (l:Z) (u:Z), (0%Z < (occ v m l u))%Z -> exists i:Z,
-  ((l <= i)%Z /\ (i < u)%Z) /\ ((map.Map.get m i) = v).
+Lemma occ_exists : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m:(Z ->
+  a)) (l:Z) (u:Z), (0%Z < (occ v m l u))%Z -> exists i:Z, ((l <= i)%Z /\
+  (i < u)%Z) /\ ((m i) = v).
 Proof.
 intros a a_WT v m l u h1.
 assert (h: (u < l \/ 0 <= u - l)%Z) by omega. destruct h.
@@ -200,7 +250,7 @@ pattern (u - l)%Z; apply Z_lt_induction. 2: omega.
 clear H; intros.
 assert (h: (x = 0 \/ x <> 0)%Z) by omega. destruct h.
 rewrite occ_empty in h0. elimtype False; omega. omega.
-destruct (why_decidable_eq (Map.get m (l + (x-1))%Z) v).
+destruct (why_decidable_eq (m (l + (x-1))%Z) v).
 exists (l+(x-1))%Z. split. omega. now trivial.
 destruct (H (x-1))%Z as (i,(hi1,hi2)). omega. omega.
 rewrite occ_right_no_add in h0.
@@ -211,12 +261,11 @@ exists i. split. omega. assumption.
 Qed.
 
 (* Why3 goal *)
-Lemma occ_pos : forall {a:Type} {a_WT:WhyType a}, forall (m:(map.Map.map Z
-  a)) (l:Z) (u:Z) (i:Z), ((l <= i)%Z /\ (i < u)%Z) ->
-  (0%Z < (occ (map.Map.get m i) m l u))%Z.
+Lemma occ_pos : forall {a:Type} {a_WT:WhyType a}, forall (m:(Z -> a)) (l:Z)
+  (u:Z) (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> (0%Z < (occ (m i) m l u))%Z.
 Proof.
 intros a a_WT m l u i (h1,h2).
-pose (v := (Map.get m i)). fold v.
+pose (v := m i). fold v.
 assert (occ v m l u = occ v m l i + occ v m i u)%Z.
   apply occ_append. omega.
 assert (occ v m i u = occ v m i (i+1) + occ v m (i+1) u)%Z.
@@ -232,10 +281,9 @@ omega.
 Qed.
 
 (* Why3 goal *)
-Lemma occ_eq : forall {a:Type} {a_WT:WhyType a}, forall (v:a)
-  (m1:(map.Map.map Z a)) (m2:(map.Map.map Z a)) (l:Z) (u:Z), (forall (i:Z),
-  ((l <= i)%Z /\ (i < u)%Z) -> ((map.Map.get m1 i) = (map.Map.get m2 i))) ->
-  ((occ v m1 l u) = (occ v m2 l u)).
+Lemma occ_eq : forall {a:Type} {a_WT:WhyType a}, forall (v:a) (m1:(Z -> a))
+  (m2:(Z -> a)) (l:Z) (u:Z), (forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> ((m1
+  i) = (m2 i))) -> ((occ v m1 l u) = (occ v m2 l u)).
 Proof.
 intros a a_WT v m1 m2 l u h1.
 assert (h: (u < l \/ 0 <= u - l)%Z) by omega. destruct h.
@@ -249,7 +297,7 @@ pattern (u - l)%Z; apply Z_lt_induction. 2: omega.
 clear H; intros.
 assert (h: (x = 0 \/ x <> 0)%Z) by omega. destruct h.
 rewrite occ_empty. rewrite occ_empty. trivial. omega. omega.
-destruct (why_decidable_eq (Map.get m1 (l + (x-1))%Z) v).
+destruct (why_decidable_eq (m1 (l + (x-1))%Z) v).
 rewrite occ_right_add.
 rewrite (occ_right_add v m2).
 apply f_equal.