feat(library/standard): add decidability of le for int
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
937c465685
commit
3afad10a72
11 changed files with 180 additions and 168 deletions
|
|
@ -12,7 +12,7 @@ inductive bool : Type :=
|
|||
|
||||
namespace bool
|
||||
|
||||
theorem induction_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
|
||||
theorem cases_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
|
||||
bool_rec H0 H1 b
|
||||
|
||||
theorem bool_inhabited [instance] : inhabited bool :=
|
||||
|
|
@ -22,7 +22,7 @@ definition cond {A : Type} (b : bool) (t e : A) :=
|
|||
bool_rec e t b
|
||||
|
||||
theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
|
||||
induction_on b (or_inl (refl ff)) (or_inr (refl tt))
|
||||
cases_on b (or_inl (refl ff)) (or_inr (refl tt))
|
||||
|
||||
theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
|
||||
refl (cond ff t e)
|
||||
|
|
@ -52,24 +52,24 @@ refl (bor tt a)
|
|||
infixl `||`:65 := bor
|
||||
|
||||
theorem bor_tt_right (a : bool) : a || tt = tt :=
|
||||
induction_on a (refl (ff || tt)) (refl (tt || tt))
|
||||
cases_on a (refl (ff || tt)) (refl (tt || tt))
|
||||
|
||||
theorem bor_ff_left (a : bool) : ff || a = a :=
|
||||
induction_on a (refl (ff || ff)) (refl (ff || tt))
|
||||
cases_on a (refl (ff || ff)) (refl (ff || tt))
|
||||
|
||||
theorem bor_ff_right (a : bool) : a || ff = a :=
|
||||
induction_on a (refl (ff || ff)) (refl (tt || ff))
|
||||
cases_on a (refl (ff || ff)) (refl (tt || ff))
|
||||
|
||||
theorem bor_id (a : bool) : a || a = a :=
|
||||
induction_on a (refl (ff || ff)) (refl (tt || tt))
|
||||
cases_on a (refl (ff || ff)) (refl (tt || tt))
|
||||
|
||||
theorem bor_comm (a b : bool) : a || b = b || a :=
|
||||
induction_on a
|
||||
(induction_on b (refl (ff || ff)) (refl (ff || tt)))
|
||||
(induction_on b (refl (tt || ff)) (refl (tt || tt)))
|
||||
cases_on a
|
||||
(cases_on b (refl (ff || ff)) (refl (ff || tt)))
|
||||
(cases_on b (refl (tt || ff)) (refl (tt || tt)))
|
||||
|
||||
theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
|
||||
induction_on a
|
||||
cases_on a
|
||||
(calc (ff || b) || c = b || c : {bor_ff_left b}
|
||||
... = ff || (b || c) : bor_ff_left (b || c)⁻¹)
|
||||
(calc (tt || b) || c = tt || c : {bor_tt_left b}
|
||||
|
|
@ -93,24 +93,24 @@ theorem band_ff_left (a : bool) : ff && a = ff :=
|
|||
refl (ff && a)
|
||||
|
||||
theorem band_tt_left (a : bool) : tt && a = a :=
|
||||
induction_on a (refl (tt && ff)) (refl (tt && tt))
|
||||
cases_on a (refl (tt && ff)) (refl (tt && tt))
|
||||
|
||||
theorem band_ff_right (a : bool) : a && ff = ff :=
|
||||
induction_on a (refl (ff && ff)) (refl (tt && ff))
|
||||
cases_on a (refl (ff && ff)) (refl (tt && ff))
|
||||
|
||||
theorem band_tt_right (a : bool) : a && tt = a :=
|
||||
induction_on a (refl (ff && tt)) (refl (tt && tt))
|
||||
cases_on a (refl (ff && tt)) (refl (tt && tt))
|
||||
|
||||
theorem band_id (a : bool) : a && a = a :=
|
||||
induction_on a (refl (ff && ff)) (refl (tt && tt))
|
||||
cases_on a (refl (ff && ff)) (refl (tt && tt))
|
||||
|
||||
theorem band_comm (a b : bool) : a && b = b && a :=
|
||||
induction_on a
|
||||
(induction_on b (refl (ff && ff)) (refl (ff && tt)))
|
||||
(induction_on b (refl (tt && ff)) (refl (tt && tt)))
|
||||
cases_on a
|
||||
(cases_on b (refl (ff && ff)) (refl (ff && tt)))
|
||||
(cases_on b (refl (tt && ff)) (refl (tt && tt)))
|
||||
|
||||
theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
|
||||
induction_on a
|
||||
cases_on a
|
||||
(calc (ff && b) && c = ff && c : {band_ff_left b}
|
||||
... = ff : band_ff_left c
|
||||
... = ff && (b && c) : band_ff_left (b && c)⁻¹)
|
||||
|
|
@ -135,7 +135,7 @@ definition bnot (a : bool) := bool_rec tt ff a
|
|||
prefix `!`:85 := bnot
|
||||
|
||||
theorem bnot_bnot (a : bool) : !!a = a :=
|
||||
induction_on a (refl (!!ff)) (refl (!!tt))
|
||||
cases_on a (refl (!!ff)) (refl (!!tt))
|
||||
|
||||
theorem bnot_false : !ff = tt := refl _
|
||||
|
||||
|
|
|
|||
|
|
@ -8,11 +8,6 @@
|
|||
import ..nat.basic ..nat.order ..nat.sub ..prod ..quotient ..quotient tools.tactic struc.relation
|
||||
import struc.binary
|
||||
|
||||
-- TODO: show decidability of le and remove this
|
||||
import logic.classes.decidable
|
||||
import logic.axioms.classical
|
||||
import logic.axioms.prop_decidable
|
||||
|
||||
import tools.fake_simplifier
|
||||
|
||||
namespace int
|
||||
|
|
@ -214,43 +209,30 @@ exists_intro (pr1 (rep a))
|
|||
|
||||
definition of_nat (n : ℕ) : ℤ := psub (pair n 0)
|
||||
|
||||
theorem int_eq_decidable [instance] (a b : ℤ) : decidable (a = b) := _
|
||||
-- subtype_eq_decidable _ _ (prod_eq_decidable _ _ _ _)
|
||||
|
||||
opaque_hint (hiding int)
|
||||
coercion of_nat
|
||||
|
||||
-- TODO: why doesn't the coercion work?
|
||||
theorem eq_zero_intro (n : ℕ) : psub (pair n n) = 0 :=
|
||||
have H : rel (pair n n) (pair 0 0), by simp,
|
||||
eq_abs quotient H
|
||||
|
||||
-- TODO: this is not a good name -- we want to use abs for the function from int to int.
|
||||
-- Rename to int.to_nat?
|
||||
|
||||
-- ## absolute value
|
||||
|
||||
definition to_nat : ℤ → ℕ := rec_constant quotient (fun v, dist (pr1 v) (pr2 v))
|
||||
|
||||
-- TODO: set binding strength: is this right?
|
||||
notation `|`:40 x:40 `|` := to_nat x
|
||||
|
||||
-- TODO: delete -- prod.destruct should be enough
|
||||
---move to other library or remove
|
||||
-- add_rewrite pair_tproj_eq
|
||||
-- theorem pair_translate {A B : Type} (P : A → B → A × B → Prop)
|
||||
-- : (∀v, P (pr1 v) (pr2 v) v) ↔ (∀a b, P a b (pair a b)) :=
|
||||
-- iff_intro
|
||||
-- (assume H, take a b, subst (by simp) (H (pair a b)))
|
||||
-- (assume H, take v, subst (by simp) (H (pr1 v) (pr2 v)))
|
||||
|
||||
theorem abs_comp (n m : ℕ) : (to_nat (psub (pair n m))) = dist n m :=
|
||||
theorem to_nat_comp (n m : ℕ) : (to_nat (psub (pair n m))) = dist n m :=
|
||||
have H : ∀v w : ℕ × ℕ, rel v w → dist (pr1 v) (pr2 v) = dist (pr1 w) (pr2 w),
|
||||
from take v w H, dist_eq_intro H,
|
||||
have H2 : ∀v : ℕ × ℕ, (to_nat (psub v)) = dist (pr1 v) (pr2 v),
|
||||
from take v, (comp_constant quotient H (rel_refl v)),
|
||||
(by simp) ◂ H2 (pair n m)
|
||||
|
||||
-- add_rewrite abs_comp --local
|
||||
-- add_rewrite to_nat_comp --local
|
||||
|
||||
--the following theorem includes abs_zero
|
||||
theorem to_nat_of_nat (n : ℕ) : to_nat (of_nat n) = n :=
|
||||
calc
|
||||
(to_nat (psub (pair n 0))) = dist n 0 : by simp
|
||||
|
|
@ -262,7 +244,7 @@ calc
|
|||
... = to_nat (of_nat m) : {H}
|
||||
... = m : to_nat_of_nat m
|
||||
|
||||
theorem abs_eq_zero {a : ℤ} (H : (to_nat a) = 0) : a = 0 :=
|
||||
theorem to_nat_eq_zero {a : ℤ} (H : to_nat a = 0) : a = 0 :=
|
||||
obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
|
||||
have H2 : dist xa ya = 0, from
|
||||
calc
|
||||
|
|
@ -275,11 +257,10 @@ calc
|
|||
... = psub (pair ya ya) : {H3}
|
||||
... = 0 : eq_zero_intro ya
|
||||
|
||||
-- add_rewrite abs_of_nat
|
||||
-- add_rewrite to_nat_of_nat
|
||||
|
||||
-- ## neg
|
||||
|
||||
|
||||
definition neg : ℤ → ℤ := quotient_map quotient flip
|
||||
|
||||
-- TODO: is this good?
|
||||
|
|
@ -309,7 +290,7 @@ theorem neg_inj {a b : ℤ} (H : -a = -b) : a = b :=
|
|||
theorem neg_move {a b : ℤ} (H : -a = b) : -b = a :=
|
||||
subst H (neg_neg a)
|
||||
|
||||
theorem abs_neg (a : ℤ) : (to_nat (-a)) = (to_nat a) :=
|
||||
theorem to_nat_neg (a : ℤ) : (to_nat (-a)) = (to_nat a) :=
|
||||
obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
|
||||
by simp
|
||||
|
||||
|
|
@ -324,7 +305,7 @@ have H5 : n + m = 0, from
|
|||
... = 0 : by simp,
|
||||
add_eq_zero H5
|
||||
|
||||
-- add_rewrite abs_neg
|
||||
-- add_rewrite to_nat_neg
|
||||
|
||||
---reverse equalities
|
||||
|
||||
|
|
@ -354,7 +335,8 @@ or_imp_or (or_swap (proj_zero_or (rep a)))
|
|||
opaque_hint (hiding int)
|
||||
|
||||
---rename to by_cases in Lean 0.2 (for now using this to avoid name clash)
|
||||
theorem int_by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) : P a :=
|
||||
theorem int_by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) :
|
||||
P a :=
|
||||
or_elim (cases a)
|
||||
(assume H, obtain (n : ℕ) (H3 : a = n), from H, subst (symm H3) (H1 n))
|
||||
(assume H, obtain (n : ℕ) (H3 : a = -n), from H, subst (symm H3) (H2 n))
|
||||
|
|
@ -378,7 +360,8 @@ or_elim (cases a)
|
|||
have H4 : a = - of_nat (succ k), from subst H3 H2,
|
||||
or_intro_right _ (exists_intro k H4)))
|
||||
|
||||
theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-of_nat (succ n))) : P a :=
|
||||
theorem int_by_cases_succ {P : ℤ → Prop} (a : ℤ)
|
||||
(H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-of_nat (succ n))) : P a :=
|
||||
or_elim (cases_succ a)
|
||||
(assume H, obtain (n : ℕ) (H3 : a = of_nat n), from H, subst (symm H3) (H1 n))
|
||||
(assume H, obtain (n : ℕ) (H3 : a = -of_nat (succ n)), from H, subst (symm H3) (H2 n))
|
||||
|
|
@ -460,7 +443,8 @@ obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
|
|||
obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
|
||||
by simp
|
||||
|
||||
theorem triangle_inequality (a b : ℤ) : (to_nat (a + b)) ≤ (to_nat a) + (to_nat b) := --note: ≤ is nat::≤
|
||||
theorem to_nat_add_le (a b : ℤ) : to_nat (a + b) ≤ to_nat a + to_nat b :=
|
||||
--note: ≤ is nat::≤
|
||||
obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
|
||||
obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
|
||||
have H : dist (xa + xb) (ya + yb) ≤ dist xa ya + dist xb yb,
|
||||
|
|
@ -619,24 +603,25 @@ calc
|
|||
... = (to_nat (of_nat n - m)) : sorry -- {symm H}
|
||||
|
||||
-- ## mul
|
||||
-- TODO: remove this when order changes
|
||||
theorem rel_mul_prep {xa ya xb yb xn yn xm ym : ℕ}
|
||||
(H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm)
|
||||
: xa * xn + ya * yn + (xb * ym + yb * xm) = xa * yn + ya * xn + (xb * xm + yb * ym) :=
|
||||
have H3 : xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn))
|
||||
= xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)), from
|
||||
= xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)), from
|
||||
calc
|
||||
xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn))
|
||||
= xa * xn + yb * xn + (ya * yn + xb * yn) + (xb * xn + xb * ym + (yb * yn + yb * xm)) : by simp
|
||||
... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : by simp
|
||||
... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : by simp
|
||||
... = ya * xn + xb * xn + (xa * yn + yb * yn) + (xb * yn + xb * xm + (yb*xn + yb*ym))
|
||||
: by simp
|
||||
... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)) : by simp,
|
||||
= xa * xn + yb * xn + (ya * yn + xb * yn) + (xb * xn + xb * ym + (yb * yn + yb * xm))
|
||||
: by simp
|
||||
... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : by simp
|
||||
... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : by simp
|
||||
... = ya * xn + xb * xn + (xa * yn + yb * yn) + (xb * yn + xb * xm + (yb*xn + yb*ym))
|
||||
: by simp
|
||||
... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn))
|
||||
: by simp,
|
||||
nat.add_cancel_right H3
|
||||
|
||||
theorem rel_mul {u u' v v' : ℕ × ℕ} (H1 : rel u u') (H2 : rel v v')
|
||||
: rel (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
|
||||
theorem rel_mul {u u' v v' : ℕ × ℕ} (H1 : rel u u') (H2 : rel v v') :
|
||||
rel (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
|
||||
(pair (pr1 u' * pr1 v' + pr2 u' * pr2 v') (pr1 u' * pr2 v' + pr2 u' * pr1 v')) :=
|
||||
calc
|
||||
pr1 (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v))
|
||||
|
|
@ -651,8 +636,8 @@ definition mul : ℤ → ℤ → ℤ := quotient_map_binary quotient
|
|||
|
||||
infixl `*` := int.mul
|
||||
|
||||
theorem mul_comp (n m k l : ℕ)
|
||||
: psub (pair n m) * psub (pair k l) = psub (pair (n * k + m * l) (n * l + m * k)) :=
|
||||
theorem mul_comp (n m k l : ℕ) :
|
||||
psub (pair n m) * psub (pair k l) = psub (pair (n * k + m * l) (n * l + m * k)) :=
|
||||
have H : ∀u v,
|
||||
psub u * psub v = psub (pair (pr1 u * pr1 v + pr2 u * pr2 v) (pr1 u * pr2 v + pr2 u * pr1 v)),
|
||||
from comp_quotient_map_binary_refl rel_refl quotient @rel_mul,
|
||||
|
|
@ -671,7 +656,6 @@ obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
|
|||
obtain (xc yc : ℕ) (Hc : c = psub (pair xc yc)), from destruct c,
|
||||
by simp
|
||||
|
||||
|
||||
theorem mul_left_comm : ∀a b c : ℤ, a * (b * c) = b * (a * c) :=
|
||||
left_comm mul_comm mul_assoc
|
||||
|
||||
|
|
@ -709,27 +693,27 @@ subst (mul_comm b a) (subst (mul_comm b (-a)) (mul_neg_right b a))
|
|||
theorem mul_neg_neg (a b : ℤ) : -a * -b = a * b :=
|
||||
by simp
|
||||
|
||||
theorem mul_distr_right (a b c : ℤ) : (a + b) * c = a * c + b * c :=
|
||||
theorem mul_right_distr (a b c : ℤ) : (a + b) * c = a * c + b * c :=
|
||||
obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
|
||||
obtain (xb yb : ℕ) (Hb : b = psub (pair xb yb)), from destruct b,
|
||||
obtain (xc yc : ℕ) (Hc : c = psub (pair xc yc)), from destruct c,
|
||||
by simp
|
||||
|
||||
theorem mul_distr_left (a b c : ℤ) : a * (b + c) = a * b + a * c :=
|
||||
theorem mul_left_distr (a b c : ℤ) : a * (b + c) = a * b + a * c :=
|
||||
calc
|
||||
a * (b + c) = (b + c) * a : mul_comm a (b + c)
|
||||
... = b * a + c * a : mul_distr_right b c a
|
||||
... = b * a + c * a : mul_right_distr b c a
|
||||
... = a * b + c * a : {mul_comm b a}
|
||||
... = a * b + a * c : {mul_comm c a}
|
||||
|
||||
theorem mul_sub_distr_right (a b c : ℤ) : (a - b) * c = a * c - b * c :=
|
||||
theorem mul_sub_right_distr (a b c : ℤ) : (a - b) * c = a * c - b * c :=
|
||||
calc
|
||||
(a + -b) * c = a * c + -b * c : mul_distr_right a (-b) c
|
||||
(a + -b) * c = a * c + -b * c : mul_right_distr a (-b) c
|
||||
... = a * c + - (b * c) : {mul_neg_left b c}
|
||||
|
||||
theorem mul_sub_distr_left (a b c : ℤ) : a * (b - c) = a * b - a * c :=
|
||||
theorem mul_sub_left_distr (a b c : ℤ) : a * (b - c) = a * b - a * c :=
|
||||
calc
|
||||
a * (b + -c) = a * b + a * -c : mul_distr_left a b (-c)
|
||||
a * (b + -c) = a * b + a * -c : mul_left_distr a b (-c)
|
||||
... = a * b + - (a * c) : {mul_neg_right a c}
|
||||
|
||||
theorem mul_of_nat (n m : ℕ) : of_nat n * of_nat m = n * m :=
|
||||
|
|
@ -745,8 +729,7 @@ by simp
|
|||
|
||||
-- add_rewrite mul_zero_left mul_zero_right mul_one_right mul_one_left
|
||||
-- add_rewrite mul_comm mul_assoc mul_left_comm
|
||||
-- add_rewrite mul_distr_right mul_distr_left mul_of_nat
|
||||
--mul_sub_distr_left mul_sub_distr_right
|
||||
-- add_rewrite mul_distr_right mul_distr_left mul_of_nat mul_sub_distr_left mul_sub_distr_right
|
||||
|
||||
|
||||
-- ---------- inversion
|
||||
|
|
@ -759,8 +742,8 @@ have H2 : (to_nat a) * (to_nat b) = 0, from
|
|||
... = 0 : to_nat_of_nat 0,
|
||||
have H3 : (to_nat a) = 0 ∨ (to_nat b) = 0, from mul_eq_zero H2,
|
||||
or_imp_or H3
|
||||
(assume H : (to_nat a) = 0, abs_eq_zero H)
|
||||
(assume H : (to_nat b) = 0, abs_eq_zero H)
|
||||
(assume H : (to_nat a) = 0, to_nat_eq_zero H)
|
||||
(assume H : (to_nat b) = 0, to_nat_eq_zero H)
|
||||
|
||||
theorem mul_cancel_left_or {a b c : ℤ} (H : a * b = a * c) : a = 0 ∨ b = c :=
|
||||
have H2 : a * (b - c) = 0, by simp,
|
||||
|
|
@ -797,29 +780,6 @@ definition le (a b : ℤ) : Prop := ∃n : ℕ, a + n = b
|
|||
infix `<=` := int.le
|
||||
infix `≤` := int.le
|
||||
|
||||
-- definition le : ℤ → ℤ → Prop := rec_binary quotient (fun a b, pr1 a + pr2 b ≤ pr2 a + pr1 b)
|
||||
-- theorem le_comp_alt (u v : ℕ × ℕ) : (psub u ≤ psub v) ↔ (pr1 u + pr2 v ≤ pr2 u + pr1 v)
|
||||
-- :=
|
||||
-- comp_binary_refl quotient rel_refl
|
||||
-- (take u u' v v' : ℕ × ℕ,
|
||||
-- assume Hu : rel u u',
|
||||
-- assume Hv : rel v v',)
|
||||
|
||||
-- u v
|
||||
|
||||
-- theorem le_intro {a b : ℤ} {n : ℕ} (H : a + of_nat n = b) : a ≤ b
|
||||
-- :=
|
||||
-- have lemma : ∀u v, rel (map_pair2 nat::add u (pair n 0)) v → pr1 u + pr2 v + n = pr2 u + pr1 v, from
|
||||
-- take u v,
|
||||
-- assume H : rel (map_pair2 nat::add u (pair n 0)) v,
|
||||
-- calc
|
||||
-- pr1 u + pr2 v + n = pr1 u + n + pr2 v : nat::add_right_comm (pr1 u) (pr2 v) n
|
||||
-- ... = pr1 (map_pair2 nat::add u (pair n 0)) + pr2 v : by simp
|
||||
-- ... = pr2 (map_pair2 nat::add u (pair n 0)) + pr1 v : H
|
||||
-- ... = pr2 u + 0 + pr1 v : by simp
|
||||
-- ... = pr2 u + pr1 v : {nat::add_zero_right (pr2 u)},
|
||||
-- have H2 :
|
||||
|
||||
theorem le_intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b :=
|
||||
exists_intro n H
|
||||
|
||||
|
|
@ -968,6 +928,12 @@ add_le_cancel_right H
|
|||
theorem sub_le_left_inv {a b c : ℤ} (H : c - a ≤ c - b) : b ≤ a :=
|
||||
le_neg_inv (add_le_cancel_left H)
|
||||
|
||||
theorem le_iff_sub_nonneg (a b : ℤ) : a ≤ b ↔ 0 ≤ b - a :=
|
||||
iff_intro
|
||||
(assume H, subst (sub_self _) (sub_le_right H a))
|
||||
(assume H, subst (sub_add_inverse _ _) (subst (add_zero_left _) (add_le_right H a)))
|
||||
|
||||
|
||||
-- Less than, Greater than, Greater than or equal
|
||||
-- ----------------------------------------------
|
||||
|
||||
|
|
@ -1208,23 +1174,40 @@ obtain (n : ℕ) (Hn : -a = n), from pos_imp_exists_nat H2,
|
|||
have H3 : a = -n, from symm (neg_move Hn),
|
||||
exists_intro n H3
|
||||
|
||||
theorem abs_pos {a : ℤ} (H : a ≥ 0) : (to_nat a) = a :=
|
||||
theorem to_nat_nonneg_eq {a : ℤ} (H : a ≥ 0) : (to_nat a) = a :=
|
||||
obtain (n : ℕ) (Hn : a = n), from pos_imp_exists_nat H,
|
||||
subst (symm Hn) (congr_arg of_nat (to_nat_of_nat n))
|
||||
|
||||
--abs_neg is already taken... rename?
|
||||
theorem abs_negative {a : ℤ} (H : a ≤ 0) : (to_nat a) = -a :=
|
||||
theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
|
||||
iff_mp (iff_symm (le_of_nat _ _)) (zero_le _)
|
||||
|
||||
theorem le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
|
||||
have aux : ∀x, decidable (0 ≤ x), from
|
||||
take x,
|
||||
have H : 0 ≤ x ↔ of_nat (to_nat x) = x, from
|
||||
iff_intro
|
||||
(assume H1, to_nat_nonneg_eq H1)
|
||||
(assume H1, subst H1 (of_nat_nonneg (to_nat x))),
|
||||
decidable_iff_equiv _ (iff_symm H),
|
||||
decidable_iff_equiv (aux _) (iff_symm (le_iff_sub_nonneg a b))
|
||||
|
||||
theorem ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b)
|
||||
theorem lt_decidable [instance] {a b : ℤ} : decidable (a < b)
|
||||
theorem gt_decidable [instance] {a b : ℤ} : decidable (a > b)
|
||||
|
||||
--to_nat_neg is already taken... rename?
|
||||
theorem to_nat_negative {a : ℤ} (H : a ≤ 0) : (to_nat a) = -a :=
|
||||
obtain (n : ℕ) (Hn : a = -n), from neg_imp_exists_nat H,
|
||||
calc
|
||||
(to_nat a) = (to_nat ( -n)) : {Hn}
|
||||
... = (to_nat n) : {abs_neg n}
|
||||
... = (to_nat n) : {to_nat_neg n}
|
||||
... = n : {to_nat_of_nat n}
|
||||
... = -a : symm (neg_move (symm Hn))
|
||||
|
||||
theorem abs_cases (a : ℤ) : a = (to_nat a) ∨ a = - (to_nat a) :=
|
||||
theorem to_nat_cases (a : ℤ) : a = (to_nat a) ∨ a = - (to_nat a) :=
|
||||
or_imp_or (le_total 0 a)
|
||||
(assume H : a ≥ 0, symm (abs_pos H))
|
||||
(assume H : a ≤ 0, symm (neg_move (symm (abs_negative H))))
|
||||
(assume H : a ≥ 0, symm (to_nat_nonneg_eq H))
|
||||
(assume H : a ≤ 0, symm (neg_move (symm (to_nat_negative H))))
|
||||
|
||||
-- ### interaction of mul with le and lt
|
||||
|
||||
|
|
@ -1233,7 +1216,7 @@ obtain (n : ℕ) (Hn : b + n = c), from le_elim H,
|
|||
have H2 : a * b + of_nat ((to_nat a) * n) = a * c, from
|
||||
calc
|
||||
a * b + of_nat ((to_nat a) * n) = a * b + (to_nat a) * of_nat n : by simp
|
||||
... = a * b + a * n : {abs_pos Ha}
|
||||
... = a * b + a * n : {to_nat_nonneg_eq Ha}
|
||||
... = a * (b + n) : by simp
|
||||
... = a * c : by simp,
|
||||
le_intro H2
|
||||
|
|
@ -1339,7 +1322,7 @@ have H2 : (to_nat a) * (to_nat b) = 1, from
|
|||
... = (to_nat 1) : {H}
|
||||
... = 1 : to_nat_of_nat 1,
|
||||
have H3 : (to_nat a) = 1, from mul_eq_one_left H2,
|
||||
or_imp_or (abs_cases a)
|
||||
or_imp_or (to_nat_cases a)
|
||||
(assume H4 : a = (to_nat a), subst H3 H4)
|
||||
(assume H4 : a = - (to_nat a), subst H3 H4)
|
||||
|
||||
|
|
@ -1365,7 +1348,7 @@ trans (if_neg (lt_antisym H) _ _) (if_pos H _ _)
|
|||
theorem sign_zero : sign 0 = 0 :=
|
||||
trans (if_neg (lt_irrefl 0) _ _) (if_neg (lt_irrefl 0) _ _)
|
||||
|
||||
-- add_rewrite sign_negative sign_pos abs_negative abs_pos sign_zero mul_abs
|
||||
-- add_rewrite sign_negative sign_pos to_nat_negative to_nat_nonneg_eq sign_zero mul_to_nat
|
||||
|
||||
theorem mul_sign_to_nat (a : ℤ) : sign a * (to_nat a) = a :=
|
||||
have temp1 : ∀a : ℤ, a < 0 → a ≤ 0, from take a, lt_imp_le,
|
||||
|
|
@ -1390,7 +1373,7 @@ or_elim (em (a = 0))
|
|||
... = sign a * (to_nat a) * (sign b * (to_nat b)) : {symm (mul_sign_to_nat b)}
|
||||
... = sign a * sign b * (to_nat (a * b)) : by simp,
|
||||
have H2 : (to_nat (a * b)) ≠ 0, from
|
||||
take H2', mul_ne_zero Ha Hb (abs_eq_zero H2'),
|
||||
take H2', mul_ne_zero Ha Hb (to_nat_eq_zero H2'),
|
||||
have H3 : (to_nat (a * b)) ≠ of_nat 0, from contrapos of_nat_inj H2,
|
||||
mul_cancel_right H3 H))
|
||||
|
||||
|
|
@ -1418,7 +1401,7 @@ or_elim3 (trichotomy a 0) sorry sorry sorry
|
|||
|
||||
-- add_rewrite sign_neg
|
||||
|
||||
theorem abs_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (to_nat (sign a)) = 1 :=
|
||||
theorem to_nat_sign_ne_zero {a : ℤ} (H : a ≠ 0) : (to_nat (sign a)) = 1 :=
|
||||
or_elim3 (trichotomy a 0) sorry
|
||||
-- (by simp)
|
||||
(assume H2 : a = 0, absurd_elim _ H2 H)
|
||||
|
|
|
|||
|
|
@ -2,4 +2,4 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
|
||||
import data.nat.basic
|
||||
import data.int.basic
|
||||
|
|
|
|||
|
|
@ -24,16 +24,6 @@ using fake_simplifier decidable
|
|||
|
||||
namespace nat
|
||||
|
||||
|
||||
-- TODO: settle on a name, and move this
|
||||
theorem by_cases (a : Prop) {b : Prop} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b :=
|
||||
or_elim (em a) (assume Ha, Hab Ha) (assume Hna, Hnab Hna)
|
||||
|
||||
-- move to nat
|
||||
theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 :=
|
||||
ne_symm (lt_imp_ne H)
|
||||
|
||||
|
||||
-- A general recursion principle
|
||||
-- =============================
|
||||
--
|
||||
|
|
@ -102,7 +92,7 @@ case_strong_induction_on m
|
|||
funext
|
||||
(take x : dom,
|
||||
show f' (succ m) x = restrict default measure f (succ m) x, from
|
||||
by_cases (measure x < succ m)
|
||||
by_cases -- (measure x < succ m)
|
||||
(assume H1 : measure x < succ m,
|
||||
have H2 [fact] : f' (succ m) x = rec_val x f, from
|
||||
calc
|
||||
|
|
@ -165,14 +155,14 @@ theorem div_aux_decreasing (y : ℕ) (g : ℕ → ℕ) (m : ℕ) (x : ℕ) (H :
|
|||
let lhs := div_aux_rec y x g in
|
||||
let rhs := div_aux_rec y x (restrict 0 (fun x, x) g m) in
|
||||
show lhs = rhs, from
|
||||
by_cases (y = 0 ∨ x < y)
|
||||
by_cases -- (y = 0 ∨ x < y)
|
||||
(assume H1 : y = 0 ∨ x < y,
|
||||
calc
|
||||
lhs = 0 : if_pos H1 _ _
|
||||
... = rhs : symm (if_pos H1 _ _))
|
||||
(assume H1 : ¬ (y = 0 ∨ x < y),
|
||||
have H2 : y ≠ 0 ∧ ¬ x < y, from not_or _ _ ◂ H1,
|
||||
have ypos : y > 0, from ne_zero_pos (and_elim_left H2),
|
||||
have ypos : y > 0, from ne_zero_imp_pos (and_elim_left H2),
|
||||
have xgey : x ≥ y, from not_lt_imp_ge (and_elim_right H2),
|
||||
have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
|
||||
have H5 : x - y < m, from lt_le_trans H4 H,
|
||||
|
|
@ -241,14 +231,14 @@ theorem mod_aux_decreasing (y : ℕ) (g : ℕ → ℕ) (m : ℕ) (x : ℕ) (H :
|
|||
let lhs := mod_aux_rec y x g in
|
||||
let rhs := mod_aux_rec y x (restrict 0 (fun x, x) g m) in
|
||||
show lhs = rhs, from
|
||||
by_cases (y = 0 ∨ x < y)
|
||||
by_cases -- (y = 0 ∨ x < y)
|
||||
(assume H1 : y = 0 ∨ x < y,
|
||||
calc
|
||||
lhs = x : if_pos H1 _ _
|
||||
... = rhs : symm (if_pos H1 _ _))
|
||||
(assume H1 : ¬ (y = 0 ∨ x < y),
|
||||
have H2 : y ≠ 0 ∧ ¬ x < y, from not_or _ _ ◂ H1,
|
||||
have ypos : y > 0, from ne_zero_pos (and_elim_left H2),
|
||||
have ypos : y > 0, from ne_zero_imp_pos (and_elim_left H2),
|
||||
have xgey : x ≥ y, from not_lt_imp_ge (and_elim_right H2),
|
||||
have H4 : x - y < x, from sub_lt (lt_le_trans ypos xgey) ypos,
|
||||
have H5 : x - y < m, from lt_le_trans H4 H,
|
||||
|
|
@ -325,7 +315,7 @@ case_strong_induction_on x
|
|||
(take x,
|
||||
assume IH : ∀x', x' ≤ x → x' mod y < y,
|
||||
show succ x mod y < y, from
|
||||
by_cases (succ x < y)
|
||||
by_cases -- (succ x < y)
|
||||
(assume H1 : succ x < y,
|
||||
have H2 : succ x mod y = succ x, from mod_lt_eq H1,
|
||||
show succ x mod y < y, from subst (symm H2) H1)
|
||||
|
|
@ -351,7 +341,7 @@ case_zero_pos y
|
|||
(take x,
|
||||
assume IH : ∀x', x' ≤ x → x' = x' div y * y + x' mod y,
|
||||
show succ x = succ x div y * y + succ x mod y, from
|
||||
by_cases (succ x < y)
|
||||
by_cases -- (succ x < y)
|
||||
(assume H1 : succ x < y,
|
||||
have H2 : succ x div y = 0, from div_less H1,
|
||||
have H3 : succ x mod y = succ x, from mod_lt_eq H1,
|
||||
|
|
@ -393,10 +383,10 @@ have H6 : y > 0, from le_lt_trans (zero_le _) H1,
|
|||
show q1 = q2, from mul_cancel_right H6 H5
|
||||
|
||||
theorem div_mul_mul {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) div (z * y) = x div y :=
|
||||
by_cases (y = 0)
|
||||
by_cases -- (y = 0)
|
||||
(assume H : y = 0, by simp)
|
||||
(assume H : y ≠ 0,
|
||||
have ypos : y > 0, from ne_zero_pos H,
|
||||
have ypos : y > 0, from ne_zero_imp_pos H,
|
||||
have zypos : z * y > 0, from mul_pos zpos ypos,
|
||||
have H1 : (z * x) mod (z * y) < z * y, from mod_lt _ zypos,
|
||||
have H2 : z * (x mod y) < z * y, from mul_lt_left zpos (mod_lt _ ypos),
|
||||
|
|
@ -410,10 +400,10 @@ by_cases (y = 0)
|
|||
--- ... = (x div y) * (z * y) + z * (x mod y) : by simp))
|
||||
|
||||
theorem mod_mul_mul {z : ℕ} (x y : ℕ) (zpos : z > 0) : (z * x) mod (z * y) = z * (x mod y) :=
|
||||
by_cases (y = 0)
|
||||
by_cases -- (y = 0)
|
||||
(assume H : y = 0, by simp)
|
||||
(assume H : y ≠ 0,
|
||||
have ypos : y > 0, from ne_zero_pos H,
|
||||
have ypos : y > 0, from ne_zero_imp_pos H,
|
||||
have zypos : z * y > 0, from mul_pos zpos ypos,
|
||||
have H1 : (z * x) mod (z * y) < z * y, from mod_lt _ zypos,
|
||||
have H2 : z * (x mod y) < z * y, from mul_lt_left zpos (mod_lt _ ypos),
|
||||
|
|
@ -477,7 +467,7 @@ have H2 : (z - x div y) * y = x mod y, from
|
|||
... = x mod y + x div y * y - x div y * y : {H1}
|
||||
... = x mod y : sub_add_left _ _,
|
||||
show x mod y = 0, from
|
||||
by_cases (y = 0)
|
||||
by_cases -- (y = 0)
|
||||
(assume yz : y = 0,
|
||||
have xz : x = 0, from
|
||||
calc
|
||||
|
|
@ -489,7 +479,7 @@ show x mod y = 0, from
|
|||
... = x : mod_zero _
|
||||
... = 0 : xz)
|
||||
(assume ynz : y ≠ 0,
|
||||
have ypos : y > 0, from ne_zero_pos ynz,
|
||||
have ypos : y > 0, from ne_zero_imp_pos ynz,
|
||||
have H3 : (z - x div y) * y < y, from subst (symm H2) (mod_lt x ypos),
|
||||
have H4 : (z - x div y) * y < 1 * y, from subst (symm (mul_one_left y)) H3,
|
||||
have H5 : z - x div y < 1, from mul_lt_cancel_right H4,
|
||||
|
|
@ -578,7 +568,7 @@ theorem dvd_add_cancel_right {m n1 n2 : ℕ} (H : m | (n1 + n2)) : m | n2 → m
|
|||
dvd_add_cancel_left (subst (add_comm _ _) H)
|
||||
|
||||
theorem dvd_sub {m n1 n2 : ℕ} (H1 : m | n1) (H2 : m | n2) : m | (n1 - n2) :=
|
||||
by_cases _
|
||||
by_cases
|
||||
(assume H3 : n1 ≥ n2,
|
||||
have H4 : n1 = n1 - n2 + n2, from symm (add_sub_ge_left H3),
|
||||
show m | n1 - n2, from dvd_add_cancel_right (subst H4 H1) H2)
|
||||
|
|
@ -608,13 +598,13 @@ let p' := pair y (x mod y) in
|
|||
let lhs := gcd_aux_rec p g in
|
||||
let rhs := gcd_aux_rec p (restrict 0 gcd_aux_measure g m) in
|
||||
show lhs = rhs, from
|
||||
by_cases (y = 0)
|
||||
by_cases -- (y = 0)
|
||||
(assume H1 : y = 0,
|
||||
calc
|
||||
lhs = x : if_pos H1 _ _
|
||||
... = rhs : symm (if_pos H1 _ _))
|
||||
(assume H1 : y ≠ 0,
|
||||
have ypos : y > 0, from ne_zero_pos H1,
|
||||
have ypos : y > 0, from ne_zero_imp_pos H1,
|
||||
have H2 : gcd_aux_measure p' = x mod y, from pr2_pair _ _,
|
||||
have H3 : gcd_aux_measure p' < gcd_aux_measure p, from subst (symm H2) (mod_lt _ ypos),
|
||||
have H4: gcd_aux_measure p' < m, from lt_le_trans H3 H,
|
||||
|
|
|
|||
|
|
@ -276,12 +276,6 @@ infix `>` : 50 := gt
|
|||
|
||||
theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := refl (n < m)
|
||||
|
||||
-- theorem gt_def (n m : ℕ) : n > m ↔ m < n
|
||||
-- := refl (n > m)
|
||||
|
||||
-- theorem ge_def (n m : ℕ) : n ≥ m ↔ m ≤ n
|
||||
-- := refl (n ≥ m)
|
||||
|
||||
-- add_rewrite gt_def ge_def --it might be possible to remove this in Lean 0.2
|
||||
|
||||
theorem lt_intro {n m k : ℕ} (H : succ n + k = m) : n < m :=
|
||||
|
|
@ -491,9 +485,12 @@ or_imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H)
|
|||
theorem succ_imp_pos {n m : ℕ} (H : n = succ m) : n > 0 :=
|
||||
H⁻¹ ▸ (succ_pos m)
|
||||
|
||||
theorem ne_zero_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
|
||||
theorem ne_zero_imp_pos {n : ℕ} (H : n ≠ 0) : n > 0 :=
|
||||
or_elim (zero_or_pos n) (take H2 : n = 0, absurd_elim _ H2 H) (take H2 : n > 0, H2)
|
||||
|
||||
theorem pos_imp_ne_zero {n : ℕ} (H : n > 0) : n ≠ 0 :=
|
||||
ne_symm (lt_imp_ne H)
|
||||
|
||||
theorem pos_imp_eq_succ {n : ℕ} (H : n > 0) : exists l, n = succ l :=
|
||||
lt_imp_eq_succ H
|
||||
|
||||
|
|
@ -606,4 +603,5 @@ mul_eq_one_left ((mul_comm n m) ▸ H)
|
|||
|
||||
--- theorem mul_eq_one {n m : ℕ} (H : n * m = 1) : n = 1 ∧ m = 1
|
||||
--- := and_intro (mul_eq_one_left H) (mul_eq_one_right H)
|
||||
|
||||
end nat
|
||||
|
|
|
|||
|
|
@ -2,9 +2,9 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
import logic.classes.inhabited logic.connectives.eq
|
||||
import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
|
||||
|
||||
using inhabited
|
||||
using inhabited decidable
|
||||
|
||||
inductive prod (A B : Type) : Type :=
|
||||
| pair : A → B → prod A B
|
||||
|
|
@ -43,8 +43,17 @@ section
|
|||
theorem prod_inhabited (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
|
||||
inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (pair a b)))
|
||||
|
||||
theorem prod_eq_decidable (u v : A × B) (H1 : decidable (pr1 u = pr1 v))
|
||||
(H2 : decidable (pr2 u = pr2 v)) : decidable (u = v) :=
|
||||
have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
|
||||
iff_intro
|
||||
(assume H, subst H (and_intro (refl _) (refl _)))
|
||||
(assume H, and_elim H (assume H4 H5, prod_eq H4 H5)),
|
||||
decidable_iff_equiv _ (iff_symm H3)
|
||||
|
||||
end
|
||||
|
||||
instance prod_inhabited
|
||||
instance prod_eq_decidable
|
||||
|
||||
end prod
|
||||
|
|
|
|||
|
|
@ -126,8 +126,8 @@ have H2 [fact] : R a (rep (abs a)), from R_rep_abs Q Ha,
|
|||
calc
|
||||
rec Q f (abs a) = eq_rec_on _ (f (rep (abs a))) : rfl
|
||||
... = eq_rec_on _ (eq_rec_on _ (f a)) : {symm (H _ _ H2)}
|
||||
... = eq_rec_on _ (f a) : eq_rec_on_compose _ _ _
|
||||
... = f a : eq_rec_on_id _ _
|
||||
... = eq_rec_on _ (f a) : eq_rec_on_compose (eq_abs Q H2) _ _
|
||||
... = f a : eq_rec_on_id (trans (eq_abs Q H2) (abs_rep Q (abs a))) _
|
||||
|
||||
definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
|
||||
(Q : is_quotient R abs rep) {C : Type} (f : A → C) (b : B) : C :=
|
||||
|
|
|
|||
|
|
@ -48,7 +48,7 @@ section
|
|||
∀(H1 : dpr1 p1 = dpr1 p2) (H2 : eq_rec_on H1 (dpr2 p1) = (dpr2 p2)), p1 = p2 :=
|
||||
sigma_destruct p1 (take a1 b1, sigma_destruct p2 (take a2 b2 H1 H2, dpair_eq H1 H2))
|
||||
|
||||
theorem sigma_inhabited (H1 : inhabited A) (H2 : inhabited (B (default A))) :
|
||||
theorem sigma_inhabited [instance] (H1 : inhabited A) (H2 : inhabited (B (default A))) :
|
||||
inhabited (sigma B) :=
|
||||
inhabited_destruct H1 (λa, inhabited_destruct H2 (λb, inhabited_mk (dpair (default A) b)))
|
||||
|
||||
|
|
|
|||
|
|
@ -2,7 +2,9 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
import logic.classes.inhabited logic.connectives.eq
|
||||
import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
|
||||
|
||||
using decidable
|
||||
|
||||
inductive subtype {A : Type} (P : A → Prop) : Type :=
|
||||
| tag : Πx : A, P x → subtype P
|
||||
|
|
@ -36,10 +38,18 @@ section
|
|||
theorem subtype_eq {a1 a2 : {x | P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
|
||||
subtype_destruct a1 (take x1 H1, subtype_destruct a2 (take x2 H2 H, tag_eq H))
|
||||
|
||||
-- TODO: need inhabited
|
||||
theorem subtype_inhabited {a : A} (H : P a) : inhabited {x | P x} :=
|
||||
inhabited_mk (tag a H)
|
||||
|
||||
theorem subtype_eq_decidable (a1 a2 : {x | P x})
|
||||
(H : decidable (elt_of a1 = elt_of a2)) : decidable (a1 = a2) :=
|
||||
have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
|
||||
iff_intro (assume H, subst H rfl) (assume H, subtype_eq H),
|
||||
decidable_iff_equiv _ (iff_symm H1)
|
||||
|
||||
end
|
||||
|
||||
end subtype
|
||||
instance subtype_inhabited
|
||||
instance subtype_eq_decidable
|
||||
|
||||
-- instance subtype_inhabited
|
||||
end subtype
|
||||
|
|
|
|||
|
|
@ -1,18 +1,33 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
----------------------------------------------------------------------------------------------------
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
import logic.connectives.prop
|
||||
import logic.connectives.prop logic.classes.inhabited logic.classes.decidable
|
||||
|
||||
using inhabited decidable
|
||||
|
||||
namespace sum
|
||||
|
||||
-- TODO: take this outside the namespace when the inductive package handles it better
|
||||
inductive sum (A B : Type) : Type :=
|
||||
| inl : A → sum A B
|
||||
| inr : B → sum A B
|
||||
|
||||
infixr `+`:25 := sum
|
||||
|
||||
theorem induction_on {A B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C :=
|
||||
theorem cases_on {A B : Type} {C : Prop} (s : A + B) (H1 : A → C) (H2 : B → C) : C :=
|
||||
sum_rec H1 H2 s
|
||||
|
||||
-- TODO: need equality lemmas
|
||||
-- theorem inl_eq {A : Type} (B : Type) {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 := sorry
|
||||
|
||||
theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) :=
|
||||
inhabited_mk (inl B (default A))
|
||||
|
||||
theorem sum_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A + B) :=
|
||||
inhabited_mk (inr A (default B))
|
||||
|
||||
--theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A + B) : decidable (s1 = s2) :=
|
||||
--cases_
|
||||
|
||||
end sum
|
||||
|
|
@ -1,8 +1,6 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import logic.connectives.basic logic.connectives.eq
|
||||
|
||||
|
|
@ -12,16 +10,17 @@ inductive decidable (p : Prop) : Type :=
|
|||
| inl : p → decidable p
|
||||
| inr : ¬p → decidable p
|
||||
|
||||
theorem decidable_true [instance] : decidable true :=
|
||||
theorem true_decidable [instance] : decidable true :=
|
||||
inl trivial
|
||||
|
||||
theorem decidable_false [instance] : decidable false :=
|
||||
theorem false_decidable [instance] : decidable false :=
|
||||
inr not_false_trivial
|
||||
|
||||
theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
|
||||
decidable_rec H1 H2 H
|
||||
|
||||
definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
|
||||
definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) :
|
||||
C :=
|
||||
decidable_rec H1 H2 H
|
||||
|
||||
theorem irrelevant {p : Prop} (d1 d2 : decidable p) : d1 = d2 :=
|
||||
|
|
@ -39,40 +38,48 @@ decidable_rec
|
|||
theorem em (p : Prop) {H : decidable p} : p ∨ ¬p :=
|
||||
induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp)
|
||||
|
||||
theorem by_cases {a b : Prop} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b :=
|
||||
or_elim (em a) (assume Ha, Hab Ha) (assume Hna, Hnab Hna)
|
||||
|
||||
theorem by_contradiction {p : Prop} {Hp : decidable p} (H : ¬p → false) : p :=
|
||||
or_elim (em p)
|
||||
(assume H1 : p, H1)
|
||||
(assume H1 : ¬p, false_elim p (H H1))
|
||||
|
||||
theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∧ b) :=
|
||||
theorem and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
|
||||
decidable (a ∧ b) :=
|
||||
rec_on Ha
|
||||
(assume Ha : a, rec_on Hb
|
||||
(assume Hb : b, inl (and_intro Ha Hb))
|
||||
(assume Hnb : ¬b, inr (and_not_right a Hnb)))
|
||||
(assume Hna : ¬a, inr (and_not_left b Hna))
|
||||
|
||||
theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b) :=
|
||||
theorem or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
|
||||
decidable (a ∨ b) :=
|
||||
rec_on Ha
|
||||
(assume Ha : a, inl (or_inl Ha))
|
||||
(assume Hna : ¬a, rec_on Hb
|
||||
(assume Hb : b, inl (or_inr Hb))
|
||||
(assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
|
||||
|
||||
theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
|
||||
theorem not_decidable [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
|
||||
rec_on Ha
|
||||
(assume Ha, inr (not_not_intro Ha))
|
||||
(assume Hna, inl Hna)
|
||||
|
||||
theorem decidable_iff [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ↔ b) :=
|
||||
theorem iff_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
|
||||
decidable (a ↔ b) :=
|
||||
rec_on Ha
|
||||
(assume Ha, rec_on Hb
|
||||
(assume Hb : b, inl (iff_intro (assume H, Hb) (assume H, Ha)))
|
||||
(assume Hnb : ¬b, inr (assume H : a ↔ b, absurd (iff_elim_left H Ha) Hnb)))
|
||||
(assume Hna, rec_on Hb
|
||||
(assume Hb : b, inr (assume H : a ↔ b, absurd (iff_elim_right H Hb) Hna))
|
||||
(assume Hnb : ¬b, inl (iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
|
||||
(assume Hnb : ¬b, inl
|
||||
(iff_intro (assume Ha, absurd_elim b Ha Hna) (assume Hb, absurd_elim a Hb Hnb))))
|
||||
|
||||
theorem decidable_implies [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a → b) :=
|
||||
theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
|
||||
decidable (a → b) :=
|
||||
rec_on Ha
|
||||
(assume Ha : a, rec_on Hb
|
||||
(assume Hb : b, inl (assume H, Hb))
|
||||
|
|
|
|||
Loading…
Reference in a new issue