Commit 4b810a5b authored by Martin Clochard's avatar Martin Clochard

(Work in progress) formalization of why3 logic

parent dc9cfb96
This diff is collapsed.
This diff is collapsed.
module HO
use export HighOrd
predicate extensional_equal (f g:'a -> 'b) =
forall x. f x = g x
(* Hackish way to prove functional extensionality. *)
predicate hack (f g h:'a -> 'b) =
f = g = h
let lemma extensionality (f g:'a -> 'b)
requires { extensional_equal f g }
ensures { f = g }
= assert { hack f (\x. f x) g }
meta remove_logic predicate hack
function compose (g:'b -> 'c) (f:'a -> 'b) : 'a -> 'c =
\x. g (f x)
function rcompose (f:'a -> 'b) (g:'b -> 'c) : 'a -> 'c = compose g f
function identity : 'a -> 'a = \x. x
let lemma compose_associative (f:'a -> 'b) (g:'b -> 'c) (h:'c -> 'd)
ensures { compose (compose h g) f = compose h (compose g f) }
= extensionality (compose (compose h g) f) (compose h (compose g f))
let lemma id_neutral (f:'a -> 'b)
ensures { compose identity f = f = compose f identity }
= extensionality (compose identity f) f;
extensionality f (compose f identity)
function const (x:'b) : 'a -> 'b = \_.x
let lemma compose_const_right (x:'c) (f:'a -> 'b)
ensures { compose (const x) f = const x }
= extensionality (compose (const x) f) (const x)
let lemma compose_const_left (x:'b) (f:'b -> 'c)
ensures { compose f (const x:'a -> 'b) = const (f x) }
= extensionality (compose f (const x:'a -> 'b)) (const (f x))
function ho_ite (p:'a -> bool) (t e:'a -> 'b) : 'a -> 'b =
\x. if p x then t x else e x
let lemma ho_ite_compose_left (p:'a -> bool) (t e:'a -> 'b) (g:'b -> 'c)
ensures { compose g (ho_ite p t e) = ho_ite p (compose g t) (compose g e) }
= extensionality (compose g (ho_ite p t e))
(ho_ite p (compose g t) (compose g e))
module Bind
use import HO
type bind 'a 'b =
| Old 'a
| Fresh 'b
function bfold (o:'a -> 'c) (f:'b -> 'c) : bind 'a 'b -> 'c =
\x. match x with Old x -> o x | Fresh y -> f y end
let lemma bfold_identity ()
ensures { bfold Old Fresh = (identity:bind 'a 'b -> bind 'a 'b) }
= assert { extensional_equal (bfold Old Fresh)
(identity:bind 'a 'b -> bind 'a 'b) }
let lemma bfold_compose (o:'a -> 'c) (f:'b -> 'c) (g:'c -> 'd)
ensures { compose g (bfold o f) = bfold (compose g o) (compose g f) }
= assert { let a = compose g (bfold o f) in
let b = bfold (compose g o) (compose g f) in
forall x. a x <> b x -> match x with
| Old _ -> a x = b x && false | Fresh _ -> false end && false }
let lemma bfold_constructor (o:'a -> 'c) (f:'b -> 'c)
ensures { compose (bfold o f) Old = o }
ensures { compose (bfold o f) Fresh = f }
= assert { extensional_equal (compose (bfold o f) Old) o /\
extensional_equal (compose (bfold o f) Fresh) f }
(* There is no need to map over second component for bindings,
so keep it simple. *)
function bmap (f:'a -> 'b) : bind 'a 'c -> bind 'b 'c =
bfold (compose Old f) Fresh
lemma bmap_compose : forall g:'b -> 'c,f:'a -> 'b.
bmap (compose g f) = compose (bmap g) (bmap f:bind 'a 'd -> bind 'b 'd)
lemma bmap_id : bmap identity = (identity:bind 'a 'b -> bind 'a 'b)
(* Standard renamings for opening/closing binders in program. *)
function open (f:'b -> 'a) : bind 'a 'b -> 'a =
bfold identity f
function close (bound:'a -> bool) (f:'a -> 'b) : 'a -> bind 'a 'b =
ho_ite bound (compose Fresh f) Old
(* Identity useful to caracterise folding values upon opening/closing
binders in programs. *)
lemma close_fold : forall bound:'a -> bool,f:'a -> 'b,g:'a -> 'c,h:'b -> 'c.
compose (bfold g h) (close bound f) = ho_ite bound (compose h f) g
module Choice
use import HighOrd
constant default : 'a
function choice (p:'a -> bool) : 'a
lemma choice_def : forall p:'a -> bool. (exists x. p x) -> p (choice p)
val choice_def (p:'a -> bool) : unit
requires { exists x. p x }
ensures { p (choice p) }
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="5" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" memlimit="1000"/>
<prover id="2" name="Spass" version="3.7" timelimit="5" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="0.95.2" timelimit="5" memlimit="1000"/>
<file name="../support.mlw" expanded="true">
<theory name="HO" sum="cacf043d990e8fc0b8032e0b3427633c">
<goal name="WP_parameter extensionality" expl="VC for extensionality">
<transf name="split_goal_wp">
<goal name="WP_parameter extensionality.1" expl="1. assertion">
<transf name="inline_goal">
<goal name="WP_parameter extensionality.1.1" expl="1. assertion">
<proof prover="3"><result status="valid" time="0.01" steps="1"/></proof>
<goal name="WP_parameter extensionality.2" expl="2. postcondition">
<proof prover="3"><result status="valid" time="0.01" steps="4"/></proof>
<goal name="WP_parameter compose_associative" expl="VC for compose_associative">
<proof prover="3"><result status="valid" time="0.01" steps="7"/></proof>
<goal name="WP_parameter id_neutral" expl="VC for id_neutral">
<proof prover="3"><result status="valid" time="0.01" steps="43"/></proof>
<goal name="WP_parameter compose_const_right" expl="VC for compose_const_right">
<proof prover="3"><result status="valid" time="0.01" steps="6"/></proof>
<goal name="WP_parameter compose_const_left" expl="VC for compose_const_left">
<proof prover="3"><result status="valid" time="0.01" steps="6"/></proof>
<goal name="WP_parameter ho_ite_compose_left" expl="VC for ho_ite_compose_left">
<proof prover="3"><result status="valid" time="0.02" steps="13"/></proof>
<theory name="Bind" sum="052c79c65246d9ae2ba93971e7aa46ab">
<goal name="WP_parameter bfold_identity" expl="VC for bfold_identity">
<proof prover="3"><result status="valid" time="0.04" steps="36"/></proof>
<goal name="WP_parameter bfold_compose" expl="VC for bfold_compose">
<transf name="split_goal_wp">
<goal name="WP_parameter bfold_compose.1" expl="1. assertion">
<transf name="split_goal_wp">
<goal name="WP_parameter bfold_compose.1.1" expl="1. assertion">
<proof prover="3"><result status="valid" time="0.01" steps="31"/></proof>
<goal name="WP_parameter bfold_compose.1.2" expl="2. assertion">
<proof prover="3"><result status="valid" time="0.01" steps="2"/></proof>
<goal name="WP_parameter bfold_compose.1.3" expl="3. assertion">
<proof prover="3"><result status="valid" time="0.02" steps="29"/></proof>
<goal name="WP_parameter bfold_compose.1.4" expl="4. assertion">
<proof prover="3"><result status="valid" time="0.01" steps="2"/></proof>
<goal name="WP_parameter bfold_compose.2" expl="2. postcondition">
<proof prover="2"><result status="valid" time="0.06"/></proof>
<goal name="WP_parameter bfold_constructor" expl="VC for bfold_constructor">
<proof prover="3"><result status="valid" time="0.01" steps="23"/></proof>
<goal name="bmap_compose">
<proof prover="0"><result status="unknown" time="0.84"/></proof>
<proof prover="1"><result status="valid" time="0.09"/></proof>
<proof prover="3"><result status="unknown" time="0.00"/></proof>
<goal name="bmap_id">
<proof prover="0"><result status="valid" time="0.02"/></proof>
<goal name="close_fold">
<proof prover="3"><result status="valid" time="0.01" steps="7"/></proof>
<theory name="Choice" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
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