Commit 2023-01-31 12:38 59ce0e86

View on Github →

feat: port Data.Sign (#1744) This is now done, but had some difficulties.

  • A lot of theorems used to be proved by decide!, which is not yet implemented.
  • deriving FinType does not work yet, manually inserted that instance
  • Many proofs relied on casesm and casesm*, which appear to work differently than they did in lean3 (see also this zulip thread).
  • Lean 4 was unable to infer DecidableEq for SignType, manually inserted that instance as well.

Estimated changes

added theorem Int.sign_eq_sign
added theorem Left.sign_neg
added theorem Right.sign_neg
added inductive SignType.Le
added def SignType.cast
added def SignType.castHom
added theorem SignType.coe_neg_one
added theorem SignType.coe_one
added theorem SignType.coe_zero
added theorem SignType.le_one
added theorem SignType.lt_one_iff
added theorem SignType.neg_iff
added theorem SignType.neg_one_le
added theorem SignType.nonneg_iff
added theorem SignType.nonpos_iff
added theorem SignType.not_one_lt
added theorem SignType.one_le_iff
added theorem SignType.pos_eq_one
added theorem SignType.pos_iff
added theorem SignType.range_eq
added def SignType.sign
added theorem SignType.univ_eq
added theorem SignType.zero_eq_zero
added inductive SignType
added theorem exists_signed_sum'
added theorem exists_signed_sum
added def signHom
added theorem sign_apply
added theorem sign_eq_neg_one_iff
added theorem sign_eq_one_iff
added theorem sign_eq_zero_iff
added theorem sign_mul
added theorem sign_ne_zero
added theorem sign_neg
added theorem sign_nonneg_iff
added theorem sign_nonpos_iff
added theorem sign_one
added theorem sign_pos
added theorem sign_pow
added theorem sign_sum
added theorem sign_zero