latte-prelude.prop

Basic definitions and theorems for (intuitionistic) propositional logic. Most natural deduction rules are provided as theorems in this namespace.

<=>

(<=> [A :type] [B :type])
(and (==> A B) (==> B A))

Definition: Logical equivalence or ‘if and only if’.

absurd

(absurd)
(forall [α :type] α)

Definition: Absurdity.

absurd-intro

(absurd-intro [A :type])
(==> A (not A) absurd)

Theorem: Introduction rule for absurdity.

and

(and [A :type] [B :type])
(forall [C :type] (==> (==> A B C) C))

Definition: logical conjunction.

and*

A notation defining an n-ary variant of and, which exploits the fact that conjunction is associative. By default we use the leaf-leaning expansion:

(and* p1 p2 ... pN-1 pN) ≡ (and (and ... (and p1 p2) pN-1) pN)))

We favor this variant because it is often the case that we use conjunction for a form of “subclassing”. Consider some mathematical <object> defined as having some properties (and p1 p2) (e.g. a preorder with reflexivity and transitivity). Then we might “subclass” such an object by considering a supplementary property, i.e. we want (and <object> p3) (e.g. a preorder with antisymetry hence a partial order). This is exactly (and (and p1 p2) p3), and if it is of course isomorphic to the right-leaning version (and p1 (and p2 p3)), only the left variant reflects the “subclassing” aspect.
A right-leaning nary conjunction is provided by r-and*.

and*-arity

(and*-arity def-env ctx and-type)

and-elim*

This is a generic elimination rule for n-ary conjunction (e.g. as introduced by the and* notation). In (and-elim* n and-term) the index n corresponds to the n-th operand of the term.

For example (informally ):

  • (and-elim* 1 (and* a b c)≡(and (and a b) c)) ==> a
  • (and-elim* 2 (and* a b c)) ==> b
  • (and-elim* 3 (and* a b c)) ==> c

Internally, the correct nesting of and-elim-left and and-elim-right is constructed. Errors are raised if the index is incorrect or if the specificied term is not a conjunction.

and-elim-left

(and-elim-left [?A ?B :type] [p (and A B)])

An implicit elimination rule that takes a proof p of type (and A B) and yields a proof of A.

This is an implicit version of and-elim-left-thm.

and-elim-left-thm

(and-elim-left-thm [A :type] [B :type])
(==> (and A B) A)

Theorem: Elimination rule for logical conjunction. This one only keeps the left-side of the conjunction

and-elim-right

(and-elim-right [?A ?B :type] [p (and A B)])

An implicit elimination rule that takes a proof p of type (and A B) and yields a proof of B.

This is an implicit version of and-elim-right-thm.

and-elim-right-thm

(and-elim-right-thm [A :type] [B :type])
(==> (and A B) B)

Theorem: Elimination rule for logical conjunction. This one only keeps the right-side of the conjunction

and-intro

(and-intro [?A ?B :type] [a A] [b B])

An introduction rule that takes a proof a of type A, a proof b of type B and yields a proof of type (and A B).

This is an implicit version of and-intro-thm.

and-intro*

A nary variant of and-intro, the introduction rule for conjunction. It builds a proof of (and* A1 A2 ... AN) from proofs of the Ai’s

and-intro-thm

(and-intro-thm [A :type] [B :type])
(==> A B (and A B))

Theorem: Introduction rule for logical conjunction.

and-sym

(and-sym [?A ?B :type] [p (and A B)])

Symmetry of conjunction. Proves (and B A) from a proof p that (and A B).

This is an implicit version of and-sym-thm.

and-sym-thm

(and-sym-thm [A :type] [B :type])
(==> (and A B) (and B A))

Theorem: Symmetry of conjunction.

and-unparser

(and-unparser term)

build-and-elim

(build-and-elim def-env ctx n and-term and-type)

build-and-intros-left-leaning

(build-and-intros-left-leaning args)

build-and-intros-right-leaning

(build-and-intros-right-leaning args)

build-or-elim*

(build-or-elim* def-env ctx index or-term or-type case-proofs)

