Commit 97c8be21 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Port examples/vstte10_inverting.

parent fc6117c4
(* 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) :=
| 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]].
(* Why3 assumption *)
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)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
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)) (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).
(* Why3 assumption *)
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
(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 -> 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.
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.
subst o.
rewrite h10; try omega.
rewrite h10; try omega.
red; intro h.
subst i1.
omega.
Qed.
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require HighOrd.
Require int.Int.
Require map.Map.
Require map.Occ.
Require map.MapInjection.
Axiom array : forall (a:Type), Type.
Parameter array_WhyType : forall (a:Type) {a_WT:WhyType a},
WhyType (array a).
Existing Instance array_WhyType.
Parameter elts: forall {a:Type} {a_WT:WhyType a}, (array a) -> (Z -> a).
Parameter length: forall {a:Type} {a_WT:WhyType a}, (array a) -> Z.
Axiom array'invariant : forall {a:Type} {a_WT:WhyType a}, forall (self:(array
a)), (0%Z <= (length self))%Z.
(* Why3 assumption *)
Definition mixfix_lbrb {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
((elts a1) i).
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)).
(* Why3 assumption *)
Definition injective (a:(array Z)) (n:Z): Prop := (map.MapInjection.injective
(elts a) n).
(* Why3 assumption *)
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
(elts a) n).
(* Why3 goal *)
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 ->
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.
intros a n (h1,(h2,h3)) b (h4,h5) o h6 b1 h7 h8.
assert (MapInjection.surjective (elts a) n).
now apply MapInjection.injective_surjective.
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.
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment