vstte10_inverting: fixed renaming of a Coq proof

examples/vstte10_inverting/vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting2_2.v → examples/vstte10_inverting/vstte10_inverting_InvertingAnInjection_WP_parameter_inverting2_1.v

-(* This file is generated by Why3's Coq 8.4 driver *)
+(* This file is generated by Why3's Coq driver *)
 (* Beware! Only edit allowed sections below    *)
 Require Import BuiltIn.
 Require BuiltIn.
 Require int.Int.
 Require map.Map.
+Require map.Occ.
 Require map.MapInjection.
 
 (* Why3 assumption *)
 Definition unit := unit.
 
+Axiom qtmark : Type.
+Parameter qtmark_WhyType : WhyType qtmark.
+Existing Instance qtmark_WhyType.
+
 (* Why3 assumption *)
-Inductive array
-  (a:Type) {a_WT:WhyType a} :=
-  | mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
+Inductive array (a:Type) :=
+  | mk_array : Z -> (map.Map.map Z a) -> array a.
 Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
 Existing Instance array_WhyType.
-Implicit Arguments mk_array [[a] [a_WT]].
+Implicit Arguments mk_array [[a]].
 
 (* Why3 assumption *)
-Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
-  Z _ a a_WT) := match v with
+Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
+  match v with
   | (mk_array x x1) => x1
   end.
 
 (* Why3 assumption *)
-Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
+Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
   match v with
   | (mk_array x x1) => x
   end.
 
 (* Why3 assumption *)
-Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
+Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
   (map.Map.get (elts a1) i).
 
 (* Why3 assumption *)
-Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
-  (v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
-  v)).
-
-(* Why3 assumption *)
-Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
-  (mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
+Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
+  a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
 
 (* Why3 assumption *)
-Definition injective (a:(@array Z _)) (n:Z): Prop :=
-  (map.MapInjection.injective (elts a) n).
+Definition injective (a:(array Z)) (n:Z): Prop := (map.MapInjection.injective
+  (elts a) n).
 
 (* Why3 assumption *)
-Definition surjective (a:(@array Z _)) (n:Z): Prop :=
+Definition surjective (a:(array Z)) (n:Z): Prop :=
   (map.MapInjection.surjective (elts a) n).
 
 (* Why3 assumption *)
-Definition range (a:(@array Z _)) (n:Z): Prop := (map.MapInjection.range
+Definition range (a:(array Z)) (n:Z): Prop := (map.MapInjection.range
   (elts a) n).
 
 (* Why3 goal *)
-Theorem WP_parameter_inverting2 : forall (a:Z) (a1:(@map.Map.map Z _ Z _))
-  (n:Z), ((0%Z <= a)%Z /\ ((n = a) /\ ((map.MapInjection.injective a1 n) /\
-  (map.MapInjection.range a1 n)))) -> ((0%Z <= n)%Z -> ((0%Z <= n)%Z ->
-  let o := (n - 1%Z)%Z in ((0%Z <= o)%Z -> forall (b:(@map.Map.map Z _ Z _)),
-  (forall (j:Z), ((0%Z <= j)%Z /\ (j < (o + 1%Z)%Z)%Z) -> ((map.Map.get b
-  (map.Map.get a1 j)) = j)) -> ((0%Z <= n)%Z -> (map.MapInjection.injective b
-  n))))).
-(* Why3 intros a a1 n (h1,(h2,(h3,h4))) h5 h6 o h7 b h8 h9. *)
-(* YOU MAY EDIT THE PROOF BELOW *)
-intuition.
-intuition.
-red; intros.
-unfold get; simpl.
+Theorem WP_parameter_inverting2 : forall (a:Z) (a1:(map.Map.map Z Z)) (n:Z),
+  ((0%Z <= a)%Z /\ ((n = a) /\ ((map.MapInjection.injective a1 n) /\
+  (map.MapInjection.range a1 n)))) -> ((0%Z <= n)%Z -> forall (b:Z)
+  (b1:(map.Map.map Z Z)), ((0%Z <= b)%Z /\ ((b = n) /\ forall (i:Z),
+  ((0%Z <= i)%Z /\ (i < n)%Z) -> ((map.Map.get b1 i) = 0%Z))) -> let o :=
+  (n - 1%Z)%Z in ((0%Z <= o)%Z -> forall (b2:(map.Map.map Z Z)),
+  (forall (j:Z), ((0%Z <= j)%Z /\ (j < (o + 1%Z)%Z)%Z) -> ((map.Map.get b2
+  (map.Map.get a1 j)) = j)) -> ((0%Z <= b)%Z -> (map.MapInjection.injective
+  b2 n)))).
+intros a a1 n (h1,(h2,(h3,h4))) h5 b b1 (h6,(h7,h8)) o h9 b2 h10 h11.
 assert (MapInjection.surjective a1 n).
 apply MapInjection.injective_surjective; assumption.
-generalize (H11 i H8); unfold get; simpl; intros (i1, (Hi1,Hi2)).
-generalize (H11 j H9); unfold get; simpl; intros (j1, (Hj1,Hj2)).
+red; intros.
+generalize (H i H0); unfold get; simpl; intros (i1, (Hi1,Hi2)).
+generalize (H j H1); unfold get; simpl; intros (j1, (Hj1,Hj2)).
 rewrite <- Hi2.
 rewrite <- Hj2.
-rewrite H6; try omega.
-rewrite H6; try omega.
-intro.
-apply H10.
-subst.
-auto.
+subst o.
+rewrite h10; try omega.
+rewrite h10; try omega.
+red; intro h.
+subst i1.
+omega.
 Qed.