Commit 37ff1dfb by MARCHE Claude

### Stdlib: more lemmas on sets

parent a652866a
 ... ... @@ -2,8 +2,8 @@ theory ConvexSet use import int.Int use import real.RealInfix use export int.Int use export real.RealInfix type pt = { x : real ; y : real } ... ... @@ -14,29 +14,139 @@ 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 lemma knuth1: forall p1 p2 p3:pt. turns_left p1 p2 p3 -> turns_left p2 p3 p1 lemma knuth2: forall p1 p2 p3:pt. turns_left p1 p2 p3 -> not (turns_left p2 p1 p3) lemma knuth4: forall p1 p2 p3 p4:pt. turns_left p1 p2 p4 -> turns_left p2 p3 p4 -> turns_left p3 p1 p4 -> turns_left p1 p2 p3 lemma knuth5: forall p1 p2 p3 p4 p5:pt. turns_left p1 p2 p3 -> turns_left p1 p2 p4 -> turns_left p1 p2 p5 -> turns_left p3 p2 p4 -> turns_left p4 p2 p5 -> turns_left p3 p2 p5 lemma knuth3: forall p1 p2 p3:pt. not (colinear p1 p2 p3) -> turns_left p1 p2 p3 \/ turns_left p1 p3 p2 (* test: p1 = (0,0), p2 = (1,0) p3 = (1,1) *) 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 = length p in predicate is_inside_convex_hull (p:pt) (pa:path) = let l = length pa in forall i:int. 0 <= i < l -> let i' = if i = l-1 then 0 else i+1 in let p0 = nth i pa in let p1 = nth i' pa in turns_left p0 p1 p predicate is_ccw_convex (pa:path) = let l = length pa in forall i:int. 0 <= i < l -> let i' = if i = l-1 then 0 else i+1 in let p0 = nth i p in let p1 = nth i' p in let p0 = nth i pa in let p1 = nth i' pa in forall j:int. 0 <= j < l /\ j <> i /\ j <> i' -> turns_left p0 p1 (nth j p) turns_left p0 p1 (nth j pa) end module Incremental end module Jarvis (* on calcule le point p d'ordonnee minimale, et d'abscisse minimale parmi ceux-ci on recherche le point q minimum pour la relation R x y = turns_left p x y p0 = p p1 = q si q = p0: fini sinon recommencer avec p := q *) use import ConvexSet use import set.Fset use import ref.Ref predicate lower (p q:pt) = p.y <. q.y \/ (p.y = q.y /\ p.x <=. q.x) let lowest_pt (s:set pt) : (pt, set pt) requires { not (is_empty s) } ensures { let (p,r) = result in s = add p r /\ forall q:pt. mem q r -> lower p q } = let p = ref (choose s) in let r = ref (remove !p s) in while not (is_empty !r) do invariant { mem !p s } invariant { subset !r s } invariant { forall q:pt. mem q s /\ not (mem q !r) -> lower !p q } let q = choose !r in if lower q !p then p := q; r := remove q !r done; (!p,remove !p s) (* let rightest_pt (p:pt) (s:set pt) : (pt, set pt) requires { not (is_empty s) } ensures { let (p,r) = result in s = add p r /\ forall q:pt. mem q r -> lower p q } = let p = ref (choose s) in let r = ref (remove !p s) in while not (is_empty !r) do invariant { mem !p s } invariant { subset !r s } invariant { forall q:pt. mem q s /\ not (mem q !r) -> lower !p q } let q = choose !r in if lower q !p then p := q; r := remove q !r done; (!p,remove !p s) let jarvis (s:set pt) : list pt = let p0 = lowest_pt s in *) end module Graham ... ... @@ -46,8 +156,14 @@ use import ConvexSet (* let convex_hull (l:path) : path = (* all pts of the result are points of the input *) ensures { forall p:pt. List.mem p result -> List.mem p l } (* the output forms a ccw convex circuit *) ensures { is_ccw_convex result } (* all pt of the input are inside the convex hull of the output *) ensures { forall p:pt. List.mem p l /\ not List.mem p result -> is_inside_convex_hull p result } let min,rem = find_minimum_pt l in let sorted = sorted_increasing_angle min rem in match sorted with ... ...
This diff is collapsed.
 ... ... @@ -3,6 +3,8 @@ Require Import BuiltIn. Require BuiltIn. Global Instance list_WhyType : forall T {T_WT : WhyType T}, WhyType (list T). split. apply nil. ... ...
 ... ... @@ -26,14 +26,14 @@ Qed. (* Why3 goal *) Definition get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b. (@map a a_WT b b_WT) -> a -> b. intros a a_WT b b_WT (m) x. exact (m x). Defined. (* Why3 goal *) Definition set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b -> (map a b). (@map a a_WT b b_WT) -> a -> b -> (@map a a_WT b b_WT). intros a a_WT b b_WT (m) x y. split. intros x'. ... ... @@ -44,8 +44,8 @@ Defined. (* Why3 goal *) Lemma Select_eq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1). forall (m:(@map a a_WT b b_WT)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1). Proof. intros a a_WT b b_WT (m) a1 a2 b1 h1. unfold get, set. ... ... @@ -54,8 +54,9 @@ Qed. (* Why3 goal *) Lemma Select_neq : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). {b:Type} {b_WT:WhyType b}, forall (m:(@map a a_WT b b_WT)), forall (a1:a) (a2:a), forall (b1:b), (~ (a1 = a2)) -> ((get (set m a1 b1) a2) = (get m a2)). Proof. intros a a_WT b b_WT (m) a1 a2 b1 h1. unfold get, set. ... ... @@ -64,14 +65,14 @@ Qed. (* Why3 goal *) Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, b -> (map a b). b -> (@map a a_WT b b_WT). intros a a_WT b b_WT y. exact (_map_constr _ _ (fun _ => y)). Defined. (* Why3 goal *) Lemma Const : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, forall (b1:b) (a1:a), ((get (const b1:(map a b)) a1) = b1). forall (b1:b) (a1:a), ((get (const b1:(@map a a_WT b b_WT)) a1) = b1). Proof. easy. Qed. ... ...
 ... ... @@ -6,15 +6,15 @@ Require int.Int. Require map.Map. (* Why3 assumption *) Definition exchange {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) (i:Z) (j:Z): Prop := ((map.Map.get a1 Definition exchange {a:Type} {a_WT:WhyType a} (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (i:Z) (j:Z): Prop := ((map.Map.get a1 i) = (map.Map.get a2 j)) /\ (((map.Map.get a2 i) = (map.Map.get a1 j)) /\ forall (k:Z), ((~ (k = i)) /\ ~ (k = j)) -> ((map.Map.get a1 k) = (map.Map.get a2 k))). (* Why3 goal *) Lemma exchange_set : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z a)), forall (i:Z) (j:Z), (exchange a1 forall (a1:(@map.Map.map Z _ a a_WT)), forall (i:Z) (j:Z), (exchange a1 (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) i j). Proof. ... ... @@ -32,25 +32,27 @@ now rewrite 2!Map.Select_neq by now apply sym_not_eq. Qed. (* Why3 assumption *) Inductive permut_sub{a:Type} {a_WT:WhyType a} : (map.Map.map Z a) -> (map.Map.map Z a) -> Z -> Z -> Prop := | permut_refl : forall (a1:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a1 l u) | permut_sym : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> (permut_sub a2 a1 l u) | permut_trans : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)) (a3:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> ((permut_sub a2 a3 l u) -> (permut_sub a1 a3 l u)) | permut_exchange : forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> (permut_sub a1 a2 l u))). Inductive permut_sub {a:Type} {a_WT:WhyType a} : (@map.Map.map Z _ a a_WT) -> (@map.Map.map Z _ a a_WT) -> Z -> Z -> Prop := | permut_refl : forall (a1:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), ((@permut_sub _ _) a1 a1 l u) | permut_sym : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), ((@permut_sub _ _) a1 a2 l u) -> ((@permut_sub _ _) a2 a1 l u) | permut_trans : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)) (a3:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), ((@permut_sub _ _) a1 a2 l u) -> (((@permut_sub _ _) a2 a3 l u) -> ((@permut_sub _ _) a1 a3 l u)) | permut_exchange : forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> ((exchange a1 a2 i j) -> ((@permut_sub _ _) a1 a2 l u))). (* Why3 goal *) Lemma permut_weakening : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l1:Z) (r1:Z) (l2:Z) (r2:Z), (((l1 <= l2)%Z /\ (l2 <= r2)%Z) /\ (r2 <= r1)%Z) -> ((permut_sub a1 a2 l2 r2) -> (permut_sub a1 a2 l1 r1)). Proof. intros a a_WT a1 a2 l1 r1 l2 r2 ((h1,h2),h3) h4. induction h4. ... ... @@ -66,10 +68,10 @@ omega. Qed. (* Why3 goal *) Lemma permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2 i) = (map.Map.get a1 i)). Lemma permut_eq : forall {a:Type} {a_WT:WhyType a}, forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((i < l)%Z \/ (u <= i)%Z) -> ((map.Map.get a2 i) = (map.Map.get a1 i)). Proof. intros a a_WT a1 a2 l u h1 i h2. induction h1. ... ... @@ -85,9 +87,9 @@ Qed. (* Why3 goal *) Lemma permut_exists : forall {a:Type} {a_WT:WhyType a}, forall (a1:(map.Map.map Z a)) (a2:(map.Map.map Z a)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a2 forall (a1:(@map.Map.map Z _ a a_WT)) (a2:(@map.Map.map Z _ a a_WT)), forall (l:Z) (u:Z), (permut_sub a1 a2 l u) -> forall (i:Z), ((l <= i)%Z /\ (i < u)%Z) -> exists j:Z, ((l <= j)%Z /\ (j < u)%Z) /\ ((map.Map.get a2 i) = (map.Map.get a1 j)). Proof. intros a a_WT a1 a2 l u h1 i Hi. ... ...
 ... ... @@ -3,6 +3,8 @@ Require Import BuiltIn. Require BuiltIn. Global Instance option_WhyType : forall T {T_WT : WhyType T}, WhyType (option T). split. apply @None. ... ...