vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting_1.v 2.53 KB
Newer Older
1
(* This file is generated by Why3's Coq 8.4 driver *)
2
(* Beware! Only edit allowed sections below    *)
3 4 5 6
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
7
Require map.MapInjection.
8

9
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
Definition unit := unit.
11

12
(* Why3 assumption *)
Andrei Paskevich's avatar
Andrei Paskevich committed
13 14
Inductive array
  (a:Type) {a_WT:WhyType a} :=
15
  | mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
16 17 18 19 20
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].

(* Why3 assumption *)
21 22
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
  Z _ a a_WT) := match v with
23
  | (mk_array x x1) => x1
24 25
  end.

26
(* Why3 assumption *)
27
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
28 29
  match v with
  | (mk_array x x1) => x
30 31
  end.

32
(* Why3 assumption *)
33
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
34
  (map.Map.get (elts a1) i).
35

36
(* Why3 assumption *)
37 38 39
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)).
40 41

(* Why3 assumption *)
42 43
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))).
44

45
(* Why3 assumption *)
46 47
Definition injective (a:(@array Z _)) (n:Z): Prop :=
  (map.MapInjection.injective (elts a) n).
48

49
(* Why3 assumption *)
50 51
Definition surjective (a:(@array Z _)) (n:Z): Prop :=
  (map.MapInjection.surjective (elts a) n).
52

53
(* Why3 assumption *)
54 55
Definition range (a:(@array Z _)) (n:Z): Prop := (map.MapInjection.range
  (elts a) n).
56

57
(* Why3 goal *)
58 59 60 61 62 63 64 65
Theorem WP_parameter_inverting : forall (a:Z) (a1:(@map.Map.map Z _ Z _))
  (b:Z) (n:Z), (((0%Z <= a)%Z /\ (0%Z <= b)%Z) /\ (((n = a) /\ (a = b)) /\
  ((map.MapInjection.injective a1 n) /\ (map.MapInjection.range a1 n)))) ->
  let o := (n - 1%Z)%Z in ((0%Z <= o)%Z -> forall (b1:(@map.Map.map Z _
  Z _)), (forall (j:Z), ((0%Z <= j)%Z /\ (j < (o + 1%Z)%Z)%Z) ->
  ((map.Map.get b1 (map.Map.get a1 j)) = j)) -> ((0%Z <= b)%Z ->
  (map.MapInjection.injective b1 n))).
(* Why3 intros a a1 b n ((h1,h2),((h3,h4),(h5,h6))) o h7 b1 h8 h9. *)
66 67 68
intuition.
intuition.
red; intros.
69
unfold get; simpl.
70 71
assert (MapInjection.surjective a1 n).
apply MapInjection.injective_surjective; assumption.
Andrei Paskevich's avatar
Andrei Paskevich committed
72 73
generalize (H11 i H8); unfold get; simpl; intros (i1, (Hi1,Hi2)).
generalize (H11 j H9); unfold get; simpl; intros (j1, (Hj1,Hj2)).
74 75
rewrite <- Hi2.
rewrite <- Hj2.
Andrei Paskevich's avatar
Andrei Paskevich committed
76 77
rewrite H6; try omega.
rewrite H6; try omega.
78
intro.
Andrei Paskevich's avatar
Andrei Paskevich committed
79
apply H10.
80 81 82 83
subst.
auto.
Qed.