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.