Comment: core_2_intro
Introduces a variety of general-purpose definitions and
theorems.
Definition: ycomb
Y == λf.((λx.(f (x x))) (λx.(f (x x))))
Definition: recind-ycomb
Y' == λf,x. letrec x(y) = f x y in x(x)
Definition: pi2
snd(t) == let x,y = t in y
Definition: pi1
fst(t) == let x,y = t in x
Definition: so_apply1
x[s] == x s
Definition: so_apply2
x[s1;s2] == x s1 s2
Definition: so_apply3
x[s1;s2;s3] == x s1 s2 s3
Definition: so_apply4
x[s1;s2;s3;s4] == x s1 s2 s3 s4
Definition: so_apply5
x[s1;s2;s3;s4;s5] == x s1 s2 s3 s4 s5
Definition: so_apply6
x[a;b;c;d;e;f] == x a b c d e f
Definition: so_apply7
x[a;b;c;d;e;f;g] == x a b c d e f g
Definition: so_apply8
x[a;b;c;d;e;f;g;h] == x a b c d e f g h
Definition: so_apply9
x[a;b;c;d;e;f;g;h;i] == x a b c d e f g h i
Definition: so_apply10
x[a;b;c;d;e;f;g;h;i;j] == x a b c d e f g h i j
Definition: so_apply11
x[a;b;c;d;e;f;g;h;i;j;k] == x a b c d e f g h i j k
Definition: so_apply12
x[a;b;c;d;e;f;g;h;i;j;k;l] == x a b c d e f g h i j k l
Definition: so_apply13
x[a;b;c;d;e;f;g;h;i;j;k;l;m] == x a b c d e f g h i j k l m
Definition: so_apply14
x[a;b;c;d;e;f;g;h;i;j;k;l;m;n] == x a b c d e f g h i j k l m n
Definition: infix_ap
x f y == f x y
Definition: so_lambda1
λ2x.t[x] == λx.t[x]
Definition: so_lambda2
λ2x y.t[x; y] == λx,y. t[x; y]
Definition: so_lambda3
so_lambda(x,y,z.t[x;
y;
z]) ==
λx,y,z. t[x;
y;
z]
Definition: so_lambda4
so_lambda(x,y,z,w.t[x;
y;
z;
w]) ==
λx,y,z,w. t[x;
y;
z;
w]
Definition: so_lambda5
so_lambda(x,y,z,w,v.t[x;
y;
z;
w;
v]) ==
λx,y,z,w,v. t[x;
y;
z;
w;
v]
Definition: so_lambda6
so_lambda(x,y,z,u,v,w.t[x;
y;
z;
u;
v;
w]) ==
λx,y,z,u,v,w. t[x;
y;
z;
u;
v;
w]
Definition: so_lambda7
so_lambda(x,y,z,u,v,w,q.t[x;
y;
z;
u;
v;
w;
q]) ==
λx,y,z,u,v,w,q. t[x;
y;
z;
u;
v;
w;
q]
Definition: so_lambda8
so_lambda(x,y,z,u,v,w,q,p.t[x;
y;
z;
u;
v;
w;
q;
p]) ==
λx,y,z,u,v,w,q,p. t[x;
y;
z;
u;
v;
w;
q;
p]
Definition: so_lambda9
so_lambda(x,y,z,u,v,w,q,p,r.t[x;
y;
z;
u;
v;
w;
q;
p;
r]) ==
λx,y,z,u,v,w,q,p,r. t[x;
y;
z;
u;
v;
w;
q;
p;
r]
Definition: label
...$L... t == t
Definition: guard
{T} == T
Definition: show
The term show(x) unfolds to x. It has a special display form that makes it
easy to spot. We make a conversion ShowAddrC addr that folds `show` at the
given addr. That helps when working with conversions so that we can
easily see what term is at a given address. ⋅
⇒⇒ x ⇐⇐ == x
Definition: error
??? == "error"
Definition: prop
ℙ == Type
Definition: cand
A c∧ B == A × B
Definition: parameter
parm{i} == !null_abstraction
Comment: top_com
⌜Top⌝ is the type that contains all terms
Definition: top
⌜Top⌝ is the type that contains all terms⋅
Top == ⋂x:Void. Void
Lemma: top_wf
Top ∈ Type
Lemma: istype-top
istype(Top)
Lemma: istype-void
istype(Void)
Lemma: istype-int
istype(ℤ)
Lemma: istype-atom
istype(Atom)
Definition: uall
This is "uniform" universal quantification.
Evidence for ⌜∀[x:A]. B[x]⌝ must be something that is a member of ⌜B[x]⌝
whenever ⌜x ∈ A⌝. Such evidence is independent of the choice of ⌜x ∈ A⌝. ⋅
∀[x:A]. B[x] == ⋂x:A. B[x]
Lemma: uall_wf
∀[A:Type]. ∀[B:A ⟶ ℙ]. (∀[x:A]. B[x] ∈ ℙ)
Lemma: isect_wf
∀[A:Type]. ∀[B:A ⟶ ℙ]. (⋂x:A. B[x] ∈ ℙ)
Lemma: base_wf
Base ∈ Type
Lemma: istype-base
istype(Base)
Lemma: image-type_wf
∀[A:Type]. ∀[f:Base]. (Image(A,f) ∈ Type)
Definition: tunion_def
The union of a family types B[x], x ∈ A is obtained from the type
x:A × B[x] of all pairs <a, b>, a ∈ A, b ∈ B[a] by projection onto the
second component. That means that b ∈ ⋃x:A.B[x] if for some a ∈ A,
<a, b> ∈ x:A × B[x].⋅
⋃x:A.B[x] == Image((x:A × B[x]),(λp.(snd(p))))
Lemma: tunion_wf
∀[A:Type]. ∀[B:A ⟶ Type]. (⋃x:A.B[x] ∈ Type)
Lemma: set_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ({a:A| B[a]} ∈ Type)
Lemma: set-elim
∀[A:Type]. ∀[B:A ⟶ Type]. ∀x:Image((a:A × B[a]),(λp.(fst(p)))). ((x ∈ A) ∧ (↓B[x]))
Lemma: equal-wf-base
∀[A:Type]. ∀[a,b:Base]. (a = b ∈ A ∈ ℙ)
Lemma: trivial-equal
∀[A:Type]. ∀[a:A]. (a = a ∈ A)
Definition: respects-equality
respects-equality(S;T) == ∀x,y:Base. ((x = y ∈ S) ⇒ (x ∈ T) ⇒ (x = y ∈ T))
Lemma: respects-equality_wf
∀[S,T:Type]. (respects-equality(S;T) ∈ Type)
Lemma: base-respects-equality
∀[T:Type]. respects-equality(Base;T)
Lemma: respects-equality-trivial
∀[T:Type]. respects-equality(T;T)
Lemma: respects-equality-set-trivial
∀[T:Type]. ∀[P:T ⟶ ℙ]. respects-equality(T;{x:T| P[x]} )
Lemma: respects-equality-set-trivial2
∀[T:Type]. ∀[P:T ⟶ ℙ]. respects-equality({x:T| P[x]} ;T)
Lemma: respects-equality-set
∀[A,T:Type]. ∀[P:T ⟶ ℙ]. (respects-equality(A;T) ⇒ respects-equality(A;{x:T| P[x]} ))
Lemma: respects-equality-sets
∀[A,T:Type]. ∀[P:T ⟶ ℙ]. ∀[Q:A ⟶ ℙ]. (respects-equality(A;T) ⇒ respects-equality({x:A| Q[x]} ;{x:T| P[x]} ))
Lemma: equal-wf
∀[X,Y,A:Type]. (respects-equality(Y;A) ⇒ respects-equality(X;A) ⇒ (∀[a:X]. ∀[b:Y]. (a = b ∈ A ∈ ℙ)))
Lemma: equal_wf
∀[A:Type]. ∀[a,b:A]. (a = b ∈ A ∈ ℙ)
Lemma: equal-wf-T-base
∀[T:Type]. ∀[a:T]. ∀[b:Base]. (a = b ∈ T ∈ ℙ)
Lemma: equal-wf-base-T
∀[T:Type]. ∀[a:Base]. ∀[b:T]. (a = b ∈ T ∈ ℙ)
Lemma: change-equality-type
∀[A,B:Type]. (respects-equality(A;B) ⇒ (∀x,y:A. ((x = y ∈ A) ⇒ (x ∈ B) ⇒ (x = y ∈ B))))
Definition: subtype_rel
A ⊆r B == λx.x ∈ A ⟶ B
Lemma: subtype_rel_wf
∀[A,B:Type]. (A ⊆r B ∈ Type)
Definition: istype
istype(T) == T ⊆r T
Lemma: istype_wf
∀[T:Type]. (istype(T) ∈ Type)
Lemma: istype-universe
∀[T:Type]. istype(T)
Lemma: respects-equality_weakening
∀[T,S:Type]. ((S = T ∈ Type) ⇒ respects-equality(S;T))
Lemma: respects-equality-function
∀[A,A':Type]. ∀[B:A ⟶ Type]. ∀[B':A' ⟶ Type].
((A' ⊆r A) ⇒ (∀a:A'. respects-equality(B[a];B'[a])) ⇒ respects-equality(a:A ⟶ B[a];a:A' ⟶ B'[a]))
Lemma: false_wf
False ∈ ℙ
Lemma: istype-false
istype(False)
Lemma: void_wf
Void ∈ Type
Lemma: int-wf
ℤ ∈ Type
Comment: no apply_wf
The "true" _wf for apply would be
⌜∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:x:A ⟶ B[x]]. ∀[a:A]. (f a ∈ B[a])⌝
an "approximation" is
⌜∀[A,B:Type]. ∀[f:x:A ⟶ B]. ∀[a:A]. (f a ∈ B)⌝
Both of these are true, but if we add them to the library
then they would be used by type inference and by Auto
At present, they interfere too much with the working of other tactic.
So, until we understand the problems better, we do not add a _wf lemma
for apply.⋅
Lemma: infix_ap_wf
∀[A,B,C:Type]. ∀[f:A ⟶ B ⟶ C]. ∀[x:A]. ∀[y:B]. (x f y ∈ C)
Lemma: lambda-wf
∀[A,B:Type]. ∀[f:A ⟶ B]. (λx.f[x] ∈ A ⟶ B)
Lemma: product-wf
∀[A:Type]. ∀[B:A ⟶ Type]. (a:A × B[a] ∈ Type)
Lemma: exists_wf
∀[A:Type]. ∀[B:A ⟶ ℙ]. (∃a:A. B[a] ∈ ℙ)
Lemma: and_wf
∀[A,B:ℙ]. (A ∧ B ∈ ℙ)
Lemma: cand_wf
∀[A,B:ℙ]. (A c∧ B ∈ ℙ)
Lemma: or_wf
∀[A,B:ℙ]. (A ∨ B ∈ ℙ)
Lemma: function-wf
∀[A:Type]. ∀[B:A ⟶ Type]. (a:A ⟶ B[a] ∈ Type)
Lemma: all_wf
∀[A:Type]. ∀[B:A ⟶ ℙ]. (∀a:A. B[a] ∈ ℙ)
Lemma: sq_exists_wf
∀[A:Type]. ∀[B:A ⟶ ℙ]. (∃a:A [B[a]] ∈ ℙ)
Lemma: set-wf
∀[A:Type]. ∀[P:A ⟶ ℙ]. ({a:A| P[a]} ∈ Type)
Lemma: union-wf
∀[A,B:Type]. (A + B ∈ Type)
Lemma: add-wf
∀[x,y:ℤ]. (x + y ∈ ℤ)
Lemma: minus_wf
∀[x:ℤ]. (-x ∈ ℤ)
Lemma: multiply_wf
∀[x,y:ℤ]. (x * y ∈ ℤ)
Lemma: subtract_wf
∀[x,y:ℤ]. (x - y ∈ ℤ)
Lemma: uall_subtype
∀[F:Type ⟶ Type]. ∀[A:Type]. ((∀[A:Type]. F[A]) ⊆r F[A])
Definition: uimplies
This is "uniform" implication.
Evidence for (a ⇒ b) is a function from evidence for a to evidence for b,
but evidence for (b supposing a) is something that is evidence for b
as long as a is not empty (i.e. supposing that a has evidence).
Thus, the evidence must be "uniform" because it does not depend on
the the evidence for a. ⋅
b supposing a == ⋂:a. b
Lemma: uimplies-wf
∀[A:ℙ]. ∀[B:⋂a:A. ℙ]. (B supposing A ∈ ℙ)
Lemma: implies-wf
∀[A:ℙ]. ∀[B:⋂a:A. ℙ]. (A ⇒ B ∈ ℙ)
Definition: rev_uimplies
rev_uimplies(P;Q) == P supposing Q
Lemma: rev_uimplies_wf
∀[P,Q:ℙ]. (rev_uimplies(P;Q) ∈ ℙ)
Definition: uiff
uiff(P;Q) == Q supposing P ∧ P supposing Q
Lemma: uiff_wf
∀[P,Q:ℙ]. (uiff(P;Q) ∈ ℙ)
Lemma: iff_weakening_uiff
∀[P,Q:ℙ]. (uiff(P;Q) ⇒ (P ⇐⇒ Q))
Lemma: iff_weakening_equal
∀[A,B:Type]. {A ⇐⇒ B} supposing A = B ∈ Type
Lemma: implies_weakening_uimplies
∀[P,Q:ℙ]. (Q supposing P ⇒ {P ⇒ Q})
Lemma: rev_implies_weakening_rev_uimplies
∀[P,Q:ℙ]. (rev_uimplies(P;Q) ⇒ {P ⇐ Q})
Lemma: uiff_functionality_wrt_uiff
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇐⇒ P2} ⇒ {Q1 ⇐⇒ Q2} ⇒ {uiff(P1;Q1) ⇐⇒ uiff(P2;Q2)})
Lemma: uiff_functionality_wrt_uiff2
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇐⇒ P2} ⇒ {Q1 ⇐⇒ Q2} ⇒ {uiff(P1;Q1) ⇐⇒ uiff(P2;Q2)})
Lemma: uimplies_functionality_wrt_uimplies
∀[P1,P2,Q1,Q2:ℙ]. ({P1 supposing P2} ⇒ {Q2 supposing Q1} ⇒ {Q1 supposing P1 ⇒ Q2 supposing P2})
Lemma: uimplies_functionality_wrt_uiff
∀[P1,P2,Q1,Q2:ℙ]. ({uiff(P1;P2)} ⇒ {uiff(Q1;Q2)} ⇒ {uiff(Q1 supposing P1;Q2 supposing P2)})
Lemma: uimplies-iff-squash-implies
∀[P,Q:ℙ]. (Q supposing P ⇐⇒ (↓P) ⇒ Q)
Lemma: and_functionality_wrt_uimplies
∀[P1,P2,Q1,Q2:ℙ]. ({P2 supposing P1} ⇒ {Q2 supposing Q1} ⇒ {P2 ∧ Q2 supposing P1 ∧ Q1})
Lemma: and_functionality_wrt_rev_uimplies
∀[P1,P2,Q1,Q2:ℙ]. ({rev_uimplies(P1;P2)} ⇒ {rev_uimplies(Q1;Q2)} ⇒ {rev_uimplies(P1 ∧ Q1;P2 ∧ Q2)})
Lemma: and_functionality_wrt_uiff
∀[P1,P2,Q1,Q2:ℙ]. ({uiff(P1;P2)} ⇒ {uiff(Q1;Q2)} ⇒ {uiff(P1 ∧ Q1;P2 ∧ Q2)})
Lemma: not_functionality_wrt_uimplies
∀[P,Q:ℙ]. ({P supposing Q} ⇒ {¬Q supposing ¬P})
Lemma: not_functionality_wrt_uiff
∀[P,Q:ℙ]. ({uiff(P;Q)} ⇒ {uiff(¬P;¬Q)})
Lemma: uall_functionality_wrt_iff
∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ]. (∀[x:S]. (P[x] ⇐⇒ Q[x])) ⇒ {∀[x:S]. P[x] ⇐⇒ ∀[y:T]. Q[y]} supposing S = T ∈ Type
Lemma: uimplies_antisymmetry
∀[P,Q:ℙ]. (Q supposing P ⇒ P supposing Q ⇒ uiff(P;Q))
Lemma: uimplies_transitivity
∀[P,Q,R:ℙ]. (Q supposing P ⇒ R supposing Q ⇒ {R supposing P})
Lemma: uiff_transitivity
∀[P,Q,R:ℙ]. (uiff(P;Q) ⇒ uiff(Q;R) ⇒ uiff(P;R))
Lemma: uiff_transitivity2
∀[P,Q,R:ℙ]. (uiff(P;Q) ⇒ (Q = R ∈ ℙ) ⇒ uiff(P;R))
Lemma: uiff_transitivity3
∀[P,Q,R:ℙ]. ((P = Q ∈ ℙ) ⇒ uiff(Q;R) ⇒ uiff(P;R))
Comment: CORE_WF_THEOREMS
Wf theorems for definitions introduced
in core_1 theory.
Lemma: true_wf
True ∈ ℙ
Lemma: istype-true
istype(True)
Lemma: squash_wf
∀[A:ℙ]. (↓A ∈ ℙ)
Lemma: squash-test
∀[P:ℙ]. (P ⇒ (↓P))
Lemma: guard_wf
∀[T:Type]. ({T} ∈ Type)
Lemma: unit_wf
Unit ∈ Type
Lemma: not_wf
∀[A:ℙ]. (¬A ∈ ℙ)
Lemma: member-not
∀[A:ℙ]. ∀[z:Top]. λx.z ∈ ¬A supposing ¬A
Lemma: comb_for_not_wf
λA,z. (¬A) ∈ A:ℙ ⟶ (↓True) ⟶ ℙ
Lemma: rev_implies_wf
∀[A,B:ℙ]. (A ⇐ B ∈ ℙ)
Lemma: comb_for_rev_implies_wf
λA,B,z. (A ⇐ B) ∈ A:ℙ ⟶ B:ℙ ⟶ (↓True) ⟶ ℙ
Lemma: iff_wf
∀[A,B:ℙ]. (A ⇐⇒ B ∈ ℙ)
Lemma: comb_for_iff_wf
λA,B,z. (A ⇐⇒ B) ∈ A:ℙ ⟶ B:ℙ ⟶ (↓True) ⟶ ℙ
Lemma: nequal_wf
∀[A:Type]. ∀[x,y:A]. (x ≠ y ∈ A ∈ ℙ)
Lemma: member_wf
∀[A:Type]. ∀[a:A]. (a ∈ A ∈ Type)
Comment: COMBS_acom
Common Combinators
Definition: icomb
I == λx.x
Lemma: icomb_wf
∀[A:Type]. (I ∈ A ⟶ A)
Definition: kcomb
K == λx,y. x
Lemma: kcomb_wf
∀[A,B:Type]. (K ∈ A ⟶ B ⟶ A)
Definition: scomb
S == λx,y,z. (x z (y z))
Lemma: scomb_wf
∀[A,B,C:Type]. (S ∈ (A ⟶ B ⟶ C) ⟶ (A ⟶ B) ⟶ A ⟶ C)
Comment: PRODUCT_DEFS_acom
Projection functions for pairs
Lemma: pi2_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]]. (snd(p) ∈ B[fst(p)])
Lemma: pi1_wf
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]]. (fst(p) ∈ A)
Lemma: pair_eta_rw
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:a:A × B[a]]. (<fst(p), snd(p)> = p ∈ (a:A × B[a]))
Lemma: respects-equality-product
∀[A,A':Type]. ∀[B:A ⟶ Type]. ∀[B':A' ⟶ Type].
(respects-equality(A;A')
⇒ (∀a:Base. ((a ∈ A) ⇒ (a ∈ A') ⇒ respects-equality(B[a];B'[a])))
⇒ respects-equality(a:A × B[a];a:A' × B'[a]))
Definition: spread3
let x,y,z = a in
t[x;
y;
z] ==
let x,zz = a
in let y,z = zz
in t[x;
y;
z]
Definition: spread4
let w,x,y,z = a
in t[w;
x;
y;
z] ==
let w,zz1 = a
in let x,zz2 = zz1
in let y,z = zz2
in t[w;
x;
y;
z]
Definition: spread5
let a,b,c,d,e = u in v[a;
b;
c;
d;
e] ==
let a,zz1 = u
in let b,zz2 = zz1
in let c,zz3 = zz2
in let d,e = zz3
in v[a;
b;
c;
d;
e]
Definition: spread6
let a,b,c,d,e,f = u in
v[a;
b;
c;
d;
e;
f] ==
let a,zz1 = u
in let b,zz2 = zz1
in let c,zz3 = zz2
in let d,zz4 = zz3
in let e,f = zz4
in v[a;
b;
c;
d;
e;
f]
Definition: spread7
let a,b,c,d,e,f,g = u in
v[a;
b;
c;
d;
e;
f;
g] ==
let a,zz1 = u
in let b,zz2 = zz1
in let c,zz3 = zz2
in let d,zz4 = zz3
in let e,zz5 = zz4
in let f,g = zz5
in v[a;
b;
c;
d;
e;
f;
g]
Lemma: all_functionality_wrt_uimplies
∀[S,T:Type]. ∀[P:S ⟶ ℙ]. ∀[Q:T ⟶ ℙ].
(∀x:T. {Q[x] supposing P[x]}) ⇒ {∀x:T. Q[x] supposing ∀x:S. P[x]} supposing S = T ∈ Type
Lemma: all_functionality_wrt_uiff
∀[S,T:Type]. ∀[P:S ⟶ ℙ]. ∀[Q:T ⟶ ℙ].
(∀x:T. {uiff(P[x];Q[x])}) ⇒ {uiff(∀x:S. P[x];∀x:T. Q[x])} supposing S = T ∈ Type
Comment: UNIT_DEFS_acom
Inhabitant of Unit type
Definition: it
⋅ == Ax
Definition: exposed-it
exposed-it == Ax
Lemma: it_wf
⋅ ∈ Unit
Lemma: unit_triviality
∀[a:Unit]. (a = ⋅ ∈ Unit)
Comment: CONSTR_PROPERTIES_com
Predicates for constructive properties of propositions, and
lemmas characterizing how these predicates are inherited.
Worthwhile sometime redoing thms for soft abstractions
in terms of the underlying hard abstractions / primitives.
Definition: decidable
Dec(P) == P ∨ (¬P)
Lemma: decidable_wf
∀[A:ℙ]. (Dec(A) ∈ ℙ)
Lemma: decidable__or
∀[P,Q:ℙ]. (Dec(P) ⇒ Dec(Q) ⇒ Dec(P ∨ Q))
Lemma: decidable__and
∀[P,Q:ℙ]. (Dec(P) ⇒ (P ⇒ Dec(Q)) ⇒ Dec(P ∧ Q))
Lemma: decidable__and2
∀[P:ℙ]. ∀[Q:⋂:P. ℙ]. (Dec(P) ⇒ (P ⇒ Dec(Q)) ⇒ Dec(P ∧ Q))
Lemma: decidable__implies
∀[P:ℙ]. ∀[Q:⋂p:P. ℙ]. (Dec(P) ⇒ (P ⇒ Dec(Q)) ⇒ Dec(P ⇒ Q))
Lemma: decidable__false
Dec(False)
Lemma: decidable__true
Dec(True)
Lemma: decidable__not
∀[P:ℙ]. (Dec(P) ⇒ Dec(¬P))
Lemma: decidable__iff
∀[P,Q:ℙ]. (Dec(P) ⇒ Dec(Q) ⇒ Dec(P ⇐⇒ Q))
Lemma: atom_subtype_base
Atom ⊆r Base
Lemma: decidable__atom_equal
∀a,b:Atom. Dec(a = b ∈ Atom)
Lemma: iff_preserves_decidability
∀[A,B:ℙ]. (Dec(A) ⇒ (A ⇐⇒ B) ⇒ Dec(B))
Definition: stable
Stable{P} == P supposing ¬¬P
Lemma: stable_wf
∀[A:ℙ]. (Stable{A} ∈ ℙ)
Lemma: stable__not
∀[P:ℙ]. Stable{¬P}
Lemma: stable__false
Stable{False}
Lemma: stable__and
∀[P,Q:ℙ]. (Stable{P} ⇒ Stable{Q} ⇒ Stable{P ∧ Q})
Lemma: stable__all
∀[T:Type]. ∀[P:T ⟶ ℙ]. ((∀x:T. Stable{P[x]}) ⇒ Stable{∀x:T. P[x]})
Lemma: stable__implies
∀[P,Q:ℙ]. (Stable{P} ⇒ Stable{Q ⇒ P})
Lemma: stable__function_equal
∀[A,B:Type]. ∀[f,g:A ⟶ B]. Stable{f = g ∈ (A ⟶ B)} supposing ∀x:A. Stable{(f x) = (g x) ∈ B}
Lemma: stable__from_decidable
∀[P:ℙ]. (Dec(P) ⇒ Stable{P})
Definition: sq_stable
SqStable(P) == (↓P) ⇒ P
Lemma: sq_stable_wf
∀[A:ℙ]. (SqStable(A) ∈ ℙ)
Lemma: sq_stable_functionality
∀[A,B:ℙ]. ((A ⇐⇒ B) ⇒ (SqStable(A) ⇐⇒ SqStable(B)))
Lemma: sq_stable__and
∀[P:ℙ]. ∀[Q:⋂p:P. ℙ]. (SqStable(P) ⇒ (P ⇒ SqStable(Q)) ⇒ SqStable(P ∧ Q))
Lemma: sq_stable__implies
∀[P,Q:ℙ]. (SqStable(Q) ⇒ SqStable(P ⇒ Q))
Lemma: sq_stable__uimplies
∀[P,Q:ℙ]. (SqStable(Q) ⇒ SqStable(Q supposing P))
Lemma: sq_stable__iff
∀[P,Q:ℙ]. (SqStable(P) ⇒ SqStable(Q) ⇒ SqStable(P ⇐⇒ Q))
Lemma: sq_stable__uiff
∀[P,Q:ℙ]. (SqStable(P) ⇒ SqStable(Q) ⇒ SqStable(uiff(P;Q)))
Lemma: sq_stable__all
∀[A:Type]. ∀[P:A ⟶ ℙ]. ((∀x:A. SqStable(P[x])) ⇒ SqStable(∀x:A. P[x]))
Lemma: sq_stable__uall
∀[A:Type]. ∀[P:A ⟶ ℙ]. ((∀[x:A]. SqStable(P[x])) ⇒ SqStable(∀[x:A]. P[x]))
Lemma: sq_stable__equal
∀[A:Type]. ∀[x,y:A]. SqStable(x = y ∈ A)
Lemma: sq_stable__squash
∀[P:ℙ]. SqStable(↓P)
Lemma: sq_stable__from_stable
∀[P:ℙ]. (Stable{P} ⇒ SqStable(P))
Lemma: sq_stable__not
∀[P:ℙ]. SqStable(¬P)
Lemma: sq_stable_from_decidable
∀[P:ℙ]. (Dec(P) ⇒ SqStable(P))
Lemma: sq_stable__respects-equality
∀[A,B:Type]. SqStable(respects-equality(A;B))
Lemma: uiff_weakening
∀[P:ℙ]. (SqStable(P) ⇒ {uiff(P;P)})
Definition: xmiddle
XM == ∀P:ℙ. Dec(P)
Lemma: xmiddle_wf
XM ∈ ℙ'
Definition: weak-xmiddle
WeakXM == ∀P:ℙ. (↓Dec(P))
Lemma: weak-xmiddle_wf
WeakXM ∈ ℙ'
Lemma: xmiddle-implies-stable
XM ⇒ (∀P:ℙ. Stable{P})
Lemma: sq_stable_iff_stable
XM ⇒ (∀P:ℙ. (SqStable(P) ⇐⇒ Stable{P}))
Lemma: squash_elim
∀[P:ℙ]. (SqStable(P) ⇒ (↓P ⇐⇒ P))
Lemma: sq_stable_iff_uimplies
∀[P:ℙ]. (SqStable(P) ⇐⇒ P supposing P)
Comment: LOGIC_THMS_tcom
Theorems of inituitionistic propositional and
predicate logic.
Lemma: dneg_elim
∀[A:ℙ]. (Dec(A) ⇒ A supposing ¬¬A)
Lemma: dneg_elim_a
∀[A:ℙ]. (Dec(A) ⇒ (¬¬A ⇐⇒ A))
Lemma: iff_symmetry
∀[A,B:ℙ]. (A ⇐⇒ B ⇐⇒ B ⇐⇒ A)
Lemma: and_assoc
∀[A,B,C:ℙ]. (A ∧ B ∧ C ⇐⇒ (A ∧ B) ∧ C)
Lemma: and_comm
∀[A,B:ℙ]. (A ∧ B ⇐⇒ B ∧ A)
Lemma: or_assoc
∀[A,B,C:ℙ]. (A ∨ B ∨ C ⇐⇒ (A ∨ B) ∨ C)
Lemma: or_comm
∀[A,B:ℙ]. (A ∨ B ⇐⇒ B ∨ A)
Lemma: not_over_or
∀[A,B:ℙ]. uiff(¬(A ∨ B);(¬A) ∧ (¬B))
Lemma: not_over_or_a
∀[A,B:ℙ]. uiff(¬(A ∨ B);{(¬A) ∧ (¬B)})
Lemma: not_over_and_b
∀[A,B:ℙ]. ¬(A ∧ B) supposing (¬A) ∨ (¬B)
Lemma: not_over_and
∀[A,B:ℙ]. (Dec(A) ⇒ (¬(A ∧ B) ⇐⇒ (¬A) ∨ (¬B)))
Lemma: not_over_not
∀[A:ℙ]. (Dec(A) ⇒ (¬¬A ⇐⇒ A))
Lemma: not_over_implies
∀[A,B:ℙ]. (¬(A ⇒ B) ⇐⇒ (¬¬A) ∧ (¬B))
Lemma: and_false_l
∀[A:Top]. (False ∧ A ⇐⇒ False)
Lemma: and_false_r
∀[A:ℙ]. (A ∧ False ⇐⇒ False)
Lemma: and_true_l
∀[A:ℙ]. (True ∧ A ⇐⇒ A)
Lemma: and_true_r
∀[A:ℙ]. (A ∧ True ⇐⇒ A)
Lemma: or_false_l
∀[A:ℙ]. (False ∨ A ⇐⇒ A)
Lemma: or_false_r
∀[A:ℙ]. (A ∨ False ⇐⇒ A)
Lemma: or_true_l
∀[A:ℙ]. (True ∨ A ⇐⇒ True)
Lemma: or_true_r
∀[A:ℙ]. (A ∨ True ⇐⇒ True)
Lemma: exists_over_and_r
∀[T:Type]. ∀[A:ℙ]. ∀[B:T ⟶ ℙ]. (∃x:T. (A ∧ B[x]) ⇐⇒ A ∧ (∃x:T. B[x]))
Lemma: not_over_exists
∀[T:Type]. ∀[Q:T ⟶ ℙ]. uiff(¬(∃x:T. Q[x]);∀x:T. (¬Q[x]))
Lemma: not_over_exists_uniform
∀[T:Type]. ∀[Q:T ⟶ ℙ]. uiff(¬(∃x:T. Q[x]);∀[x:T]. (¬Q[x]))
Lemma: triple-neg
∀[A:ℙ]. uiff(¬¬¬A;¬A)
Lemma: non-uniform-triple-neg
∀A:ℙ. (¬¬¬A ⇐⇒ ¬A)
Lemma: minimal-triple-neg
∀[E:Type]. ∀[A:ℙ]. (((A ⇒ E) ⇒ E) ⇒ E ⇐⇒ A ⇒ E)
Lemma: triple-neg-ext
∀[A:ℙ]. uiff(¬¬¬A;¬A)
Lemma: non-uniform-triple-neg-ext
∀A:ℙ. (¬¬¬A ⇐⇒ ¬A)
Lemma: minimal-triple-neg-ext
∀[E:Type]. ∀[A:ℙ]. (((A ⇒ E) ⇒ E) ⇒ E ⇐⇒ A ⇒ E)
Comment: EQUALITY_THMS_tcom
Equality Theorems
Lemma: equal_symmetry
∀[T:Type]. ∀[x,y:T]. uiff(x = y ∈ T;y = x ∈ T)
Comment: REWRITE_SUPPORT_tcom
Lemma support for rewriting.
Lemma: iff_transitivity
∀[P,Q,R:ℙ]. ((P ⇐⇒ Q) ⇒ (Q ⇐⇒ R) ⇒ (P ⇐⇒ R))
Lemma: implies_transitivity
∀[P,Q,R:ℙ]. ((P ⇒ Q) ⇒ (Q ⇒ R) ⇒ {P ⇒ R})
Lemma: and_functionality_wrt_iff
∀[P1,P2,Q1,Q2:ℙ]. ((P1 ⇐⇒ P2) ⇒ (Q1 ⇐⇒ Q2) ⇒ (P1 ∧ Q1 ⇐⇒ P2 ∧ Q2))
Lemma: and_functionality_wrt_implies
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇒ P2} ⇒ {Q1 ⇒ Q2} ⇒ {(P1 ∧ Q1) ⇒ (P2 ∧ Q2)})
Lemma: and_functionality_wrt_uiff2
∀[P1,P2,Q1,Q2:ℙ]. ({uiff(P1;P2)} ⇒ (Q1 = Q2 ∈ ℙ) ⇒ {P1 ∧ Q1 ⇐⇒ P2 ∧ Q2})
Lemma: and_functionality_wrt_uiff3
∀[P1,P2,Q1,Q2:ℙ]. ((P1 = P2 ∈ ℙ) ⇒ {uiff(Q1;Q2)} ⇒ {P1 ∧ Q1 ⇐⇒ P2 ∧ Q2})
Lemma: implies_functionality_wrt_iff
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇐⇒ P2} ⇒ {Q1 ⇐⇒ Q2} ⇒ {P1 ⇒ Q1 ⇐⇒ P2 ⇒ Q2})
Lemma: implies_functionality_wrt_implies
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇐ P2} ⇒ {Q1 ⇒ Q2} ⇒ {(P1 ⇒ Q1) ⇒ P2 ⇒ Q2})
Lemma: decidable_functionality
∀[P,Q:ℙ]. ((P ⇐⇒ Q) ⇒ (Dec(P) ⇐⇒ Dec(Q)))
Lemma: iff_functionality_wrt_iff
∀[P1,P2,Q1,Q2:ℙ]. ((P1 ⇐⇒ P2) ⇒ (Q1 ⇐⇒ Q2) ⇒ (P1 ⇐⇒ Q1 ⇐⇒ P2 ⇐⇒ Q2))
Lemma: all_functionality_wrt_iff
∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ]. (∀x:S. (P[x] ⇐⇒ Q[x])) ⇒ (∀x:S. P[x] ⇐⇒ ∀y:T. Q[y]) supposing S = T ∈ Type
Lemma: all_functionality_wrt_implies
∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ]. (∀z:S. {P[z] ⇒ Q[z]}) ⇒ {(∀x:S. P[x]) ⇒ (∀y:T. Q[y])} supposing S = T ∈ Type
Lemma: exists_functionality_wrt_iff
∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ]. (∀x:S. (P[x] ⇐⇒ Q[x])) ⇒ (∃x:S. P[x] ⇐⇒ ∃y:T. Q[y]) supposing S = T ∈ Type
Lemma: exists_functionality_wrt_implies
∀[S,T:Type]. ∀[P,Q:S ⟶ ℙ]. (∀x:S. {P[x] ⇒ Q[x]}) ⇒ {(∃x:S. P[x]) ⇒ (∃y:T. Q[y])} supposing S = T ∈ Type
Lemma: not_functionality_wrt_iff
∀[P,Q:ℙ]. {¬P ⇐⇒ ¬Q} supposing P ⇐⇒ Q
Lemma: not_functionality_wrt_implies
∀[P,Q:ℙ]. {(¬P) ⇒ (¬Q)} supposing {P ⇐ Q}
Lemma: or_functionality_wrt_iff
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇐⇒ P2} ⇒ {Q1 ⇐⇒ Q2} ⇒ {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})
Lemma: or_functionality_wrt_uiff
∀[P1,P2,Q1,Q2:ℙ]. ({uiff(P1;P2)} ⇒ {uiff(Q1;Q2)} ⇒ {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})
Lemma: or_functionality_wrt_uiff2
∀[P1,P2,Q1,Q2:ℙ]. ({uiff(P1;P2)} ⇒ (Q1 = Q2 ∈ ℙ) ⇒ {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})
Lemma: or_functionality_wrt_uiff3
∀[P1,P2,Q1,Q2:ℙ]. ((P1 = P2 ∈ ℙ) ⇒ {uiff(Q1;Q2)} ⇒ {P1 ∨ Q1 ⇐⇒ P2 ∨ Q2})
Lemma: union_functionality_wrt_iff
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇐⇒ P2} ⇒ {Q1 ⇐⇒ Q2} ⇒ {P1 + Q1 ⇐⇒ P2 + Q2})
Lemma: union_functionality_wrt_uiff
∀[P1,P2,Q1,Q2:ℙ]. ({uiff(P1;P2)} ⇒ {uiff(Q1;Q2)} ⇒ {P1 + Q1 ⇐⇒ P2 + Q2})
Lemma: union_functionality_wrt_uiff2
∀[P1,P2,Q1,Q2:ℙ]. ({uiff(P1;P2)} ⇒ (Q1 = Q2 ∈ ℙ) ⇒ {P1 + Q1 ⇐⇒ P2 + Q2})
Lemma: union_functionality_wrt_uiff3
∀[P1,P2,Q1,Q2:ℙ]. ((P1 = P2 ∈ ℙ) ⇒ {uiff(Q1;Q2)} ⇒ {P1 + Q1 ⇐⇒ P2 + Q2})
Lemma: and-iff
∀[A:ℙ]. ∀[B,C:⋂a:A. ℙ]. ((A ⇒ (B ⇐⇒ C)) ⇒ {A ∧ B ⇐⇒ A ∧ C})
Definition: sq_or
a ↓∨ b == ↓a ∨ b
Lemma: sq_or_wf
∀[a,b:ℙ]. (a ↓∨ b ∈ ℙ)
Lemma: sq_stable__sq_or
∀[a,b:ℙ]. SqStable(a ↓∨ b)
Lemma: sq_or_simp
∀[a:ℙ]. ({uiff(a ↓∨ False;↓a)} ∧ {uiff(False ↓∨ a;↓a)} ∧ {uiff(a ↓∨ True;True)} ∧ {uiff(True ↓∨ a;True)})
Lemma: sq_or_sq_or
∀[a,b,c:ℙ]. ({uiff(a ↓∨ b ↓∨ c;a ↓∨ (b ∨ c))} ∧ {uiff((b ↓∨ c) ↓∨ a;(b ∨ c) ↓∨ a)})
Lemma: sq_or_functionality_wrt_iff
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇐⇒ P2} ⇒ {Q1 ⇐⇒ Q2} ⇒ {P1 ↓∨ Q1 ⇐⇒ P2 ↓∨ Q2})
Lemma: squash_squash
∀[a:ℙ]. uiff(↓↓a;↓a)
Lemma: squash_true
uiff(↓True;True)
Lemma: squash_false
uiff(↓False;False)
Lemma: sq_or_squash
∀[a,b:ℙ]. uiff((↓a) ↓∨ (↓b);a ↓∨ b)
Lemma: squash_sq_or
∀[a,b:ℙ]. uiff(↓a ↓∨ b;a ↓∨ b)
Lemma: sq_or_squash2
∀[a,b:ℙ]. uiff((↓a) ↓∨ b;a ↓∨ b)
Lemma: sq_or_squash3
∀[a,b:ℙ]. uiff(a ↓∨ (↓b);a ↓∨ b)
Lemma: squash_and
∀[a,b:ℙ]. uiff(↓a ∧ b;(↓a) ∧ (↓b))
Lemma: squash_not
∀[p:ℙ]. uiff(↓¬p;¬p)
Lemma: not_squash
∀[p:ℙ]. uiff(¬↓p;¬p)
Lemma: squash_equal
∀[T:Type]. ∀[x,y:T]. uiff(↓x = y ∈ T;x = y ∈ T)
Lemma: uimplies_functionality_wrt_uiff2
∀[P,Q1,Q2:ℙ]. ({uiff(Q1;Q2)} ⇒ {uiff(Q1 supposing P;Q2 supposing P)})
Lemma: uimplies_functionality_wrt_uiff3
∀[P,Q1,Q2:ℙ]. (Dec(P) ⇒ {uiff(Q1;Q2)} ⇒ {uiff(P supposing Q1;P supposing Q2)})
Lemma: or_functionality_wrt_implies
∀[P1,P2,Q1,Q2:ℙ]. ({P1 ⇒ P2} ⇒ {Q1 ⇒ Q2} ⇒ {(P1 ∨ Q1) ⇒ (P2 ∨ Q2)})
Lemma: squash_functionality_wrt_implies
∀[P,Q:ℙ]. ({P ⇒ Q} ⇒ {(↓P) ⇒ (↓Q)})
Lemma: squash_functionality_wrt_iff
∀[P,Q:ℙ]. ({P ⇐⇒ Q} ⇒ {↓P ⇐⇒ ↓Q})
Lemma: squash_functionality_wrt_uiff
∀[P,Q:ℙ]. ({P ⇐⇒ Q} ⇒ {uiff(↓P;↓Q)})
Lemma: implies_antisymmetry
∀[P,Q:ℙ]. ((P ⇒ Q) ⇒ (Q ⇒ P) ⇒ (P ⇐⇒ Q))
Comment: GENERALIZATION_tcom
⋅
Lemma: gen_hyp_tp
∀[A:Type]. ∀[e:A]. ∀[H:A ⟶ 𝕌{j}]. ∀[z:H e]. {{{False ⇒ True}}}
Comment: MISC_DEFS_com
Miscellaneous General Definitions
Definition: let
let x = a in b[x] == (λx.b[x]) a
Lemma: let_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[x:A]. (let v = x in f[v] ∈ B)
Comment: type_inj_acom
type_inj is intended chiefly for injecting into quotient
types. For convenience, typing lemmas should be proven
for each application. e.g.
... ∀x:T. [x]{a,b:T//Eab}
A general typing lemma for type_inj(x;T) cannot
be proven, because it's antecedent would involve the subtype
predicate which isn't typeable.
Definition: type_inj
[x]{T} == x
Comment: choicef_com
Hilbert choice operator. Set up for use in theorems where
assume_xm abstraction is used outermost.
Select the correctly instantiated display form by entering the
editor alias "eps". This display form contains variable that
is bound by assume_xm.
Sequent display routine needs fixing, so that pretty choicef
display form is used when XM becomes explicit hypothesis.
Definition: choicef
∈x:T. P[x] == case xm {y:T| P[y]} of inl(z) => z | inr(w) => "???"
Lemma: choicef_wf
∀[xm:XM]. ∀[T:Type]. ∀[P:T ⟶ ℙ]. ∈x:T. P[x] ∈ T supposing ∃a:T. P[a]
Lemma: fun_thru_spread
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:x:A × B[x]]. ∀[C,D:Type]. ∀[f:C ⟶ D]. ∀[b:x:A ⟶ B[x] ⟶ C].
((f let x,y = p in b[x;y]) = let x,y = p in f b[x;y] ∈ D)
Lemma: spread_to_pi12
∀[A:Type]. ∀[B:A ⟶ Type]. ∀[p:x:A × B[x]]. ∀[C:Type]. ∀[b:x:A ⟶ B[x] ⟶ C].
(let x,y = p in b[x;y] = b[fst(p);snd(p)] ∈ C)
Definition: singleton
{a:T} == {x:T| x = a ∈ T}
Lemma: singleton_wf
∀[T:Type]. ∀[a:T]. ({a:T} ∈ Type)
Lemma: singleton_properties
∀[T:Type]. ∀[a:T]. ∀[x:{a:T}]. (x = a ∈ T)
Definition: unique_set
{!x:T | P[x]} == {x:T| P[x] ∧ (∀y:T. (P[y] ⇒ (y = x ∈ T)))}
Lemma: unique_set_wf
∀[T:Type]. ∀[P:T ⟶ ℙ]. ({!x:T | P[x]} ∈ Type)
Definition: uni_sat
a = !x:T. Q[x] == Q[a] ∧ (∀a':T. (Q[a'] ⇒ (a' = a ∈ T)))
Lemma: uni_sat_wf
∀[T:Type]. ∀[a:T]. ∀[Q:T ⟶ ℙ]. (a = !x:T. Q[x] ∈ ℙ)
Lemma: uni_sat_imp_in_uni_set
∀[T:Type]. ∀[a:T]. ∀[Q:T ⟶ ℙ]. ((a = !x:T. Q[x]) ⇒ (a ∈ {!x:T | Q[x]}))
Lemma: sq_stable__uni_sat
∀[T:Type]. ∀a:T. ∀[Q:T ⟶ ℙ]. ((∀x:T. SqStable(Q[x])) ⇒ SqStable(a = !x:T. Q[x]))
Lemma: comb_for_pi1_wf
λA,B,p,z. (fst(p)) ∈ A:Type ⟶ B:(A ⟶ Type) ⟶ p:(a:A × B[a]) ⟶ (↓True) ⟶ A
Lemma: image-type_wf
∀[A:Type]. ∀[f:Base]. (Image(A,f) ∈ Type)
Lemma: int_eq_wf
∀[T:Type]. ∀[a,b:T]. ∀[x,y:ℤ]. (if x=y then a else b ∈ T)
Lemma: atom_eq_wf
∀[T:Type]. ∀[a,b:T]. ∀[x,y:Atom]. (if x=y then a else b fi ∈ T)
Lemma: not-0-eq-1
¬(0 = 1 ∈ ℤ)
Definition: baseof
baseof(T) == ⋂x:Unit?. case x of inl(z) => T | inr(z) => Base
Lemma: baseof_wf
∀[T:Type]. (baseof(T) ∈ Type)
Lemma: equal-top
∀[x,y:Top]. (x = y ∈ Top)
Lemma: equal-unit
∀[x,y:Unit]. (x = y ∈ Unit)
Lemma: decidable__squash
∀[p:ℙ]. (Dec(p) ⇒ Dec(↓p))
Lemma: squash_thru_implies_dec
∀[P,Q:ℙ]. uiff(↓P ⇒ Q;P ⇒ (↓Q)) supposing Dec(P)
Lemma: equality-test
∀[A,B,C:Type]. ((A = B ∈ Type) ⇒ (C = B ∈ Type) ⇒ (∀[x,y,z:A]. ((x = y ∈ A) ⇒ (z = y ∈ A) ⇒ (x = z ∈ C))))
Lemma: equality-test2
∀[A,B,C:Type].
((A = B ∈ Type)
⇒ (C = B ∈ Type)
⇒ (∀[f:A ⟶ A]. ∀[x,y,z,u,w:A]. ((x = (f y) ∈ A) ⇒ (z = (f y) ∈ A) ⇒ (w = u ∈ C) ⇒ (w = z ∈ C) ⇒ (u = x ∈ C))))
Lemma: or-to-and-by-cases
∀[X:ℙ]. (Dec(X) ⇒ (∀[P,Q:ℙ]. ((P ⇒ X) ⇒ (Q ⇒ (¬X)) ⇒ {P ∨ Q ⇐⇒ (X ⇒ P) ∧ ((¬X) ⇒ Q)})))
Definition: exists!
∃!x:T. P[x] == ∃x:T. (P[x] ∧ (∀y:T. (P[y] ⇒ (y = x ∈ T))))
Lemma: exists!_wf
∀[T:Type]. ∀[P:T ⟶ ℙ]. (∃!x:T. P[x] ∈ ℙ)
Lemma: less-member
∀[T:Type]. ∀[n,m:ℤ]. ∀[a,b:T]. (if (n) < (m) then a else b ∈ T)
Definition: less_than'
At one time, ⌜a < b⌝ was a primitive type, and the equality rule for it
said that ⌜a < b⌝ was a type if ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝.
An elimination rule said that if ⌜t ∈ a < b⌝ then ⌜t ~ Ax⌝.
All of these properties are easily derivable if we simply define
⌜a < b⌝ using the primitive `less` comparison operator
⌜if (a) < (b) then True else False⌝
However, from the fact that ⌜if (a) < (b) then True else False⌝
is a proposition (even when we know that it is a true proposition)
it does not follow that ⌜a ∈ ℤ⌝ and ⌜b ∈ ℤ⌝ because, for example
from a:⇃({...3}), b:⇃({4...}) we can prove that
⌜if (a) < (b) then True else False ∈ ℙ⌝.
Therefore, we call ⌜if (a) < (b) then True else False⌝ ⌜less_than'(a;b)⌝
and reserve ⌜a < b⌝ for the proposition that includes ⌜(a ∈ ℤ) ∧ (b ∈ ℤ)⌝⋅
less_than'(a;b) == if (a) < (b) then True else False
Lemma: less_than'_wf
∀[a,b:ℤ]. (less_than'(a;b) ∈ ℙ)
Definition: less_than
At one time, ⌜a < b⌝ was a primitive type but the properties we need all
follow from the definition of ⌜less_than'(a;b)⌝ except for the
property that from ⌜a < b⌝ we can derive ⌜(a ∈ ℤ) ∧ (b ∈ ℤ)⌝.
So we simply add those to the definition..
⋅
a < b == ↓less_than'(a;b) ∧ (a ∈ ℤ) ∧ (b ∈ ℤ)
Lemma: less_than_wf
∀[a,b:ℤ]. (a < b ∈ ℙ)
Lemma: istype-less_than
∀[a,b:ℤ]. istype(a < b)
Lemma: less_wf
∀[T:Type]. ∀[a,b:T]. ∀[x,y:ℤ]. (if (x) < (y) then a else b ∈ T)
Lemma: int_subtype_base
ℤ ⊆r Base
Lemma: unit_subtype_base
Unit ⊆r Base
Lemma: decidable__equal_set
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀[P:T ⟶ Type]. ∀x,y:{x:T| P[x]} . Dec(x = y ∈ {x:T| P[x]} )))
Lemma: decidable__equal_unit
∀x,y:Unit. Dec(x = y ∈ Unit)
Lemma: test-compute-all
2 * (1 + 2 + 3) ~ 12
Lemma: minimal-example1
∀[A,B,X:ℙ]. ((((A ⇒ B) ⇒ X) ⇒ X) ⇒ ((A ⇒ X) ⇒ X) ⇒ (B ⇒ X) ⇒ X)
Lemma: minimal-example1-ext
∀[A,B,X:ℙ]. ((((A ⇒ B) ⇒ X) ⇒ X) ⇒ ((A ⇒ X) ⇒ X) ⇒ (B ⇒ X) ⇒ X)
Lemma: not-not-p-or-not-p
∀P,A:ℙ. (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)
Lemma: not-not-p-or-not-p-example
∀P:ℙ. (¬¬(P ∨ (¬P)))
Lemma: not-not-p-or-not-p-prgram
∀P,A:ℙ. (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)
Lemma: curry-lemma
∀A,B,C:ℙ. (((A ∧ B) ⇒ C) ⇒ A ⇒ B ⇒ C)
Lemma: curry-lemma-program
∀A,B,C:ℙ. (((A ∧ B) ⇒ C) ⇒ A ⇒ B ⇒ C)
Lemma: minimal-not-not-xmiddle
∀[P,A:ℙ]. (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)
Lemma: not-not-1-xmiddle
∀[P:ℙ]. (¬¬(P ∨ (¬P)))
Lemma: minimal-not-not-implies
∀[P,A:ℙ]. (((((P ⇒ A) ⇒ A) ⇒ (P ∨ A)) ⇒ A) ⇒ A)
Lemma: minimal-not-not-implies-program
∀[P,A:ℙ]. (((((P ⇒ A) ⇒ A) ⇒ (P ∨ A)) ⇒ A) ⇒ A)
Lemma: minimal-not-not-implies-from-program
∀[P,A:ℙ]. (((((P ⇒ A) ⇒ A) ⇒ (P ∨ A)) ⇒ A) ⇒ A)
Lemma: example
∀[P,A:ℙ]. (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)
Lemma: minimal-not-not-xmiddle-program
∀[P,A:ℙ]. (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)
Lemma: minimal-not-not-xmiddle-from-program
∀[P,A:ℙ]. (((P ∨ (P ⇒ A)) ⇒ A) ⇒ A)
Home
Index