Commit 4e44421f authored by MARCHE Claude's avatar MARCHE Claude

updated sessions

parent a869eaa9
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require map.Map.
Require map.MapInjection.
(* Why3 assumption *)
Definition unit := unit.
......@@ -11,77 +12,64 @@ Definition unit := unit.
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> 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]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): 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 :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (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)).
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) :=
(mk_array n (map.Map.const v:(map.Map.map Z a))).
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))).
(* Why3 assumption *)
Definition injective (a:(map.Map.map 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)))).
Definition injective (a:(@array Z _)) (n:Z): Prop :=
(map.MapInjection.injective (elts a) n).
(* Why3 assumption *)
Definition surjective (a:(map.Map.map 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).
Definition surjective (a:(@array Z _)) (n:Z): Prop :=
(map.MapInjection.surjective (elts a) n).
(* 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).
Axiom injective_surjective : forall (a:(map.Map.map Z Z)) (n:Z), (injective a
n) -> ((range a n) -> (surjective a n)).
(* Why3 assumption *)
Definition injective1 (a:(array Z)) (n:Z): Prop := (injective (elts a) n).
(* Why3 assumption *)
Definition surjective1 (a:(array Z)) (n:Z): Prop := (surjective (elts a) n).
(* Why3 assumption *)
Definition range1 (a:(array Z)) (n:Z): Prop := (range (elts a) n).
Definition range (a:(@array Z _)) (n:Z): Prop := (map.MapInjection.range
(elts a) n).
(* Why3 goal *)
Theorem WP_parameter_inverting2 : forall (a:Z) (n:Z), forall (a1:(map.Map.map
Z Z)), ((0%Z <= a)%Z /\ ((n = a) /\ ((injective a1 n) /\ (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 -> (injective b n))))).
(* Why3 intros a n a1 (h1,(h2,(h3,h4))) h5 h6 o h7 b h8 h9. *)
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.
assert (surjective a1 n).
apply injective_surjective; assumption.
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)).
rewrite <- Hi2.
......@@ -94,4 +82,3 @@ subst.
auto.
Qed.
......@@ -191,8 +191,8 @@
name="expl:VC for inverting"/>
<proof
prover="2"
timelimit="10"
memlimit="0"
timelimit="5"
memlimit="4000"
edited="vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting_1.v"
obsolete="false"
archived="false">
......@@ -409,7 +409,7 @@
edited="vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting2_2.v"
obsolete="false"
archived="false">
<result status="valid" time="1.06"/>
<result status="valid" time="1.02"/>
</proof>
</goal>
<goal
......
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