Commit 3c3019a6 authored by Martin Clochard's avatar Martin Clochard

examples/in_progress: add old verified prover development

parent 03436ae5
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
module Choice
use import HighOrd
(* no why3 type is empty. *)
constant default : 'a
(* Axiom of choice : we can explicitely pick an element whom
existence is proven. *)
function choice (p:pred 'a) : 'a
axiom choice_behaviour : forall p:pred 'a,x:'a.
p x -> p (choice p)
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="3">
<file
name="../Choice.mlw"
verified="true"
expanded="true">
<theory
name="Choice"
locfile="../Choice.mlw"
loclnum="2" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
</theory>
</file>
</why3session>
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
module Func
use export HighOrd
predicate extensionalEqual (f g:func 'a 'b) =
forall x:'a. f x = g x
(* Assume extensionality of function. *)
axiom functionExtensionality : forall f g:func 'a 'b.
extensionalEqual f g -> f = g
(* Mainly for use in whyml *)
function eval (f:func 'a 'b) (x:'a) : 'b = f x
(* Abstraction definition axiom :
update (f:func 'a 'b) (x:'a) (y:'b) : func 'a 'b =
(\ z:'a. if x = z then y else f z) *)
function update (f:func 'a ~'b) (x:'a) (y:'b) : func 'a 'b
axiom update_def : forall f:func 'a 'b,x:'a,y:'b,z:'a.
update f x y z = if x = z then y else f z
function ([<-])(f:func 'a 'b) (x:'a) (y:'b) : func 'a 'b = update f x y
lemma update_eq : forall f:func 'a 'b,x:'a,y:'b.
update f x y x = y
lemma update_neq : forall f:func 'a 'b,x:'a,y:'b,z:'a.
x <> z -> update f x y z = f z
(* Abstraction definition axiom :
constant identity : func 'a 'a = (\ x:'a. x) *)
constant identity : func 'a 'a
axiom identity_def : forall x:'a. identity x = x
(* Abstraction definition axiom :
function compose (g:func 'b 'c) (f:func 'a 'b) : func 'a 'c =
(\ x:'a. g (f x)) *)
function compose (g:func 'b 'c) (f:func 'a 'b) : func 'a 'c
axiom compose_def : forall g:func 'b 'c,f:func 'a 'b,x:'a.
compose g f x = g (f x)
function rcompose (f:func 'a 'b) (g:func 'b 'c) : func 'a 'c = compose g f
let lemma compose_associative (h:func 'c 'd) (g:func 'b 'c) (f:func 'a 'b) : unit
ensures { compose (compose h g) f = compose h (compose g f) }
=
assert { extensionalEqual (compose (compose h g) f) (compose h (compose g f)) }
let lemma identity_neutral (f:func 'a 'b) : unit
ensures { compose f identity = f }
ensures { compose identity f = f }
=
assert { extensionalEqual (compose f identity) f } ;
assert { extensionalEqual (compose identity f) f }
(* Abstraction definition axiom :
function const (x:'b) : func 'a 'b =
(\ z:'a.x) *)
function const (x: ~'b) : func 'a 'b
axiom const_def : forall x:'b,z:'a. const x z = x
let lemma const_compose_left (f:func 'a 'b) (x:'c) : unit
ensures { compose (const x) f = const x }
=
assert { extensionalEqual (const x) (compose (const x) f) }
let lemma const_compose_right (f:func 'a 'b) (x:'a) : unit
ensures { compose f (const x) = (const (f x):func 'c 'b) }
=
assert { extensionalEqual (const (f x) : func 'c 'b) (compose f (const x)) }
end
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
(* non-negative integers. For mutual induction using size variant. *)
module Nat
use import int.Int
type nat = ONat | SNat nat
function nat_to_int (n:nat) : int = match n with
| ONat -> 0 | SNat n -> 1 + nat_to_int n end
function add_nat (n1 n2:nat) : nat = match n1 with
| ONat -> n2 | SNat n1 -> SNat (add_nat n1 n2) end
let rec lemma nat_to_int_nonnegative (n:nat) : unit
ensures { nat_to_int n >= 0 }
variant { n }
=
match n with ONat -> () | SNat n -> nat_to_int_nonnegative n end
let rec lemma add_nat_simulate_add_int (n1 n2:nat) : unit
ensures { nat_to_int (add_nat n1 n2) = nat_to_int n1 + nat_to_int n2 }
variant { n1 }
=
match n1 with ONat -> () | SNat n1 -> add_nat_simulate_add_int n1 n2 end
constant one_nat : nat = SNat ONat
lemma one_nat_value : nat_to_int one_nat = 1
end
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
theory Sum
type sum 'a 'b =
| Left 'a
| Right 'b
end
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
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