Maj terminée. Pour consulter la release notes associée voici le lien :

### update sessions

parent 7497d447
This source diff could not be displayed because it is too large. You can view the blob instead.
 name="examples/programs/algo64/why3session.xml" shape_version="2">
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
 ... ... @@ -72,6 +72,10 @@ Definition get1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z): a := Definition set1 {a:Type} {a_WT:WhyType a}(a1:(array a)) (i:Z) (v:a): (array a) := (mk_array (length a1) (set (elts a1) i v)). (* Why3 assumption *) Definition make {a:Type} {a_WT:WhyType a}(n:Z) (v:a): (array a) := (mk_array n (const v:(map Z a))). Parameter n: Z. Axiom n_nonneg : (0%Z < n)%Z. ... ... @@ -99,21 +103,21 @@ Theorem WP_parameter_distance : (0%Z <= n)%Z -> ((((0%Z < 0%Z)%Z \/ (0%Z = 0%Z)) /\ (0%Z < n)%Z) -> forall (g:(map Z Z)), (g = (set (const 0%Z:(map Z Z)) 0%Z (-1%Z)%Z)) -> ((0%Z <= n)%Z -> (((1%Z < (n - 1%Z)%Z)%Z \/ (1%Z = (n - 1%Z)%Z)) -> forall (count:Z) (d:(map Z Z)) (g1:(map Z Z)), (((get d 0%Z) = 0%Z) /\ (((get g1 0%Z) = (-1%Z)%Z) /\ ((((count + (get d Z Z)) (g1:(map Z Z)), (((((get d 0%Z) = 0%Z) /\ (((get g1 0%Z) = (-1%Z)%Z) /\ (((count + (get d (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z))%Z < (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z)%Z \/ ((count + (get d (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z))%Z = (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z)) /\ ((forall (k:Z), ((0%Z < k)%Z /\ (k < ((n - 1%Z)%Z + 1%Z)%Z)%Z) -> (((((get g1 (get g1 k)) < (f k))%Z /\ (((f k) < (get g1 k))%Z \/ ((f k) = (get g1 k)))) /\ ((get g1 k) < k)%Z) /\ ((((0%Z < (get d k))%Z \/ (0%Z = (get d k))) /\ ((get d k) = ((get d (get g1 k)) + 1%Z)%Z)) /\ forall (k':Z), (((get g1 k) < k')%Z /\ (k' < k)%Z) -> ((get d (get g1 k)) < (get d k'))%Z))) /\ forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\ (k < ((n - 1%Z)%Z + 1%Z)%Z)%Z) -> (path (get d k) k))))) -> ((count < n)%Z -> forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\ (k < n)%Z) -> forall (d':Z), (path d' k) -> ((get d k) <= d')%Z)))). intros h1 (h2,h3) g h4 h5 h6 count d g1 (h7,(h8,(h9,(h10,h11)))) h12 k (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z))%Z = (((n - 1%Z)%Z + 1%Z)%Z - 1%Z)%Z)))) /\ forall (k:Z), ((0%Z < k)%Z /\ (k < ((n - 1%Z)%Z + 1%Z)%Z)%Z) -> (((((get g1 (get g1 k)) < (f k))%Z /\ (((f k) < (get g1 k))%Z \/ ((f k) = (get g1 k)))) /\ ((get g1 k) < k)%Z) /\ (((0%Z < (get d k))%Z /\ ((get d k) = ((get d (get g1 k)) + 1%Z)%Z)) /\ forall (k':Z), (((get g1 k) < k')%Z /\ (k' < k)%Z) -> ((get d (get g1 k)) < (get d k'))%Z))) /\ forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\ (k < ((n - 1%Z)%Z + 1%Z)%Z)%Z) -> (path (get d k) k)) -> ((count < n)%Z -> forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\ (k < n)%Z) -> forall (d':Z), (path d' k) -> ((get d k) <= d')%Z)))). intros h1 (h2,h3) g h4 h5 h6 count d g1 (((h7,(h8,h9)),h10),h11) h12 k (h13,h14) d' h15. clear h1 h2. clear h5 h6. ... ...
This diff is collapsed.
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Definition unit := unit. Parameter mark : Type. Require Import BuiltIn. Require BuiltIn. Require int.Int. Require int.MinMax. Parameter at1: forall (a:Type), a -> mark -> a. (* Why3 assumption *) Definition unit := unit. Implicit Arguments at1. (* Why3 assumption *) Inductive list (a:Type) {a_WT:WhyType a} := | Nil : list a | Cons : a -> (list a) -> list a. Axiom list_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (list a). Existing Instance list_WhyType. Implicit Arguments Nil [[a] [a_WT]]. Implicit Arguments Cons [[a] [a_WT]]. Parameter old: forall (a:Type), a -> a. (* Why3 assumption *) Fixpoint length {a:Type} {a_WT:WhyType a}(l:(list a)) {struct l}: Z := match l with | Nil => 0%Z | (Cons _ r) => (1%Z + (length r))%Z end. Implicit Arguments old. Axiom Length_nonnegative : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Max_is_ge : forall (x:Z) (y:Z), (x <= (Zmax x y))%Z /\ (y <= (Zmax x y))%Z. Axiom Length_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil :(list a))). Axiom Max_is_some : forall (x:Z) (y:Z), ((Zmax x y) = x) \/ ((Zmax x y) = y). Axiom char : Type. Parameter char_WhyType : WhyType char. Existing Instance char_WhyType. Axiom Min_is_le : forall (x:Z) (y:Z), ((Zmin x y) <= x)%Z /\ ((Zmin x y) <= y)%Z. (* Why3 assumption *) Definition word := (list char). Axiom Min_is_some : forall (x:Z) (y:Z), ((Zmin x y) = x) \/ ((Zmin x y) = y). (* Why3 assumption *) Inductive dist : (list char) -> (list char) -> Z -> Prop := | dist_eps : (dist (Nil :(list char)) (Nil :(list char)) 0%Z) | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z) | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z) | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n). Axiom Max_x : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = x). (* Why3 assumption *) Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1 w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z. Axiom Max_y : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmax x y) = y). (* Why3 assumption *) Fixpoint infix_plpl {a:Type} {a_WT:WhyType a}(l1:(list a)) (l2:(list a)) {struct l1}: (list a) := match l1 with | Nil => l2 | (Cons x1 r1) => (Cons x1 (infix_plpl r1 l2)) end. Axiom Min_x : forall (x:Z) (y:Z), (x <= y)%Z -> ((Zmin x y) = x). Axiom Append_assoc : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)) (l3:(list a)), ((infix_plpl l1 (infix_plpl l2 l3)) = (infix_plpl (infix_plpl l1 l2) l3)). Axiom Min_y : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = y). Axiom Append_l_nil : forall {a:Type} {a_WT:WhyType a}, forall (l:(list a)), ((infix_plpl l (Nil :(list a))) = l). Axiom Max_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmax x y) = (Zmax y x)). Axiom Append_length : forall {a:Type} {a_WT:WhyType a}, forall (l1:(list a)) (l2:(list a)), ((length (infix_plpl l1 l2)) = ((length l1) + (length l2))%Z). Axiom Min_sym : forall (x:Z) (y:Z), (y <= x)%Z -> ((Zmin x y) = (Zmin y x)). (* Why3 assumption *) Fixpoint mem {a:Type} {a_WT:WhyType a}(x:a) (l:(list a)) {struct l}: Prop := match l with | Nil => False | (Cons y r) => (x = y) \/ (mem x r) end. Inductive list (a:Type) := | Nil : list a | Cons : a -> (list a) -> list a. Set Contextual Implicit. Implicit Arguments Nil. Unset Contextual Implicit. Implicit Arguments Cons. Axiom mem_append : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l1:(list a)) (l2:(list a)), (mem x (infix_plpl l1 l2)) <-> ((mem x l1) \/ (mem x l2)). Parameter length: forall (a:Type), (list a) -> Z. Axiom mem_decomp : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (l:(list a)), (mem x l) -> exists l1:(list a), exists l2:(list a), (l = (infix_plpl l1 (Cons x l2))). Implicit Arguments length. (* Why3 assumption *) Fixpoint last_char(a:char) (u:(list char)) {struct u}: char := match u with | Nil => a | (Cons c u') => (last_char c u') end. Axiom length_def : forall (a:Type), forall (l:(list a)), match l with | Nil => ((length l) = 0%Z) | Cons _ r => ((length l) = (1%Z + (length r))%Z) (* Why3 assumption *) Fixpoint but_last(a:char) (u:(list char)) {struct u}: (list char) := match u with | Nil => (Nil :(list char)) | (Cons c u') => (Cons a (but_last c u')) end. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom first_last_explicit : forall (u:(list char)) (a:char), ((infix_plpl (but_last a u) (Cons (last_char a u) (Nil :(list char)))) = (Cons a u)). Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Axiom first_last : forall (a:char) (u:(list char)), exists v:(list char), exists b:char, ((infix_plpl v (Cons b (Nil :(list char)))) = (Cons a u)) /\ ((length v) = (length u)). Parameter char : Type. Axiom key_lemma_right : forall (w1:(list char)) (w'2:(list char)) (m:Z) (a:char), (dist w1 w'2 m) -> forall (w2:(list char)), (w'2 = (Cons a w2)) -> exists u1:(list char), exists v1:(list char), exists k:Z, (w1 = (infix_plpl u1 v1)) /\ ((dist v1 w2 k) /\ ((k + (length u1))%Z <= (m + 1%Z)%Z)%Z). Definition word := (list char). Axiom dist_symetry : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> (dist w2 w1 n). Inductive dist : (list char) -> (list char) -> Z -> Prop := | dist_eps : (dist (Nil:(list char)) (Nil:(list char)) 0%Z) | dist_add_left : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist (Cons a w1) w2 (n + 1%Z)%Z) | dist_add_right : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist w1 (Cons a w2) (n + 1%Z)%Z) | dist_context : forall (w1:(list char)) (w2:(list char)) (n:Z), (dist w1 w2 n) -> forall (a:char), (dist (Cons a w1) (Cons a w2) n). Axiom key_lemma_left : forall (w1:(list char)) (w2:(list char)) (m:Z) (a:char), (dist (Cons a w1) w2 m) -> exists u2:(list char), exists v2:(list char), exists k:Z, (w2 = (infix_plpl u2 v2)) /\ ((dist w1 v2 k) /\ ((k + (length u2))%Z <= (m + 1%Z)%Z)%Z). Definition min_dist(w1:(list char)) (w2:(list char)) (n:Z): Prop := (dist w1 w2 n) /\ forall (m:Z), (dist w1 w2 m) -> (n <= m)%Z. Axiom dist_concat_left : forall (u:(list char)) (v:(list char)) (w:(list char)) (n:Z), (dist v w n) -> (dist (infix_plpl u v) w ((length u) + n)%Z). Axiom dist_concat_right : forall (u:(list char)) (v:(list char)) (w:(list char)) (n:Z), (dist v w n) -> (dist v (infix_plpl u w) ((length u) + n)%Z). Axiom min_dist_equal : forall (w1:(list char)) (w2:(list char)) (a:char) (n:Z), (min_dist w1 w2 n) -> (min_dist (Cons a w1) (Cons a w2) n). ... ... @@ -85,79 +136,85 @@ Axiom min_dist_diff : forall (w1:(list char)) (w2:(list char)) (a:char) ((Zmin m p) + 1%Z)%Z))). Axiom min_dist_eps : forall (w:(list char)) (a:char) (n:Z), (min_dist w (Nil:(list char)) n) -> (min_dist (Cons a w) (Nil:(list char)) (Nil :(list char)) n) -> (min_dist (Cons a w) (Nil :(list char)) (n + 1%Z)%Z). Axiom min_dist_eps_length : forall (w:(list char)), (min_dist (Nil:(list Axiom min_dist_eps_length : forall (w:(list char)), (min_dist (Nil :(list char)) w (length w)). Inductive ref (a:Type) := (* Why3 assumption *) Inductive ref (a:Type) {a_WT:WhyType a} := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | mk_ref contents1 => contents1 Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a). Existing Instance ref_WhyType. Implicit Arguments mk_ref [[a] [a_WT]]. (* Why3 assumption *) Definition contents {a:Type} {a_WT:WhyType a}(v:(ref a)): a := match v with | (mk_ref x) => x end. Implicit Arguments contents. Parameter map : forall (a:Type) (b:Type), Type. Axiom map : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, Type. Parameter map_WhyType : forall (a:Type) {a_WT:WhyType a} (b:Type) {b_WT:WhyType b}, WhyType (map a b). Existing Instance map_WhyType. Parameter get: forall (a:Type) (b:Type), (map a b) -> a -> b. Parameter get: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b. Implicit Arguments get. Parameter set: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b}, (map a b) -> a -> b -> (map a b). Parameter set: forall (a:Type) (b:Type), (map a b) -> a -> b -> (map a b). Axiom 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). Implicit Arguments set. Axiom 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)). Axiom Select_eq : forall (a:Type) (b:Type), forall (m:(map a b)), forall (a1:a) (a2:a), forall (b1:b), (a1 = a2) -> ((get (set m a1 b1) a2) = b1). Parameter const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},