From 85edfb97e05e690aae41685977ce7e1e65bf068d Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Wed, 8 Jul 2015 09:05:10 +0200 Subject: [PATCH] vstte10_inverting: fixed renaming of a Coq proof --- ...ingAnInjection_WP_parameter_inverting2_1.v | 81 ++++++++++++++++++ ...ingAnInjection_WP_parameter_inverting2_2.v | 84 ------------------- 2 files changed, 81 insertions(+), 84 deletions(-) create mode 100644 examples/vstte10_inverting/vstte10_inverting_InvertingAnInjection_WP_parameter_inverting2_1.v delete mode 100644 examples/vstte10_inverting/vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting2_2.v diff --git a/examples/vstte10_inverting/vstte10_inverting_InvertingAnInjection_WP_parameter_inverting2_1.v b/examples/vstte10_inverting/vstte10_inverting_InvertingAnInjection_WP_parameter_inverting2_1.v new file mode 100644 index 000000000..92563b6c5 --- /dev/null +++ b/examples/vstte10_inverting/vstte10_inverting_InvertingAnInjection_WP_parameter_inverting2_1.v @@ -0,0 +1,81 @@ +(* 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. + diff --git a/examples/vstte10_inverting/vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting2_2.v b/examples/vstte10_inverting/vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting2_2.v deleted file mode 100644 index e42bcd1a3..000000000 --- a/examples/vstte10_inverting/vstte10_inverting_WP_InvertingAnInjection_WP_parameter_inverting2_2.v +++ /dev/null @@ -1,84 +0,0 @@ -(* 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. - -(* Why3 assumption *) -Inductive array - (a:Type) {a_WT:WhyType 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 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 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 a_WT)) (i:Z): a := - (map.Map.get (elts a1) i). - -(* Why3 assumption *) -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 a_WT) := - (mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))). - -(* 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 -> ((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 (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. -rewrite <- Hj2. -rewrite H6; try omega. -rewrite H6; try omega. -intro. -apply H10. -subst. -auto. -Qed. - -- GitLab