Symm tactic implementation

Stream: mathlib4

[Siddhartha Gadgil]

I believe I have implemented the symm tactic, given a couple of examples. This was modelled on ext (with copious copy-paste too). I have made a pull request at https://github.com/leanprover-community/mathlib4/pull/253

Once more I have to bother you @Mario Carneiro to ask what I am missing and/or what I should do further.

[Siddhartha Gadgil]

Also @Gabriel Ebner - if you have the time I would be grateful for comments.

[Arthur Paulino]

@Siddhartha Gadgil it's reasonable to fearlessly run lake build on Mathlib4 at the moment because it's still small. You don't need to wait on CI runs to know if your branch builds at this stage

[Siddhartha Gadgil]

Now I have also implemented trans tactic with two variants in the same pull request. To illustrate, here is the test code.

@[trans] def nleqTrans (a b c : Nat) : a ≤ b → b ≤ c → a ≤ c := Nat.le_trans

@[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 h₁
    assumption

I assume the idea for reflexivity is to use refl as a more general tactic handling reflexivity of equality. I will go ahead with this assumption unless someone corrects me.

[Sebastian Ullrich]

Should trans make use of Lean 4's Trans class?

[Siddhartha Gadgil]

I did not know of this. I assume that it is a typeclass. Thanks.

[Siddhartha Gadgil]

I will look for it. Surely it should be used (presumably in addition to annotations)

[Siddhartha Gadgil]

What is the best way to search for instances within Meta?

[Siddhartha Gadgil]

I found it in the source code. I will try to use trySynthInstance as in Extra.lean

[Mario Carneiro]

the behavior of trans h₁ is incorrect. If you pass an argument to trans it should be the middle element and you get two subgoals, hence trans b here

[Siddhartha Gadgil]

I see. I thought it should be a proof of the first term. Thanks.

[Siddhartha Gadgil]

I will modify that.

[Siddhartha Gadgil]

And also use instances of the typeclass Trans if available.