Commit 48ab8464 by Jean-Christophe Filliâtre

### updated proof sessions

parent 5307d60a
 ... ... @@ -5,7 +5,7 @@ ... ... @@ -19,39 +19,39 @@ ... ...
 (* This file is generated by Why3's Coq driver *) (* Beware! Only edit allowed sections below *) Require Import ZArith. Require Import Rbase. Require Import ZOdiv. Require Import Zdiv. Definition unit := unit. Parameter mark : Type. Parameter at1: forall (a:Type), a -> mark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. Axiom Abs_pos : forall (x:Z), (0%Z <= (Zabs x))%Z. Axiom Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (ZOdiv x y))%Z + (ZOmod x y))%Z). Axiom Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (ZOdiv x y))%Z /\ ((ZOdiv x y) <= x)%Z). Axiom Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (((-(Zabs y))%Z < (ZOmod x y))%Z /\ ((ZOmod x y) < (Zabs y))%Z). Axiom Div_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> (0%Z <= (ZOdiv x y))%Z. Axiom Div_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ (0%Z < y)%Z) -> ((ZOdiv x y) <= 0%Z)%Z. Axiom Mod_sign_pos : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ ~ (y = 0%Z)) -> (0%Z <= (ZOmod x y))%Z. Axiom Mod_sign_neg : forall (x:Z) (y:Z), ((x <= 0%Z)%Z /\ ~ (y = 0%Z)) -> ((ZOmod x y) <= 0%Z)%Z. Axiom Rounds_toward_zero : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((Zabs ((ZOdiv x y) * y)%Z) <= (Zabs x))%Z. Axiom Div_1 : forall (x:Z), ((ZOdiv x 1%Z) = x). Axiom Mod_1 : forall (x:Z), ((ZOmod x 1%Z) = 0%Z). Axiom Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZOdiv x y) = 0%Z). Axiom Mod_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((ZOmod x y) = x). Axiom Div_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> ((ZOdiv ((x * y)%Z + z)%Z x) = (y + (ZOdiv z x))%Z). Axiom Mod_mult : forall (x:Z) (y:Z) (z:Z), ((0%Z < x)%Z /\ ((0%Z <= y)%Z /\ (0%Z <= z)%Z)) -> ((ZOmod ((x * y)%Z + z)%Z x) = (ZOmod z x)). Definition divides(a:Z) (b:Z): Prop := exists q:Z, (b = (q * a)%Z). Axiom Divides_x_zero : forall (x:Z), (divides x 0%Z). Axiom Divides_one_x : forall (x:Z), (divides 1%Z x). Definition gcd(a:Z) (b:Z) (g:Z): Prop := (divides g a) /\ ((divides g b) /\ forall (x:Z), (divides x a) -> ((divides x b) -> (divides x g))). Axiom Gcd_sym : forall (a:Z) (b:Z) (g:Z), (gcd a b g) -> (gcd b a g). Axiom Gcd_0 : forall (a:Z), (gcd a 0%Z a). Axiom Gcd_euclid : forall (a:Z) (b:Z) (q:Z) (g:Z), (gcd a (b - (q * a)%Z)%Z g) -> (gcd a b g). Axiom Gcd_computer_mod : forall (a:Z) (b:Z) (g:Z), (~ (b = 0%Z)) -> ((gcd a (ZOmod a b) g) -> (gcd a b g)). Axiom Div_mod1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (Zdiv x y))%Z + (Zmod x y))%Z). Axiom Div_bound1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> ((0%Z <= (Zdiv x y))%Z /\ ((Zdiv x y) <= x)%Z). Axiom Mod_bound1 : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (Zmod x y))%Z /\ ((Zmod x y) < (Zabs y))%Z). Axiom Mod_11 : forall (x:Z), ((Zmod x 1%Z) = 0%Z). Axiom Div_11 : forall (x:Z), ((Zdiv x 1%Z) = x). Axiom Gcd_euclidean_mod : forall (a:Z) (b:Z) (g:Z), (~ (b = 0%Z)) -> ((gcd a (Zmod a b) g) -> (gcd a b g)). Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | mk_ref contents1 => contents1 end. Implicit Arguments contents. Theorem WP_parameter_gcd : forall (x:Z), forall (y:Z), ((0%Z <= x)%Z /\ (0%Z <= y)%Z) -> forall (d:Z), forall (c:Z), forall (b:Z), forall (a:Z), forall (y1:Z), forall (x1:Z), ((0%Z <= x1)%Z /\ ((0%Z <= y1)%Z /\ ((forall (d1:Z), (gcd x1 y1 d1) -> (gcd x y d1)) /\ ((((a * x)%Z + (b * y)%Z)%Z = x1) /\ (((c * x)%Z + (d * y)%Z)%Z = y1))))) -> ((0%Z < y1)%Z -> forall (x2:Z), (x2 = y1) -> forall (y2:Z), (y2 = (ZOmod x1 y1)) -> forall (a1:Z), (a1 = c) -> forall (b1:Z), (b1 = d) -> forall (c1:Z), (c1 = (a - (c * (ZOdiv x1 y1))%Z)%Z) -> forall (d1:Z), (d1 = (b - (d * (ZOdiv x1 y1))%Z)%Z) -> forall (d2:Z), (gcd x2 y2 d2) -> (gcd x y d2)). (* YOU MAY EDIT THE PROOF BELOW *) intuition. apply H4. subst x2 y2. apply Gcd_sym. apply Gcd_euclid with (q:=(ZOdiv x1 y1)). assert (x1 - (ZOdiv x1 y1) * y1 = ZOmod x1 y1)%Z. generalize (Div_mod x1 y1); intuition. replace ((ZOdiv x1 y1) * y1) with (y1 * (ZOdiv x1 y1)) by ring. omega. rewrite H6; assumption. Qed. (* DO NOT EDIT BELOW *)
 ... ... @@ -62,9 +53,9 @@ ... ...
 ... ... @@ -3,19 +3,19 @@ ... ... @@ -23,31 +23,31 @@ ... ...
 ... ... @@ -3,43 +3,43 @@ ... ...
 (* 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. Parameter at1: forall (a:Type), a -> mark -> a. Implicit Arguments at1. Parameter old: forall (a:Type), a -> a. Implicit Arguments old. 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. Parameter length: forall (a:Type), (list a) -> Z. Implicit Arguments length. 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) end. Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)), (0%Z <= (length l))%Z. Axiom Length_nil : forall (a:Type), forall (l:(list a)), ((length l) = 0%Z) <-> (l = (Nil:(list a))). Inductive option (a:Type) := | None : option a | Some : a -> option a. Set Contextual Implicit. Implicit Arguments None. Unset Contextual Implicit. Implicit Arguments Some. Parameter nth: forall (a:Type), Z -> (list a) -> (option a). Implicit Arguments nth. Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)), match l with | Nil => ((nth n l) = (None:(option a))) | Cons x r => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) -> ((nth n l) = (nth (n - 1%Z)%Z r))) end. Definition zero_at(l:(list Z)) (i:Z): Prop := ((nth i l) = (Some 0%Z)) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j l) = (Some 0%Z)). Definition no_zero(l:(list Z)): Prop := forall (j:Z), ((0%Z <= j)%Z /\ (j < (length l))%Z) -> ~ ((nth j l) = (Some 0%Z)). Inductive ref (a:Type) := | mk_ref : a -> ref a. Implicit Arguments mk_ref. Definition contents (a:Type)(u:(ref a)): a := match u with | mk_ref contents1 => contents1 end. Implicit Arguments contents. Definition hd (a:Type)(l:(list a)): (option a) := match l with | Nil => (None:(option a)) | Cons h _ => (Some h) end. Implicit Arguments hd. Definition tl (a:Type)(l:(list a)): (option (list a)) := match l with | Nil => (None:(option (list a))) | Cons _ t => (Some t) end. Implicit Arguments tl. Theorem WP_parameter_search_loop : forall (l:(list Z)), forall (s:(list Z)), forall (i:Z), ((0%Z <= i)%Z /\ (((i + (length s))%Z = (length l)) /\ ((forall (j:Z), (0%Z <= j)%Z -> ((nth j s) = (nth (i + j)%Z l))) /\ forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j l) = (Some 0%Z))))) -> ((~ (s = (Nil:(list Z)))) -> ((~ (s = (Nil:(list Z)))) -> forall (result:Z), (match s with | Nil => (None:(option Z)) | Cons h _ => (Some h) end = (Some result)) -> ((result = 0%Z) -> ((((0%Z <= i)%Z /\ (i < (length l))%Z) /\ (zero_at l i)) \/ ((i = (length l)) /\ (no_zero l)))))). (* YOU MAY EDIT THE PROOF BELOW *) intuition. destruct s. discriminate H4. injection H4; intros; subst; clear H4. clear H0 H1. left. split. rewrite (length_def _ (Cons 0%Z s)) in H. generalize (Length_nonnegative _ s). omega. red; intuition. assert (H0: (0 <= 0)%Z) by omega. generalize (H3 0%Z H0). generalize (nth_def _ 0%Z (Cons 0%Z s)). ring_simplify (i+0)%Z. intuition. rewrite H4 in H1. auto. Qed. (* DO NOT EDIT BELOW *)
 (* 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.