Commit 9706083b authored by MARCHE Claude's avatar MARCHE Claude

more proofs updated

parent 211eb279
......@@ -5,14 +5,14 @@
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="2" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="3" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../formula.why">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
<file name="../formula.why" expanded="true">
<theory name="Formula" sum="d41d8cd98f00b204e9800998ecf8427e">
<theory name="PropositionalCalculus" sum="8e90228c74fc9a58ce016c323f7a8bff" expanded="true">
<theory name="PropositionalCalculus" sum="006c6d79ffb672881234e4a2aa8e3016" expanded="true">
<goal name="Test1" expanded="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.19"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="46"/></proof>
<proof prover="3"><result status="valid" time="0.05" steps="48"/></proof>
......@@ -186,7 +186,7 @@ function subst_expr (e:expr) (x:ident) (t:expr) : expr =
lemma eval_subst_expr:
forall s:state, e:expr, x:ident, t:expr.
forall s:state, e "induction":expr, x:ident, t:expr.
eval_expr s (subst_expr e x t) =
eval_expr (IdMap.set s x (eval_expr s t)) e
......@@ -4,67 +4,66 @@
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="5" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../imp_n.why" expanded="true">
<theory name="Imp" sum="c5b2f605219b1db882298415fdd56cc4" expanded="true">
<theory name="Imp" sum="5dd0f4706664ed444265b03d0a9e3322" expanded="true">
<goal name="ident_eq_dec">
<proof prover="6"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
<goal name="check_skip">
<proof prover="6"><result status="valid" time="0.00" steps="1"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="2"/></proof>
<goal name="Test13">
<proof prover="6"><result status="valid" time="0.02" steps="4"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
<goal name="Test42">
<proof prover="6"><result status="valid" time="0.02" steps="2"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
<goal name="Test55">
<proof prover="6"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="4"><result status="valid" time="0.00" steps="17"/></proof>
<goal name="Ass42">
<proof prover="6"><result status="valid" time="0.09" steps="90"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="128"/></proof>
<goal name="If42">
<proof prover="5" timelimit="5" memlimit="1000"><result status="valid" time="0.06"/></proof>
<proof prover="6" timelimit="5" memlimit="1000"><result status="valid" time="0.29" steps="489"/></proof>
<proof prover="7"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.13" steps="543"/></proof>
<goal name="progress">
<proof prover="0" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
<goal name="steps_non_neg">
<proof prover="0" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="0" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.50"/></proof>
<goal name="many_steps_seq">
<proof prover="0" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
<goal name="eval_subst_expr">
<proof prover="0" edited="imp_n_Imp_eval_subst_expr_1.v"><result status="valid" time="0.34"/></proof>
<transf name="induction_ty_lex">
<goal name="eval_subst_expr.1" expl="1.">
<proof prover="4"><result status="valid" time="0.02" steps="113"/></proof>
<goal name="eval_subst">
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.35"/></proof>
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.51"/></proof>
<goal name="skip_rule">
<proof prover="6"><result status="valid" time="0.04" steps="113"/></proof>
<proof prover="4"><result status="valid" time="0.04" steps="148"/></proof>
<goal name="assign_rule">
<proof prover="0" edited="imp_n_Imp_assign_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="4"><result status="valid" time="1.39" steps="1910"/></proof>
<goal name="seq_rule">
<proof prover="0" edited="imp_n_Imp_seq_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="4"><result status="valid" time="3.09" steps="7135"/></proof>
<goal name="if_rule">
<proof prover="0" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
<goal name="while_rule">
<proof prover="0" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="0" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.57"/></proof>
<goal name="consequence_rule">
<proof prover="1"><result status="valid" time="0.05"/></proof>
<proof prover="5"><result status="timeout" time="2.98"/></proof>
This diff is collapsed.
(* 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.
(* Why3 assumption *)
Definition unit := unit.
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)).
Axiom sparse_array : forall (a:Type), Type.
Parameter sparse_array_WhyType : forall (a:Type) {a_WT:WhyType a},
WhyType (sparse_array a).
Existing Instance sparse_array_WhyType.
Parameter values: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) ->
(array a).
Parameter index: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> (array
Parameter back: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> (array
Parameter card: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z.
Parameter def: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> a.
Axiom sparse_array'invariant : forall {a:Type} {a_WT:WhyType a},
forall (self:(sparse_array a)), ((0%Z <= (card self))%Z /\
(((card self) <= (length (values self)))%Z /\
((length (values self)) <= 1000%Z)%Z)) /\
((((length (values self)) = (length (index self))) /\
((length (index self)) = (length (back self)))) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < (card self))%Z) -> (((0%Z <= (mixfix_lbrb (back self)
i))%Z /\ ((mixfix_lbrb (back self) i) < (length (values self)))%Z) /\
((mixfix_lbrb (index self) (mixfix_lbrb (back self) i)) = i))).
(* Why3 assumption *)
Definition is_elt {a:Type} {a_WT:WhyType a} (a1:(sparse_array a))
(i:Z): Prop := ((0%Z <= (mixfix_lbrb (index a1) i))%Z /\
((mixfix_lbrb (index a1) i) < (card a1))%Z) /\ ((mixfix_lbrb (back a1)
(mixfix_lbrb (index a1) i)) = i).
Parameter value: forall {a:Type} {a_WT:WhyType a}, (sparse_array a) -> Z ->
Axiom value_def : forall {a:Type} {a_WT:WhyType a}, forall (a1:(sparse_array
a)) (i:Z), ((is_elt a1 i) -> ((value a1 i) = (mixfix_lbrb (values a1)
i))) /\ ((~ (is_elt a1 i)) -> ((value a1 i) = (def a1))).
(* Why3 assumption *)
Definition length1 {a:Type} {a_WT:WhyType a} (a1:(sparse_array a)): Z :=
(length (values a1)).
Require Import Why3.
Ltac ae := why3 "Alt-Ergo,0.99.1," timelimit 5; admit.
(* Why3 goal *)
Theorem permutation : forall {a:Type} {a_WT:WhyType a},
forall (a1:(sparse_array a)), (((0%Z <= (card a1))%Z /\
(((card a1) <= (length (values a1)))%Z /\
((length (values a1)) <= 1000%Z)%Z)) /\
((((length (values a1)) = (length (index a1))) /\
((length (index a1)) = (length (back a1)))) /\ forall (i:Z),
((0%Z <= i)%Z /\ (i < (card a1))%Z) -> (((0%Z <= (mixfix_lbrb (back a1)
i))%Z /\ ((mixfix_lbrb (back a1) i) < (length (values a1)))%Z) /\
((mixfix_lbrb (index a1) (mixfix_lbrb (back a1) i)) = i)))) ->
(((card a1) = (length1 a1)) -> forall (i:Z), ((0%Z <= i)%Z /\
(i < (length1 a1))%Z) -> (is_elt a1 i)).
(* Why3 intros a a_WT a1 ((h1,(h2,h3)),((h4,h5),h6)) h7 i (h8,h9). *)
intros a _a a1.
destruct a1 as ((n0, a_values), (n1, a_index), (n2, a_back), a_card, a_def); simpl.
unfold is_elt, length1, get; simpl.
intro H; decompose [and] H; clear H.
subst n1 n2.
intros. subst a_card.
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)).
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment