Skip to content
Snippets Groups Projects
Commit 16c86135 authored by ComFreek's avatar ComFreek
Browse files

add missing equality ND rules

parent 60fb75d5
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 97 additions and 74 deletions
source/math.mmt
+ 97
− 74
View file @ 16c86135
......@@ -13,84 +13,84 @@ theory Metadata =
/T We define a formal language for basic mathematical objects in LF. ❚
theory Subtyping =
include ☞http://gl.mathhub.info/MMT/LFX/Subtyping?LFSubtyped ❙
include ☞http://gl.mathhub.info/MMT/LFX/Subtyping?LFSubtyped ❙
❚
/T First, some logic. ❚
theory Logic : http://gl.mathhub.info/MMT/LFX/TypedHierarchy?LFHierarchy =
include ☞http://gl.mathhub.info/MMT/LFX/Records?LFRecords ❙
include ☞http://cds.omdoc.org/urtheories?Ded ❙
include ☞http://gl.mathhub.info/MMT/LFX/Subtyping?LFWithVariance ❙
// rule rules?ApplyRule ❙
/T the type of booleans, i.e., all formulas are represented as terms of LF-type $prop$ ❙
// bool : type ❘ // = BOOL ❙
prop : type ❘ @ bool ❘ = BOOL ❙
/T one LF-type for each formula holding its proofs
For example, the LF type ⊦ 0 ≐ 1 is empty because that formula has no proofs.
Axioms are declared as constants of the corresponding type, e.g., a constant of type $⊦ true$ for the axiom of truth.❙
ded : prop ⟶ type ❘ # ⊦ 1 prec -500 ❘ role Judgment ❘ = DED ❙
ImplicitProof : {A} ⊦ A ❘ # ImplicitProof 1 ❙
rule lf?TermIrrelevanceRule (ded) ([A : prop] ImplicitProof A) ❙
/T Equality on terms. The type A is left implicit and can be inferred by MMT ❙
eq : {A:𝒰 100} A ⟶ A ⟶ bool ❘ # 2 ≐ 3 prec -5 ❘ role Eq ❘ // = EQUAL ❙
// coercion : {A : type, P : A ⟶ prop,a} ⊦ P a ⟶ ⟨ A | ([x] ⊦ P x) ⟩ ❘ # coerce 3 %I4❙
// coercion_theorem : {A : type,P : A ⟶ prop,a,p : ⊦ P a} ⊦ eq ⟨ A | ([x] ⊦ P x) ⟩ (coercion A P a p) a ❙
rule rules?BooleanLiterals ❙
// false_is_FALSE : ded (FALSE ≐ false) ❙
// true_is_TRUE : ded (TRUE ≐ true) ❙
not : bool ⟶ bool ❘ # ¬ 1 prec -100 ❙
neq : {A: 𝒰 100} A ⟶ A ⟶ prop ❘ # 2 ≠ 3 prec -5 ❘ = [A,a,b] ¬ (a ≐ b) ❙
and : bool ⟶ bool ⟶ bool❘# 1 ∧ 2 prec -110 ❙
or : bool ⟶ bool ⟶ bool ❘# 1 ∨ 2 prec -120 ❘ // = [A,B] ¬ (¬A ∧ ¬ B) ❙
implies : bool ⟶ bool ⟶ bool ❘# 1 ⇒ 2 prec -130 ❘ // = [A,B] B ∨ ¬A ❙
iff : bool ⟶ bool ⟶ bool ❘ # 1 ⇔ 2 prec -140 ❘// = [A,B] (A ⇒ B) ∧ (B ⇒ A) ❙
include ☞http://gl.mathhub.info/MMT/LFX/Records?LFRecords ❙
include ☞http://cds.omdoc.org/urtheories?Ded ❙
include ☞http://gl.mathhub.info/MMT/LFX/Subtyping?LFWithVariance ❙
// rule rules?ApplyRule ❙
/T the type of booleans, i.e., all formulas are represented as terms of LF-type $prop$ ❙
// bool : type ❘ // = BOOL ❙
prop : type ❘ @ bool ❘ = BOOL ❙
/T one LF-type for each formula holding its proofs
For example, the LF type ⊦ 0 ≐ 1 is empty because that formula has no proofs.
Axioms are declared as constants of the corresponding type, e.g., a constant of type $⊦ true$ for the axiom of truth.❙
ded : prop ⟶ type ❘ # ⊦ 1 prec -500 ❘ role Judgment ❘ = DED ❙
ImplicitProof : {A} ⊦ A ❘ # ImplicitProof 1 ❙
rule lf?TermIrrelevanceRule (ded) ([A : prop] ImplicitProof A) ❙
/T Equality on terms. The type A is left implicit and can be inferred by MMT ❙
eq : {A:𝒰 100} A ⟶ A ⟶ bool ❘ # 2 ≐ 3 prec -5 ❘ role Eq ❘ // = EQUAL ❙
// coercion : {A : type, P : A ⟶ prop,a} ⊦ P a ⟶ ⟨ A | ([x] ⊦ P x) ⟩ ❘ # coerce 3 %I4❙
// coercion_theorem : {A : type,P : A ⟶ prop,a,p : ⊦ P a} ⊦ eq ⟨ A | ([x] ⊦ P x) ⟩ (coercion A P a p) a ❙
rule rules?BooleanLiterals ❙
// false_is_FALSE : ded (FALSE ≐ false) ❙
// true_is_TRUE : ded (TRUE ≐ true) ❙
not : bool ⟶ bool ❘ # ¬ 1 prec -100 ❙
neq : {A: 𝒰 100} A ⟶ A ⟶ prop ❘ # 2 ≠ 3 prec -5 ❘ = [A,a,b] ¬ (a ≐ b) ❙
and : bool ⟶ bool ⟶ bool❘# 1 ∧ 2 prec -110 ❙
or : bool ⟶ bool ⟶ bool ❘# 1 ∨ 2 prec -120 ❘ // = [A,B] ¬ (¬A ∧ ¬ B) ❙
implies : bool ⟶ bool ⟶ bool ❘# 1 ⇒ 2 prec -130 ❘ // = [A,B] B ∨ ¬A ❙
iff : bool ⟶ bool ⟶ bool ❘ # 1 ⇔ 2 prec -140 ❘// = [A,B] (A ⇒ B) ∧ (B ⇒ A) ❙
forall : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∀ 2 prec -100❙
exists : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∃ 2 prec -100 ❘// = [A,f] ¬ ∀ [x:A] ¬ f x ❙
unique : {A : 𝒰 100} (A ⟶ bool) ⟶ A ⟶ bool ❘ = [A,P,x] ∀ [y:A] P y ⇒ y ≐ x ❘ # unique 2 3 ❙
exists_unique : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∃! 2 prec -101 ❘ = [A,P] ∃ [x] (P x ∧ unique P x) ❙
forall : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∀ 2 prec -100❙
exists : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∃ 2 prec -100 ❘// = [A,f] ¬ ∀ [x:A] ¬ f x ❙
unique : {A : 𝒰 100} (A ⟶ bool) ⟶ A ⟶ bool ❘ = [A,P,x] ∀ [y:A] P y ⇒ y ≐ x ❘ # unique 2 3 ❙
exists_unique : {A : 𝒰 100} (A ⟶ bool) ⟶ bool ❘ # ∃! 2 prec -101 ❘ = [A,P] ∃ [x] (P x ∧ unique P x) ❙
/T Equality on types (semantics missing) ❙
tpeq : type ⟶ type ⟶ bool ❘ # 1 ≐≐ 2 prec -6 ❘ role Eq ❙
/T Equality on types (semantics missing) ❙
tpeq : type ⟶ type ⟶ bool ❘ # 1 ≐≐ 2 prec -6 ❘ role Eq ❙
❚
theory NaturalDeduction : ur:?LF =
include ?Logic ❙
tru_introduction : ⊦ true ❙
fals_elimination : {A} ⊦ false ⟶ ⊦ A ❙
fals_introduction : {A} ⊦ A ⟶ ⊦ ¬ A ⟶ ⊦ false ❙
forall_elim : {A : 𝒰 100, P : A ⟶ bool}⊦ ∀ P ⟶ {x : A}⊦ P x ❘ # forallE 3 4❙
forall_introduction : {A : 𝒰 100, P : A ⟶ bool, p : {x : A}⊦P x}⊦ ∀[x] P x ❘ # forallI 3 ❙
exists_intro : {A : 𝒰 100, P : A ⟶ bool, c:A} ⊦ (P c) ⟶ ⊦ ∃ [x] P x ❘ # existsI 4 ❙
include ?Logic ❙
tru_introduction : ⊦ true ❙
fals_elimination : {A} ⊦ false ⟶ ⊦ A ❙
fals_introduction : {A} ⊦ A ⟶ ⊦ ¬ A ⟶ ⊦ false ❙
forall_elim : {A : 𝒰 100, P : A ⟶ bool}⊦ ∀ P ⟶ {x : A}⊦ P x ❘ # forallE 3 4❙
forall_introduction : {A : 𝒰 100, P : A ⟶ bool, p : {x : A}⊦P x}⊦ ∀[x] P x ❘ # forallI 3 ❙
exists_intro : {A : 𝒰 100, P : A ⟶ bool, c:A} ⊦ (P c) ⟶ ⊦ ∃ [x] P x ❘ # existsI 4 ❙
exists_elim : {A : 𝒰 100, P : A ⟶ bool, C:bool} (⊦ ∃ [x:A] (P x)) ⟶ ({c:A} ⊦ (P c) ⟶ ⊦ C) ⟶ ⊦ C ❘# existsE 4 5❙
and_introduction : {A,B} ⊦ A ⟶ ⊦ B ⟶ ⊦ (A ∧ B) ❙
and_elim_left : {A,B} ⊦ (A ∧ B) ⟶ ⊦ A ❙
and_elim_right : {A,B} ⊦ (A ∧ B) ⟶ ⊦ B ❙
not_introduction : {A} (⊦ A ⟶ ⊦ false) ⟶ ⊦ ¬ A ❙
not_elim : {A} ⊦ ¬ ¬ A ⟶ ⊦ A ❙
and_introduction : {A,B} ⊦ A ⟶ ⊦ B ⟶ ⊦ (A ∧ B) ❙
and_elim_left : {A,B} ⊦ (A ∧ B) ⟶ ⊦ A ❙
and_elim_right : {A,B} ⊦ (A ∧ B) ⟶ ⊦ B ❙
not_introduction : {A} (⊦ A ⟶ ⊦ false) ⟶ ⊦ ¬ A ❙
not_elim : {A} ⊦ ¬ ¬ A ⟶ ⊦ A ❙
tnd : {A} ⊦ A ∨ ¬A ❘ // = [A: bool] not_introduction ([p : ⊦ (¬A ∧ ¬¬A)] fals_introduction (not_elim (and_elim_right p)) (and_elim_left p)) ❙
/T Some more rules for convenience. ❙
tnd : {A} ⊦ A ∨ ¬A ❘ // = [A: bool] not_introduction ([p : ⊦ (¬A ∧ ¬¬A)] fals_introduction (not_elim (and_elim_right p)) (and_elim_left p)) ❙
/T Some more rules for convenience. ❙
or_introduction_right : {A,B} ⊦ A ⟶ ⊦ (A ∨ B) ❘ # orinr 3❙
or_introduction_left : {A,B} ⊦ B ⟶ ⊦ (A ∨ B) ❘ # orinl 3❙
implication_introduction : {A,B} (⊦ A ⟶ ⊦ B) ⟶ ⊦ A ⇒ B ❘ # impli 3❙
......@@ -99,12 +99,35 @@ theory NaturalDeduction : ur:?LF =
biimplication_elimination_right : {A,B}⊦ (A ⇔ B) ⟶ ⊦ (B ⇒ A) ❘ # bielr 3❙
or_elimination : {A,B,C} ⊦ (A ∨ B) ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C ❘ # orelim 4 5 6❙
modus_ponens : {A,B} (⊦ A ⇒ B) ⟶ ⊦ A ⟶ ⊦ B ❘# MP 3 4 ❙
/T basic axioms governing Equality. Again, all the type parameters can be left implicit ❙
eq_refl : {t:𝒰 100,A: t} ⊦ A ≐ A ❘ # eq_refl 2❙
eq_cong : {t : 𝒰 100, s : 𝒰 100, f : t ⟶ s, A : t, B: t}
⊦ A ≐ B ⟶ ⊦ (f A) ≐ (f B) ❘ # eq_cong 3 6❙
/T The only two basic axioms governing equality that we need (see 1).
Again, all the type parameters can be left implicit.
Ref. 1: https://web.archive.org/web/20201012120105/https://leanprover.github.io/logic_and_proof/natural_deduction_for_first_order_logic.html#equality ❙
eq_refl : {t:𝒰 100,A: t} ⊦ A ≐ A ❘ # eq_refl 2❙
eq_congProp : {t: 𝒰 100, P: t ⟶ prop, A: t, B: t} ⊦ A ≐ B ⟶ ⊦ P A ⟶ ⊦ P B ❘ # eq_congP 2 5 6❙
/T Common theorems about equality ❙
eq_symm: {t: 𝒰 100, A: t, B: t} ⊦ A ≐ B ⟶ ⊦ B ≐ A
❘ = [t, A, B, AEqB] eq_congP ([z] z ≐ A) AEqB (eq_refl A)
❘ # eq_symm 4 ❙
/T A symmetric variant of eq_congProp ❙
eq_congPropReversed: {t: 𝒰 100, P: t ⟶ prop, A: t, B: t} ⊦ A ≐ B ⟶ ⊦ P B ⟶ ⊦ P A
❘ = [t, P, A, B, AEqB, PB] eq_congP P (eq_symm AEqB) PB
❘ # eq_congPR 2 5 6 ❙
eq_trans: {t : 𝒰 100, A : t, B: t, C: t} ⊦ A ≐ B ⟶ ⊦ B ≐ C ⟶ ⊦ A ≐ C
❘ = [t, A, B, C, AEqB, BEqC] eq_congPR ([z] z ≐ C) AEqB BEqC
❘ # eq_trans 5 6 ❙
/T A form of congruence wrt. the equality sign that is weaker than (and hence definable by) eq_congProp ❙
eq_cong : {t: 𝒰 100, s: 𝒰 100, f: t ⟶ s, A: t, B: t} ⊦ A ≐ B ⟶ ⊦ (f A) ≐ (f B)
❘ = [t, s, f, A, B, AEqB] eq_congP ([z] (f A) ≐ (f z)) AEqB (eq_refl (f A))
❘ # eq_cong 3 6 ❙
❚
/T Now some theories that introduce primitive types and literals for them.
Because literals must modify the parser, they are supplied as rules that are implemented in a plugin.❚
......@@ -192,7 +215,7 @@ theory Literals : ur:?LF =
// test : ⊦ leq_lit 0 1 ❘ = tru_introduction ❙
// test2 : ⊦ nat_lit_succ 1 ≐ 2 ❘ = eq_refl 2 ❙
❚
theory Trigonometry : ur:?LF =
......@@ -214,14 +237,14 @@ theory Trigonometry : ur:?LF =
pi_num = 3.1415926535897932384626 ❙
❚
/T String literals are also needed occasionally, e.g., in the LMFDB.❚
theory Strings : ur:?LF =
include ?Logic❙
string: type ❙
rule rules?StringLiterals ❙
concat: string ⟶ string ⟶ string❙
rule rules?StringLiterals ❙
concat: string ⟶ string ⟶ string❙
❚
/T Now some more complex types. First lists.❚
......@@ -232,7 +255,7 @@ theory Lists : ur:?LF =
theory InformalProofs : ur:?LF =
include ?Strings ❙
proofsketch : {A : prop} string ⟶ ⊦ A ❘ # sketch 2 ❙
byproof : {A,B} ⊦ A ⟶ ⊦ B ❘ # by 3 ❙
addproofstep : {A,B,C: prop} ⊦ A ⟶ ⊦ B ⟶ ⊦ B ❘ # 4 and 5 ❙
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment