Skip to content

GitLab

Commit 3c0b61f8 authored by MARCHE Claude's avatar MARCHE Claude
Browse files
Options

moved set theory and its realizations into Bware repository

parent f3a91eff
Hide whitespace changes
Inline Side-by-side
Showing with 11 additions and 1188 deletions
.gitignore
View file @ 3c0b61f8
......@@ -204,3 +204,4 @@ pvsbin/
/src/jessie/config.status
/src/jessie/Makefile
/src/jessie/ptests_local_config.ml
/src/jessie/tests/basic/result/*.log
\ No newline at end of file
Makefile.in
View file @ 3c0b61f8
......@@ -848,17 +848,13 @@ COQLIBS_NUMBER = $(addprefix lib/coq/number/, $(COQLIBS_NUMBER_FILES))
COQLIBS_SET_FILES = Set
COQLIBS_SET = $(addprefix lib/coq/set/, $(COQLIBS_SET_FILES))
COQLIBS_SETTHEORY_FILES = Interval PowerSet Relation Identity Image \
InverseDomRan Function
COQLIBS_SETTHEORY = $(addprefix lib/coq/settheory/, $(COQLIBS_SETTHEORY_FILES))
ifeq (@enable_coq_fp_libs@,yes)
COQLIBS_FP_FILES = Rounding SingleFormat Single DoubleFormat Double
COQLIBS_FP_ALL_FILES = GenFloat $(COQLIBS_FP_FILES)
COQLIBS_FP = $(addprefix lib/coq/floating_point/, $(COQLIBS_FP_ALL_FILES))
endif
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_SETTHEORY) $(COQLIBS_FP)
COQLIBS_FILES = lib/coq/BuiltIn $(COQLIBS_INT) $(COQLIBS_REAL) $(COQLIBS_NUMBER) $(COQLIBS_SET) $(COQLIBS_FP)
COQV = $(addsuffix .v, $(COQLIBS_FILES))
COQVO = $(addsuffix .vo, $(COQLIBS_FILES))
......@@ -884,8 +880,6 @@ drivers/coq-realizations.aux: Makefile
echo 'theory number.'"$$f"' meta "realized_theory" "number.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_SET_FILES); do \
echo 'theory set.'"$$f"' meta "realized_theory" "set.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_SETTHEORY_FILES); do \
echo 'theory settheory.'"$$f"' meta "realized_theory" "settheory.'"$$f"'", "" end'; done; \
for f in $(COQLIBS_FP_FILES); do \
echo 'theory floating_point.'"$$f"' meta "realized_theory" "floating_point.'"$$f"'", "" end'; done; \
) > $@
......@@ -903,8 +897,6 @@ install_no_local::
cp $(addsuffix .vo, $(COQLIBS_NUMBER)) $(LIBDIR)/why3/coq/number/
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)) $(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/
......@@ -924,7 +916,7 @@ depend: $(COQVD)
clean::
rm -f $(COQVO) $(COQVD) $(addsuffix .glob, $(COQLIBS_FILES))
update-coq: update-coq-int update-coq-real update-coq-number update-coq-set update-coq-settheory update-coq-fp
update-coq: update-coq-int update-coq-real update-coq-number update-coq-set update-coq-fp
update-coq-int: bin/why3 drivers/coq-realizations.aux theories/int.why
for f in $(COQLIBS_INT_ALL_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T int.$$f -o lib/coq/int/; done
......@@ -938,9 +930,6 @@ update-coq-number: bin/why3 drivers/coq-realizations.aux theories/number.why
update-coq-set: bin/why3 drivers/coq-realizations.aux theories/set.why
for f in $(COQLIBS_SET_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T set.$$f -o lib/coq/set/; done
update-coq-settheory: bin/why3 drivers/coq-realizations.aux theories/settheory.why
for f in $(COQLIBS_SETTHEORY_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T settheory.$$f -o lib/coq/settheory/; done
update-coq-fp: bin/why3 drivers/coq-realizations.aux theories/floating_point.why
for f in $(COQLIBS_FP_FILES); do WHY3CONFIG="" bin/why3.@OCAMLBEST@ --realize -L theories -D drivers/coq-realize.drv -T floating_point.$$f -o lib/coq/floating_point/; done
......@@ -1293,8 +1282,7 @@ STDLIBS = algebra \
option \
real \
relations \
set \
settheory
set
# function ? sum ? tptp ?
STDMODS = arith array hashtbl impset pqueue queue random ref stack string
......
Version
View file @ 3c0b61f8
# Why version
VERSION=0.73+git
VERSION=0.80
......
doc/intro.tex
View file @ 3c0b61f8
......@@ -22,7 +22,7 @@ extended with
%\item Hilbert's epsilon construct
\end{itemize}
\todo{continue}
% \todo{continue}
\section{Organization of this document}
......
doc/macros.tex
View file @ 3c0b61f8
\newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
% \newcommand{\todo}[1]{{\Huge\bfseries TODO: #1}}
\newcommand{\why}{\textsf{Why3}\xspace}
\newcommand{\whyml}{\textsf{WhyML}\xspace}
......
doc/manual.tex
View file @ 3c0b61f8
......@@ -91,7 +91,7 @@
\vfill
\todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
% \todo{NE PAS DISTRIBUER TANT QU'IL RESTE DES TODOS}
%BEGIN LATEX
\begin{LARGE}
......@@ -121,15 +121,15 @@
\begin{flushleft}
\begin{tabular}{l}
$^1$ LRI, CNRS, Univ Paris-Sud, Orsay, F-91405 \\
$^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
$^1$ LRI, CNRS \& University Paris-Sud, Orsay, F-91405 \\
$^2$ Inria Saclay -- \^Ile-de-France, Palaiseau, F-91120
\end{tabular}
%BEGIN LATEX
\bigskip
%END LATEX
\textcopyright 2010-2012 Univ Paris-Sud, CNRS, Inria
\textcopyright 2010-2012 University Paris-Sud, CNRS, Inria
\urldef{\urlutcat}{\url}{http://frama-c.cea.fr/u3cat}
\urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
......
lib/coq/settheory/Function.v deleted 100644 → 0
View file @ f3a91eff
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require set.Set.
Require settheory.Relation.
Require settheory.InverseDomRan.
Import set.Set.
Import settheory.InverseDomRan.
(* Why3 goal *)
Definition infix_plmngt: forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, (set.Set.set a) -> (set.Set.set b) ->
(set.Set.set (set.Set.set (a* b)%type)).
intros a a_WT b b_WT s t.
exact (fun r => subset (dom r) s /\ subset (ran r) t /\
forall x y1 y2, mem (x,y1) r /\ mem (x,y2) r ->
y1 = y2).
Defined.
(* Why3 goal *)
Lemma mem_function : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)), (set.Set.mem f (infix_plmngt s
t)) <-> ((forall (x:a) (y:b), (set.Set.mem (x, y) f) -> ((set.Set.mem x
s) /\ (set.Set.mem y t))) /\ forall (x:a) (y1:b) (y2:b), ((set.Set.mem (x,
y1) f) /\ (set.Set.mem (x, y2) f)) -> (y1 = y2)).
intros a a_WT b b_WT f s t.
unfold infix_plmngt, mem.
unfold dom, ran.
unfold subset.
unfold mem.
split.
intros (h1 & h2 & h3).
split; auto.
intros x y h.
split.
apply h1.
now exists y.
apply h2.
now exists x.
intros (h1 & h2).
split.
intros x (y,h).
generalize (h1 x y h); tauto.
split.
intros y (x,h).
generalize (h1 x y h); tauto.
assumption.
Qed.
(* Why3 goal *)
Lemma domain_function : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)) (x:a) (y:b), (set.Set.mem f
(infix_plmngt s t)) -> ((set.Set.mem (x, y) f) -> (set.Set.mem x s)).
intros a a_WT b b_WT f s t x y (h1 & _) h4.
apply h1.
apply dom_def.
now exists y.
Qed.
(* Why3 goal *)
Lemma range_function : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)) (x:a) (y:b), (set.Set.mem f
(infix_plmngt s t)) -> ((set.Set.mem (x, y) f) -> (set.Set.mem y t)).
intros a a_WT b b_WT f s t x y h1 h2.
apply h1.
apply ran_def.
now exists x.
Qed.
(* Why3 goal *)
Lemma function_extend_range : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)) (u:(set.Set.set b)),
(set.Set.subset t u) -> ((set.Set.mem f (infix_plmngt s t)) ->
(set.Set.mem f (infix_plmngt s u))).
intros a a_WT b b_WT f s t u h1 h2.
unfold infix_plmngt, mem in *.
intuition.
now apply subset_trans with t.
Qed.
(* Why3 goal *)
Lemma function_reduce_range : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)) (u:(set.Set.set b)),
(set.Set.subset u t) -> ((set.Set.mem f (infix_plmngt s t)) ->
((forall (x:a) (y:b), (set.Set.mem (x, y) f) -> (set.Set.mem y u)) ->
(set.Set.mem f (infix_plmngt s u)))).
intros a a_WT b b_WT f s t u h1 h2 h3.
unfold infix_plmngt, mem in *.
intuition.
unfold subset.
intros y h.
destruct h as (x,h).
unfold ran, mem in h.
unfold mem; now apply h3 with (x:=x).
Qed.
(* Why3 goal *)
Definition infix_mnmngt: forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, (set.Set.set a) -> (set.Set.set b) ->
(set.Set.set (set.Set.set (a* b)%type)).
intros a a_WT b b_WT s t.
exact (fun f => mem f (infix_plmngt s t) /\ dom f = s).
Defined.
(* Why3 goal *)
Lemma mem_total_functions : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)), (set.Set.mem f (infix_mnmngt s
t)) <-> ((set.Set.mem f (infix_plmngt s t)) /\
((settheory.InverseDomRan.dom f) = s)).
intros a a_WT b b_WT f s t.
unfold infix_mnmngt, mem.
intuition.
Qed.
(* Why3 goal *)
Lemma total_function_is_function : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)), (set.Set.mem f (infix_mnmngt s
t)) -> (set.Set.mem f (infix_plmngt s t)).
intros a a_WT b b_WT f s t h1.
unfold infix_mnmngt, mem in h1.
unfold mem; tauto.
Qed.
(* Why3 goal *)
Lemma singleton_is_function : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (x:a) (y:b), (set.Set.mem (set.Set.add (
x, y) (set.Set.empty :(set.Set.set (a* b)%type)))
(infix_mnmngt (set.Set.add x (set.Set.empty :(set.Set.set a)))
(set.Set.add y (set.Set.empty :(set.Set.set b))))).
intros a a_WT b b_WT x y.
rewrite mem_total_functions.
split.
rewrite mem_function.
split.
intros x' y'.
repeat rewrite set.Set.add_def1.
(*
repeat rewrite set.Set.mem_empty.
Anomaly: unknown meta ?1230. Please report.
*)
intuition; inversion H0; auto.
intros x0 y1 y2.
repeat rewrite set.Set.add_def1.
intuition; inversion H; inversion H0; auto.
rewrite dom_add.
rewrite dom_empty; auto.
Qed.
Require Import ClassicalEpsilon.
(* Why3 goal *)
Definition apply: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(set.Set.set (a* b)%type) -> a -> b.
intros a a_WT b b_WT f x.
assert (i: inhabited b) by (apply inhabits; assumption).
exact (epsilon i (fun y:b => mem x (dom f) -> mem (x,y) f)).
Defined.
(* Why3 goal *)
Lemma apply_def0 : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)) (a1:a), ((set.Set.mem f
(infix_plmngt s t)) /\ (set.Set.mem a1 (settheory.InverseDomRan.dom f))) ->
(set.Set.mem (a1, (apply f a1)) f).
intros a a_WT b b_WT f s t a1 (h1,h2).
unfold apply.
unfold mem.
unfold mem in h2.
generalize h2.
apply epsilon_spec.
destruct (classic (dom f a1)).
destruct H as (x, h).
exists x.
intro.
apply h.
exists b_WT.
tauto.
Qed.
(* Why3 goal *)
Lemma apply_def1 : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)) (a1:a), ((set.Set.mem f
(infix_mnmngt s t)) /\ (set.Set.mem a1 s)) -> (set.Set.mem (a1, (apply f
a1)) f).
intros a a_WT b b_WT f s t a1 (h1 & h2).
eapply apply_def0.
split.
apply total_function_is_function; eauto.
destruct h1.
subst s; auto.
Qed.
(* Why3 goal *)
Lemma apply_def2 : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (f:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set b)) (a1:a) (b1:b), ((set.Set.mem f
(infix_plmngt s t)) /\ (set.Set.mem (a1, b1) f)) -> ((apply f a1) = b1).
intros a a_WT b b_WT f s t a1 b1 (h1,h2).
generalize h1; intro h1'.
rewrite mem_function in h1.
destruct h1 as (_ & h).
apply h with (x:=a1).
split; auto.
eapply apply_def0; split.
eauto.
rewrite dom_def.
exists b1; auto.
Qed.
(* Why3 goal *)
Lemma injection : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (f:(set.Set.set (a* b)%type)) (s:(set.Set.set a)) (t:(set.Set.set
b)), forall (x:a) (y:a), (set.Set.mem f (infix_mnmngt s t)) ->
((set.Set.mem (settheory.InverseDomRan.inverse f) (infix_plmngt t s)) ->
((set.Set.mem x s) -> ((set.Set.mem y s) -> (((apply f x) = (apply f y)) ->
(x = y))))).
intros a a_WT b b_WT f s t x y h1 h2 h3 h4 h5.
destruct h2 as (h6 & h7 & h8).
apply h8 with (apply f x).
split.
unfold inverse, mem.
apply apply_def1 with s t; tauto.
rewrite h5.
unfold inverse, mem.
apply apply_def1 with s t; tauto.
Qed.
(* Why3 goal *)
Lemma apply_singleton : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (x:a) (y:b), ((apply (set.Set.add (x, y)
(set.Set.empty :(set.Set.set (a* b)%type))) x) = y).
intros a a_WT b b_WT x y.
rewrite apply_def2 with (s:=(add x empty))
(t:=(add y empty)) (b1 := y); auto.
split.
apply total_function_is_function.
apply singleton_is_function.
apply add_def1; auto.
Qed.
(* Why3 goal *)
Definition semicolon: forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b} {c:Type} {c_WT:WhyType c}, (set.Set.set (a*
b)%type) -> (set.Set.set (b* c)%type) -> (set.Set.set (a* c)%type).
intros a a_WT b b_WT c c_WT f g.
exact (fun p => match p with
(x,z) => exists y:b, f (x,y) /\ g (y,z) end).
Defined.
(* Why3 goal *)
Lemma semicolon_def : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b} {c:Type} {c_WT:WhyType c}, forall (x:a) (z:c)
(p:(set.Set.set (a* b)%type)) (q:(set.Set.set (b* c)%type)), (set.Set.mem (
x, z) (semicolon p q)) <-> exists y:b, (set.Set.mem (x, y) p) /\
(set.Set.mem (y, z) q).
intros a a_WT b b_WT c c_WT x z p q.
tauto.
Qed.
(* Why3 goal *)
Lemma semicolon_is_function : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b} {c:Type} {c_WT:WhyType c}, forall (f:(set.Set.set
(a* b)%type)) (g:(set.Set.set (b* c)%type)) (s:(set.Set.set a))
(t:(set.Set.set b)) (u:(set.Set.set c)), ((set.Set.mem f (infix_plmngt s
t)) /\ (set.Set.mem g (infix_plmngt t u))) -> (set.Set.mem (semicolon f g)
(infix_plmngt s u)).
intros a a_WT b b_WT c c_WT f g s t u ((f1&f2&f3),(g1&g2&g3)).
rewrite mem_function.
split.
intros x z (y & h1 & h2).
split.
apply f1; exists y; auto.
apply g2; exists y; auto.
intros x y1 y2 ((h1&h2&h3)&(i1&i2&i3)).
eapply g3.
split. apply h3.
assert (h1=i1).
eapply f3.
split. apply h2. apply i2.
subst i1.
apply i3.
Qed.
(* Why3 goal *)
Lemma apply_compose : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b} {c:Type} {c_WT:WhyType c}, forall (x:a)
(f:(set.Set.set (a* b)%type)) (g:(set.Set.set (b* c)%type)) (s:(set.Set.set
a)) (t:(set.Set.set b)) (u:(set.Set.set c)), ((set.Set.mem f
(infix_plmngt s t)) /\ ((set.Set.mem g (infix_plmngt t u)) /\
((set.Set.mem x (settheory.InverseDomRan.dom f)) /\ (set.Set.mem (apply f
x) (settheory.InverseDomRan.dom g))))) -> ((apply (semicolon f g)
x) = (apply g (apply f x))).
intros a a_WT b b_WT c c_WT x f g s t u (h1 & h2 & h3 & h4).
eapply apply_def2.
split.
eapply semicolon_is_function.
split; eauto.
rewrite semicolon_def.
exists (apply f x).
split.
eapply apply_def0.
split.
eauto.
assumption.
eapply apply_def0.
split.
eauto.
assumption.
Qed.
lib/coq/settheory/Identity.v deleted 100644 → 0
View file @ f3a91eff
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require set.Set.
Require settheory.Relation.
Require settheory.InverseDomRan.
Require settheory.Function.
Import set.Set.
(* Why3 goal *)
Definition id: forall {a:Type} {a_WT:WhyType a}, (set.Set.set a) ->
(set.Set.set (a* a)%type).
intros a a_WT s.
exact (fun p => match p with (x,y) => s x /\ x=y end).
Defined.
(* Why3 goal *)
Lemma id_def : forall {a:Type} {a_WT:WhyType a}, forall (x:a) (y:a)
(s:(set.Set.set a)), (set.Set.mem (x, y) (id s)) <-> ((set.Set.mem x s) /\
(x = y)).
intros a a_WT x y s.
unfold id, mem; tauto.
Qed.
Import settheory.InverseDomRan.
(* Why3 goal *)
Lemma id_dom : forall {a:Type} {a_WT:WhyType a}, forall (s:(set.Set.set a)),
((settheory.InverseDomRan.dom (id s)) = s).
intros a a_WT s.
apply predicate_extensionality.
unfold id, dom, mem; split.
unfold mem.
intros (y, (h1, h2)); auto.
unfold mem.
intro h.
exists x; tauto.
Qed.
(* Why3 goal *)
Lemma id_ran : forall {a:Type} {a_WT:WhyType a}, forall (s:(set.Set.set a)),
((settheory.InverseDomRan.ran (id s)) = s).
intros a a_WT s.
apply predicate_extensionality.
unfold id, ran, mem; split.
unfold mem.
intros (y, (h1, h2)); subst; auto.
unfold mem.
intro h.
exists x; tauto.
Qed.
(* Why3 goal *)
Lemma id_fun : forall {a:Type} {a_WT:WhyType a}, forall (s:(set.Set.set a)),
(set.Set.mem (id s) (settheory.Function.infix_plmngt s s)).
intros a a_WT s.
unfold Function.infix_plmngt, mem.
split.
rewrite id_dom.
apply subset_refl.
split.
rewrite id_ran.
apply subset_refl.
unfold id; intuition.
subst; auto.
Qed.
(* Why3 goal *)
Lemma id_total_fun : forall {a:Type} {a_WT:WhyType a}, forall (s:(set.Set.set
a)), (set.Set.mem (id s) (settheory.Function.infix_mnmngt s s)).
intros a a_WT s.
unfold Function.infix_mnmngt, mem.
split.
apply id_fun.
apply id_dom.
Qed.
lib/coq/settheory/Image.v deleted 100644 → 0
View file @ f3a91eff
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
Require set.Set.
Require settheory.Relation.
Import set.Set.
(* Why3 goal *)
Definition image: forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
(set.Set.set (a* b)%type) -> (set.Set.set a) -> (set.Set.set b).
intros a a_WT b b_WT r s.
exact (fun y => exists x:a, mem x s /\ mem (x,y) r).
Defined.
(* Why3 goal *)
Lemma mem_image : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (r:(set.Set.set (a* b)%type)) (dom:(set.Set.set a)) (y:b),
(set.Set.mem y (image r dom)) <-> exists x:a, (set.Set.mem x dom) /\
(set.Set.mem (x, y) r).
intros a a_WT b b_WT r dom y.
unfold image, mem; intuition.
Qed.
(* Why3 goal *)
Lemma image_union : forall {a:Type} {a_WT:WhyType a}
{b:Type} {b_WT:WhyType b}, forall (r:(set.Set.set (a* b)%type))
(s:(set.Set.set a)) (t:(set.Set.set a)), ((image r (set.Set.union s
t)) = (set.Set.union (image r s) (image r t))).
intros a a_WT b b_WT r s t.
apply predicate_extensionality; intros y.
unfold image, union, mem.
split.
intros (x, ([h1 | h2] & h3)).
left; exists x; auto.
right; exists x; auto.
intros [(x, h) | (x, h)]; exists x; intuition.
Qed.
(* Why3 goal *)
Lemma image_add : forall {a:Type} {a_WT:WhyType a} {b:Type} {b_WT:WhyType b},
forall (r:(set.Set.set (a* b)%type)) (dom:(set.Set.set a)) (x:a), ((image r
(set.Set.add x dom)) = (set.Set.union (image r (set.Set.add x
(set.Set.empty :(set.Set.set a)))) (image r dom))).