Commit 2021-08-12 12:17 b5285cb7

View on Github →

split out Lean 3 prelude items from Logic/Basic.lean to Init/Logic.lean (#34)

Estimated changes

added theorem And.assoc
added theorem And.comm
added def And.elim
added theorem And.imp
added theorem And.symm
added theorem Decidable.not_not_iff
added theorem Eq.to_iff
added theorem ExistsUnique.elim
added theorem ExistsUnique.intro
added def ExistsUnique
added def Iff.elim
added def Iff.elim_left
added def Iff.elim_right
added theorem Ne.def
added theorem Not.intro
added theorem Or.assoc
added theorem Or.comm
added theorem Or.elim
added theorem Or.elim_on
added theorem Or.imp
added theorem Or.imp_left
added theorem Or.imp_right
added theorem Or.left_comm
added theorem Or.neg_resolve_left
added theorem Or.neg_resolve_right
added theorem Or.resolve_left
added theorem Or.resolve_right
added theorem Or.swap
added theorem Or.symm
added theorem and.swap
added theorem and_assoc
added theorem and_comm
added theorem and_congr
added theorem and_congr_right
added theorem and_iff_left
added theorem and_iff_right
added theorem and_implies
added theorem and_left_comm
added theorem and_not_self
added def as_false
added def as_true
added theorem bool.ff_ne_tt
added theorem cast_proof_irrel
added def congr_arg
added def congr_fun
added theorem decidable_eq_inl_refl
added theorem decidable_eq_inr_neg
added theorem dif_ctx_congr
added theorem dif_ctx_simp_congr
added theorem eq_comm
added def eq_rec_heq
added theorem eq_self_iff_true
added theorem exists_congr
added theorem exists_imp_exists
added theorem exists_unique_congr
added theorem false_iff_true
added theorem false_implies_iff
added theorem false_of_true_eq_false
added theorem forall_congr'
added theorem heq_of_eq_rec_left
added theorem heq_of_eq_rec_right
added theorem heq_self_iff_true
added theorem if_congr
added theorem if_congr_prop
added theorem if_ctx_congr
added theorem if_ctx_congr_prop
added theorem if_ctx_simp_congr_prop
added theorem if_false
added theorem if_simp_congr_prop
added theorem if_t_t
added theorem if_true
added theorem iff_congr
added theorem iff_false_intro
added theorem iff_not_self
added theorem iff_true_intro
added theorem imp_congr
added theorem imp_congr_ctx
added theorem imp_congr_left
added theorem imp_congr_right
added theorem implies_of_if_neg
added theorem implies_of_if_pos
added theorem implies_true_iff
added def is_dec_eq
added def is_dec_refl
added theorem let_body_eq
added theorem let_eq
added theorem let_value_eq
added theorem let_value_heq
added theorem ne_self_iff_false
added theorem neq_of_not_iff
added theorem non_contradictory_em
added theorem not_and_self
added theorem not_congr
added theorem not_false_iff
added theorem not_iff_false_intro
added theorem not_iff_not_of_iff
added theorem not_iff_self
added theorem not_not_intro
added theorem not_of_eq_false
added theorem not_of_iff_false
added theorem not_of_not_not_not
added theorem not_or
added theorem not_or_intro
added theorem not_true
added theorem of_as_true
added theorem of_heq_true
added theorem of_iff_true
added theorem opt_param_eq
added theorem or_assoc
added theorem or_comm
added theorem or_congr
added theorem or_iff_left_of_imp
added theorem or_iff_right_of_imp
added theorem plift.down_up
added theorem plift.up_down
added structure plift
added def proof_irrel
added theorem to_bool_false_eq_ff
added theorem to_bool_true_eq_tt
added theorem trans_rel_left
added theorem trans_rel_right
added theorem true_eq_false_of_false
added theorem true_iff_false
added theorem true_implies_iff
added theorem ulift.down_up
added theorem ulift.up_down
added structure ulift.{r,
added def xor
deleted def And.elim
deleted theorem And.imp
deleted theorem And.symm
deleted def Decidable.by_cases
added theorem Decidable.eq_or_ne
added theorem Decidable.ne_or_eq
added def Empty.elim
deleted theorem Eq.to_iff
added theorem Exists.choose_spec
modified theorem Exists.imp
deleted theorem ExistsUnique.intro
deleted theorem ExistsUnique.unique
deleted def ExistsUnique
deleted def Iff.elim
deleted def Iff.elim_left
deleted def Iff.elim_right
deleted theorem Ne.def
modified def Not.elim
added theorem Not.imp
deleted theorem Not.intro
deleted def Or.by_cases
deleted theorem Or.elim
deleted theorem Or.imp
deleted theorem Or.imp_left
deleted theorem Or.imp_right
deleted theorem Or.neg_resolve_left
deleted theorem Or.neg_resolve_right
deleted theorem Or.resolve_left
deleted theorem Or.resolve_right
deleted theorem Or.symm
deleted theorem and_assoc
deleted theorem and_comm
deleted theorem and_congr
deleted theorem and_congr_right
deleted theorem and_iff_left
deleted theorem and_iff_right
deleted theorem and_left_comm
deleted theorem and_not_self
added theorem by_contradiction
deleted theorem cast_proof_irrel
deleted def congr_arg
deleted def congr_fun
added theorem dec_em'
added theorem dec_em
added theorem em'
added theorem em
deleted theorem eq_comm
added theorem eq_iff_iff
added theorem eq_or_ne
deleted def eq_rec_heq
deleted theorem eq_self_iff_true
deleted theorem exists_congr
modified theorem exists_imp_distrib
added theorem exists_imp_exists'
deleted theorem exists_unique_congr
added theorem exists₂_congr
added theorem exists₃_congr
added theorem exists₄_congr
deleted theorem false_imp_iff
added theorem false_ne_true
deleted theorem forall_congr'
added theorem forall_imp
deleted theorem forall_not_of_not_exists
added theorem forall₂_congr
added theorem forall₃_congr
added theorem forall₄_congr
deleted theorem heq_of_eq_rec_left
deleted theorem heq_of_eq_rec_right
deleted theorem heq_self_iff_true
added def hidden
deleted theorem if_false
deleted theorem if_true
deleted theorem iff_comm
deleted theorem iff_congr
added theorem iff_def'
added theorem iff_def
deleted theorem iff_false_intro
added theorem iff_iff_eq
deleted theorem iff_not_self
deleted theorem iff_true_intro
added theorem imp_and_distrib
deleted theorem imp_congr
deleted theorem imp_congr_ctx
deleted theorem imp_congr_left
deleted theorem imp_congr_right
added theorem imp_false
added theorem imp_iff_right
added theorem imp_intro
added theorem imp_self
modified theorem imp_true_iff
added theorem ne_or_eq
deleted theorem ne_self_iff_false
deleted theorem neq_of_not_iff
modified theorem not.decidable_imp_symm
deleted theorem not_and_self
deleted theorem not_congr
modified theorem not_exists
deleted theorem not_false_iff
deleted theorem not_iff_false_intro
deleted theorem not_iff_not_of_iff
deleted theorem not_iff_self
deleted theorem not_not_intro
added theorem not_not_of_not_imp
deleted theorem not_of_eq_false
deleted theorem not_of_iff_false
added theorem not_of_not_imp
deleted theorem not_or
deleted theorem not_or_intro
deleted theorem not_true
deleted theorem of_heq_true
deleted theorem of_iff_true
added theorem or.elim3
added theorem or.right_comm
deleted theorem or_assoc
deleted theorem or_comm
deleted theorem or_congr
added theorem or_congr_left
added theorem or_congr_right
added theorem or_not
added theorem or_of_or_of_imp_left
added theorem or_of_or_of_imp_of_imp
added theorem or_of_or_of_imp_right
deleted theorem plift.down_up
deleted theorem plift.up_down
deleted structure plift
deleted def proof_irrel
added theorem proof_irrel_heq
deleted theorem ulift.down_up
deleted theorem ulift.up_down
deleted structure ulift.{r,