Commit ac61df48 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

in progress

parent 39ac5765
...@@ -866,7 +866,7 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES)) ...@@ -866,7 +866,7 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET_FILES = Set COQLIBS_SET_FILES = Set
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES)) COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_MAP_FILES = Map Occ MapPermut MapInjection COQLIBS_MAP_FILES = Map Const Occ MapPermut MapInjection
COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES)) COQLIBS_MAP = $(addprefix lib/coq/map/, $(COQLIBS_MAP_FILES))
COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut COQLIBS_LIST_FILES = List Length Mem Nth NthLength HdTl NthHdTl Append NthLengthAppend Reverse HdTlNoOpt NthNoOpt RevAppend Combine Distinct NumOcc Permut
......
...@@ -282,3 +282,4 @@ intros p1 p2 a b h1. ...@@ -282,3 +282,4 @@ intros p1 p2 a b h1.
apply le_ge_eq. apply le_ge_eq.
split; apply numof_change_any; apply h1. split; apply numof_change_any; apply h1.
Qed. Qed.
...@@ -77,17 +77,13 @@ unfold get, set. ...@@ -77,17 +77,13 @@ unfold get, set.
now case why_decidable_eq. now case why_decidable_eq.
Qed. Qed.
(* Why3 goal *) (* Unused content named const
Definition const: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
b -> (map a b).
intros a a_WT b b_WT y. intros a a_WT b b_WT y.
exact (_map_constr _ _ (fun _ => y)). exact (_map_constr _ _ (fun _ => y)).
Defined. Defined.
*)
(* Why3 goal *) (* Unused content named Const
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).
Proof. Proof.
easy. easy.
Qed. Qed.
*)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2015 -- INRIA - CNRS - Paris-Sud University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
(* This file is generated by Why3's Coq-realize driver *) (* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *) (* Beware! Only edit allowed sections below *)
Require Import BuiltIn. Require Import BuiltIn.
...@@ -59,6 +70,36 @@ exact ((fix nth n l := match l with ...@@ -59,6 +70,36 @@ exact ((fix nth n l := match l with
| cons h t => if Zeq_bool n 0%Z then h else nth (n - 1)%Z t end) i s). | cons h t => if Zeq_bool n 0%Z then h else nth (n - 1)%Z t end) i s).
Defined. Defined.
(* Why3 goal *)
Definition set: forall {a:Type} {a_WT:WhyType a}, (seq a) -> Z -> a -> (seq
a).
admit.
Defined.
(* Why3 goal *)
Lemma set_def1 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
(v:a), ((0%Z <= i)%Z /\ (i < (length s))%Z) -> ((length (set s i
v)) = (length s)).
intros a a_WT s i v (h1,h2).
admit.
Qed.
(* Why3 goal *)
Lemma set_def2 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
(v:a), ((0%Z <= i)%Z /\ (i < (length s))%Z) -> ((get (set s i v) i) = v).
intros a a_WT s i v (h1,h2).
admit.
Qed.
(* Why3 goal *)
Lemma set_def3 : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (i:Z)
(v:a), ((0%Z <= i)%Z /\ (i < (length s))%Z) -> forall (j:Z),
((0%Z <= j)%Z /\ (j < (length s))%Z) -> ((~ (j = i)) -> ((get (set s i v)
j) = (get s j))).
intros a a_WT s i v (h1,h2) j (h3,h4) h5.
admit.
Qed.
(* Why3 assumption *) (* Why3 assumption *)
Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(seq a)) (s2:(seq Definition infix_eqeq {a:Type} {a_WT:WhyType a} (s1:(seq a)) (s2:(seq
a)): Prop := ((length s1) = (length s2)) /\ forall (i:Z), ((0%Z <= i)%Z /\ a)): Prop := ((length s1) = (length s2)) /\ forall (i:Z), ((0%Z <= i)%Z /\
...@@ -179,6 +220,7 @@ Lemma snoc_get : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (x:a) ...@@ -179,6 +220,7 @@ Lemma snoc_get : forall {a:Type} {a_WT:WhyType a}, forall (s:(seq a)) (x:a)
(i:Z), ((0%Z <= i)%Z /\ (i <= (length s))%Z) -> (((i < (length s))%Z -> (i:Z), ((0%Z <= i)%Z /\ (i <= (length s))%Z) -> (((i < (length s))%Z ->
((get (snoc s x) i) = (get s i))) /\ ((~ (i < (length s))%Z) -> ((get (snoc s x) i) = (get s i))) /\ ((~ (i < (length s))%Z) ->
((get (snoc s x) i) = x))). ((get (snoc s x) i) = x))).
admit.
(* (*
intros a a_WT (l, d) x i (h1,h2). intros a a_WT (l, d) x i (h1,h2).
split; intros. split; intros.
...@@ -200,9 +242,8 @@ subst i. ...@@ -200,9 +242,8 @@ subst i.
rewrite (Zabs2Nat.id (Datatypes.length l)). omega. rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
subst i. subst i.
rewrite (Zabs2Nat.id (Datatypes.length l)). omega. rewrite (Zabs2Nat.id (Datatypes.length l)). omega.
Qed.
*) *)
Admitted. (* TODO *) Qed.
(* Why3 goal *) (* Why3 goal *)
Definition mixfix_lb_dtdt_rb: forall {a:Type} {a_WT:WhyType a}, (seq a) -> Definition mixfix_lb_dtdt_rb: forall {a:Type} {a_WT:WhyType a}, (seq a) ->
...@@ -242,14 +283,14 @@ Defined. ...@@ -242,14 +283,14 @@ Defined.
Lemma concat_length : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a)) Lemma concat_length : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
(s2:(seq a)), ((length (infix_plpl s1 (s2:(seq a)), ((length (infix_plpl s1
s2)) = ((length s1) + (length s2))%Z). s2)) = ((length s1) + (length s2))%Z).
admit.
(* (*
intros a a_WT s1 s2. intros a a_WT s1 s2.
unfold length, infix_plpl. unfold length, infix_plpl.
rewrite List.app_length. rewrite List.app_length.
rewrite Nat2Z.inj_add. auto. rewrite Nat2Z.inj_add. auto.
Qed.
*) *)
Admitted. (* TODO *) Qed.
(* Why3 goal *) (* Why3 goal *)
Lemma concat_get1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a)) Lemma concat_get1 : forall {a:Type} {a_WT:WhyType a}, forall (s1:(seq a))
......
...@@ -49,11 +49,17 @@ module Array ...@@ -49,11 +49,17 @@ module Array
= if i < 0 || i >= length a then raise OutOfBounds; = if i < 0 || i >= length a then raise OutOfBounds;
a[i] <- v a[i] <- v
function make (n: int) (v: ~'a) : array 'a = function make (n: int) (v: ~'a) : array 'a
{ length = n; elts = M.const v } axiom make_length:
forall n:int, v:'a. length (make n v) = n
axiom make_elts:
forall n i:int, v:'a. get (make n v) i = v
val make (n: int) (v: ~'a) : array 'a val make (n: int) (v: ~'a) : array 'a
requires { "expl:array creation size" n >= 0 } ensures { result = make n v } requires { "expl:array creation size" n >= 0 }
ensures { length result = n }
ensures { forall i:int. result[i] = v }
val append (a1: array ~'a) (a2: array 'a) : array 'a val append (a1: array ~'a) (a2: array 'a) : array 'a
ensures { length result = length a1 + length a2 } ensures { length result = length a1 + length a2 }
......
...@@ -28,6 +28,13 @@ theory Map ...@@ -28,6 +28,13 @@ theory Map
forall b : 'b [m[a1 <- b][a2]]. forall b : 'b [m[a1 <- b][a2]].
a1 <> a2 -> m[a1 <- b][a2] = m[a2] a1 <> a2 -> m[a1 <- b][a2] = m[a2]
end
theory Const
use import Map
function const ~'b : map 'a 'b function const ~'b : map 'a 'b
axiom Const : forall b:'b, a:'a. (const b)[a] = b axiom Const : forall b:'b, a:'a. (const b)[a] = b
...@@ -239,4 +246,3 @@ theory MapParam ...@@ -239,4 +246,3 @@ theory MapParam
end end
*) *)
...@@ -339,6 +339,7 @@ end ...@@ -339,6 +339,7 @@ end
theory SetMap theory SetMap
use import map.Map use import map.Map
use import map.Const
use import bool.Bool use import bool.Bool
type set 'a = map 'a bool type set 'a = map 'a bool
......
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