Commit 7fc10633 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Reflection toy example

parent d7cf96b1
use import int.Int
use import list.List
type t = Var int | Add t t | Mul t t | Cst int
function interp (x:t) (y:int->int) : int =
match x with
| Var n -> y n
| Add x1 x2 -> interp x1 y + interp x2 y
| Mul x1 x2 -> interp x1 y * interp x2 y
| Cst c -> c end
goal interp: forall y. interp (Add (Var 3) (Var 5)) y = y 3 + y 5
(** Conversion *)
type m = M int (list int)
type t' = list m (* sum of monomials *)
function mon (x:list int) (y:int -> int) : int =
match x with
| Nil -> 1
| Cons x r -> (y x) * mon r y end
function interp' (x:t') (y:int->int) : int =
match x with
| Nil -> 0
| Cons (M a m) r -> a * mon m y + interp' r y end
predicate eq_mon (m1 m2: list int) = forall y: int->int. mon m1 y = mon m2 y
predicate eq' (x1 x2: t') = forall y: int->int. interp' x1 y = interp' x2 y
use import list.Append
use import list.Length
let rec lemma mon_append (x1 x2: list int) (y:int -> int)
ensures { mon (x1 ++ x2) y = mon x1 y * mon x2 y }
variant { x1 }
=
match x1 with Nil -> () | Cons _ x -> mon_append x x2 y end
lemma interp_nil : forall y:int -> int. interp' Nil y = 0
lemma interp_cons : forall m:m, x:t', y:int->int.
interp' (Cons m x) y = interp' (Cons m Nil) y + interp' x y
let rec lemma interp_sum (x1 x2:t') (y:int->int)
ensures { interp' (x1 ++ x2) y = interp' x1 y + interp' x2 y }
variant { x1 }
=
match x1 with
| Nil -> ()
| Cons _ x -> interp_sum x x2 y
end
let function append_mon (m1 m2:m)
ensures { forall y. interp' (Cons result Nil) y
= interp' (Cons m1 Nil) y * interp' (Cons m2 Nil) y }
= match m1,m2 with M a1 l1, M a2 l2 -> M (a1 * a2) (l1 ++ l2) end
let rec function mul_mon (x:t') (mon:m) : t'
ensures { forall y.
interp' result y = interp' x y * interp' (Cons mon Nil) y } =
match x with
| Nil -> Nil
| Cons m r ->
let mr = append_mon m mon in
let lr = mul_mon r mon in
let res = Cons mr lr in
assert { forall y. interp' res y
= interp' (Cons mr Nil) y + interp' lr y
= interp' (Cons m Nil) y * interp' (Cons mon Nil) y
+ interp' r y * interp' (Cons mon Nil) y
= (interp' (Cons m Nil) y + interp' r y) * interp' (Cons mon Nil) y
= interp' x y * interp' (Cons mon Nil) y };
res
end
let rec function mul_devel (x1 x2:t') : t'
ensures { forall y. interp' result y = interp' x1 y * interp' x2 y } =
match x1 with
| Nil -> Nil
| Cons (M a m) r -> (mul_mon x2 (M a m)) ++ (mul_devel r x2)
end
let rec function conv (x:t) : t'
ensures { forall y. interp x y = interp' result y } =
match x with
| Var v -> Cons (M 1 (Cons v Nil)) Nil
| Add x1 x2 -> (conv x1) ++ (conv x2)
| Mul x1 x2 -> mul_devel (conv x1) (conv x2)
| Cst n -> Cons (M n Nil) Nil
end
(** Normalisation *)
use import list.Permut
let rec function insert (x: int) (l: list int) : list int
ensures { eq_mon (Cons x l) result }
variant { l }
= match l with
| Nil -> Cons x Nil
| Cons y r -> if x <= y then Cons x l else Cons y (insert x r)
end
(*no need to prove that this actually sorts the list*)
let rec function insertion_sort (l: list int) : list int
ensures { eq_mon l result }
variant { l }
= match l with
| Nil -> Nil
| Cons x r -> insert x (insertion_sort r)
end
let function sort_mon (x:m) : m
ensures { eq' (Cons x Nil) (Cons result Nil) }
= match x with M a m -> M a (insertion_sort m) end
let rec function sort_mons (x:t') : t'
ensures { eq' result x }
variant { x }
= match x with Nil -> Nil | Cons m r -> Cons (sort_mon m) (sort_mons r) end
(*lexicographic order on monomials with variables sorted using sort_mons*)
let rec function le_mon (x1 x2: list int) : bool
= match x1, x2 with
| Nil, _ -> true
| _, Nil -> false
| Cons v1 r1, Cons v2 r2 -> v1 <= v2 && le_mon r1 r2
end
let rec function insert_mon (m: m) (x: t') : t'
ensures { eq' result (Cons m x) }
variant { x }
= match m,x with
| _,Nil -> Cons m Nil
| M _ l1, Cons (M a2 l2) r ->
if le_mon l1 l2 then Cons m x else Cons (M a2 l2) (insert_mon m r)
end
let rec function insertion_sort_mon (x: t') : t'
ensures { eq' result x }
variant { x }
= match x with
| Nil -> Nil
| Cons m r -> insert_mon m (insertion_sort_mon r)
end
let rec function same (l1 l2: list int) : bool
ensures { result -> eq_mon l1 l2 }
= match l1, l2 with
| Nil, Nil -> true
| Nil, _ | _, Nil -> false
| Cons x1 l1, Cons x2 l2 -> x1 = x2 && same l1 l2
end
let rec squash (x: t') : t'
ensures { eq' result x }
variant { length x }
= match x with
| Nil -> Nil
| Cons _ Nil -> x
| Cons (M a1 l1) (Cons (M a2 l2) r)
-> if same l1 l2
then squash (Cons (M (a1+a2) l1) r)
else Cons (M a1 l1) (squash (Cons (M a2 l2) r))
end
let function normalize (x: t') : t'
ensures { eq' result x }
=
(* sort inside each monomial *)
let x = sort_mons x in
(* sort monomials lexicographically *)
let x = insertion_sort_mon x in
(* squash together identical monoms *)
squash x
lemma norm: forall x1 x2:t', y:int -> int.
normalize x1 = normalize x2 -> interp' x1 y = interp' x2 y
(** Tests *)
constant radix : int = 1
constant d : int = 0
constant x1 : t = Add (Add (Var radix) (Cst (-1)))
(Mul (Var radix)
(Add (Var radix) (Mul (Cst (-1)) (Add (Cst 1) (Var d)))))
constant x2 : t = Add (Mul (Var radix) (Var radix))
(Add (Cst (-1)) (Mul (Cst (-1)) (Mul (Var radix) (Var d))))
constant x3 : t = Mul (Add (Add (Var radix) (Cst (-1)))
(Mul (Var radix)
(Add (Var radix) (Mul (Cst (-1)) (Add (Cst 1) (Var d))))))
(Add (Add (Var radix) (Cst (-1)))
(Mul (Var radix)
(Add (Var radix) (Mul (Cst (-1)) (Add (Cst 1) (Var d))))))
constant x4 : t = Mul (Add (Mul (Var radix) (Var radix))
(Add (Cst (-1)) (Mul (Cst (-1)) (Mul (Var radix) (Var d)))))
(Add (Mul (Var radix) (Var radix))
(Add (Cst (-1)) (Mul (Cst (-1)) (Mul (Var radix) (Var d)))))
constant z : int = 2
constant x5 : t = Mul (Add (Add (Var radix) (Var z))
(Mul (Var radix)
(Add (Var radix) (Mul (Var z) (Add (Cst 1) (Var d))))))
(Add (Add (Var radix) (Var z))
(Mul (Var radix)
(Add (Var radix) (Mul (Var z) (Add (Cst 1) (Var d))))))
constant x6 : t = Mul (Add (Mul (Var radix) (Var radix))
(Add (Var z) (Mul (Var z) (Mul (Var radix) (Var d)))))
(Add (Mul (Var radix) (Var radix))
(Add (Var z) (Mul (Var z) (Mul (Var radix) (Var d)))))
constant x7 : t = Mul x3 x5
constant x8 : t = Mul x4 x6
constant x9 : t = Mul x3 x3
constant x10 : t = Mul x4 x4
meta "compute_max_steps" 0x1000000
goal devel_1: forall y. interp x1 y = interp x2 y
goal devel_2: forall y. interp x3 y = interp x4 y
goal devel_3: forall y. interp x5 y = interp x6 y
goal devel_4: forall y. interp x7 y = interp x8 y (*not proved*)
goal devel_5: forall y. interp x9 y = interp x10 y
goal devel_conv_1: forall y. interp' (conv x1) y = interp' (conv x2) y
goal devel_conv_2: forall y. interp' (conv x3) y = interp' (conv x4) y
goal devel_conv_3: forall y. interp' (conv x5) y = interp' (conv x6) y
goal devel_conv_4: forall y. interp' (conv x7) y = interp' (conv x8) y
(* not proved *)
goal devel_conv_5: forall y. interp' (conv x9) y = interp' (conv x10) y
(*alt ergo solves in 2s *)
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="1" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="3" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="2000"/>
<file name="../compute.mlw" expanded="true">
<theory name="Top" sum="51e3e42f2718a96f151b7a57bc7dc865" expanded="true">
<goal name="interp" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="VC mon_append" expl="VC for mon_append">
<proof prover="0"><result status="valid" time="0.01" steps="59"/></proof>
</goal>
<goal name="interp_nil" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="interp_cons" expl="">
<transf name="compute_in_goal">
<goal name="interp_cons.1" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
</transf>
</goal>
<goal name="VC interp_sum" expl="VC for interp_sum">
<transf name="split_goal_wp">
<goal name="VC interp_sum.1" expl="variant decrease">
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="VC interp_sum.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
</transf>
</goal>
<goal name="VC append_mon" expl="VC for append_mon">
<transf name="split_goal_wp">
<goal name="VC append_mon.1" expl="postcondition">
<transf name="compute_in_goal">
<goal name="VC append_mon.1.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="53"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC mul_mon" expl="VC for mul_mon">
<transf name="split_goal_wp">
<goal name="VC mul_mon.1" expl="assertion">
<transf name="split_goal_wp">
<goal name="VC mul_mon.1.1" expl="assertion">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="VC mul_mon.1.2" expl="assertion">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="VC mul_mon.1.3" expl="assertion">
<proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="VC mul_mon.1.4" expl="assertion">
<proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mul_mon.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="VC mul_devel" expl="VC for mul_devel">
<proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
<transf name="split_goal_wp">
<goal name="VC mul_devel.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
<goal name="VC mul_devel.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
</transf>
</goal>
<goal name="VC conv" expl="VC for conv">
<transf name="split_goal_wp">
<goal name="VC conv.1" expl="postcondition">
<transf name="compute_in_goal">
<goal name="VC conv.1.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="101"/></proof>
</goal>
</transf>
</goal>
<goal name="VC conv.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC conv.3" expl="postcondition">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
<goal name="VC conv.4" expl="postcondition">
<transf name="compute_in_goal">
<goal name="VC conv.4.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="54"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC insert" expl="VC for insert">
<transf name="split_goal_wp">
<goal name="VC insert.1" expl="variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC insert.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="66"/></proof>
</goal>
</transf>
</goal>
<goal name="VC insertion_sort" expl="VC for insertion_sort">
<transf name="split_goal_wp">
<goal name="VC insertion_sort.1" expl="variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
</goal>
<goal name="VC insertion_sort.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sort_mon" expl="VC for sort_mon">
<transf name="compute_in_goal">
<goal name="VC sort_mon.1" expl="VC for sort_mon">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sort_mons" expl="VC for sort_mons">
<proof prover="0"><result status="valid" time="0.02" steps="76"/></proof>
</goal>
<goal name="VC le_mon" expl="VC for le_mon">
<proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="VC insert_mon" expl="VC for insert_mon">
<transf name="split_goal_wp">
<goal name="VC insert_mon.1" expl="variant decrease">
<proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
</goal>
<goal name="VC insert_mon.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.02" steps="100"/></proof>
</goal>
</transf>
</goal>
<goal name="VC insertion_sort_mon" expl="VC for insertion_sort_mon">
<transf name="split_goal_wp">
<goal name="VC insertion_sort_mon.1" expl="variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="VC insertion_sort_mon.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="30"/></proof>
</goal>
</transf>
</goal>
<goal name="VC same" expl="VC for same" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
<goal name="VC squash" expl="VC for squash" expanded="true">
<proof prover="0" obsolete="true"><result status="timeout" time="4.99"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="VC squash.1" expl="variant decrease">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="VC squash.2" expl="variant decrease" expanded="true">
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="VC squash.3" expl="postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<transf name="split_goal_wp" expanded="true">
<goal name="VC squash.3.1" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
</goal>
<goal name="VC squash.3.2" expl="postcondition">
<proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC squash.3.3" expl="postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="5.00"/></proof>
<transf name="compute_in_goal" expanded="true">
<goal name="VC squash.3.3.1" expl="postcondition" expanded="true">
<proof prover="0"><result status="timeout" time="5.01"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC normalize" expl="VC for normalize">
<proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
<goal name="norm" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="devel_1" expl="">
<transf name="compute_in_goal">
<goal name="devel_1.1" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_2" expl="">
<transf name="compute_in_goal">
<goal name="devel_2.1" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_3" expl="" expanded="true">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="compute_in_goal" expanded="true">
<goal name="devel_3.1" expl="" expanded="true">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_4" expl="" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="devel_4.1" expl="" expanded="true">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_5" expl="">
<transf name="compute_in_goal">
<goal name="devel_5.1" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_1" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_1.1" expl="">
<proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_2" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_2.1" expl="">
<proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="4.94"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_3" expl="" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="devel_conv_3.1" expl="">
<proof prover="0" obsolete="true"><result status="timeout" time="5.01"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_4" expl="" expanded="true">
<transf name="compute_in_goal" expanded="true">
<goal name="devel_conv_4.1" expl="" expanded="true">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
<goal name="devel_conv_5" expl="">
<transf name="compute_in_goal">
<goal name="devel_conv_5.1" expl="">
<proof prover="0"><result status="valid" time="1.83" steps="6"/></proof>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment