Commit f024a78f authored by MARCHE Claude's avatar MARCHE Claude
Browse files

simplified Coq proofs

parent 3de9196e
......@@ -455,7 +455,7 @@ end
(*
Local Variables:
compile-command: "why3ide -I . wp2.mlw"
compile-command: "why3ide wp2.mlw"
End:
*)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session
name="examples/hoare_logic/wp2/why3session.xml">
name="wp2/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -32,13 +32,13 @@
expanded="true">
<theory
name="Imp"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="3" loccnumb="7" loccnume="10"
verified="true"
expanded="false">
<goal
name="eval_subst_term"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="96" loccnumb="6" loccnume="21"
sum="57686028d06a25fd21f0d145ae3c39cc"
proved="true"
......@@ -55,7 +55,7 @@
</goal>
<goal
name="eval_term_change_free"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="102" loccnumb="6" loccnume="27"
sum="bc8ecc8fa47f6b0378862b9ff6c140b4"
proved="true"
......@@ -72,7 +72,7 @@
</goal>
<goal
name="eval_subst"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="128" loccnumb="6" loccnume="16"
sum="e7187a74f15a81f5d32beb4c7e17ebd5"
proved="true"
......@@ -89,7 +89,7 @@
</goal>
<goal
name="eval_swap"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="134" loccnumb="6" loccnume="15"
sum="df0a3794f91d81e47b10e6e3cbb7ffd5"
proved="true"
......@@ -112,7 +112,7 @@
</goal>
<goal
name="eval_change_free"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="140" loccnumb="6" loccnume="22"
sum="d5dd6566baac671168e7b098cdc7b9d5"
proved="true"
......@@ -129,7 +129,7 @@
</goal>
<goal
name="check_skip"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="155" loccnumb="6" loccnume="16"
sum="d0110d5cf0e45b1a226959c69106f31e"
proved="true"
......@@ -173,7 +173,7 @@
</goal>
<goal
name="steps_non_neg"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="224" loccnumb="6" loccnume="19"
sum="6192ae6d220dcba9ed5131230fef77d7"
proved="true"
......@@ -190,7 +190,7 @@
</goal>
<goal
name="many_steps_seq"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="228" loccnumb="6" loccnume="20"
sum="701bc2e3c241588769058c0765a02a42"
proved="true"
......@@ -208,20 +208,20 @@
</theory>
<theory
name="TestSemantics"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="258" loccnumb="7" loccnume="20"
verified="true"
expanded="false">
</theory>
<theory
name="HoareLogic"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="299" loccnumb="7" loccnume="17"
verified="true"
expanded="false">
<goal
name="consequence_rule"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="306" loccnumb="6" loccnume="22"
sum="c1f5595ddd954b6361531a9cb635279b"
proved="true"
......@@ -244,7 +244,7 @@
</goal>
<goal
name="skip_rule"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="313" loccnumb="6" loccnume="15"
sum="73e47f5d6901d2f852f0c089cfe9027d"
proved="true"
......@@ -261,7 +261,7 @@
</goal>
<goal
name="assign_rule"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="316" loccnumb="6" loccnume="17"
sum="5ad7f36cb5982497693bbd3917b38dd5"
proved="true"
......@@ -278,7 +278,7 @@
</goal>
<goal
name="seq_rule"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="321" loccnumb="6" loccnume="14"
sum="1a26088dc2dd29482c5092b6ac4ff809"
proved="true"
......@@ -301,7 +301,7 @@
</goal>
<goal
name="if_rule"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="326" loccnumb="6" loccnume="13"
sum="3bebb0334fdf15d6238553f897994e1d"
proved="true"
......@@ -318,7 +318,7 @@
</goal>
<goal
name="assert_rule"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="332" loccnumb="6" loccnume="17"
sum="b11afd1baac4615f908daadec96d093c"
proved="true"
......@@ -335,7 +335,7 @@
</goal>
<goal
name="assert_rule_ext"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="336" loccnumb="6" loccnume="21"
sum="189817af6b3e698754f066618e6681a5"
proved="true"
......@@ -352,7 +352,7 @@
</goal>
<goal
name="while_rule"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="340" loccnumb="6" loccnume="16"
sum="a1136f47e552feb3c79f635b836bda93"
proved="true"
......@@ -369,7 +369,7 @@
</goal>
<goal
name="while_rule_ext"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="345" loccnumb="6" loccnume="20"
sum="2b6ff464c6bc40e843b0c4d2e7536e09"
proved="true"
......@@ -387,13 +387,13 @@
</theory>
<theory
name="WP WP"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="356" loccnumb="7" loccnume="9"
verified="true"
expanded="false">
expanded="true">
<goal
name="assigns_refl"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="366" loccnumb="6" loccnume="18"
sum="aa2d95740fab1e3635f694dc96c50567"
proved="true"
......@@ -409,7 +409,7 @@
</goal>
<goal
name="assigns_trans"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="369" loccnumb="6" loccnume="19"
sum="0cbbe8a4a0bb524c9eb5267c2e165996"
proved="true"
......@@ -425,7 +425,7 @@
</goal>
<goal
name="assigns_union_left"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="374" loccnumb="6" loccnume="24"
sum="00edb9a60872fe96f7f07d1664b5b784"
proved="true"
......@@ -441,7 +441,7 @@
</goal>
<goal
name="assigns_union_right"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="378" loccnumb="6" loccnume="25"
sum="70bd82cb54615334f173042f254c5bd9"
proved="true"
......@@ -457,7 +457,7 @@
</goal>
<goal
name="WP_parameter compute_writes"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="3849436ee1eee91832ef0eacdb5cc631"
......@@ -473,7 +473,7 @@
expanded="false">
<goal
name="WP_parameter compute_writes.1"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="617e33b55d788337118c187682240436"
......@@ -493,7 +493,7 @@
</goal>
<goal
name="WP_parameter compute_writes.2"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="a171b6344c0547d9efeb5733ca857b31"
......@@ -514,7 +514,7 @@
</goal>
<goal
name="WP_parameter compute_writes.3"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="2b26b707574663ac9ea048af46720f50"
......@@ -541,7 +541,7 @@
</goal>
<goal
name="WP_parameter compute_writes.4"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="2164b09f70565800acd808d0bf162dd5"
......@@ -562,7 +562,7 @@
</goal>
<goal
name="WP_parameter compute_writes.5"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="0be8bdb7f61dabda5ba8bc28b2d663e0"
......@@ -583,7 +583,7 @@
</goal>
<goal
name="WP_parameter compute_writes.6"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="392" loccnumb="10" loccnume="24"
expl="parameter compute_writes"
sum="48ff95e748cba004c021eb0709567b1b"
......@@ -606,12 +606,12 @@
</goal>
<goal
name="WP_parameter wp"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="34b3d52289eaeeee07953c5b8aa31cd4"
proved="true"
expanded="false"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleaFletV8V7asubstV1V6V8V0V1Iafresh_in_fmlaV8V1FaSifVVVavalid_tripleaFandaFimpliesaFtermV9V12aFimpliesaFnotaFtermV9V13V0V1Iavalid_tripleV13V11V1FIavalid_tripleV12V10V1FaSassertVavalid_tripleaFimpliesV14V1V0V1aSwhileVVVavalid_tripleaFandV16V19V0V1Iaeval_fmlaV22V23V19Iamany_stepsV20V21V17V22V23aSskipV24FAaeval_fmlaV20V21aFandaFimpliesaFandaFtermV15V16V18aFimpliesaFandaFnotaFtermV15V16V1Iaeval_fmlaV20V21V19FFIavalid_tripleV18V17V16FFF">
<label
name="expl:parameter wp">
......@@ -619,10 +619,10 @@
<transf
name="split_goal"
proved="true"
expanded="false">
expanded="true">
<goal
name="WP_parameter wp.1"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="0ce0bf0a1a09361d7e5c1fae11f4320c"
......@@ -670,7 +670,7 @@
</goal>
<goal
name="WP_parameter wp.2"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="659a8041ce0bdaf08e7037f521c9f105"
......@@ -718,7 +718,7 @@
</goal>
<goal
name="WP_parameter wp.3"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="6130c16879ea5938d8b47ef1d0ab33a4"
......@@ -766,7 +766,7 @@
</goal>
<goal
name="WP_parameter wp.4"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="5071f85b66d874821196c755dd2cc8d3"
......@@ -787,7 +787,7 @@
</goal>
<goal
name="WP_parameter wp.5"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="50f5658baca164788a4475bd94d7bef2"
......@@ -835,12 +835,12 @@
</goal>
<goal
name="WP_parameter wp.6"
locfile="examples/hoare_logic/wp2/../wp2.mlw"
locfile="wp2/../wp2.mlw"
loclnum="428" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="d3e0dde6c1ad5bc98557979667bae2d1"
proved="true"
expanded="false"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11V14V0V1Iaeval_fmlaV17V18V14Iamany_stepsV15V16V12V17V18aSskipV19FAaeval_fmlaV15V16aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1Iaeval_fmlaV15V16V14FFIavalid_tripleV13V12V11FFF">
<label
name="expl:parameter wp">
......@@ -851,7 +851,7 @@
edited="wp2_WP_WP_WP_parameter_wp_2.v"
obsolete="false"
archived="false">
<result status="valid" time="0.73"/>
<result status="valid" time="0.74"/>
</proof>
</goal>
</transf>
......
......@@ -439,8 +439,7 @@ intros Post WP_body H_WP_body.
intros abstracted_fmla H_abstracted.
red.
intros s1 p1 H1 s2 p2 n Hsteps.
generalize (steps_non_neg _ _ _ _ _ _ _ Hsteps).
intro H_n_pos.
assert (H_n_pos := steps_non_neg _ _ _ _ _ _ _ Hsteps).
generalize s1 p1 H1 Hsteps; clear s1 p1 H1 Hsteps.
apply Z_lt_induction with (P :=
fun n => forall s1 p1 : map Z value,
......@@ -452,26 +451,24 @@ elim H0; clear H0; intros H_inv_in_s2 H_abstr_in_s2.
inversion H1; subst; clear H1.
inversion H0; subst; clear H0.
(* case cond = true *)
generalize (many_steps_seq _ _ _ _ _ _ _ H2); clear H2.
intros (s3 & p3 & n1 & n2 & First_iter & Next_iter & Hn1n2).
destruct (many_steps_seq _ _ _ _ _ _ _ H2) as
(s3 & p3 & n1 & n2 & First_iter & Next_iter & Hn1n2).
clear H2.
apply H with (3:=Next_iter).
generalize (steps_non_neg _ _ _ _ _ _ _ First_iter); intro Hn1_pos.
generalize (steps_non_neg _ _ _ _ _ _ _ Next_iter); intro Hn2_pos.
assert (Hn1_pos := steps_non_neg _ _ _ _ _ _ _ First_iter).
assert (Hn2_pos := steps_non_neg _ _ _ _ _ _ _ Next_iter).
omega.
generalize (H_abstracted sigma2 pi2 H_abstr_in_s2); clear H_abstracted.
simpl.
intros ((Htrue,_) & Hnext).
generalize (Hnext s3 p3 n1 First_iter); clear Hnext.
intro H_abstr_in_s3.
destruct (H_abstracted sigma2 pi2 H_abstr_in_s2) as ((Htrue,_) & Hnext).
clear H_abstracted.
assert (H_abstr_in_s3 := Hnext s3 p3 n1 First_iter); clear Hnext.
split; auto.
red in H_WP_body.
apply H_WP_body with (2:=First_iter).
apply Htrue; auto.
(* case cond = false *)
inversion H2; [subst; clear H2 | inversion H0].
generalize (H_abstracted s2 p2 H_abstr_in_s2); clear H_abstracted.
simpl.
intros ((_,Hfalse) & Hnext).
destruct (H_abstracted s2 p2 H_abstr_in_s2) as ((_,Hfalse) & Hnext).
clear H_abstracted.
apply Hfalse; split; auto.
rewrite H11; discriminate.
Qed.
......
......@@ -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.
......@@ -30,19 +32,18 @@ Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter head: forall (a:Type), (list a) -> a.
Implicit Arguments head.
Axiom head_cons : forall (a:Type), forall (x:a) (l:(list a)), ((head (Cons x
l)) = x).
Parameter tail: forall (a:Type), (list a) -> (list a).
Implicit Arguments tail.
Axiom tail_cons : forall (a:Type), forall (x:a) (l:(list a)), ((tail (Cons x
l)) = l).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
match l with
......@@ -51,10 +52,12 @@ Fixpoint mem (a:Type)(x:a) (l:(list a)) {struct l}: Prop :=
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Definition disjoint (a:Type)(l1:(list a)) (l2:(list a)): Prop :=
forall (x:a), ~ ((mem x l1) /\ (mem x l2)).
Implicit Arguments disjoint.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint no_repet (a:Type)(l:(list a)) {struct l}: Prop :=
match l with
......@@ -63,6 +66,7 @@ Fixpoint no_repet (a:Type)(l:(list a)) {struct l}: Prop :=
end.
Unset Implicit Arguments.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint infix_plpl (a:Type)(l1:(list a)) (l2:(list a)) {struct l1}: (list
a) :=
......@@ -77,8 +81,9 @@ Axiom Append_assoc : forall (a:Type), forall (l1:(list a)) (l2:(list a))
l3)) = (infix_plpl (infix_plpl l1 l2) l3)).
Axiom Append_l_nil : forall (a:Type), forall (l:(list a)), ((infix_plpl l
(Nil:(list a))) = l).
(Nil :(list a))) = l).
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
......@@ -91,7 +96,7 @@ 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))).
((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).
......@@ -102,11 +107,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 *)
Set Implicit Arguments.
Fixpoint reverse (a:Type)(l:(list a)) {struct l}: (list a) :=
match l with
| Nil => (Nil:(list a))
| (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil:(list a))))
| Nil => (Nil :(list a))
| (Cons x r) => (infix_plpl (reverse r) (Cons x (Nil :(list a))))
end.
Unset Implicit Arguments.
......@@ -123,11 +129,9 @@ Axiom Reverse_length : forall (a:Type), forall (l:(list a)),
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)),
......@@ -139,22 +143,21 @@ Axiom Select_neq : forall (a:Type) (b:Type), forall (m:(map a b)),
a2) = (get m a2)).
Parameter const: forall (b:Type) (a: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 (b:Type) (a:Type), forall (b1:b) (a1:a),
((get (const b1:(map a b)) a1) = b1).
Parameter loc : Type.
Parameter null: loc.
(* Why3 assumption *)
Inductive list_seg : loc -> (map loc loc) -> (list loc) -> loc -> Prop :=
| list_seg_nil : forall (p:loc) (next:(map loc loc)), (list_seg p next
(Nil:(list loc)) p)
(Nil :(list loc)) p)
| list_seg_cons : forall (p:loc) (q:loc) (next:(map loc loc)) (l:(list
loc)), ((~ (p = null)) /\ (list_seg (get next p) next l q)) ->
(list_seg p next (Cons p l) q).
......@@ -163,10 +166,9 @@ Axiom list_seg_frame : forall (next1:(map loc loc)) (next2:(map loc loc))
(p:loc) (q:loc) (v:loc) (pM:(list loc)), ((list_seg p next1 pM null) /\
((next2 = (set next1 q v)) /\ ~ (mem q pM))) -> (list_seg p next2 pM null).
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
(* Why3 goal *)
Theorem list_seg_functional : forall (next:(map loc loc)) (l1:(list loc))
(l2:(list loc)) (p:loc), ((list_seg p next l1 null) /\ (list_seg p next l2
null)) -> (l1 = l2).
......@@ -181,6 +183,5 @@ inversion h2; subst; clear h2; intuition.
apply f_equal.
apply IHl1 with (p:=get next a); auto.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -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.
......@@ -30,19 +32,18 @@ Unset Contextual Implicit.
Implicit Arguments Cons.
Parameter head: forall (a:Type), (list a) -> a.