refactor(library/data): cleanup datatypes
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
6632a50015
commit
9412e604c8
14 changed files with 240 additions and 256 deletions
|
|
@ -4,143 +4,142 @@
|
|||
|
||||
import logic.core.connectives logic.classes.decidable logic.classes.inhabited
|
||||
|
||||
open eq_ops decidable
|
||||
open eq_ops eq decidable
|
||||
|
||||
inductive bool : Type :=
|
||||
ff : bool,
|
||||
tt : bool
|
||||
|
||||
ff : bool,
|
||||
tt : bool
|
||||
namespace bool
|
||||
definition rec_on [protected] {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b :=
|
||||
rec H₁ H₂ b
|
||||
|
||||
theorem cases_on {p : bool → Prop} (b : bool) (H0 : p ff) (H1 : p tt) : p b :=
|
||||
rec H0 H1 b
|
||||
theorem cases_on [protected] {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b :=
|
||||
rec H₁ H₂ b
|
||||
|
||||
theorem bool_inhabited [instance] : inhabited bool :=
|
||||
inhabited.mk ff
|
||||
definition cond {A : Type} (b : bool) (t e : A) :=
|
||||
rec_on b e t
|
||||
|
||||
definition cond {A : Type} (b : bool) (t e : A) :=
|
||||
rec e t b
|
||||
theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
|
||||
cases_on b (or.inl rfl) (or.inr rfl)
|
||||
|
||||
theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
|
||||
cases_on b (or.inl (eq.refl ff)) (or.inr (eq.refl tt))
|
||||
theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
|
||||
rfl
|
||||
|
||||
theorem cond_ff {A : Type} (t e : A) : cond ff t e = e :=
|
||||
rfl
|
||||
theorem cond_tt {A : Type} (t e : A) : cond tt t e = t :=
|
||||
rfl
|
||||
|
||||
theorem cond_tt {A : Type} (t e : A) : cond tt t e = t :=
|
||||
rfl
|
||||
theorem ff_ne_tt : ¬ ff = tt :=
|
||||
assume H : ff = tt, absurd
|
||||
(calc true = cond tt true false : (cond_tt _ _)⁻¹
|
||||
... = cond ff true false : {H⁻¹}
|
||||
... = false : cond_ff _ _)
|
||||
true_ne_false
|
||||
|
||||
theorem ff_ne_tt : ¬ ff = tt :=
|
||||
assume H : ff = tt, absurd
|
||||
(calc true = cond tt true false : (cond_tt _ _)⁻¹
|
||||
... = cond ff true false : {H⁻¹}
|
||||
... = false : cond_ff _ _)
|
||||
true_ne_false
|
||||
definition bor (a b : bool) :=
|
||||
rec_on a (rec_on b ff tt) tt
|
||||
|
||||
theorem decidable_eq [instance] (a b : bool) : decidable (a = b) :=
|
||||
rec
|
||||
(rec (inl (eq.refl ff)) (inr ff_ne_tt) b)
|
||||
(rec (inr (ne.symm ff_ne_tt)) (inl (eq.refl tt)) b)
|
||||
a
|
||||
theorem bor_tt_left (a : bool) : bor tt a = tt :=
|
||||
rfl
|
||||
|
||||
definition bor (a b : bool) :=
|
||||
rec (rec ff tt b) tt a
|
||||
infixl `||` := bor
|
||||
|
||||
theorem bor_tt_left (a : bool) : bor tt a = tt :=
|
||||
rfl
|
||||
theorem bor_tt_right (a : bool) : a || tt = tt :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
infixl `||` := bor
|
||||
theorem bor_ff_left (a : bool) : ff || a = a :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
theorem bor_tt_right (a : bool) : a || tt = tt :=
|
||||
cases_on a (eq.refl (ff || tt)) (eq.refl (tt || tt))
|
||||
theorem bor_ff_right (a : bool) : a || ff = a :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
theorem bor_ff_left (a : bool) : ff || a = a :=
|
||||
cases_on a (eq.refl (ff || ff)) (eq.refl (ff || tt))
|
||||
theorem bor_id (a : bool) : a || a = a :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
theorem bor_ff_right (a : bool) : a || ff = a :=
|
||||
cases_on a (eq.refl (ff || ff)) (eq.refl (tt || ff))
|
||||
theorem bor_comm (a b : bool) : a || b = b || a :=
|
||||
cases_on a
|
||||
(cases_on b rfl rfl)
|
||||
(cases_on b rfl rfl)
|
||||
|
||||
theorem bor_id (a : bool) : a || a = a :=
|
||||
cases_on a (eq.refl (ff || ff)) (eq.refl (tt || tt))
|
||||
theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
|
||||
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}
|
||||
... = tt : bor_tt_left c
|
||||
... = tt || (b || c) : bor_tt_left (b || c)⁻¹)
|
||||
|
||||
theorem bor_comm (a b : bool) : a || b = b || a :=
|
||||
cases_on a
|
||||
(cases_on b (eq.refl (ff || ff)) (eq.refl (ff || tt)))
|
||||
(cases_on b (eq.refl (tt || ff)) (eq.refl (tt || tt)))
|
||||
theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
|
||||
rec_on a
|
||||
(assume H : ff || b = tt,
|
||||
have Hb : b = tt, from (bor_ff_left b) ▸ H,
|
||||
or.inr Hb)
|
||||
(assume H, or.inl rfl)
|
||||
|
||||
theorem bor_assoc (a b c : bool) : (a || b) || c = a || (b || c) :=
|
||||
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}
|
||||
... = tt : bor_tt_left c
|
||||
... = tt || (b || c) : bor_tt_left (b || c)⁻¹)
|
||||
definition band (a b : bool) :=
|
||||
rec_on a ff (rec_on b ff tt)
|
||||
|
||||
theorem bor_to_or {a b : bool} : a || b = tt → a = tt ∨ b = tt :=
|
||||
rec
|
||||
(assume H : ff || b = tt,
|
||||
have Hb : b = tt, from (bor_ff_left b) ▸ H,
|
||||
or.inr Hb)
|
||||
(assume H, or.inl (eq.refl tt))
|
||||
a
|
||||
infixl `&&` := band
|
||||
|
||||
definition band (a b : bool) :=
|
||||
rec ff (rec ff tt b) a
|
||||
theorem band_ff_left (a : bool) : ff && a = ff :=
|
||||
rfl
|
||||
|
||||
infixl `&&` := band
|
||||
theorem band_tt_left (a : bool) : tt && a = a :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
theorem band_ff_left (a : bool) : ff && a = ff :=
|
||||
rfl
|
||||
theorem band_ff_right (a : bool) : a && ff = ff :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
theorem band_tt_left (a : bool) : tt && a = a :=
|
||||
cases_on a (eq.refl (tt && ff)) (eq.refl (tt && tt))
|
||||
theorem band_tt_right (a : bool) : a && tt = a :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
theorem band_ff_right (a : bool) : a && ff = ff :=
|
||||
cases_on a (eq.refl (ff && ff)) (eq.refl (tt && ff))
|
||||
theorem band_id (a : bool) : a && a = a :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
theorem band_tt_right (a : bool) : a && tt = a :=
|
||||
cases_on a (eq.refl (ff && tt)) (eq.refl (tt && tt))
|
||||
theorem band_comm (a b : bool) : a && b = b && a :=
|
||||
cases_on a
|
||||
(cases_on b rfl rfl)
|
||||
(cases_on b rfl rfl)
|
||||
|
||||
theorem band_id (a : bool) : a && a = a :=
|
||||
cases_on a (eq.refl (ff && ff)) (eq.refl (tt && tt))
|
||||
theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
|
||||
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)⁻¹)
|
||||
(calc (tt && b) && c = b && c : {band_tt_left b}
|
||||
... = tt && (b && c) : band_tt_left (b && c)⁻¹)
|
||||
|
||||
theorem band_comm (a b : bool) : a && b = b && a :=
|
||||
cases_on a
|
||||
(cases_on b (eq.refl (ff && ff)) (eq.refl (ff && tt)))
|
||||
(cases_on b (eq.refl (tt && ff)) (eq.refl (tt && tt)))
|
||||
theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
|
||||
or.elim (dichotomy a)
|
||||
(assume H0 : a = ff,
|
||||
absurd
|
||||
(calc ff = ff && b : (band_ff_left _)⁻¹
|
||||
... = a && b : {H0⁻¹}
|
||||
... = tt : H)
|
||||
ff_ne_tt)
|
||||
(assume H1 : a = tt, H1)
|
||||
|
||||
theorem band_assoc (a b c : bool) : (a && b) && c = a && (b && c) :=
|
||||
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)⁻¹)
|
||||
(calc (tt && b) && c = b && c : {band_tt_left b}
|
||||
... = tt && (b && c) : band_tt_left (b && c)⁻¹)
|
||||
theorem band_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
|
||||
band_eq_tt_elim_left (band_comm b a ⬝ H)
|
||||
|
||||
theorem band_eq_tt_elim_left {a b : bool} (H : a && b = tt) : a = tt :=
|
||||
or.elim (dichotomy a)
|
||||
(assume H0 : a = ff,
|
||||
absurd
|
||||
(calc ff = ff && b : (band_ff_left _)⁻¹
|
||||
... = a && b : {H0⁻¹}
|
||||
... = tt : H)
|
||||
ff_ne_tt)
|
||||
(assume H1 : a = tt, H1)
|
||||
definition bnot (a : bool) :=
|
||||
rec_on a tt ff
|
||||
|
||||
theorem band_eq_tt_elim_right {a b : bool} (H : a && b = tt) : b = tt :=
|
||||
band_eq_tt_elim_left (eq.trans (band_comm b a) H)
|
||||
notation `!` x:max := bnot x
|
||||
|
||||
definition bnot (a : bool) := rec tt ff a
|
||||
theorem bnot_bnot (a : bool) : !!a = a :=
|
||||
cases_on a rfl rfl
|
||||
|
||||
notation `!` x:max := bnot x
|
||||
theorem bnot_false : !ff = tt :=
|
||||
rfl
|
||||
|
||||
theorem bnot_bnot (a : bool) : !!a = a :=
|
||||
cases_on a (eq.refl (!!ff)) (eq.refl (!!tt))
|
||||
theorem bnot_true : !tt = ff :=
|
||||
rfl
|
||||
|
||||
theorem bnot_false : !ff = tt :=
|
||||
rfl
|
||||
|
||||
theorem bnot_true : !tt = ff :=
|
||||
rfl
|
||||
theorem is_inhabited [protected] [instance] : inhabited bool :=
|
||||
inhabited.mk ff
|
||||
|
||||
theorem has_decidable_eq [protected] [instance] (a b : bool) : decidable (a = b) :=
|
||||
rec_on a
|
||||
(rec_on b (inl rfl) (inr ff_ne_tt))
|
||||
(rec_on b (inr (ne.symm ff_ne_tt)) (inl rfl))
|
||||
end bool
|
||||
|
|
|
|||
|
|
@ -9,4 +9,7 @@
|
|||
|
||||
inductive empty : Type
|
||||
|
||||
theorem empty_elim (A : Type) (H : empty) : A := empty.rec (λe, A) H
|
||||
namespace empty
|
||||
theorem elim [protected] (A : Type) (H : empty) : A :=
|
||||
rec (λe, A) H
|
||||
end empty
|
||||
|
|
|
|||
|
|
@ -118,7 +118,7 @@ have special : ∀a, pr2 a ≤ pr1 a → proj (flip a) = flip (proj a), from
|
|||
... = pr1 a - pr2 a : {flip_pr1 a}
|
||||
... = pr1 (proj a) : (proj_ge_pr1 H)⁻¹
|
||||
... = pr2 (flip (proj a)) : (flip_pr2 (proj a))⁻¹,
|
||||
prod_eq H3 H4,
|
||||
prod.equal H3 H4,
|
||||
or.elim le_total
|
||||
(assume H : pr2 a ≤ pr1 a, special a H)
|
||||
(assume H : pr1 a ≤ pr2 a,
|
||||
|
|
@ -162,7 +162,7 @@ have special : ∀a b, pr2 a ≤ pr1 a → rel a b → proj a = proj b, from
|
|||
calc
|
||||
pr2 (proj a) = 0 : proj_ge_pr2 H2
|
||||
... = pr2 (proj b) : {(proj_ge_pr2 H4)⁻¹},
|
||||
prod_eq H5 H6,
|
||||
prod.equal H5 H6,
|
||||
or.elim le_total
|
||||
(assume H2 : pr2 a ≤ pr1 a, special a b H2 H)
|
||||
(assume H2 : pr1 a ≤ pr2 a,
|
||||
|
|
|
|||
|
|
@ -13,12 +13,14 @@ one : pos_num,
|
|||
bit1 : pos_num → pos_num,
|
||||
bit0 : pos_num → pos_num
|
||||
|
||||
namespace pos_num
|
||||
theorem is_inhabited [instance] : inhabited pos_num :=
|
||||
inhabited.mk one
|
||||
end pos_num
|
||||
|
||||
inductive num : Type :=
|
||||
zero : num,
|
||||
pos : pos_num → num
|
||||
|
||||
theorem inhabited_pos_num [instance] : inhabited pos_num :=
|
||||
inhabited.mk pos_num.one
|
||||
|
||||
theorem num_inhabited [instance] : inhabited num :=
|
||||
inhabited.mk num.zero
|
||||
|
|
|
|||
|
|
@ -6,47 +6,45 @@ import logic.core.eq logic.classes.inhabited logic.classes.decidable
|
|||
open eq_ops decidable
|
||||
|
||||
inductive option (A : Type) : Type :=
|
||||
none {} : option A,
|
||||
some : A → option A
|
||||
none {} : option A,
|
||||
some : A → option A
|
||||
|
||||
namespace option
|
||||
theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A)
|
||||
(H1 : p none) (H2 : ∀a, p (some a)) : p o :=
|
||||
rec H1 H2 o
|
||||
|
||||
theorem induction_on [protected] {A : Type} {p : option A → Prop} (o : option A)
|
||||
(H1 : p none) (H2 : ∀a, p (some a)) : p o :=
|
||||
rec H1 H2 o
|
||||
definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A)
|
||||
(H1 : C none) (H2 : ∀a, C (some a)) : C o :=
|
||||
rec H1 H2 o
|
||||
|
||||
definition rec_on [protected] {A : Type} {C : option A → Type} (o : option A)
|
||||
(H1 : C none) (H2 : ∀a, C (some a)) : C o :=
|
||||
rec H1 H2 o
|
||||
definition is_none {A : Type} (o : option A) : Prop :=
|
||||
rec true (λ a, false) o
|
||||
|
||||
definition is_none {A : Type} (o : option A) : Prop :=
|
||||
rec true (λ a, false) o
|
||||
theorem is_none_none {A : Type} : is_none (@none A) :=
|
||||
trivial
|
||||
|
||||
theorem is_none_none {A : Type} : is_none (@none A) :=
|
||||
trivial
|
||||
theorem not_is_none_some {A : Type} (a : A) : ¬ is_none (some a) :=
|
||||
not_false_trivial
|
||||
|
||||
theorem not_is_none_some {A : Type} (a : A) : ¬ is_none (some a) :=
|
||||
not_false_trivial
|
||||
theorem none_ne_some {A : Type} (a : A) : none ≠ some a :=
|
||||
assume H : none = some a, absurd
|
||||
(H ▸ is_none_none)
|
||||
(not_is_none_some a)
|
||||
|
||||
theorem none_ne_some {A : Type} (a : A) : none ≠ some a :=
|
||||
assume H : none = some a, absurd
|
||||
(H ▸ is_none_none)
|
||||
(not_is_none_some a)
|
||||
theorem equal [protected] {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
|
||||
congr_arg (option.rec a₁ (λ a, a)) H
|
||||
|
||||
theorem some_inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
|
||||
congr_arg (option.rec a₁ (λ a, a)) H
|
||||
|
||||
theorem option_inhabited [instance] (A : Type) : inhabited (option A) :=
|
||||
inhabited.mk none
|
||||
|
||||
theorem decidable_eq [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)}
|
||||
(o₁ o₂ : option A) : decidable (o₁ = o₂) :=
|
||||
rec_on o₁
|
||||
(rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))
|
||||
(take a₁ : A, rec_on o₂
|
||||
(inr (ne.symm (none_ne_some a₁)))
|
||||
(take a₂ : A, decidable.rec_on (H a₁ a₂)
|
||||
(assume Heq : a₁ = a₂, inl (Heq ▸ rfl))
|
||||
(assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (some_inj Hn) Hne))))
|
||||
theorem is_inhabited [protected] [instance] (A : Type) : inhabited (option A) :=
|
||||
inhabited.mk none
|
||||
|
||||
theorem has_decidable_eq [protected] [instance] {A : Type} {H : ∀a₁ a₂ : A, decidable (a₁ = a₂)}
|
||||
(o₁ o₂ : option A) : decidable (o₁ = o₂) :=
|
||||
rec_on o₁
|
||||
(rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))
|
||||
(take a₁ : A, rec_on o₂
|
||||
(inr (ne.symm (none_ne_some a₁)))
|
||||
(take a₂ : A, decidable.rec_on (H a₁ a₂)
|
||||
(assume Heq : a₁ = a₂, inl (Heq ▸ rfl))
|
||||
(assume Hne : a₁ ≠ a₂, inr (assume Hn : some a₁ = some a₂, absurd (equal Hn) Hne))))
|
||||
end option
|
||||
|
|
|
|||
|
|
@ -1,30 +1,25 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
import logic.classes.inhabited logic.core.eq logic.classes.decidable
|
||||
|
||||
-- data.prod
|
||||
-- =========
|
||||
|
||||
-- The cartesian product.
|
||||
|
||||
import logic.classes.inhabited logic.core.eq logic.classes.decidable
|
||||
|
||||
open inhabited decidable
|
||||
|
||||
-- The cartesian product.
|
||||
inductive prod (A B : Type) : Type :=
|
||||
mk : A → B → prod A B
|
||||
mk : A → B → prod A B
|
||||
|
||||
abbreviation pair := @prod.mk
|
||||
|
||||
infixr `×` := prod
|
||||
|
||||
-- notation for n-ary tuples
|
||||
notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
|
||||
|
||||
namespace prod
|
||||
|
||||
section
|
||||
|
||||
parameters {A B : Type}
|
||||
|
||||
abbreviation pr1 (p : prod A B) := rec (λ x y, x) p
|
||||
|
|
@ -47,20 +42,18 @@ section
|
|||
theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) :=
|
||||
H1 ▸ H2 ▸ rfl
|
||||
|
||||
theorem prod_eq {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
|
||||
theorem equal [protected] {p1 p2 : prod A B} : ∀ (H1 : pr1 p1 = pr1 p2) (H2 : pr2 p1 = pr2 p2), p1 = p2 :=
|
||||
destruct p1 (take a1 b1, destruct p2 (take a2 b2 H1 H2, pair_eq H1 H2))
|
||||
|
||||
theorem prod_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
|
||||
theorem is_inhabited [protected] [instance] (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 [instance] (u v : A × B) (H1 : decidable (pr1 u = pr1 v))
|
||||
theorem has_decidable_eq [protected] [instance] (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, H ▸ and.intro rfl rfl)
|
||||
(assume H, and.elim H (assume H4 H5, prod_eq H4 H5)),
|
||||
(assume H, and.elim H (assume H4 H5, equal H4 H5)),
|
||||
decidable_iff_equiv _ (iff.symm H3)
|
||||
|
||||
end
|
||||
|
||||
end prod
|
||||
|
|
|
|||
|
|
@ -150,7 +150,7 @@ have Hy : pr2 (map_pair2 f v (pair e e)) = pr2 v, from
|
|||
pr2 (map_pair2 f v (pair e e)) = f (pr2 v) (pr2 (pair e e)) : by simp
|
||||
... = f (pr2 v) e : by simp
|
||||
... = pr2 v : Hid (pr2 v)),
|
||||
prod_eq Hx Hy
|
||||
prod.equal Hx Hy
|
||||
|
||||
theorem map_pair2_id_left {A B : Type} {f : B → A → A} {e : B} (Hid : ∀a : A, f e a = a)
|
||||
(v : A × A) : map_pair2 f (pair e e) v = v :=
|
||||
|
|
@ -164,7 +164,7 @@ have Hy : pr2 (map_pair2 f (pair e e) v) = pr2 v, from
|
|||
pr2 (map_pair2 f (pair e e) v) = f (pr2 (pair e e)) (pr2 v) : by simp
|
||||
... = f e (pr2 v) : by simp
|
||||
... = pr2 v : Hid (pr2 v),
|
||||
prod_eq Hx Hy
|
||||
prod.equal Hx Hy
|
||||
|
||||
opaque_hint (hiding flip map_pair map_pair2)
|
||||
|
||||
|
|
|
|||
|
|
@ -294,7 +294,7 @@ intro
|
|||
... = f (f a) : {Ha⁻¹}
|
||||
... = f a : representative_map_idempotent H1 H2 a
|
||||
... = elt_of u : Ha,
|
||||
show abs (elt_of u) = u, from subtype_eq H)
|
||||
show abs (elt_of u) = u, from subtype.equal H)
|
||||
(take u : image f,
|
||||
show R (elt_of u) (elt_of u), from
|
||||
obtain (a : A) (Ha : f a = elt_of u), from image_elt_of u,
|
||||
|
|
|
|||
|
|
@ -42,13 +42,12 @@ section
|
|||
... = dpair a1 b2' : {H2'}) H1)
|
||||
b2 H1 H2
|
||||
|
||||
theorem sigma_eq {p1 p2 : Σx : A, B x} :
|
||||
theorem equal [protected] {p1 p2 : Σx : A, B x} :
|
||||
∀(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 [instance] (H1 : inhabited A) (H2 : inhabited (B (default A))) :
|
||||
theorem is_inhabited [protected] [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)))
|
||||
|
||||
end
|
||||
end sigma
|
||||
|
|
|
|||
|
|
@ -7,14 +7,18 @@ import data.bool
|
|||
open bool inhabited
|
||||
|
||||
inductive char : Type :=
|
||||
mk : bool → bool → bool → bool → bool → bool → bool → bool → char
|
||||
mk : bool → bool → bool → bool → bool → bool → bool → bool → char
|
||||
|
||||
namespace char
|
||||
theorem is_inhabited [protected] [instance] : inhabited char :=
|
||||
inhabited.mk (mk ff ff ff ff ff ff ff ff)
|
||||
end char
|
||||
|
||||
inductive string : Type :=
|
||||
empty : string,
|
||||
str : char → string → string
|
||||
empty : string,
|
||||
str : char → string → string
|
||||
|
||||
theorem char_inhabited [instance] : inhabited char :=
|
||||
inhabited.mk (char.mk ff ff ff ff ff ff ff ff)
|
||||
|
||||
theorem string_inhabited [instance] : inhabited string :=
|
||||
inhabited.mk string.empty
|
||||
namespace string
|
||||
theorem is_inhabited [protected] [instance] : inhabited string :=
|
||||
inhabited.mk empty
|
||||
end string
|
||||
|
|
|
|||
|
|
@ -7,12 +7,11 @@ import logic.classes.inhabited logic.core.eq logic.classes.decidable
|
|||
open decidable
|
||||
|
||||
inductive subtype {A : Type} (P : A → Prop) : Type :=
|
||||
tag : Πx : A, P x → subtype P
|
||||
tag : Πx : A, P x → subtype P
|
||||
|
||||
notation `{` binders `,` r:(scoped P, subtype P) `}` := r
|
||||
|
||||
namespace subtype
|
||||
|
||||
section
|
||||
parameter {A : Type}
|
||||
parameter {P : A → Prop}
|
||||
|
|
@ -36,18 +35,16 @@ section
|
|||
theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
|
||||
eq.subst H3 (take H2, tag_irrelevant H1 H2) H2
|
||||
|
||||
theorem subtype_eq {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
|
||||
theorem equal [protected] {a1 a2 : {x, P x}} : ∀(H : elt_of a1 = elt_of a2), a1 = a2 :=
|
||||
destruct a1 (take x1 H1, destruct a2 (take x2 H2 H, tag_eq H))
|
||||
|
||||
theorem subtype_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
|
||||
theorem is_inhabited [protected] [instance] {a : A} (H : P a) : inhabited {x, P x} :=
|
||||
inhabited.mk (tag a H)
|
||||
|
||||
theorem eq_decidable [protected] [instance] (a1 a2 : {x, P x})
|
||||
theorem has_decidable_eq [protected] [instance] (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, eq.subst H rfl) (assume H, subtype_eq H),
|
||||
iff.intro (assume H, eq.subst H rfl) (assume H, equal H),
|
||||
decidable_iff_equiv _ (iff.symm H1)
|
||||
|
||||
end
|
||||
|
||||
end subtype
|
||||
|
|
|
|||
|
|
@ -1,83 +1,76 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
import logic.core.prop logic.classes.inhabited logic.classes.decidable
|
||||
open inhabited decidable eq_ops
|
||||
-- data.sum
|
||||
-- ========
|
||||
|
||||
-- The sum type, aka disjoint union.
|
||||
|
||||
import logic.core.prop logic.classes.inhabited logic.classes.decidable
|
||||
|
||||
open inhabited decidable eq_ops
|
||||
|
||||
-- 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
|
||||
inl : A → sum A B,
|
||||
inr : B → sum A B
|
||||
|
||||
namespace sum
|
||||
infixr `⊎` := sum
|
||||
infixr `⊎` := sum
|
||||
namespace extra_notation
|
||||
infixr `+`:25 := sum -- conflicts with notation for addition
|
||||
end extra_notation
|
||||
|
||||
namespace sum_plus_notation
|
||||
infixr `+`:25 := sum -- conflicts with notation for addition
|
||||
end sum_plus_notation
|
||||
abbreviation rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
|
||||
(H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
|
||||
rec H1 H2 s
|
||||
|
||||
abbreviation rec_on [protected] {A B : Type} {C : (A ⊎ B) → Type} (s : A ⊎ B)
|
||||
(H1 : ∀a : A, C (inl B a)) (H2 : ∀b : B, C (inr A b)) : C s :=
|
||||
rec H1 H2 s
|
||||
abbreviation cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
|
||||
(H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
|
||||
rec H1 H2 s
|
||||
|
||||
abbreviation cases_on [protected] {A B : Type} {P : (A ⊎ B) → Prop} (s : A ⊎ B)
|
||||
(H1 : ∀a : A, P (inl B a)) (H2 : ∀b : B, P (inr A b)) : P s :=
|
||||
rec H1 H2 s
|
||||
-- Here is the trick for the theorems that follow:
|
||||
-- Fixing a1, "f s" is a recursive description of "inl B a1 = s".
|
||||
-- When s is (inl B a1), it reduces to a1 = a1.
|
||||
-- When s is (inl B a2), it reduces to a1 = a2.
|
||||
-- When s is (inr A b), it reduces to false.
|
||||
|
||||
-- Here is the trick for the theorems that follow:
|
||||
-- Fixing a1, "f s" is a recursive description of "inl B a1 = s".
|
||||
-- When s is (inl B a1), it reduces to a1 = a1.
|
||||
-- When s is (inl B a2), it reduces to a1 = a2.
|
||||
-- When s is (inr A b), it reduces to false.
|
||||
theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
|
||||
let f := λs, rec_on s (λa, a1 = a) (λb, false) in
|
||||
have H1 : f (inl B a1), from rfl,
|
||||
have H2 : f (inl B a2), from H ▸ H1,
|
||||
H2
|
||||
|
||||
theorem inl_inj {A B : Type} {a1 a2 : A} (H : inl B a1 = inl B a2) : a1 = a2 :=
|
||||
let f := λs, rec_on s (λa, a1 = a) (λb, false) in
|
||||
have H1 : f (inl B a1), from rfl,
|
||||
have H2 : f (inl B a2), from H ▸ H1,
|
||||
H2
|
||||
theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
|
||||
let f := λs, rec_on s (λa', a = a') (λb, false) in
|
||||
have H1 : f (inl B a), from rfl,
|
||||
have H2 : f (inr A b), from H ▸ H1,
|
||||
H2
|
||||
|
||||
theorem inl_neq_inr {A B : Type} {a : A} {b : B} (H : inl B a = inr A b) : false :=
|
||||
let f := λs, rec_on s (λa', a = a') (λb, false) in
|
||||
have H1 : f (inl B a), from rfl,
|
||||
have H2 : f (inr A b), from H ▸ H1,
|
||||
H2
|
||||
theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 :=
|
||||
let f := λs, rec_on s (λa, false) (λb, b1 = b) in
|
||||
have H1 : f (inr A b1), from rfl,
|
||||
have H2 : f (inr A b2), from H ▸ H1,
|
||||
H2
|
||||
|
||||
theorem inr_inj {A B : Type} {b1 b2 : B} (H : inr A b1 = inr A b2) : b1 = b2 :=
|
||||
let f := λs, rec_on s (λa, false) (λb, b1 = b) in
|
||||
have H1 : f (inr A b1), from rfl,
|
||||
have H2 : f (inr A b2), from H ▸ H1,
|
||||
H2
|
||||
theorem is_inhabited_left [protected] [instance] {A B : Type} (H : inhabited A) : inhabited (A ⊎ B) :=
|
||||
inhabited.mk (inl B (default A))
|
||||
|
||||
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)
|
||||
(H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2))
|
||||
(H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
|
||||
rec_on s1
|
||||
(take a1, show decidable (inl B a1 = s2), from
|
||||
rec_on s2
|
||||
(take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
|
||||
(take b2,
|
||||
have H3 : (inl B a1 = inr A b2) ↔ false,
|
||||
from iff.intro inl_neq_inr (assume H4, false_elim H4),
|
||||
show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3)))
|
||||
(take b1, show decidable (inr A b1 = s2), from
|
||||
rec_on s2
|
||||
(take a2,
|
||||
have H3 : (inr A b1 = inl B a2) ↔ false,
|
||||
from iff.intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4),
|
||||
show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3))
|
||||
(take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
|
||||
theorem is_inhabited_right [protected] [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
|
||||
inhabited.mk (inr A (default B))
|
||||
|
||||
theorem has_eq_decidable [protected] [instance] {A B : Type} (s1 s2 : A ⊎ B)
|
||||
(H1 : ∀a1 a2 : A, decidable (inl B a1 = inl B a2))
|
||||
(H2 : ∀b1 b2 : B, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
|
||||
rec_on s1
|
||||
(take a1, show decidable (inl B a1 = s2), from
|
||||
rec_on s2
|
||||
(take a2, show decidable (inl B a1 = inl B a2), from H1 a1 a2)
|
||||
(take b2,
|
||||
have H3 : (inl B a1 = inr A b2) ↔ false,
|
||||
from iff.intro inl_neq_inr (assume H4, false_elim H4),
|
||||
show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3)))
|
||||
(take b1, show decidable (inr A b1 = s2), from
|
||||
rec_on s2
|
||||
(take a2,
|
||||
have H3 : (inr A b1 = inl B a2) ↔ false,
|
||||
from iff.intro (assume H4, inl_neq_inr (H4⁻¹)) (assume H4, false_elim H4),
|
||||
show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3))
|
||||
(take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
|
||||
end sum
|
||||
|
|
|
|||
|
|
@ -2,26 +2,22 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura
|
||||
import logic.classes.decidable logic.classes.inhabited
|
||||
|
||||
open decidable
|
||||
|
||||
inductive unit : Type :=
|
||||
star : unit
|
||||
|
||||
star : unit
|
||||
namespace unit
|
||||
notation `⋆`:max := star
|
||||
|
||||
notation `⋆`:max := star
|
||||
theorem equal [protected] (a b : unit) : a = b :=
|
||||
rec (rec rfl b) a
|
||||
|
||||
theorem at_most_one (a b : unit) : a = b :=
|
||||
rec (rec rfl b) a
|
||||
theorem eq_star (a : unit) : a = star :=
|
||||
equal a star
|
||||
|
||||
theorem eq_star (a : unit) : a = star :=
|
||||
at_most_one a star
|
||||
|
||||
theorem unit_inhabited [instance] : inhabited unit :=
|
||||
inhabited.mk ⋆
|
||||
|
||||
theorem decidable_eq [instance] (a b : unit) : decidable (a = b) :=
|
||||
inl (at_most_one a b)
|
||||
theorem is_inhabited [protected] [instance] : inhabited unit :=
|
||||
inhabited.mk ⋆
|
||||
|
||||
theorem has_decidable_eq [protected] [instance] (a b : unit) : decidable (a = b) :=
|
||||
inl (equal a b)
|
||||
end unit
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
empty.lean:6:25: error: type error in placeholder assigned to
|
||||
char_inhabited
|
||||
num_inhabited
|
||||
placeholder has type
|
||||
inhabited char
|
||||
inhabited num
|
||||
but is expected to have type
|
||||
inhabited ?M_1
|
||||
the assignment was attempted when trying to solve
|
||||
|
|
|
|||
Loading…
Reference in a new issue