Commit 00f2af66 authored by MARCHE Claude's avatar MARCHE Claude

update Coq proofs with explicit occurrences of idqt instead of id'

parent d16974d8
......@@ -9,7 +9,7 @@
<file
name="../12934.why"
verified="true"
expanded="false">
expanded="true">
<theory
name="BTS12934"
locfile="bts/12934/../12934.why"
......@@ -28,9 +28,10 @@
prover="0"
timelimit="10"
memlimit="0"
edited="12934_BTS12934_t_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.50"/>
<result status="valid" time="0.42"/>
</proof>
</goal>
</theory>
......
......@@ -2,21 +2,30 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require int.Int.
Parameter ident : Type.
Axiom ident_eq_dec : forall (i1:ident) (i2:ident), (i1 = i2) \/ ~ (i1 = i2).
Parameter mk_ident: Z -> ident.
Axiom mk_ident_inj : forall (i:Z) (j:Z), ((mk_ident i) = (mk_ident j)) ->
(i = j).
(* Why3 assumption *)
Inductive operator :=
| Oplus : operator
| Ominus : operator
| Omult : operator .
(* Why3 assumption *)
Inductive expr :=
| Econst : Z -> expr
| Evar : ident -> expr
| Ebin : expr -> operator -> expr -> expr .
(* Why3 assumption *)
Inductive stmt :=
| Sskip : stmt
| Sassign : ident -> expr -> stmt
......@@ -29,11 +38,9 @@ Axiom check_skip : forall (s:stmt), (s = Sskip) \/ ~ (s = Sskip).
Parameter map : forall (a:Type) (b:Type), Type.
Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b.
Implicit Arguments get.
Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b).
Implicit Arguments set.
Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)),
......@@ -44,17 +51,18 @@ Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a), ((get (const(
b1):(map a b)) a1) = b1).
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
Definition state := (map ident Z).
(* Why3 assumption *)
Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
match op with
| Oplus => (x + y)%Z
......@@ -62,6 +70,7 @@ Definition eval_bin(x:Z) (op:operator) (y:Z): Z :=
| Omult => (x * y)%Z
end.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
match e with
......@@ -71,13 +80,14 @@ Fixpoint eval_expr(s:(map ident Z)) (e:expr) {struct e}: Z :=
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| one_step_assign : forall (s:(map ident Z)) (x:ident) (e:expr),
(one_step s (Sassign x e) (set s x (eval_expr s e)) Sskip)
| one_step_seq : forall (s:(map ident Z)) (sqt:(map ident Z)) (i1:stmt)
(i1qt:stmt) (i2:stmt), (one_step s i1 sqt i1qt) -> (one_step s (Sseq i1
i2) sqt (Sseq i1qt i2))
| one_step_seq : forall (s:(map ident Z)) (s':(map ident Z)) (i1:stmt)
(i1':stmt) (i2:stmt), (one_step s i1 s' i1') -> (one_step s (Sseq i1
i2) s' (Sseq i1' i2))
| one_step_seq_skip : forall (s:(map ident Z)) (i:stmt), (one_step s
(Sseq Sskip i) s i)
| one_step_if_true : forall (s:(map ident Z)) (e:expr) (i1:stmt) (i2:stmt),
......@@ -91,8 +101,9 @@ Inductive one_step : (map ident Z) -> stmt -> (map ident Z)
((eval_expr s e) = 0%Z) -> (one_step s (Swhile e i) s Sskip).
Axiom progress : forall (s:(map ident Z)) (i:stmt), (~ (i = Sskip)) ->
exists sqt:(map ident Z), exists iqt:stmt, (one_step s i sqt iqt).
exists s':(map ident Z), exists i':stmt, (one_step s i s' i').
(* Why3 assumption *)
Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
-> stmt -> Prop :=
| many_steps_refl : forall (s:(map ident Z)) (i:stmt), (many_steps s i s i)
......@@ -100,10 +111,9 @@ Inductive many_steps : (map ident Z) -> stmt -> (map ident Z)
ident Z)) (i1:stmt) (i2:stmt) (i3:stmt), (one_step s1 i1 s2 i2) ->
((many_steps s2 i2 s3 i3) -> (many_steps s1 i1 s3 i3)).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Theorem many_steps_seq_rec : forall (s1:(map ident Z)) (s3:(map ident Z))
(i:stmt) (i3:stmt), (many_steps s1 i s3 i3) -> ((i3 = Sskip) ->
forall (i1:stmt) (i2:stmt), (i = (Sseq i1 i2)) -> exists s2:(map ident Z),
......@@ -121,7 +131,7 @@ intros H4 i5 i6 H56.
subst.
inversion Hstep; subst.
(* case 1: one_step_seq (no skip) *)
elim Hind with (i1:=i1qt) (i2:=i6); auto; clear Hind.
elim Hind with (i1:=i1') (i2:=i6); auto; clear Hind.
intros s6 (H1,H2).
exists s6.
split; auto.
......@@ -130,6 +140,5 @@ eapply many_steps_trans; eauto.
exists s4.
split; [constructor | auto].
Qed.
(* DO NOT EDIT BELOW *)
......@@ -33,7 +33,7 @@
<file
name="../imp.why"
verified="false"
expanded="false">
expanded="true">
<theory
name="Imp"
locfile="hoare_logic/imp/../imp.why"
......@@ -46,7 +46,7 @@
loclnum="8" loccnumb="6" loccnume="18"
sum="1d2fa1307a90cfa4436e58ca8c4baa8b"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0V1NOainfix =V0V1F">
<proof
prover="6"
......@@ -79,7 +79,7 @@
loclnum="32" loccnumb="6" loccnume="16"
sum="f37d9a038124492ded7dcc13c243bca4"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0aSskipNOainfix =V0aSskipF">
<proof
prover="1"
......@@ -104,7 +104,7 @@
loclnum="59" loccnumb="7" loccnume="13"
sum="79514e82972fcb9fb181a42bdd168a5d"
proved="true"
expanded="true"
expanded="false"
shape="Laconstc0ainfix =aeval_exprV0aEconstc13c13">
<proof
prover="4"
......@@ -153,7 +153,7 @@
loclnum="63" loccnumb="7" loccnume="13"
sum="2233d910dd871f7629fbd14fe21880a0"
proved="true"
expanded="true"
expanded="false"
shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEvarV0c42">
<proof
prover="4"
......@@ -202,7 +202,7 @@
loclnum="68" loccnumb="7" loccnume="13"
sum="81f3d89dbb17dd5616d61c746363e319"
proved="true"
expanded="true"
expanded="false"
shape="Lamk_identc0Lasetaconstc0V0c42ainfix =aeval_exprV1aEbinaEvarV0aOplusaEconstc13c55">
<proof
prover="1"
......@@ -227,7 +227,7 @@
loclnum="112" loccnumb="7" loccnume="12"
sum="d79dafb4b123bd6d405249e2aeae999f"
proved="true"
expanded="true"
expanded="false"
shape="Lamk_identc0Laconstc0ainfix =agetV2V0c42Iaone_stepV1aSassignV0aEconstc42V2aSskipF">
<proof
prover="1"
......@@ -252,7 +252,7 @@
loclnum="119" loccnumb="7" loccnume="11"
sum="2cf4b33a87e77dc3113cb2270027977a"
proved="true"
expanded="true"
expanded="false"
shape="Lamk_identc0Laconstc0ainfix =agetV3V0c42Iaone_stepV2V4V3aSskipIaone_stepV1aSifaEvarV0aSassignV0aEconstc13aSassignV0aEconstc42V2V4F">
<proof
prover="1"
......@@ -269,7 +269,7 @@
loclnum="131" loccnumb="8" loccnume="16"
sum="e135ae75103f2c596782b1e202f4ddb9"
proved="true"
expanded="true"
expanded="false"
shape="aone_stepV0V1V2V3EIainfix =V1aSskipNF">
<proof
prover="2"
......@@ -286,7 +286,7 @@
locfile="hoare_logic/imp/../imp.why"
loclnum="148" loccnumb="6" loccnume="24"
sum="aeea567425648bcdc8f7b73f26164f74"
proved="true"
proved="false"
expanded="true"
shape="amany_stepsV6V5V1aSskipAamany_stepsV0V4V6aSskipEIainfix =V2aSseqV4V5FIainfix =V3aSskipIamany_stepsV0V2V1V3F">
<proof
......@@ -294,9 +294,9 @@
timelimit="3"
memlimit="0"
edited="imp_Imp_many_steps_seq_rec_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.49"/>
obsolete="true"
archived="false"><undone/>
</proof>
</goal>
<goal
......@@ -305,7 +305,7 @@
loclnum="155" loccnumb="6" loccnume="20"
sum="2c0574f92883e7d75abeab91219a5f5b"
proved="true"
expanded="true"
expanded="false"
shape="amany_stepsV4V3V1aSskipAamany_stepsV0V2V4aSskipEIamany_stepsV0aSseqV2V3V1aSskipF">
<proof
prover="6"
......@@ -338,7 +338,7 @@
loclnum="185" loccnumb="6" loccnume="21"
sum="10a08076cbde9ff3d47f3756599d4269"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =aeval_exprV0asubst_exprV1V2V3aeval_exprasetV0V2aeval_exprV0V3V1F">
<proof
prover="2"
......@@ -356,7 +356,7 @@
loclnum="197" loccnumb="6" loccnume="16"
sum="9ed41003e65c3b0d6e018246af7e1910"
proved="true"
expanded="true"
expanded="false"
shape="aeval_fmlaasetV0V2aeval_exprV0V3V1qaeval_fmlaV0asubstV1V2V3F">
<proof
prover="2"
......@@ -374,7 +374,7 @@
loclnum="210" loccnumb="6" loccnume="15"
sum="86491dec98ad2def2cf841b1953670b7"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV0aSskipV0F">
<proof
prover="2"
......@@ -392,7 +392,7 @@
loclnum="213" loccnumb="6" loccnume="17"
sum="6aa1e2def89b26b124b052e7f456e1e6"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleasubstV0V1V2aSassignV1V2V0F">
<proof
prover="2"
......@@ -410,7 +410,7 @@
loclnum="217" loccnumb="6" loccnume="14"
sum="edb979d62451e4d773f12b17ae4d29e1"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV0aSseqV3V4V1Iavalid_tripleV2V4V1Aavalid_tripleV0V3V2F">
<proof
prover="6"
......@@ -436,7 +436,7 @@
loclnum="222" loccnumb="6" loccnume="13"
sum="a7f2179c110652afa53bf980838b7b3c"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV1aSifV0V3V4V2Iavalid_tripleaFandV1aFnotaFtermV0V4V2Aavalid_tripleaFandV1aFtermV0V3V2F">
<proof
prover="2"
......@@ -472,7 +472,7 @@
loclnum="246" loccnumb="6" loccnume="16"
sum="42400857028ab4b823953cc85e3146df"
proved="true"
expanded="true"
expanded="false"
shape="avalid_tripleV1aSwhileV0V2aFandaFnotaFtermV0V1Iavalid_tripleaFandaFtermV0V1V2V1F">
<proof
prover="6"
......
This diff is collapsed.
......@@ -74,12 +74,12 @@ Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1)
a2) = (get m a2)).
Parameter const: forall (b:Type) (a:Type), b -> (map a b).
Parameter const: forall (a:Type) (b:Type), b -> (map a b).
Set Contextual Implicit.
Implicit Arguments const.
Unset Contextual Implicit.
Axiom Const : forall (b:Type) (a:Type), forall (b1:b) (a1:a),
Axiom Const : forall (a:Type) (b:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
(* Why3 assumption *)
......@@ -183,7 +183,7 @@ Fixpoint subst(f:fmla) (x:Z) (v:Z) {struct f}: fmla :=
| (Fand f1 f2) => (Fand (subst f1 x v) (subst f2 x v))
| (Fnot f1) => (Fnot (subst f1 x v))
| (Fimplies f1 f2) => (Fimplies (subst f1 x v) (subst f2 x v))
| (Flet y t f1) => (Flet y t (subst f1 x v))
| (Flet y t f1) => (Flet y (subst_term t x v) (subst f1 x v))
| (Fforall y ty f1) => (Fforall y ty (subst f1 x v))
end.
Unset Implicit Arguments.
......@@ -219,9 +219,9 @@ Inductive one_step : (map Z value) -> (map Z value) -> stmt -> (map Z value)
(e:term), (one_step sigma pi (Sassign x e) (set sigma x
(eval_term sigma pi e)) pi Sskip)
| one_step_seq : forall (sigma:(map Z value)) (pi:(map Z value))
(sigmaqt:(map Z value)) (piqt:(map Z value)) (i1:stmt) (i1qt:stmt)
(i2:stmt), (one_step sigma pi i1 sigmaqt piqt i1qt) -> (one_step sigma
pi (Sseq i1 i2) sigmaqt piqt (Sseq i1qt i2))
(sigma':(map Z value)) (pi':(map Z value)) (i1:stmt) (i1':stmt)
(i2:stmt), (one_step sigma pi i1 sigma' pi' i1') -> (one_step sigma pi
(Sseq i1 i2) sigma' pi' (Sseq i1' i2))
| one_step_seq_skip : forall (sigma:(map Z value)) (pi:(map Z value))
(i:stmt), (one_step sigma pi (Sseq Sskip i) sigma pi i)
| one_step_if_true : forall (sigma:(map Z value)) (pi:(map Z value))
......@@ -272,41 +272,9 @@ Definition valid_fmla(p:fmla): Prop := forall (sigma:(map Z value)) (pi:(map
(* Why3 assumption *)
Definition valid_triple(p:fmla) (i:stmt) (q:fmla): Prop := forall (sigma:(map
Z value)) (pi:(map Z value)), (eval_fmla sigma pi p) ->
forall (sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z),
(many_steps sigma pi i sigmaqt piqt Sskip n) -> (eval_fmla sigmaqt piqt q).
Axiom skip_rule : forall (q:fmla), (valid_triple q Sskip q).
Axiom assign_rule : forall (q:fmla) (x:Z) (id:Z) (e:term), (fresh_in_fmla id
q) -> (valid_triple (Flet id e (subst q x id)) (Sassign x e) q).
Axiom seq_rule : forall (p:fmla) (q:fmla) (r:fmla) (i1:stmt) (i2:stmt),
((valid_triple p i1 r) /\ (valid_triple r i2 q)) -> (valid_triple p
(Sseq i1 i2) q).
Axiom if_rule : forall (e:term) (p:fmla) (q:fmla) (i1:stmt) (i2:stmt),
((valid_triple (Fand p (Fterm e)) i1 q) /\ (valid_triple (Fand p
(Fnot (Fterm e))) i2 q)) -> (valid_triple p (Sif e i1 i2) q).
Axiom assert_rule : forall (f:fmla) (p:fmla), (valid_fmla (Fimplies p f)) ->
(valid_triple p (Sassert f) p).
Axiom assert_rule_ext : forall (f:fmla) (p:fmla), (valid_triple (Fimplies f
p) (Sassert f) p).
Axiom while_rule : forall (e:term) (inv:fmla) (i:stmt),
(valid_triple (Fand (Fterm e) inv) i inv) -> (valid_triple inv (Swhile e
inv i) (Fand (Fnot (Fterm e)) inv)).
Axiom while_rule_ext : forall (e:term) (inv:fmla) (invqt:fmla) (i:stmt),
(valid_fmla (Fimplies invqt inv)) -> ((valid_triple (Fand (Fterm e) invqt)
i invqt) -> (valid_triple invqt (Swhile e inv i) (Fand (Fnot (Fterm e))
invqt))).
Axiom consequence_rule : forall (p:fmla) (pqt:fmla) (q:fmla) (qqt:fmla)
(i:stmt), (valid_fmla (Fimplies pqt p)) -> ((valid_triple p i q) ->
((valid_fmla (Fimplies q qqt)) -> (valid_triple pqt i qqt))).
Z value)) (pi:(map Z value)), (eval_fmla sigma pi p) -> forall (sigma':(map
Z value)) (pi':(map Z value)) (n:Z), (many_steps sigma pi i sigma' pi'
Sskip n) -> (eval_fmla sigma' pi' q).
Parameter set1 : forall (a:Type), Type.
......@@ -376,6 +344,12 @@ Axiom diff_def1 : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)) (x:a),
Axiom subset_diff : forall (a:Type), forall (s1:(set1 a)) (s2:(set1 a)),
(subset (diff s1 s2) s1).
Parameter choose: forall (a:Type), (set1 a) -> a.
Implicit Arguments choose.
Axiom choose_def : forall (a:Type), forall (s:(set1 a)), (~ (is_empty s)) ->
(mem (choose s) s).
Parameter all: forall (a:Type), (set1 a).
Set Contextual Implicit.
Implicit Arguments all.
......@@ -384,9 +358,9 @@ Unset Contextual Implicit.
Axiom all_def : forall (a:Type), forall (x:a), (mem x (all :(set1 a))).
(* Why3 assumption *)
Definition assigns(sigma:(map Z value)) (a:(set1 Z)) (sigmaqt:(map Z
Definition assigns(sigma:(map Z value)) (a:(set1 Z)) (sigma':(map Z
value)): Prop := forall (i:Z), (~ (mem i a)) -> ((get sigma
i) = (get sigmaqt i)).
i) = (get sigma' i)).
Axiom assigns_refl : forall (sigma:(map Z value)) (a:(set1 Z)),
(assigns sigma a sigma).
......@@ -395,13 +369,24 @@ Axiom assigns_trans : forall (sigma1:(map Z value)) (sigma2:(map Z value))
(sigma3:(map Z value)) (a:(set1 Z)), ((assigns sigma1 a sigma2) /\
(assigns sigma2 a sigma3)) -> (assigns sigma1 a sigma3).
Axiom assigns_union_left : forall (sigma:(map Z value)) (sigmaqt:(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s1 sigmaqt) ->
(assigns sigma (union s1 s2) sigmaqt).
Axiom assigns_union_left : forall (sigma:(map Z value)) (sigma':(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s1 sigma') ->
(assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map Z value)) (sigma':(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s2 sigma') ->
(assigns sigma (union s1 s2) sigma').
Axiom assigns_union_right : forall (sigma:(map Z value)) (sigmaqt:(map Z
value)) (s1:(set1 Z)) (s2:(set1 Z)), (assigns sigma s2 sigmaqt) ->
(assigns sigma (union s1 s2) sigmaqt).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint stmt_writes(i:stmt) (w:(set1 Z)) {struct i}: Prop :=
match i with
| (Sskip|(Sassert _)) => True
| (Sassign id _) => (mem id w)
| ((Sseq s1 s2)|(Sif _ s1 s2)) => (stmt_writes s1 w) /\ (stmt_writes s2 w)
| (Swhile _ _ s) => (stmt_writes s w)
end.
Unset Implicit Arguments.
(* Why3 goal *)
Theorem WP_parameter_compute_writes : forall (s:stmt),
......@@ -411,22 +396,20 @@ Theorem WP_parameter_compute_writes : forall (s:stmt),
| (Sseq s1 s2) => True
| (Sif _ s1 s2) => True
| (Swhile _ _ s1) => forall (result:(set1 Z)), (forall (sigma:(map Z
value)) (pi:(map Z value)) (sigmaqt:(map Z value)) (piqt:(map Z value))
(n:Z), (many_steps sigma pi s1 sigmaqt piqt Sskip n) -> (assigns sigma
result sigmaqt)) -> forall (sigma:(map Z value)) (pi:(map Z value))
(sigmaqt:(map Z value)) (piqt:(map Z value)) (n:Z), (many_steps sigma
pi s sigmaqt piqt Sskip n) -> (assigns sigma result sigmaqt)
value)) (pi:(map Z value)) (sigma':(map Z value)) (pi':(map Z value))
(n:Z), (many_steps sigma pi s1 sigma' pi' Sskip n) -> (assigns sigma
result sigma')) -> forall (sigma:(map Z value)) (pi:(map Z value))
(sigma':(map Z value)) (pi':(map Z value)) (n:Z), (many_steps sigma pi
s sigma' pi' Sskip n) -> (assigns sigma result sigma')
| (Sassert _) => True
end.
destruct s; intuition.
generalize sigma pi sigmaqt piqt H0.
generalize sigma pi sigma' pi' H0.
generalize (steps_non_neg _ _ _ _ _ _ _ H0).
clear sigma pi sigmaqt piqt H0.
clear sigma pi sigma' pi' H0.
intro H_n_pos.
apply Z_lt_induction with (P:= fun n =>
forall sigma pi sigmaqt piqt : map Z value,
many_steps sigma pi (Swhile t f s) sigmaqt piqt Sskip n ->
assigns sigma result sigmaqt); auto.
pattern n.
apply Z_lt_induction; auto.
intros x Hind sigma pi sigma' qt' Hsteps.
inversion Hsteps; subst; clear Hsteps.
inversion H0; subst; clear H0.
......
......@@ -3,24 +3,26 @@
Require Import ZArith.
Require Import Rbase.
Require int.Int.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
......@@ -29,20 +31,7 @@ Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=
......@@ -59,9 +48,25 @@ Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
(Nil :(list a))) = l).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil :(list a))).
Axiom Append_length : forall (a:Type), forall (l1:(list a)) (l2:(list a)),
((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
match l with
......@@ -76,10 +81,12 @@ Axiom mem_append : forall (a:Type), forall (x:a) (l1:(list a)) (l2:(list a)),
Axiom mem_decomp : forall (a:Type), forall (x:a) (l:(list a)), (mem x l) ->
exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))).
(* Why3 assumption *)
Inductive tree :=
| Leaf : tree
| Node : tree -> tree -> tree .
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint depths(d:Z) (t:tree) {struct t}: (list Z) :=
match t with
......@@ -98,36 +105,49 @@ Axiom depths_unique : forall (t1:tree) (t2:tree) (d:Z) (s1:(list Z))
(s2:(list Z)), ((infix_plpl (depths d t1) s1) = (infix_plpl (depths d t2)
s2)) -> ((t1 = t2) /\ (s1 = s2)).
Axiom depths_prefix : forall (t:tree) (d1:Z) (d2:Z) (s1:(list Z)) (s2:(list
Z)), ((infix_plpl (depths d1 t) s1) = (infix_plpl (depths d2 t) s2)) ->
(d1 = d2).
Axiom depths_prefix_simple : forall (t:tree) (d1:Z) (d2:Z), ((depths d1
t) = (depths d2 t)) -> (d1 = d2).
Axiom depths_subtree : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z) (s1:(list
Z)), ((infix_plpl (depths d1 t1) s1) = (depths d2 t2)) -> (d2 <= d1)%Z.
Axiom depths_unique2 : forall (t1:tree) (t2:tree) (d1:Z) (d2:Z), ((depths d1
t1) = (depths d2 t2)) -> ((d1 = d2) /\ (t1 = t2)).
(* Why3 assumption *)
Definition lex(x1:((list Z)* Z)%type) (x2:((list Z)* Z)%type): Prop :=
match x1 with
| (s1, d1) =>
match x2 with
| (s2, d2) => ((length s1) < (length s2))%Z \/
| (s2, d2) => ((length s1) < (length s2))%Z \/
(((length s1) = (length s2)) /\ match (s1,
s2) with
| ((Cons h1 _), (Cons h2 _)) => ((d2 < d1)%Z /\ (d1 <= h1)%Z) /\
| ((Cons h1 _), (Cons h2 _)) => ((d2 < d1)%Z /\ (d1 <= h1)%Z) /\
(h1 = h2)
| _ => False
end)
end
end.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Theorem WP_parameter_build_rec : forall (d:Z), forall (s:(list Z)),
match s with