Proof of proveit.numbers.ordering.min_nat_n_zero_is_zero theorem¶
In [1]:
import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import n, x, y, defaults
from proveit.logic import Equals
from proveit.numbers import zero, greater_eq, Less, LessEq
from proveit.numbers.ordering import min_def_bin
In [2]:
%proving min_nat_n_zero_is_zero
With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
min_nat_n_zero_is_zero:
(see dependencies)
min_nat_n_zero_is_zero:
(see dependencies)
In [3]:
defaults.assumptions = min_nat_n_zero_is_zero.conditions
defaults.assumptions: 
In [4]:
min_def_bin
In [5]:
min_def_bin_inst = min_def_bin.instantiate({x: n, y: zero}, auto_simplify=False)
min_def_bin_inst: 
⊢ 
⊢ 
For $n \in \mathbb{N}$, we know that $0 < n \lor 0 = n$. We show that the rhs of the instantiated definition is reducible to 0 for both of those cases.
In [6]:
greater_eq(n, zero).prove()
In [7]:
from proveit.numbers.ordering import less_eq_def
less_eq_def
In [8]:
less_eq_def_inst = less_eq_def.instantiate({x: zero, y: n})
less_eq_def_inst: ⊢ 
In [9]:
less_eq_def_inst.derive_right_via_equality()
Case 1: $0 = n$¶
In [10]:
# First we relax the equality to a LessEq
LessEq(n, zero).prove(assumptions=[Equals(zero, n)])
In [11]:
# That then allows the axiomatic definition to be evaluated
min_def_bin_inst_simpl_zero_eq_n = min_def_bin_inst.inner_expr().rhs.simplify(
assumptions=[Equals(zero, n)])
min_def_bin_inst_simpl_zero_eq_n: , 
⊢ 
, 
⊢ 
In [12]:
# But then we need to use the fact that 0 = n
min_def_bin_inst_simpl_zero_eq_n.inner_expr().rhs.substitute(
zero, assumptions=[Equals(zero, n)], auto_simplify=False)
, ⊢ 
Case 2: $0 < n$¶
In [13]:
# This one simplifies immediately
min_def_bin_inst.inner_expr().rhs.simplify(assumptions=[Less(zero, n)])
, 
⊢
Now combine the cases¶
In [14]:
less_eq_def_inst.rhs.derive_via_singular_dilemma(min_nat_n_zero_is_zero.instance_expr)
In [15]:
%qed
Out[15]:
