Zulip Chat Archive
Stream: mathlib4
Topic: Symm and Trans tactics implementation
Siddhartha Gadgil (Apr 06 2022 at 05:25):
Corrected the issue with the meaning of the argument, and also use the typeclass where available. I have stuck to the mathematical meaning of transitivity though, rather than the more general one in Trans
.
Below is the new test-code. Any further suggestions @Sebastian Ullrich @Mario Carneiro ?
def nleq : Nat → Nat → Prop
| a, b => a ≤ b
@[trans] def nleqTrans {a b c : Nat} : nleq a b → nleq b c → nleq a c := Nat.le_trans
example (a b c : Nat): nleq a b → nleq b c → nleq a c := by
intro h₁ h₂
trans b
assumption
assumption
example (a b c : Nat): nleq a b → nleq b c → nleq a c := by
intro h₁ h₂
trans
assumption
assumption
-- using `Trans` typeclass
@[trans] def eqTrans {α : Type}{a b c : α}: a = b → b = c → a = c := by
intro h₁ h₂
apply Eq.trans h₁ h₂
example (a b c : Nat): a = b → b = c → a = c := by
intro h₁ h₂
trans
assumption
assumption
example (a b c : Nat): a = b → b = c → a = c := by
intro h₁ h₂
trans b
assumption
assumption
example : Trans ((. ≤ . : Nat → Nat → Prop))
(. ≤ . : Nat → Nat → Prop) (. ≤ . : Nat → Nat → Prop) := inferInstance
example (a b c : Nat): a ≤ b → b ≤ c → a ≤ c := by
intro h₁ h₂
trans b
assumption
assumption
example (a b c : Nat): a ≤ b → b ≤ c → a ≤ c := by
intro h₁ h₂
trans
assumption
assumption
example (a b c : Nat): a < b → b < c → a < c := by
intro h₁ h₂
trans b
assumption
assumption
example (a b c : Nat): a < b → b < c → a < c := by
intro h₁ h₂
trans
assumption
assumption
Siddhartha Gadgil (Apr 06 2022 at 05:26):
For reference, the PR is at https://github.com/leanprover-community/mathlib4/pull/253
Last updated: Dec 20 2023 at 11:08 UTC