Commit 6546c95d authored by MARCHE Claude's avatar MARCHE Claude

Fixed small problems with settheory

parent 3fa07edb
......@@ -887,7 +887,8 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_SETTHEORY_FILES = Interval PowerSet Relation Identity Image InverseDomRan Function
COQLIBS_SETTHEORY_FILES = Interval PowerSet Relation Identity Image \
InverseDomRan Function Sequence
COQLIBS_SETTHEORY = $(addprefix lib/coq/settheory/, $(COQLIBS_SETTHEORY_FILES))
ifeq (@enable_coq_fp_libs@,yes)
......@@ -942,7 +943,7 @@ install_no_local::
mkdir -p $(LIBDIR)/why3/coq/set
cp $(addsuffix .vo, $(COQLIBS_SET)) $(LIBDIR)/why3/coq/set/
mkdir -p $(LIBDIR)/why3/coq/settheory
cp $(addsuffix .vo, $(COQLIBS_SETTHEORY_FILES)) $(LIBDIR)/why3/coq/settheory/
cp $(addsuffix .vo, $(COQLIBS_SETTHEORY)) $(LIBDIR)/why3/coq/settheory/
ifeq (@enable_coq_fp_libs@,yes)
mkdir -p $(LIBDIR)/why3/coq/floating_point
cp $(addsuffix .vo, $(COQLIBS_FP)) $(LIBDIR)/why3/coq/floating_point/
......@@ -1301,7 +1302,8 @@ STDLIBS = algebra \
option \
real \
relations \
set \
# function ? sum ? tptp ?
STDMODS = arith array hashtbl impset pqueue queue random ref stack string
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require set.Set.
Require settheory.Interval.
Require settheory.Relation.
Require settheory.InverseDomRan.
Require settheory.Function.
Require settheory.Identity.
Import set.Set.
Open Scope Z_scope.
(* Why3 assumption *)
Definition seq_length {a:Type} {a_WT:WhyType a}(n:Z) (s:(set.Set.set
a)): (set.Set.set (set.Set.set (Z* a)%type)) :=
(settheory.Function.infix_mnmngt ( 1%Z n) s).
(* Why3 goal *)
Definition seq: forall {a:Type} {a_WT:WhyType a}, (set.Set.set a) ->
(set.Set.set (set.Set.set (Z* a)%type)).
intros a a_WT s.
exact (fun f => exists n:Z, 0 <= n /\ mem f (seq_length n s)).
(* Why3 goal *)
Definition size: forall {a:Type} {a_WT:WhyType a}, (set.Set.set (Z*
a)%type) -> Z.
(* Why3 goal *)
Lemma mem_seq : forall {a:Type} {a_WT:WhyType a}, forall (s:(set.Set.set a))
(r:(set.Set.set (Z* a)%type)), (set.Set.mem r (seq s)) <->
((0%Z <= (size r))%Z /\ (set.Set.mem r (seq_length (size r) s))).
intros a a_WT s r.
(* Why3 goal *)
Lemma seq_as_total_function : forall {a:Type} {a_WT:WhyType a},
forall (s:(set.Set.set a)) (r:(set.Set.set (Z* a)%type)), (set.Set.mem r
(seq s)) -> (set.Set.mem r
(settheory.Function.infix_mnmngt ( 1%Z (size r)) s)).
intros a a_WT s r h1.
(* Why3 goal *)
Lemma size_def : forall {a:Type} {a_WT:WhyType a}, forall (n:Z)
(r:(set.Set.set (Z* a)%type)), ((size r) = n) <-> exists s:(set.Set.set a),
(set.Set.mem r (seq_length n s)).
intros a a_WT n r.
(* Unused content named mem_seq_length
intros a a_WT n s.
......@@ -235,6 +235,12 @@ theory Identity
(** {2 Sequences}
Finite sequences as total functions on domain 1..n
theory Sequence
......@@ -242,10 +248,8 @@ theory Sequence
use import Interval
use import Identity
function seq_length int (set 'a) : set (rel int 'a)
axiom mem_seq_length : forall n:int, s:set 'a.
seq_length n s == ((mk 1 n) --> s)
function seq_length (n:int) (s : set 'a) : set (rel int 'a) =
(mk 1 n) --> s
function seq (set 'a) : set (rel int 'a)
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment