Commit a869eaa9 by MARCHE Claude

### Fixed Coq proofs using realized MapInjection

parent cf996aca
 ... ... @@ -4,6 +4,7 @@ Require Import BuiltIn. Require BuiltIn. Require int.Int. Require map.Map. Require map.MapInjection. (* Why3 assumption *) Definition unit := unit. ... ... @@ -99,24 +100,6 @@ Axiom value_def : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@sparse_array Definition length1 {a:Type} {a_WT:WhyType a} (a1:(@sparse_array a a_WT)): Z := (length (values a1)). (* 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)))). (* 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). (* 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)). Require Import Why3. Ltac ae := why3 "alt-ergo". ... ... @@ -138,9 +121,9 @@ unfold is_elt, length1, get; simpl. intro H; decompose [and] H; clear H. subst n1 n2. intros. subst a_card. assert (inj: injective a_back n0) by ae. assert (rng: range a_back n0) by ae. generalize (injective_surjective a_back n0 inj rng); intro surj. assert (inj: MapInjection.injective a_back n0) by ae. assert (rng: MapInjection.range a_back n0) by ae. generalize (MapInjection.injective_surjective a_back n0 inj rng); intro surj. destruct (surj i H1) as (j, (hj1, hj2)). ae. Qed. ... ...
 ... ... @@ -106,7 +106,7 @@ edited="vacid_0_sparse_array_2_SparseArray_permutation_1.v" obsolete="false" archived="false"> shape="index in array boundsainfix <V8V0Aainfix <=c0V8Iainfix <V8V0Aainfix <=c0V8Aainfix <=c0V4Aainfix <=c0V2Aainfix <=c0V0Aainfix =agetV3agetV5V11V11Aainfix <agetV5V11V0Aainfix <=c0agetV5V11Iainfix <V11V6Aainfix <=c0V11FAainfix =V2V4Aainfix =V0V2Aainfix <=V0amaxlenAainfix <=V6V0Aainfix <=c0V6Lamk sparse_arrayamk arrayV0V1amk arrayV2V3amk arrayV4V5V6V7F">
 (* 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,75 +12,63 @@ 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_inverting : forall (a:Z) (b:Z) (n:Z), forall (a1:(map.Map.map Z Z)), (((0%Z <= a)%Z /\ (0%Z <= b)%Z) /\ (((n = a) /\ (a = b)) /\ ((injective a1 n) /\ (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 -> (injective b1 n))). 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. *) 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. ... ... @@ -92,4 +81,3 @@ subst. auto. Qed.
 ... ... @@ -82,11 +82,11 @@ name="WP_parameter inverting.3" locfile="../vstte10_inverting.mlw" loclnum="21" loccnumb="6" loccnume="15" expl="3. precondition" expl="3. index in array bounds" sum="d7f793ddd8deade51d85fc67451ffcfa" proved="true" expanded="true" shape="preconditionainfix <V7V0Aainfix <=c0V7Iainfix =agetV6agetV1V8V8Iainfix <V8V7Aainfix <=c0V8FIainfix <=V7V5Aainfix <=c0V7FFIainfix <=c0V5Lainfix -V4c1IarangeV1V4AainjectiveV1V4Aainfix =V0V2Aainfix =V4V0Aainfix <=c0V2Aainfix <=c0V0F"> shape="index in array boundsainfix <V7V0Aainfix <=c0V7Iainfix =agetV6agetV1V8V8Iainfix <V8V7Aainfix <=c0V8FIainfix <=V7V5Aainfix <=c0V7FFIainfix <=c0V5Lainfix -V4c1IarangeV1V4AainjectiveV1V4Aainfix =V0V2Aainfix =V4V0Aainfix <=c0V2Aainfix <=c0V0F">
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!