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