build-or-intro

(build-or-intro args)

build-r-and-elim

(build-r-and-elim def-env ctx n and-term and-type)

decompose-and-type

(decompose-and-type def-env ctx t)

decompose-iff-type

(decompose-iff-type def-env ctx t)

decompose-impl-type

(decompose-impl-type def-env ctx t)

decompose-lambda-term

(decompose-lambda-term def-env ctx t)

decompose-or-type

(decompose-or-type def-env ctx t)

elim-path

(elim-path l r n arity)

ex-falso

(ex-falso [A :type])
(==> absurd A)

Theorem: Ex falso sequitur quodlibet (proof by contradiction, elimination for absurdity).

iff-elim-if

Left (if) elimination for <=>, an implicit version of iff-elim-if-thm.

iff-elim-if-thm

(iff-elim-if-thm [A :type] [B :type])
(==> (<=> A B) (==> A B))

Theorem: Elimination rule for logical equivalence. This one only keeps the if part of the equivalence.

iff-elim-only-if

Right (only if) elimination for <=>, an implicit version of iff-elim-only-if-thm.

iff-elim-only-if-thm

(iff-elim-only-if-thm [A :type] [B :type])
(==> (<=> A B) (==> B A))

Theorem: Elimination rule for logical equivalence. This one only keeps the only-if part of the equivalence.

iff-intro

Introduction rule for logical equivalence, an implicit version of iff-intro-thm.

iff-intro-thm

(iff-intro-thm [A :type] [B :type])
(==> (==> A B) (==> B A) (<=> A B))

Theorem: Introduction rule for logical equivalence.

iff-refl

(iff-refl [A :type])
(<=> A A)

Theorem: Reflexivity of logical equivalence.

iff-sym

Symmetry of <=>, an implicit version of iff-sym-thm.

iff-sym-thm

(iff-sym-thm [A :type] [B :type])
(==> (<=> A B) (<=> B A))

Theorem: Symmetry of logical equivalence.

iff-trans

Transitivity of <=>, an implicit version of iff-trans-thm.

iff-trans-thm

(iff-trans-thm [A :type] [B :type] [C :type])
(==> (<=> A B) (<=> B C) (<=> A C))

Theorem: Transitivity of logical equivalence.

impl-ignore

(impl-ignore [A :type] [B :type])
(==> A B A)

Theorem: A variant of reflexivity.

impl-not-not

(impl-not-not [A :type])
(==> A (not (not A)))

Theorem: The if half of double negation.

This can be seen as an introduction rule for ¬¬ (not-not) propositions. Note that double-negation is a law of classical (non-intuitionistic) logic.

impl-refl

(impl-refl [A :type])
(==> A A)

Theorem: Implication is reflexive.

impl-trans

(impl-trans [?A ?B ?C :type] [pA (==> A B)] [pB (==> B C)])

Implication is transitive.

(impl-trans pAB pBC) yields (==> A C) from the proof pAB that (==> A B) and the proof pBC that (==> B C)

cf. impl-trans-thm

impl-trans-thm

(impl-trans-thm [A :type] [B :type] [C :type])
(==> (==> A B) (==> B C) (==> A C))

Theorem: Implication is transitive.

mk-nary-op-left-leaning

(mk-nary-op-left-leaning op args)

A simple utility for creating “left-leaning” n-ary operator calls. Remark: the args are reverted in input.

mk-nary-op-right-leaning

(mk-nary-op-right-leaning op args)

A simple utility for creating “right-leaning” n-ary operator calls.

not

(not [A :type])
(==> A absurd)

Definition: Logical negation.

or

(or [A :type] [B :type])
(forall [C :type] (==> (==> A C) (==> B C) C))

Definition: logical disjunction.

or*

A notation defining an n-ary variant of or, which exploits the fact that disjunction is associative. By convention we have:

(or* p1 p2 ... pN-1 pN) ≡ (or p1 (or p2 (or ... (or pN-1 pN))))

