latte-sets.quant
Quantifiers over sets (rather than types), with most definitions specialized from latte-prelude.quant.
decompose-exists-in-type
(decompose-exists-in-type def-env ctx t)decompose-forall-in-type
(decompose-forall-in-type def-env ctx t)decompose-single-in-type
(decompose-single-in-type def-env ctx t)ex-in-elim
The elimination rule for the exists-in existential quantifier over a set s (of elements of type T). A typical proof instance is of the form (ex-in-elim ex-proof A-proof) with ex-term a proof of (exists-in [x s] (P x)) and A-proof a proof of (==> (forall-in [x s] (==> (P x) A))). See ex-in-elem-rule.
ex-in-elim-rule
(ex-in-elim-rule [s (set T)] [P (==> T :type)] [A :type])(==> (exists-in [x s] (P x)) (forall-in [y s] (==> (P y) A)) A)
Theorem: Elimination rule for exists-in existentials, a set-theoretic variant of latte-prelude.quant/ex-elim-rule.
ex-in-intro
(ex-in-intro [s (set T)] [P (==> T :type)] [x T])(==> (elem x s) (P x) (exists-in [y s] (P y)))
Theorem: The introduction rule for the exists-in quantifier, cf. latte-prelude.quant/ex-intro-thm.
exists-in
Existential quantification over sets.
(exists-in [x s] (P x)) is a shortcut for (exists [x (element-type-of s)]
(and (elem x s)
(P x))).
forall-in
Universal quantification over sets.
(forall-in [x s] (P x)) is a shortcut for (forall [x (element-type-of s)]
(==> (elem x s)
(P x))).
single-in
(single-in [s (set T)] [P (==> T :type)])(forall-in [x s] (forall-in [y s] (==> (P x) (P y) (equal x y))))
Definition: The constraints that “there exists at most one element of type T in set s such that…”
This is a set-theoretic variant of latte-prelude.quant/single.
single-in-elim
Elimination rule for single-in. (single-in-elim s-proof x y) such that the type of s-proof is (single-in s P) for some property P, then we have (==> (P x) (P y) (equal x y)) thanks to [[single-in-elim-rule]].
single-in-elim-rule
(single-in-elim-rule [s (set T)] [P (==> T :type)] [x T] [y T])(==> (single-in s P) (elem x s) (elem y s) (P x) (P y) (equal x y))
Theorem: Elimination rule for single-in.
single-in-intro
(single-in-intro [s (set T)] [P (==> T :type)])(==>
(forall-in [x s] (forall-in [y s] (==> (P x) (P y) (equal x y))))
(single-in s P))
Theorem: Introduction rule for single-in.
the-element
The unique element descriptor for sets.
(the-element u) defines the unique element of set s satisfying the predicate P. This is provided thanks to the uniqueness proof u (of type (unique-in s P).
This is the set-theoretic version of the latte-prelude.quant/the.
the-element-ax
(the-element-ax [T :type] [s (set T)] [P (==> T :type)] [u (unique-in s P)])T
Axiom: The unique element descriptor axiom.
This is a set-theoretic variant of latte-prelude.quant/the-ax.
the-element-lemma
(the-element-lemma u) proves that (forall-in [y s] (==> (P y) (equal y (the-element u)))) from the proof u that (unique-in s P) for some property P and set s.
the-element-lemma-prop
(the-element-lemma-prop [s (set T)] [P (==> T :type)] [u (unique-in s P)])(forall-in [y s] (==> (P y) (equal y (the-element u))))
Theorem: The unique element … in s is … unique, cf latte-prelude.quand/the-lemma-thm.
the-element-prop
(the-element-prop u) proves (P (the-element u)) from the proof u of (unique-in s P), for some property P and set s. This is the main property of the unique descriptor the-element, cf the-element-prop-ax.
the-element-prop-ax
(the-element-prop-ax [T :type] [s (set T)] [P (==> T :type)] [u (unique-in s P)])(and (elem (the-element u) s) (P (the-element u)))
Axiom: The property of the unique element descriptor, cf. latte-prelude.quant/the-prop-ax.
unique-in
(unique-in [s (set T)] [P (==> T :type)])(and (exists-in [x s] (P x)) (single-in s P))
Definition: The constraint that “there exists a unique element of type T in set s such that …”.
This is a set-theoretic variant of latte-prelude.quant/unique-prop.