refactor(library/standard): collect notation in general_notation
This commit is contained in:
Jeremy Avigad
Leonardo de Moura
parent
ad969b4695
commit
47a1c00a6d
22 changed files with 285 additions and 178 deletions
|
|
@ -49,7 +49,7 @@ bool_rec (bool_rec ff tt b) tt a
|
|||
theorem bor_tt_left (a : bool) : bor tt a = tt :=
|
||||
refl (bor tt a)
|
||||
|
||||
infixl `||`:65 := bor
|
||||
infixl `||` := bor
|
||||
|
||||
theorem bor_tt_right (a : bool) : a || tt = tt :=
|
||||
cases_on a (refl (ff || tt)) (refl (tt || tt))
|
||||
|
|
@ -87,7 +87,7 @@ bool_rec
|
|||
definition band (a b : bool) :=
|
||||
bool_rec ff (bool_rec ff tt b) a
|
||||
|
||||
infixl `&&`:75 := band
|
||||
infixl `&&` := band
|
||||
|
||||
theorem band_ff_left (a : bool) : ff && a = ff :=
|
||||
refl (ff && a)
|
||||
|
|
@ -132,7 +132,7 @@ band_eq_tt_elim_left (trans (band_comm b a) H)
|
|||
|
||||
definition bnot (a : bool) := bool_rec tt ff a
|
||||
|
||||
prefix `!`:85 := bnot
|
||||
notation `!` x:max := bnot x
|
||||
|
||||
theorem bnot_bnot (a : bool) : !!a = a :=
|
||||
cases_on a (refl (!!ff)) (refl (!!tt))
|
||||
|
|
|
|||
|
|
@ -189,7 +189,7 @@ representative_map_idempotent_equiv proj_rel @proj_congr a
|
|||
-- ## Definition of ℤ and basic theorems and definitions
|
||||
|
||||
definition int := image proj
|
||||
notation `ℤ`:max := int
|
||||
notation `ℤ` := int
|
||||
|
||||
definition psub : ℕ × ℕ → ℤ := fun_image proj
|
||||
definition rep : ℤ → ℕ × ℕ := subtype.elt_of
|
||||
|
|
@ -221,15 +221,12 @@ eq_abs quotient H
|
|||
|
||||
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
|
||||
|
||||
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)
|
||||
iff_mp (by simp) H2 (pair n m)
|
||||
|
||||
-- add_rewrite to_nat_comp --local
|
||||
|
||||
|
|
@ -263,20 +260,20 @@ calc
|
|||
|
||||
definition neg : ℤ → ℤ := quotient_map quotient flip
|
||||
|
||||
-- TODO: is this good?
|
||||
prefix `-`:80 := neg
|
||||
-- TODO: is this good? Note: replacing 100 by max makes it bind stronger than application.
|
||||
notation `-` x:100 := neg x
|
||||
|
||||
theorem neg_comp (n m : ℕ) : -psub (pair n m) = psub (pair m n) :=
|
||||
have H : ∀a, -psub a = psub (flip a),
|
||||
theorem neg_comp (n m : ℕ) : -(psub (pair n m)) = psub (pair m n) :=
|
||||
have H : ∀a, -(psub a) = psub (flip a),
|
||||
from take a, comp_quotient_map quotient @rel_flip (rel_refl _),
|
||||
calc
|
||||
-psub (pair n m) = psub (flip (pair n m)) : H (pair n m)
|
||||
-(psub (pair n m)) = psub (flip (pair n m)) : H (pair n m)
|
||||
... = psub (pair m n) : by simp
|
||||
|
||||
-- add_rewrite neg_comp --local
|
||||
|
||||
theorem neg_zero : -0 = 0 :=
|
||||
calc -psub (pair 0 0) = psub (pair 0 0) : neg_comp 0 0
|
||||
calc -(psub (pair 0 0)) = psub (pair 0 0) : neg_comp 0 0
|
||||
|
||||
theorem neg_neg (a : ℤ) : -(-a) = a :=
|
||||
obtain (xa ya : ℕ) (Ha : a = psub (pair xa ya)), from destruct a,
|
||||
|
|
@ -285,7 +282,7 @@ by simp
|
|||
-- add_rewrite neg_neg neg_zero
|
||||
|
||||
theorem neg_inj {a b : ℤ} (H : -a = -b) : a = b :=
|
||||
(by simp) ◂ congr_arg neg H
|
||||
iff_mp (by simp) (congr_arg neg H)
|
||||
|
||||
theorem neg_move {a b : ℤ} (H : -a = b) : -b = a :=
|
||||
subst H (neg_neg a)
|
||||
|
|
@ -296,7 +293,7 @@ by simp
|
|||
|
||||
theorem pos_eq_neg {n m : ℕ} (H : n = -m) : n = 0 ∧ m = 0 :=
|
||||
have H2 : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl (n),
|
||||
have H3 : psub (pair n 0) = psub (pair 0 m), from (by simp) ◂ H,
|
||||
have H3 : psub (pair n 0) = psub (pair 0 m), from iff_mp (by simp) H,
|
||||
have H4 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient rel_refl H3,
|
||||
have H5 : n + m = 0, from
|
||||
calc
|
||||
|
|
@ -329,8 +326,8 @@ or_imp_or (or_swap (proj_zero_or (rep a)))
|
|||
a = psub (rep a) : symm (psub_rep a)
|
||||
... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {symm (prod_ext (rep a))}
|
||||
... = psub (pair 0 (pr2 (rep a))) : {H2}
|
||||
... = -psub (pair (pr2 (rep a)) 0) : by simp
|
||||
... = -of_nat (pr2 (rep a)) : refl _))
|
||||
... = -(psub (pair (pr2 (rep a)) 0)) : by simp
|
||||
... = -(of_nat (pr2 (rep a))) : refl _))
|
||||
|
||||
opaque_hint (hiding int)
|
||||
|
||||
|
|
@ -342,35 +339,35 @@ or_elim (cases a)
|
|||
(assume H, obtain (n : ℕ) (H3 : a = -n), from H, subst (symm H3) (H2 n))
|
||||
|
||||
---reverse equalities, rename
|
||||
theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - of_nat (succ n)) :=
|
||||
theorem cases_succ (a : ℤ) : (∃n : ℕ, a = of_nat n) ∨ (∃n : ℕ, a = - (of_nat (succ n))) :=
|
||||
or_elim (cases a)
|
||||
(assume H : (∃n : ℕ, a = of_nat n), or_intro_left _ H)
|
||||
(assume H,
|
||||
obtain (n : ℕ) (H2 : a = -of_nat n), from H,
|
||||
obtain (n : ℕ) (H2 : a = -(of_nat n)), from H,
|
||||
discriminate
|
||||
(assume H3 : n = 0,
|
||||
have H4 : a = of_nat 0, from
|
||||
calc
|
||||
a = - of_nat n : H2
|
||||
... = - of_nat 0 : {H3}
|
||||
a = -(of_nat n) : H2
|
||||
... = -(of_nat 0) : {H3}
|
||||
... = of_nat 0 : neg_zero,
|
||||
or_intro_left _ (exists_intro 0 H4))
|
||||
(take k : ℕ,
|
||||
assume H3 : n = succ k,
|
||||
have H4 : a = - of_nat (succ k), from subst H3 H2,
|
||||
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 :=
|
||||
(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))
|
||||
(assume H, obtain (n : ℕ) (H3 : a = -(of_nat (succ n))), from H, subst (symm H3) (H2 n))
|
||||
|
||||
theorem of_nat_eq_neg_of_nat {n m : ℕ} (H : n = - m) : n = 0 ∧ m = 0 :=
|
||||
have H2 : n = psub (pair 0 m), from
|
||||
calc
|
||||
n = -m : H
|
||||
... = -psub (pair m 0) : refl (-m)
|
||||
... = -(psub (pair m 0)) : refl (-m)
|
||||
... = psub (pair 0 m) : by simp,
|
||||
have H3 : rel (pair n 0) (pair 0 m), from R_intro_refl quotient rel_refl H2,
|
||||
have H4 : n + m = 0, from
|
||||
|
|
@ -451,9 +448,6 @@ have H : dist (xa + xb) (ya + yb) ≤ dist xa ya + dist xb yb,
|
|||
from dist_add_le_add_dist xa xb ya yb,
|
||||
by simp
|
||||
|
||||
-- TODO: add this to eq
|
||||
-- notation A `=` B `:` C := @eq C A B
|
||||
|
||||
-- TODO: note, we have to add #nat to get the right interpretation
|
||||
theorem add_of_nat (n m : nat) : of_nat n + of_nat m = #nat n + m := -- this is of_nat (n + m)
|
||||
have H : ∀n : ℕ, n = psub (pair n 0), from take n : ℕ, refl n,
|
||||
|
|
@ -466,7 +460,7 @@ by simp
|
|||
|
||||
-- ## sub
|
||||
definition sub (a b : ℤ) : ℤ := a + -b
|
||||
infixl `-`:65 := int.sub
|
||||
infixl `-` := int.sub
|
||||
|
||||
theorem sub_def (a b : ℤ) : a - b = a + -b :=
|
||||
refl (a - b)
|
||||
|
|
@ -938,14 +932,14 @@ iff_intro
|
|||
-- ----------------------------------------------
|
||||
|
||||
definition lt (a b : ℤ) := a + 1 ≤ b
|
||||
infix `<` := int.lt
|
||||
infix `<` := int.lt
|
||||
|
||||
definition ge (a b : ℤ) := b ≤ a
|
||||
infix `>=` := int.ge
|
||||
infix `≥` := int.ge
|
||||
|
||||
definition gt (a b : ℤ) := b < a
|
||||
infix `>` := int.gt
|
||||
infix `>` := int.gt
|
||||
|
||||
theorem lt_def (a b : ℤ) : a < b ↔ a + 1 ≤ b :=
|
||||
iff_refl (a < b)
|
||||
|
|
|
|||
|
|
@ -27,7 +27,7 @@ inductive list (T : Type) : Type :=
|
|||
nil {} : list T,
|
||||
cons : T → list T → list T
|
||||
|
||||
infix `::` : 65 := cons
|
||||
infix `::` := cons
|
||||
|
||||
section
|
||||
|
||||
|
|
@ -189,7 +189,7 @@ list_cases_on l
|
|||
|
||||
definition mem (x : T) : list T → Prop := list_rec false (fun y l H, x = y ∨ H)
|
||||
|
||||
infix `∈` : 50 := mem
|
||||
infix `∈` := mem
|
||||
|
||||
-- TODO: constructively, equality is stronger. Use that?
|
||||
theorem mem_nil (x : T) : x ∈ nil ↔ false := iff_refl _
|
||||
|
|
@ -202,7 +202,7 @@ list_induction_on s (or_intro_right _)
|
|||
assume IH : x ∈ s ++ t → x ∈ s ∨ x ∈ t,
|
||||
assume H1 : x ∈ (y :: s) ++ t,
|
||||
have H2 : x = y ∨ x ∈ s ++ t, from H1,
|
||||
have H3 : x = y ∨ x ∈ s ∨ x ∈ t, from imp_or_right H2 IH,
|
||||
have H3 : x = y ∨ x ∈ s ∨ x ∈ t, from or_imp_or_right H2 IH,
|
||||
iff_elim_right (or_assoc _ _ _) H3)
|
||||
|
||||
theorem mem_or_imp_concat (x : T) (s t : list T) : x ∈ s ∨ x ∈ t → x ∈ s ++ t :=
|
||||
|
|
@ -286,6 +286,6 @@ theorem nth_succ (x0 : T) (l : list T) (n : ℕ) : nth x0 l (succ n) = nth x0 (t
|
|||
end
|
||||
|
||||
-- declare global notation outside the section
|
||||
infixl `++` : 65 := concat
|
||||
infixl `++` := concat
|
||||
|
||||
end list
|
||||
|
|
|
|||
|
|
@ -2,24 +2,20 @@
|
|||
--- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
--- Author: Floris van Doorn
|
||||
|
||||
import logic data.num tools.tactic struc.binary
|
||||
using num tactic binary eq_ops
|
||||
using decidable (hiding induction_on rec_on)
|
||||
using relation -- for subst_iff
|
||||
|
||||
-- TODO: this should go in tools, I think
|
||||
namespace helper_tactics
|
||||
definition apply_refl := apply @refl
|
||||
tactic_hint apply_refl
|
||||
end helper_tactics
|
||||
using helper_tactics
|
||||
|
||||
|
||||
-- data.nat.basic
|
||||
-- ==============
|
||||
--
|
||||
-- Basic operations on the natural numbers.
|
||||
|
||||
import logic data.num tools.tactic struc.binary tools.helper_tactics
|
||||
|
||||
using num tactic binary eq_ops
|
||||
using decidable (hiding induction_on rec_on)
|
||||
using relation -- for subst_iff
|
||||
|
||||
using helper_tactics
|
||||
|
||||
|
||||
-- Definition of the type
|
||||
-- ----------------------
|
||||
|
||||
|
|
@ -28,7 +24,7 @@ inductive nat : Type :=
|
|||
zero : nat,
|
||||
succ : nat → nat
|
||||
|
||||
notation `ℕ`:max := nat
|
||||
notation `ℕ` := nat
|
||||
|
||||
theorem nat_rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x
|
||||
|
||||
|
|
@ -160,7 +156,7 @@ general m
|
|||
|
||||
definition add (x y : ℕ) : ℕ := plus x y
|
||||
|
||||
infixl `+` : 65 := add
|
||||
infixl `+` := add
|
||||
|
||||
theorem add_zero_right (n : ℕ) : n + 0 = n
|
||||
|
||||
|
|
@ -295,7 +291,7 @@ nat_rec H1 (take n IH, (add_one n) ▸ (H2 n IH)) a
|
|||
|
||||
definition mul (n m : ℕ) := nat_rec 0 (fun m x, x + n) m
|
||||
|
||||
infixl `*`:70 := mul
|
||||
infixl `*` := mul
|
||||
|
||||
theorem mul_zero_right (n:ℕ) : n * 0 = 0
|
||||
|
||||
|
|
@ -414,4 +410,5 @@ discriminate
|
|||
-- add_rewrite mul_succ_left mul_succ_right
|
||||
-- add_rewrite mul_comm mul_assoc mul_left_comm
|
||||
-- add_rewrite mul_distr_right mul_distr_left
|
||||
|
||||
end nat
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Jeremy Avigad
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
import data.nat.sub
|
||||
import .basic .order .sub .div
|
||||
|
|
|
|||
|
|
@ -8,15 +8,10 @@
|
|||
-- This is a continuation of the development of the natural numbers, with a general way of
|
||||
-- defining recursive functions, and definitions of div, mod, and gcd.
|
||||
|
||||
-- TODO: replace the two uses of "not_or" by a constructive version
|
||||
|
||||
import logic .sub struc.relation data.prod
|
||||
|
||||
-- TODO: show decidability of le and remove these
|
||||
import logic.classes.decidable
|
||||
import logic.axioms.classical
|
||||
import logic.axioms.prop_decidable
|
||||
|
||||
import logic.axioms.funext -- is this really needed?
|
||||
|
||||
import tools.fake_simplifier
|
||||
|
||||
using nat relation relation.iff_ops prod
|
||||
|
|
@ -25,7 +20,7 @@ using fake_simplifier decidable
|
|||
namespace nat
|
||||
|
||||
-- A general recursion principle
|
||||
-- =============================
|
||||
-- -----------------------------
|
||||
--
|
||||
-- Data:
|
||||
--
|
||||
|
|
@ -161,7 +156,7 @@ show lhs = rhs, from
|
|||
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 H2 : y ≠ 0 ∧ ¬ x < y, from sorry, -- subst (not_or _ _) H1,
|
||||
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,
|
||||
|
|
@ -177,7 +172,7 @@ rec_measure_spec (div_aux_rec y) (div_aux_decreasing y) x
|
|||
|
||||
definition idivide (x : ℕ) (y : ℕ) : ℕ := div_aux y x
|
||||
|
||||
infixl `div`:70 := idivide -- copied from Isabelle
|
||||
infixl `div` := idivide -- copied from Isabelle
|
||||
|
||||
theorem div_zero (x : ℕ) : x div 0 = 0 :=
|
||||
trans (div_aux_spec _ _) (if_pos (or_intro_left _ (refl _)) _ _)
|
||||
|
|
@ -237,7 +232,7 @@ show lhs = rhs, from
|
|||
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 H2 : y ≠ 0 ∧ ¬ x < y, from sorry, -- subst (not_or _ _) H1,
|
||||
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,
|
||||
|
|
@ -253,7 +248,7 @@ rec_measure_spec (mod_aux_rec y) (mod_aux_decreasing y) x
|
|||
|
||||
definition modulo (x : ℕ) (y : ℕ) : ℕ := mod_aux y x
|
||||
|
||||
infixl `mod`:70 := modulo
|
||||
infixl `mod` := modulo
|
||||
|
||||
theorem mod_zero (x : ℕ) : x mod 0 = x :=
|
||||
trans (mod_aux_spec _ _) (if_pos (or_intro_left _ (refl _)) _ _)
|
||||
|
|
@ -298,7 +293,7 @@ theorem mod_mul_self_right (m n : ℕ) : (m * n) mod n = 0 :=
|
|||
case_zero_pos n (by simp)
|
||||
(take n,
|
||||
assume npos : n > 0,
|
||||
(by simp) ◂ (mod_add_mul_self_right 0 m npos))
|
||||
subst (by simp) (mod_add_mul_self_right 0 m npos))
|
||||
|
||||
-- add_rewrite mod_mul_self_right
|
||||
|
||||
|
|
@ -425,19 +420,19 @@ case n (by simp)
|
|||
(take n,
|
||||
have H : (succ n * 1) mod (succ n * 1) = succ n * (1 mod 1),
|
||||
from mod_mul_mul 1 1 (succ_pos n),
|
||||
(by simp) ◂ H)
|
||||
subst (by simp) H)
|
||||
|
||||
-- add_rewrite mod_self
|
||||
|
||||
theorem div_one (n : ℕ) : n div 1 = n :=
|
||||
have H : n div 1 * 1 + n mod 1 = n, from symm (div_mod_eq n 1),
|
||||
(by simp) ◂ H
|
||||
subst (by simp) H
|
||||
|
||||
-- add_rewrite div_one
|
||||
|
||||
theorem pos_div_self {n : ℕ} (H : n > 0) : n div n = 1 :=
|
||||
have H1 : (n * 1) div (n * 1) = 1 div 1, from div_mul_mul 1 1 H,
|
||||
(by simp) ◂ H1
|
||||
subst (by simp) H1
|
||||
|
||||
-- add_rewrite pos_div_self
|
||||
|
||||
|
|
@ -446,7 +441,7 @@ have H1 : (n * 1) div (n * 1) = 1 div 1, from div_mul_mul 1 1 H,
|
|||
|
||||
definition dvd (x y : ℕ) : Prop := y mod x = 0
|
||||
|
||||
infix `|`:50 := dvd
|
||||
infix `|` := dvd
|
||||
|
||||
theorem dvd_iff_mod_eq_zero (x y : ℕ) : x | y ↔ y mod x = 0 :=
|
||||
refl _
|
||||
|
|
|
|||
|
|
@ -2,6 +2,11 @@
|
|||
--- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
--- Author: Floris van Doorn
|
||||
|
||||
-- data.nat.order
|
||||
-- ==============
|
||||
--
|
||||
-- The ordering on the natural numbers
|
||||
|
||||
import .basic logic.classes.decidable
|
||||
import tools.fake_simplifier
|
||||
|
||||
|
|
@ -9,27 +14,16 @@ using nat eq_ops tactic
|
|||
using fake_simplifier
|
||||
using decidable (decidable inl inr)
|
||||
|
||||
-- TODO: move these to logic.connectives
|
||||
theorem or_imp_or_left {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) : c ∨ b :=
|
||||
or_imp_or H1 H2 (λx, x)
|
||||
|
||||
theorem or_imp_or_right {a b c : Prop} (H1 : a ∨ b) (H2 : b → c) : a ∨ c :=
|
||||
or_imp_or H1 (λx, x) H2
|
||||
|
||||
namespace nat
|
||||
|
||||
-- data.nat.order
|
||||
-- ==============
|
||||
--
|
||||
-- The ordering on the natural numbers
|
||||
|
||||
-- Less than or equal
|
||||
-- ------------------
|
||||
|
||||
definition le (n m : ℕ) : Prop := exists k : nat, n + k = m
|
||||
|
||||
infix `<=`:50 := le
|
||||
infix `≤`:50 := le
|
||||
infix `<=` := le
|
||||
infix `≤` := le
|
||||
|
||||
theorem le_intro {n m k : ℕ} (H : n + k = m) : n ≤ m :=
|
||||
exists_intro k H
|
||||
|
|
@ -265,14 +259,14 @@ general n
|
|||
-- ge and gt will be transparent, so we don't need to reprove theorems for le and lt for them
|
||||
|
||||
definition lt (n m : ℕ) := succ n ≤ m
|
||||
infix `<` : 50 := lt
|
||||
infix `<` := lt
|
||||
|
||||
abbreviation ge (n m : ℕ) := m ≤ n
|
||||
infix `>=` : 50 := ge
|
||||
infix `≥` : 50 := ge
|
||||
infix `>=` := ge
|
||||
infix `≥` := ge
|
||||
|
||||
abbreviation gt (n m : ℕ) := m < n
|
||||
infix `>` : 50 := gt
|
||||
infix `>` := gt
|
||||
|
||||
theorem lt_def (n m : ℕ) : (n < m) = (succ n ≤ m) := refl (n < m)
|
||||
|
||||
|
|
@ -467,6 +461,7 @@ strong_induction_on a (
|
|||
show P (succ n), from
|
||||
Hind n (take m, assume H1 : m ≤ n, H _ (le_imp_lt_succ H1))))
|
||||
|
||||
|
||||
-- Positivity
|
||||
-- ---------
|
||||
--
|
||||
|
|
@ -474,8 +469,6 @@ strong_induction_on a (
|
|||
|
||||
-- ### basic
|
||||
|
||||
-- See also succ_pos.
|
||||
|
||||
theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0 → P y) : P y :=
|
||||
case y H0 (take y', H1 _ (succ_pos _))
|
||||
|
||||
|
|
@ -527,8 +520,6 @@ discriminate
|
|||
theorem mul_pos_imp_pos_right {m n : ℕ} (H : n * m > 0) : m > 0 :=
|
||||
mul_pos_imp_pos_left ((mul_comm n m) ▸ H)
|
||||
|
||||
-- See also mul_eq_one below.
|
||||
|
||||
-- ### interaction of mul with le and lt
|
||||
|
||||
theorem mul_lt_left {n m k : ℕ} (Hk : k > 0) (H : n < m) : k * n < k * m :=
|
||||
|
|
@ -601,7 +592,4 @@ or_elim (le_or_gt n 1)
|
|||
theorem mul_eq_one_right {n m : ℕ} (H : n * m = 1) : m = 1 :=
|
||||
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,26 +2,26 @@
|
|||
--- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
--- Author: Floris van Doorn
|
||||
|
||||
-- data.nat.sub
|
||||
-- ============
|
||||
--
|
||||
-- Subtraction on the natural numbers, as well as min, max, and distance.
|
||||
|
||||
import data.nat.order
|
||||
import tools.fake_simplifier
|
||||
|
||||
using nat eq_ops tactic
|
||||
using helper_tactics
|
||||
|
||||
using fake_simplifier
|
||||
|
||||
namespace nat
|
||||
|
||||
-- data.nat.basic2
|
||||
-- ===============
|
||||
--
|
||||
-- More basic operations on the natural numbers.
|
||||
|
||||
-- subtraction
|
||||
-- -----------
|
||||
|
||||
definition sub (n m : ℕ) : nat := nat_rec n (fun m x, pred x) m
|
||||
infixl `-` : 65 := sub
|
||||
infixl `-` := sub
|
||||
|
||||
theorem sub_zero_right (n : ℕ) : n - 0 = n
|
||||
|
||||
|
|
@ -491,7 +491,7 @@ by simp
|
|||
|
||||
-- add_rewrite dist_mul_right dist_mul_left dist_comm
|
||||
|
||||
--needed to prove |a| * |b| = |a * b| in int
|
||||
--needed to prove of_nat a * of_nat b = of_nat (a * b) in int
|
||||
theorem dist_mul_dist (n m k l : ℕ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) :=
|
||||
have aux : ∀k l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
|
||||
take k l : ℕ,
|
||||
|
|
|
|||
|
|
@ -2,6 +2,11 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
-- data.prod
|
||||
-- =========
|
||||
|
||||
-- The cartesian product.
|
||||
|
||||
import logic.classes.inhabited logic.connectives.eq logic.classes.decidable
|
||||
|
||||
using inhabited decidable
|
||||
|
|
@ -9,8 +14,7 @@ using inhabited decidable
|
|||
inductive prod (A B : Type) : Type :=
|
||||
pair : A → B → prod A B
|
||||
|
||||
precedence `×`:30
|
||||
infixr × := prod
|
||||
infixr `×` := prod
|
||||
|
||||
-- notation for n-ary tuples
|
||||
notation `(` h `,` t:(foldl `,` (e r, pair r e) h) `)` := t
|
||||
|
|
|
|||
|
|
@ -10,13 +10,13 @@ using eq_ops bool
|
|||
namespace set
|
||||
definition set (T : Type) := T → bool
|
||||
definition mem {T : Type} (x : T) (s : set T) := (s x) = tt
|
||||
infix `∈`:50 := mem
|
||||
infix `∈` := mem
|
||||
|
||||
section
|
||||
parameter {T : Type}
|
||||
|
||||
definition empty : set T := λx, ff
|
||||
notation `∅`:max := empty
|
||||
notation `∅` := empty
|
||||
|
||||
theorem mem_empty (x : T) : ¬ (x ∈ ∅) :=
|
||||
assume H : x ∈ ∅, absurd H ff_ne_tt
|
||||
|
|
@ -26,7 +26,7 @@ definition univ : set T := λx, tt
|
|||
theorem mem_univ (x : T) : x ∈ univ := refl _
|
||||
|
||||
definition inter (A B : set T) : set T := λx, A x && B x
|
||||
infixl `∩`:70 := inter
|
||||
infixl `∩` := inter
|
||||
|
||||
theorem mem_inter (x : T) (A B : set T) : x ∈ A ∩ B ↔ (x ∈ A ∧ x ∈ B) :=
|
||||
iff_intro
|
||||
|
|
@ -43,7 +43,7 @@ theorem inter_assoc (A B C : set T) : (A ∩ B) ∩ C = A ∩ (B ∩ C) :=
|
|||
funext (λx, band_assoc (A x) (B x) (C x))
|
||||
|
||||
definition union (A B : set T) : set T := λx, A x || B x
|
||||
infixl `∪`:65 := union
|
||||
infixl `∪` := union
|
||||
|
||||
theorem mem_union (x : T) (A B : set T) : x ∈ A ∪ B ↔ (x ∈ A ∨ x ∈ B) :=
|
||||
iff_intro
|
||||
|
|
@ -61,4 +61,5 @@ theorem union_assoc (A B C : set T) : (A ∪ B) ∪ C = A ∪ (B ∪ C) :=
|
|||
funext (λx, bor_assoc (A x) (B x) (C x))
|
||||
|
||||
end
|
||||
|
||||
end set
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@ using decidable
|
|||
inductive subtype {A : Type} (P : A → Prop) : Type :=
|
||||
tag : Πx : A, P x → subtype P
|
||||
|
||||
notation `{` binders `|` r:(scoped P, subtype P) `}` := r
|
||||
notation `{` binders `,` r:(scoped P, subtype P) `}` := r
|
||||
|
||||
namespace subtype
|
||||
|
||||
|
|
@ -18,12 +18,12 @@ section
|
|||
parameter {P : A → Prop}
|
||||
|
||||
-- TODO: make this a coercion?
|
||||
definition elt_of (a : {x | P x}) : A := subtype_rec (λ x y, x) a
|
||||
theorem has_property (a : {x | P x}) : P (elt_of a) := subtype_rec (λ x y, y) a
|
||||
definition elt_of (a : {x, P x}) : A := subtype_rec (λ x y, x) a
|
||||
theorem has_property (a : {x, P x}) : P (elt_of a) := subtype_rec (λ x y, y) a
|
||||
|
||||
theorem elt_of_tag (a : A) (H : P a) : elt_of (tag a H) = a := refl a
|
||||
|
||||
theorem subtype_destruct {Q : {x | P x} → Prop} (a : {x | P x})
|
||||
theorem subtype_destruct {Q : {x, P x} → Prop} (a : {x, P x})
|
||||
(H : ∀(x : A) (H1 : P x), Q (tag x H1)) : Q a :=
|
||||
subtype_rec H a
|
||||
|
||||
|
|
@ -35,13 +35,13 @@ section
|
|||
theorem tag_eq {a1 a2 : A} {H1 : P a1} {H2 : P a2} (H3 : a1 = a2) : tag a1 H1 = tag a2 H2 :=
|
||||
(show ∀(H2 : P a2), tag a1 H1 = tag a2 H2, from 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 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))
|
||||
|
||||
theorem subtype_inhabited {a : A} (H : P a) : inhabited {x | P x} :=
|
||||
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})
|
||||
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),
|
||||
|
|
|
|||
|
|
@ -2,6 +2,11 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
-- data.sum
|
||||
-- ========
|
||||
|
||||
-- The sum type, aka disjoint union.
|
||||
|
||||
import logic.connectives.prop logic.classes.inhabited logic.classes.decidable
|
||||
|
||||
using inhabited decidable
|
||||
|
|
@ -13,13 +18,17 @@ inductive sum (A B : Type) : Type :=
|
|||
inl : A → sum A B,
|
||||
inr : B → sum A B
|
||||
|
||||
infixr `+`:25 := sum
|
||||
infixr `⊎` := sum
|
||||
|
||||
abbreviation rec_on {A B : Type} {C : (A + B) → Type} (s : A + B)
|
||||
namespace sum_plus_notation
|
||||
infixr `+`:25 := sum -- conflicts with notation for addition
|
||||
end sum_plus_notation
|
||||
|
||||
abbreviation rec_on {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 :=
|
||||
sum_rec H1 H2 s
|
||||
|
||||
abbreviation cases_on {A B : Type} {P : (A + B) → Prop} (s : A + B)
|
||||
abbreviation cases_on {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 :=
|
||||
sum_rec H1 H2 s
|
||||
|
||||
|
|
@ -47,13 +56,13 @@ have H1 : f (inr A b1), from rfl,
|
|||
have H2 : f (inr A b2), from subst H H1,
|
||||
H2
|
||||
|
||||
theorem sum_inhabited_left [instance] {A B : Type} (H : inhabited A) : inhabited (A + B) :=
|
||||
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) :=
|
||||
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)
|
||||
theorem sum_eq_decidable [instance] {A B : Type} (s1 s2 : A ⊎ B)
|
||||
(H1 : ∀a1 a2, decidable (inl B a1 = inl B a2))
|
||||
(H2 : ∀b1 b2, decidable (inr A b1 = inr A b2)) : decidable (s1 = s2) :=
|
||||
rec_on s1
|
||||
|
|
|
|||
|
|
@ -2,8 +2,80 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Author: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
-- General notation
|
||||
-- ----------------
|
||||
-- general_notation
|
||||
-- ================
|
||||
|
||||
-- General operations
|
||||
-- ------------------
|
||||
|
||||
notation `assume` binders `,` r:(scoped f, f) := r
|
||||
notation `take` binders `,` r:(scoped f, f) := r
|
||||
|
||||
|
||||
-- Global declarations of right binding strength
|
||||
-- ---------------------------------------------
|
||||
|
||||
-- If a module reassigns these, it will be incompatible with other modules that adhere to these
|
||||
-- conventions.
|
||||
|
||||
-- ### Logical operations and relations
|
||||
|
||||
precedence `¬`:40
|
||||
precedence `/\`:35 -- infixr
|
||||
precedence `∧`:35 -- infixr
|
||||
precedence `\/`:30 -- infixr
|
||||
precedence `∨`:30 -- infixr
|
||||
precedence `<->`:25
|
||||
precedence `↔`:25
|
||||
|
||||
precedence `=`:50
|
||||
precedence `≠`:50
|
||||
precedence `rfl`:max -- shorthand for reflexivity
|
||||
|
||||
precedence `⁻¹`:100
|
||||
precedence `⬝`:75 -- infixr
|
||||
precedence `▸`:75 -- infixr
|
||||
|
||||
-- ### types and type constructors
|
||||
|
||||
precedence `ℕ`:max
|
||||
precedence `ℤ`:max
|
||||
|
||||
precedence `⊎`:25 -- infixr
|
||||
precedence `×`:30 -- infixr
|
||||
|
||||
-- ### arithmetic operations
|
||||
|
||||
precedence `+`:65 -- infixl
|
||||
precedence `-`:65 -- infixl; for negation, follow by rbp 100
|
||||
precedence `*`:70 -- infixl
|
||||
precedence `div`:70 -- infixl
|
||||
precedence `mod`:70 -- infixl
|
||||
|
||||
precedence `<=`:50
|
||||
precedence `≤`:50
|
||||
precedence `<`:50
|
||||
precedence `>=`:50
|
||||
precedence `≥`:50
|
||||
precedence `>`:50
|
||||
|
||||
-- ### boolean operations
|
||||
|
||||
precedence `&&`:70 -- infixl
|
||||
precedence `||`:65 -- infixl
|
||||
precedence `!`:85 -- boolean negation, follow by rbp 100
|
||||
|
||||
-- ### set operations
|
||||
|
||||
precedence `∈`:50
|
||||
precedence `∅`:max
|
||||
precedence `∩`:70
|
||||
precedence `∪`:65
|
||||
|
||||
-- ### other symbols
|
||||
|
||||
-- uncomment when inductive type syntax has changed
|
||||
|
||||
precedence `|`:55 -- used for absolute value, subtypes, divisibility
|
||||
precedence `++`:65 -- list append
|
||||
precedence `::`:65 -- list cons
|
||||
|
|
@ -15,7 +15,7 @@ namespace fibrant
|
|||
axiom unit_fibrant : fibrant unit
|
||||
axiom nat_fibrant : fibrant nat
|
||||
axiom bool_fibrant : fibrant bool
|
||||
axiom sum_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A + B)
|
||||
axiom sum_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A ⊎ B)
|
||||
axiom prod_fibrant {A B : Type} (C1 : fibrant A) (C2 : fibrant B) : fibrant (A × B)
|
||||
axiom sigma_fibrant {A : Type} {B : A → Type} (C1 : fibrant A) (C2 : Πx : A, fibrant (B x)) :
|
||||
fibrant (Σx : A, B x)
|
||||
|
|
@ -30,6 +30,6 @@ instance prod_fibrant
|
|||
instance sigma_fibrant
|
||||
instance pi_fibrant
|
||||
|
||||
theorem test_fibrant : fibrant (nat × (nat + nat)) := _
|
||||
theorem test_fibrant : fibrant (nat × (nat ⊎ nat)) := _
|
||||
|
||||
end fibrant
|
||||
|
|
@ -50,7 +50,7 @@ case (λ x, (¬¬x) = x)
|
|||
a
|
||||
|
||||
theorem not_not_elim {a : Prop} (H : ¬¬a) : a :=
|
||||
(not_not_eq a) ◂ H
|
||||
(not_not_eq a) ▸ H
|
||||
|
||||
theorem propext {a b : Prop} (Hab : a → b) (Hba : b → a) : a = b :=
|
||||
or_elim (prop_complete a)
|
||||
|
|
@ -125,7 +125,7 @@ propext
|
|||
(assume Ha : a, or_inr (H Ha))
|
||||
(assume Hna : ¬a, or_inl Hna)))
|
||||
(assume (H : ¬a ∨ b) (Ha : a),
|
||||
resolve_right H ((not_not_eq a)⁻¹ ◂ Ha))
|
||||
resolve_right H ((not_not_eq a)⁻¹ ▸ Ha))
|
||||
|
||||
theorem not_implies (a b : Prop) : (¬(a → b)) = (a ∧ ¬b) :=
|
||||
calc (¬(a → b)) = (¬(¬a ∨ b)) : {imp_or a b}
|
||||
|
|
|
|||
|
|
@ -2,29 +2,33 @@
|
|||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Leonardo de Moura, Jeremy Avigad
|
||||
|
||||
import logic.connectives.eq logic.connectives.quantifiers
|
||||
import logic.classes.inhabited logic.classes.nonempty
|
||||
import data.subtype data.sum
|
||||
|
||||
using subtype inhabited nonempty
|
||||
|
||||
-- logic.axioms.hilbert
|
||||
-- ====================
|
||||
|
||||
-- Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the
|
||||
-- constructive one).
|
||||
|
||||
import logic.connectives.eq logic.connectives.quantifiers
|
||||
import logic.classes.inhabited logic.classes.nonempty
|
||||
import data.subtype data.sum
|
||||
|
||||
using subtype inhabited nonempty
|
||||
|
||||
|
||||
-- the axiom
|
||||
-- ---------
|
||||
|
||||
axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A) :
|
||||
{x : A | (∃x : A, P x) → P x}
|
||||
{x : A, (∃x : A, P x) → P x}
|
||||
|
||||
-- In the presence of classical logic, we could prove this from the weaker
|
||||
-- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : { x : A | P x }
|
||||
-- axiom indefinite_description {A : Type} {P : A->Prop} (H : ∃x, P x) : {x : A, P x}
|
||||
|
||||
theorem nonempty_imp_exists_true {A : Type} (H : nonempty A) : ∃x : A, true :=
|
||||
nonempty_elim H (take x, exists_intro x trivial)
|
||||
|
||||
theorem nonempty_imp_inhabited {A : Type} (H : nonempty A) : inhabited A :=
|
||||
let u : {x : A | (∃x : A, true) → true} := strong_indefinite_description (λa, true) H in
|
||||
let u : {x : A, (∃x : A, true) → true} := strong_indefinite_description (λa, true) H in
|
||||
inhabited_mk (elt_of u)
|
||||
|
||||
theorem exists_imp_inhabited {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
|
||||
|
|
@ -35,13 +39,13 @@ nonempty_imp_inhabited (obtain w Hw, from H, nonempty_intro w)
|
|||
-- ----------------------------
|
||||
|
||||
definition epsilon {A : Type} {H : nonempty A} (P : A → Prop) : A :=
|
||||
let u : {x : A | (∃y, P y) → P x} :=
|
||||
let u : {x : A, (∃y, P y) → P x} :=
|
||||
strong_indefinite_description P H in
|
||||
elt_of u
|
||||
|
||||
theorem epsilon_spec_aux {A : Type} (H : nonempty A) (P : A → Prop) (Hex : ∃y, P y) :
|
||||
P (@epsilon A H P) :=
|
||||
let u : {x : A | (∃y, P y) → P x} :=
|
||||
let u : {x : A, (∃y, P y) → P x} :=
|
||||
strong_indefinite_description P H in
|
||||
has_property u Hex
|
||||
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ inductive true : Prop :=
|
|||
trivial : true
|
||||
|
||||
abbreviation not (a : Prop) := a → false
|
||||
prefix `¬`:40 := not
|
||||
prefix `¬` := not
|
||||
|
||||
|
||||
-- not
|
||||
|
|
@ -65,8 +65,8 @@ assume Hnb Ha, Hnb (Hab Ha)
|
|||
inductive and (a b : Prop) : Prop :=
|
||||
and_intro : a → b → and a b
|
||||
|
||||
infixr `/\`:35 := and
|
||||
infixr `∧`:35 := and
|
||||
infixr `/\` := and
|
||||
infixr `∧` := and
|
||||
|
||||
theorem and_elim {a b c : Prop} (H1 : a ∧ b) (H2 : a → b → c) : c :=
|
||||
and_rec H2 H1
|
||||
|
|
@ -103,8 +103,8 @@ inductive or (a b : Prop) : Prop :=
|
|||
or_intro_left : a → or a b,
|
||||
or_intro_right : b → or a b
|
||||
|
||||
infixr `\/`:30 := or
|
||||
infixr `∨`:30 := or
|
||||
infixr `\/` := or
|
||||
infixr `∨` := or
|
||||
|
||||
theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or_intro_left b Ha
|
||||
theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or_intro_right a Hb
|
||||
|
|
@ -131,12 +131,12 @@ or_elim H1
|
|||
(assume Ha : a, or_inl (H2 Ha))
|
||||
(assume Hb : b, or_inr (H3 Hb))
|
||||
|
||||
theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c :=
|
||||
theorem or_imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c :=
|
||||
or_elim H1
|
||||
(assume H2 : a, or_inl (H H2))
|
||||
(assume H2 : c, or_inr H2)
|
||||
|
||||
theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b :=
|
||||
theorem or_imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b :=
|
||||
or_elim H1
|
||||
(assume H2 : c, or_inl H2)
|
||||
(assume H2 : a, or_inr (H H2))
|
||||
|
|
@ -146,8 +146,8 @@ or_elim H1
|
|||
-- ---
|
||||
|
||||
definition iff (a b : Prop) := (a → b) ∧ (b → a)
|
||||
infix `<->`:25 := iff
|
||||
infix `↔`:25 := iff
|
||||
infix `<->` := iff
|
||||
infix `↔` := iff
|
||||
|
||||
theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_intro H1 H2
|
||||
|
||||
|
|
|
|||
|
|
@ -1,21 +1,23 @@
|
|||
----------------------------------------------------------------------------------------------------
|
||||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Leonardo de Moura, Jeremy Avigad
|
||||
----------------------------------------------------------------------------------------------------
|
||||
|
||||
-- logic.connectives.eq
|
||||
-- ====================
|
||||
|
||||
-- Equality.
|
||||
|
||||
import .basic
|
||||
|
||||
|
||||
-- eq
|
||||
-- --
|
||||
|
||||
inductive eq {A : Type} (a : A) : A → Prop :=
|
||||
refl : eq a a
|
||||
|
||||
infix `=`:50 := eq
|
||||
|
||||
-- TODO: try this out -- shorthand for "refl _"
|
||||
notation `rfl`:max := refl _
|
||||
infix `=` := eq
|
||||
notation `rfl` := refl _
|
||||
|
||||
theorem eq_id_refl {A : Type} {a : A} (H1 : a = a) : H1 = (refl a) := rfl
|
||||
|
||||
|
|
@ -48,16 +50,17 @@ theorem eq_rec_on_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) :
|
|||
theorem eq_rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : eq_rec b H = b :=
|
||||
eq_rec_on_id H b
|
||||
|
||||
theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c) (u : P a) :
|
||||
theorem eq_rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H1 : a = b) (H2 : b = c)
|
||||
(u : P a) :
|
||||
eq_rec_on H2 (eq_rec_on H1 u) = eq_rec_on (trans H1 H2) u :=
|
||||
(show ∀(H2 : b = c), eq_rec_on H2 (eq_rec_on H1 u) = eq_rec_on (trans H1 H2) u,
|
||||
from eq_rec_on H2 (take (H2 : b = b), eq_rec_on_id H2 _))
|
||||
H2
|
||||
|
||||
namespace eq_ops
|
||||
postfix `⁻¹`:100 := symm
|
||||
infixr `⬝`:75 := trans
|
||||
infixr `▸`:75 := subst
|
||||
postfix `⁻¹` := symm
|
||||
infixr `⬝` := trans
|
||||
infixr `▸` := subst
|
||||
end eq_ops
|
||||
using eq_ops
|
||||
|
||||
|
|
@ -67,7 +70,8 @@ H ▸ refl (f a)
|
|||
theorem congr_arg {A : Type} {B : Type} {a b : A} (f : A → B) (H : a = b) : f a = f b :=
|
||||
H ▸ refl (f a)
|
||||
|
||||
theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) : f a = g b :=
|
||||
theorem congr {A : Type} {B : Type} {f g : A → B} {a b : A} (H1 : f = g) (H2 : a = b) :
|
||||
f a = g b :=
|
||||
H1 ▸ H2 ▸ refl (f a)
|
||||
|
||||
theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
|
||||
|
|
@ -79,26 +83,23 @@ congr_arg not H
|
|||
theorem eqmp {a b : Prop} (H1 : a = b) (H2 : a) : b :=
|
||||
H1 ▸ H2
|
||||
|
||||
infixl `<|`:100 := eqmp
|
||||
infixl `◂`:100 := eqmp
|
||||
|
||||
theorem eqmpr {a b : Prop} (H1 : a = b) (H2 : b) : a :=
|
||||
H1⁻¹ ◂ H2
|
||||
H1⁻¹ ▸ H2
|
||||
|
||||
theorem eqt_elim {a : Prop} (H : a = true) : a :=
|
||||
H⁻¹ ◂ trivial
|
||||
H⁻¹ ▸ trivial
|
||||
|
||||
theorem eqf_elim {a : Prop} (H : a = false) : ¬a :=
|
||||
assume Ha : a, H ◂ Ha
|
||||
assume Ha : a, H ▸ Ha
|
||||
|
||||
theorem imp_trans {a b c : Prop} (H1 : a → b) (H2 : b → c) : a → c :=
|
||||
assume Ha, H2 (H1 Ha)
|
||||
|
||||
theorem imp_eq_trans {a b c : Prop} (H1 : a → b) (H2 : b = c) : a → c :=
|
||||
assume Ha, H2 ◂ (H1 Ha)
|
||||
assume Ha, H2 ▸ (H1 Ha)
|
||||
|
||||
theorem eq_imp_trans {a b c : Prop} (H1 : a = b) (H2 : b → c) : a → c :=
|
||||
assume Ha, H2 (H1 ◂ Ha)
|
||||
assume Ha, H2 (H1 ▸ Ha)
|
||||
|
||||
theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
|
||||
iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
|
||||
|
|
@ -108,7 +109,7 @@ iff_intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
|
|||
-- --
|
||||
|
||||
definition ne [inline] {A : Type} (a b : A) := ¬(a = b)
|
||||
infix `≠`:50 := ne
|
||||
infix `≠` := ne
|
||||
|
||||
theorem ne_intro {A : Type} {a b : A} (H : a = b → false) : a ≠ b := H
|
||||
|
||||
|
|
|
|||
43
library/standard/logic/connectives/identities.lean
Normal file
43
library/standard/logic/connectives/identities.lean
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
-- Released under Apache 2.0 license as described in the file LICENSE.
|
||||
-- Authors: Jeremy Avigad
|
||||
|
||||
-- logic.connectives.identities
|
||||
-- ============================
|
||||
|
||||
-- Useful logical identities. In the absence of propositional extensionality, some of the
|
||||
-- calculations use the type class support provided by logic.connectives.instances
|
||||
|
||||
import logic.connectives.instances
|
||||
|
||||
using relation
|
||||
|
||||
-- TODO: delete when calc bug is fixed
|
||||
calc_subst subst_iff
|
||||
|
||||
theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
|
||||
calc
|
||||
(a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
|
||||
... ↔ a ∨ (c ∨ b) : {or_comm b c}
|
||||
... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
|
||||
|
||||
theorem or_left_comm (a b c : Prop) : a ∨ (b ∨ c)↔ b ∨ (a ∨ c) :=
|
||||
calc
|
||||
a ∨ (b ∨ c) ↔ (a ∨ b) ∨ c : iff_symm (or_assoc _ _ _)
|
||||
... ↔ (b ∨ a) ∨ c : {or_comm a b}
|
||||
... ↔ b ∨ (a ∨ c) : or_assoc _ _ _
|
||||
|
||||
theorem and_right_comm (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b :=
|
||||
calc
|
||||
(a ∧ b) ∧ c ↔ a ∧ (b ∧ c) : and_assoc _ _ _
|
||||
... ↔ a ∧ (c ∧ b) : {and_comm b c}
|
||||
... ↔ (a ∧ c) ∧ b : iff_symm (and_assoc _ _ _)
|
||||
|
||||
theorem and_left_comm (a b c : Prop) : a ∧ (b ∧ c)↔ b ∧ (a ∧ c) :=
|
||||
calc
|
||||
a ∧ (b ∧ c) ↔ (a ∧ b) ∧ c : iff_symm (and_assoc _ _ _)
|
||||
... ↔ (b ∧ a) ∧ c : {and_comm a b}
|
||||
... ↔ b ∧ (a ∧ c) : and_assoc _ _ _
|
||||
|
||||
-- TODO: delete when calc bug is fixed
|
||||
calc_subst subst
|
||||
|
|
@ -3,4 +3,5 @@ tools
|
|||
|
||||
Various additional tools.
|
||||
|
||||
* [tactic](tactic.lean) : reflected syntax for tactics
|
||||
* [tactic](tactic.lean) : reflected syntax for tactics
|
||||
* [helper_tactics](helper_tactics.lean) : useful tactics
|
||||
|
|
@ -65,23 +65,23 @@ theorem not_zero_add_right [instance] (x y : nat) (H : not_zero y) : not_zero (x
|
|||
theorem not_zero_succ [instance] (x : nat) : not_zero (succ x)
|
||||
:= not_zero_intro (not_is_zero_succ x)
|
||||
|
||||
variable div : Π (x y : nat) {H : not_zero y}, nat
|
||||
variable dvd : Π (x y : nat) {H : not_zero y}, nat
|
||||
|
||||
variables a b : nat
|
||||
|
||||
set_option pp.implicit true
|
||||
opaque_hint (hiding [module])
|
||||
check div a (succ b)
|
||||
check (λ H : not_zero b, div a b)
|
||||
check dvd a (succ b)
|
||||
check (λ H : not_zero b, dvd a b)
|
||||
check (succ zero)
|
||||
check a + (succ zero)
|
||||
check div a (a + (succ b))
|
||||
check dvd a (a + (succ b))
|
||||
|
||||
opaque_hint (exposing [module])
|
||||
check div a (a + (succ b))
|
||||
check dvd a (a + (succ b))
|
||||
|
||||
opaque_hint (hiding add)
|
||||
check div a (a + (succ b))
|
||||
check dvd a (a + (succ b))
|
||||
|
||||
opaque_hint (exposing add)
|
||||
check div a (a + (succ b))
|
||||
check dvd a (a + (succ b))
|
||||
|
|
|
|||
|
|
@ -592,7 +592,7 @@ theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤
|
|||
:= resolve_left (le_imp_succ_le_or_eq H1) H2
|
||||
|
||||
theorem le_succ_imp_le_or_eq {n m : ℕ} (H : n ≤ succ m) : n ≤ m ∨ n = succ m
|
||||
:= imp_or_left (le_imp_succ_le_or_eq H)
|
||||
:= or_imp_or_left (le_imp_succ_le_or_eq H)
|
||||
(take H2 : succ n ≤ succ m, show n ≤ m, from succ_le_cancel H2)
|
||||
|
||||
theorem succ_le_imp_le_and_ne {n m : ℕ} (H : succ n ≤ m) : n ≤ m ∧ n ≠ m
|
||||
|
|
@ -912,7 +912,7 @@ theorem case_zero_pos {P : ℕ → Prop} (y : ℕ) (H0 : P 0) (H1 : ∀y, y > 0
|
|||
:= case y H0 (take y', H1 _ (succ_pos _))
|
||||
|
||||
theorem zero_or_pos (n : ℕ) : n = 0 ∨ n > 0
|
||||
:= imp_or_left (or_swap (le_imp_lt_or_eq (zero_le n))) (take H : 0 = n, symm H)
|
||||
:= 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
|
||||
:= subst (symm H) (succ_pos m)
|
||||
|
|
|
|||
Loading…
Reference in a new issue