Remark: unlike for conjunction, there is no real motivation to use a left-leaning variant by default, so the simpler right-leaning encoding is prefered.

or-assoc

Associativity of disjunction, an implicit that subsumes both or-assoc-thm and or-assoc-conv-thm.

or-assoc-conv-thm

(or-assoc-conv-thm [A :type] [B :type] [C :type])
(==> (or A (or B C)) (or (or A B) C))

Theorem:

or-assoc-thm

(or-assoc-thm [A :type] [B :type] [C :type])
(==> (or (or A B) C) (or A (or B C)))

Theorem:

or-elim

An elimination rule that takes a proof or-term of type (or A B), a proof left-proof of type (==> A prop), a proof right-proof of type (==> B prop), and thus concludes that prop holds by [[or-elim-thm]].

This is (for now) the easiest rule to use for proof-by-cases.

or-elim*

Elimination rule for n-ary disjunction (or* T1 T2 ... TN).

(or-elim* or-term case1 case2 ... caseN)

is the same thing as the repeated and nested uses of [[or-elim]] for binary disjunction.

or-elim-thm

(or-elim-thm [A :type] [B :type])
(==> (or A B) (forall [C :type] (==> (==> A C) (==> B C) C)))

Theorem: Elimination rule for logical disjunction. This corresponds to a important scheme of reasoning by cases. To prove a proposition C under the assumption (or A B): - first case: assume A and prove C - second case: assume B and prove C

or-intro*

A generic introduction rule for or*. Suppose we have a proof p of a proposition Ai, and suppose also the sequence of types A1,…,Ai,…,An.

Then (or-intro* A1 ... p ... An) is a proof of (or* A1 ... Ai ... An).

or-intro-left

Left introduction for a disjunction (or A B), with proofA a proof of A. This is an implicit version of or-intro-left-thm.

or-intro-left-thm

(or-intro-left-thm [A :type] [B :type])
(==> A (or A B))

Theorem: Introduction rule for logical disjunction. This is the introduction by the left operand.

or-intro-right

Right introduction for a disjunction (or A B), with proofB a proof of B. This is an implicit version of or-intro-left-thm.

or-intro-right-thm

(or-intro-right-thm [A :type] [B :type])
(==> B (or A B))

Theorem: Introduction rule for logical disjunction. This is the introduction by the right operand.

or-not-elim-left

(or-not-elim-left [A :type] [B :type])
(==> (or A B) (not B) A)

Theorem: An elimination rule for disjunction, simpler than or-elim. This eliminates to the left operand.

or-not-elim-right

(or-not-elim-right [A :type] [B :type])
(==> (or A B) (not A) B)

Theorem: An elimination rule for disjunction, simpler than or-elim. This eliminates to the right operand.

or-not-impl-elim

(or-not-impl-elim [A :type] [B :type])
(==> (or A B) (==> (not A) B))

Theorem: An alternative elimination rule for disjunction.

or-sym

Symmetry of disjunction, an implicit version of or-sym-thm.

or-sym-thm

(or-sym-thm [A :type] [B :type])
(==> (or A B) (or B A))

Theorem: Symmetry of disjunction.

or-unparser

(or-unparser term)

r-and*

A notation defining an n-ary variant of and, which exploits the fact that conjunction is associative. This version is the right-leaning variant of and*, which means the following:

(and* p1 p2 ... pN-1 pN) ≡ (and p1 (and p2 (and ... (and pN-1 pN))))

r-and-elim*

This is a generic elimination rule for (right-leaning) n-ary conjunction (e.g. as introduced by the r-and* notation). In (r-and-elim* n r-and-term) the index n corresponds to the n-th operand of the term.

This is the right-leaning version of the default and-elim*.

r-and-intro*

A nary “right-leaning” variant of and-intro, the introduction rule for conjunction. It builds a proof of (r-and* A1 A2 ... AN) from proofs of the Ai’s

Remark: the default “left-leaning” varient is and-intro*.

truth

(truth)
(not absurd)

Definition: Logical truth.

truth-is-true

(truth-is-true)
truth

Theorem: The truth is true (really ?).