vstte10_inverting_InvertingAnInjection_VC_inverting2_1.v 2.21 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1
(* This file is generated by Why3's Coq driver *)
2
(* Beware! Only edit allowed sections below    *)
3 4
Require Import BuiltIn.
Require BuiltIn.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
5
Require HighOrd.
6 7
Require int.Int.
Require map.Map.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
8
Require map.Occ.
9
Require map.MapInjection.
10

Guillaume Melquiond's avatar
Guillaume Melquiond committed
11 12 13
Axiom array : forall (a:Type), Type.
Parameter array_WhyType : forall (a:Type) {a_WT:WhyType a},
  WhyType (array a).
14 15
Existing Instance array_WhyType.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
16
Parameter elts: forall {a:Type} {a_WT:WhyType a}, (array a) -> (Z -> a).
17

Guillaume Melquiond's avatar
Guillaume Melquiond committed
18
Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> Z.
19

Guillaume Melquiond's avatar
Guillaume Melquiond committed
20 21
Axiom array'invariant : forall {a:Type} {a_WT:WhyType a}, forall (self:(array
  a)), (0%Z <= (length self))%Z.
22

23
(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
24 25
Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
  ((elts a1) i).
26

Guillaume Melquiond's avatar
Guillaume Melquiond committed
27 28 29 30 31 32 33
Parameter mixfix_lblsmnrb: forall {a:Type} {a_WT:WhyType a}, (array a) ->
  Z -> a -> (array a).

Axiom mixfix_lblsmnrb_spec : forall {a:Type} {a_WT:WhyType a},
  forall (a1:(array a)) (i:Z) (v:a), ((length (mixfix_lblsmnrb a1 i
  v)) = (length a1)) /\ ((elts (mixfix_lblsmnrb a1 i
  v)) = (map.Map.set (elts a1) i v)).
34

35
(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
36 37
Definition injective (a:(array Z)) (n:Z): Prop := (map.MapInjection.injective
  (elts a) n).
38

39
(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
40
Definition surjective (a:(array Z)) (n:Z): Prop :=
41
  (map.MapInjection.surjective (elts a) n).
42

43
(* Why3 assumption *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
44
Definition range (a:(array Z)) (n:Z): Prop := (map.MapInjection.range
45
  (elts a) n).
46

47
(* Why3 goal *)
48 49 50 51
Theorem VC_inverting2 : forall (a:(array Z)) (n:Z), ((n = (length a)) /\
  ((injective a n) /\ (range a n))) -> forall (b:(array Z)), ((forall (i:Z),
  ((0%Z <= i)%Z /\ (i < n)%Z) -> ((mixfix_lbrb b i) = 0%Z)) /\
  ((length b) = n)) -> let o := (n - 1%Z)%Z in ((0%Z <= (o + 1%Z)%Z)%Z ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
52 53 54 55
  forall (b1:(array Z)), ((length b1) = (length b)) -> ((forall (j:Z),
  ((0%Z <= j)%Z /\ (j < (o + 1%Z)%Z)%Z) -> ((mixfix_lbrb b1 (mixfix_lbrb a
  j)) = j)) -> (injective b1 n))).
Proof.
56
intros a n (h1,(h2,h3)) b (h4,h5) o h6 b1 h7 h8.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
57 58
assert (MapInjection.surjective (elts a) n).
now apply MapInjection.injective_surjective.
59 60 61 62 63 64 65 66 67
intros i j H0 H1.
destruct (H i H0) as (i1, (Hi1, <-)).
destruct (H j H1) as (j1, (Hj1, <-)).
unfold o, mixfix_lbrb in h8.
rewrite h8 by omega.
rewrite h8 by omega.
intros H2.
contradict H2.
now rewrite H2.
68
Qed.
69