Commit a652866a authored by MARCHE Claude's avatar MARCHE Claude

Fixed new example convex_hull

parent 66e37945
......@@ -2,16 +2,17 @@
theory ConvexSet
use import real.Real
use import int.Int
use import real.RealInfix
type pt = { x : real ; y : real }
function crossproduct (p1 p2 p3:pt) : real =
(p2.x - p1.x) * (p3.y - p1.y) - (p3.x - p1.x) * (p2.y - p1.y)
(p2.x -. p1.x) *. (p3.y -. p1.y) -. (p3.x -. p1.x) *. (p2.y -. p1.y)
predicate colinear (p1 p2 p3:pt) = crossproduct p1 p2 p3 = 0.0
predicate turns_left (p1 p2 p3:pt) = crossproduct p1 p2 p3 > 0.0
predicate turns_left (p1 p2 p3:pt) = crossproduct p1 p2 p3 >. 0.0
(* test: p1 = (0,0), p2 = (1,0) p3 = (1,1) *)
......@@ -19,17 +20,19 @@ goal test1 :
turns_left {x=0.0;y=0.0} {x=1.0;y=0.0} {x=1.0;y=1.0}
use import list.List
use import list.Length
use import list.NthNoOpt
type path = list pt
predicate is_ccw_convex (p:path) =
let l = List.length p in
let l = length p in
forall i:int. 0 <= i < l ->
let i' = if i = l-1 then 0 else i+1 in
let p0 = List.nth p i in
let p1 = List.nth p i' in
let p0 = nth i p in
let p1 = nth i' p in
forall j:int. 0 <= j < l /\ j <> i /\ j <> i' ->
turns_left p0 p1 (List.nth p j)
turns_left p0 p1 (nth j 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="2">
<prover
id="0"
name="Alt-Ergo"
version="0.95.1"/>
<file
name="../convex_hull.mlw"
verified="true"
expanded="true">
<theory
name="ConvexSet"
locfile="../convex_hull.mlw"
loclnum="3" loccnumb="7" loccnume="16"
verified="true"
expanded="true">
<goal
name="test1"
locfile="../convex_hull.mlw"
loclnum="19" loccnumb="5" loccnume="10"
sum="c9d9f8369aae9598819ebfa27b05e177"
proved="true"
expanded="true"
shape="aturns_leftamk ptc0.0c0.0amk ptc1.0c0.0amk ptc1.0c1.0">
<proof
prover="0"
timelimit="60"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
</theory>
<theory
name="Graham"
locfile="../convex_hull.mlw"
loclnum="42" loccnumb="7" loccnume="13"
verified="true"
expanded="true">
</theory>
</file>
</why3session>
......@@ -72,6 +72,19 @@ theory Nth
end
theory NthNoOpt
use export List
use import int.Int
function nth (n: int) (l: list 'a) : 'a
axiom nth_cons_0: forall x:'a, r:list 'a. nth 0 (Cons x r) = x
axiom nth_cons_n: forall x:'a, r:list 'a, n:int.
n > 0 -> nth n (Cons x r) = nth (n-1) r
end
theory NthLength
use export Nth
......
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