rw for an equivalence relation

Stream: lean4

[Anirudh Suresh]

import Mathlib
import Lean.Elab.Tactic
open scoped Matrix
open Lean Elab Tactic

open Matrix

def com_equiv (c1 c2 :ℕ) : Prop :=
  ∀ n:ℕ, c1+n = c2+n

infix:80 " ≡ " => com_equiv

lemma seq_congr {c1 c1' c2} (h1 : c1 ≡ c1') (h2 : c2 ≡ c1') :
  (c1 ≡ c2) := by
  rw[h1]

In my above code, I want to use rw on an equivalence relation which is not the "=". How is this possible? I believe the presence of the +n in the definition is causing Lean to not directly rewrite it. Is there a way I can make it do so?

[Kyle Miller]

rw only can rewrite using Eq and Iff.

rw also doesn't unfold definitions when finding matches. In this case, you can do

lemma seq_congr {c1 c1' c2} (h1 : c1 ≡ c1') (h2 : c2 ≡ c1') :
    (c1 ≡ c2) := by
  rw [com_equiv] at *
  intro n
  rw [h1, h2]

[Anirudh Suresh]

This does make sense but I wanted some form of functionality which would replace the c1 by c1' in the goal (something that would change c1 ≡ c2 to c1' ≡ c2)

[Aaron Liu]

Then you would have to prove that it's an equivalence relation

[Aaron Liu]

If you set it up right you can make calc work for this.

[Anirudh Suresh]

import Mathlib
import Lean.Elab.Tactic
open scoped Matrix
open Lean Elab Tactic

open Matrix

def com_equiv (c1 c2 :ℕ) : Prop :=
  ∀ n:ℕ, c1+n = c2+n

infix:80 " ≡ " => com_equiv

--Reflexive
theorem com_equiv_refl (c : ℕ) : c ≡ c :=
  fun n => rfl

-- Symmetry
theorem com_equiv_symm {c1 c2 : ℕ} (h : c1 ≡ c2) : c2 ≡ c1 :=
  fun n => Eq.symm (h n)

-- Transitivity
theorem com_equiv_trans {c1 c2 c3 : ℕ} (h1 : c1 ≡ c2) (h2 : c2 ≡ c3) : c1 ≡ c3 :=
  fun n => Eq.trans (h1 n) (h2 n)

instance : Equivalence com_equiv where
  refl := com_equiv_refl
  symm := com_equiv_symm
  trans := com_equiv_trans

What should I do after I have proved equivalence relation?

[Aaron Liu]

theorem equivalence_com_equiv : Equivalence com_equiv where
  refl := com_equiv_refl
  symm := com_equiv_symm
  trans := com_equiv_trans

lemma seq_congr {c1 c1' c2} (h1 : c1 ≡ c1') (h2 : c2 ≡ c1') :
    (c1 ≡ c2) := by
  apply equivalence_com_equiv.trans h1
  -- goal is now c1' ≡ c2
  sorry

[Anirudh Suresh]

This works. Thank you!

[Anirudh Suresh]

Is it possible, however to make it similar to a rewrite where every instance of c1 gets replaced by c1' and c2 gets replaced by c2'?

[Aaron Liu]

Can you give an example goal, with the before and after of what you want to do?

[Anirudh Suresh]

import Mathlib
import Lean.Elab.Tactic
open scoped Matrix
open Lean Elab Tactic

open Matrix

def com_equiv (c1 c2 :ℕ) : Prop :=
  ∀ n:ℕ, c1+n = c2+n

infix:80 " ≡ " => com_equiv

--Reflexive
theorem com_equiv_refl (c : ℕ) : c ≡ c :=
  fun n => rfl

-- Symmetry
theorem com_equiv_symm {c1 c2 : ℕ} (h : c1 ≡ c2) : c2 ≡ c1 :=
  fun n => Eq.symm (h n)

-- Transitivity
theorem com_equiv_trans {c1 c2 c3 : ℕ} (h1 : c1 ≡ c2) (h2 : c2 ≡ c3) : c1 ≡ c3 :=
  fun n => Eq.trans (h1 n) (h2 n)

instance : Equivalence com_equiv where
  refl := com_equiv_refl
  symm := com_equiv_symm
  trans := com_equiv_trans

theorem equivalence_com_equiv : Equivalence com_equiv where
  refl := com_equiv_refl
  symm := com_equiv_symm
  trans := com_equiv_trans

lemma lm1 {c1 c1' c2:ℕ} (h1 : c1 ≡ c1') (h2 : c2 ≡ c1') :
  ((c1+c2+c1) ≡ (c2+c1+c1)) := by

an operation where I can replace all the c1 with c1' and c2 with c1'

[Aaron Liu]

You have to prove that addition respects the equivalence relation.

[Aaron Liu]

You might want to have a look at #new members > ✔ Generalized rewrite.

[Robin Arnez]

One way to handle this is to convert values into a quotient type and then define the usual operations. That however means that e.g. the usual proofs about Nat wouldn't apply and you would need to transfer the necessary lemmas and instances over. An alternative is writing a tactic, I actually did something like this in a lean without axioms experiment here. It would then be something like

def com_equiv (c1 c2 :ℕ) : Prop :=
  ∀ n:ℕ, c1+n = c2+n

infix:80 " ≡ " => com_equiv

--Reflexive
theorem com_equiv.refl (c : ℕ) : c ≡ c :=
  fun n => rfl

-- Symmetry
theorem com_equiv.symm {c1 c2 : ℕ} (h : c1 ≡ c2) : c2 ≡ c1 :=
  fun n => Eq.symm (h n)

-- Transitivity
theorem com_equiv.trans {c1 c2 c3 : ℕ} (h1 : c1 ≡ c2) (h2 : c2 ≡ c3) : c1 ≡ c3 :=
  fun n => Eq.trans (h1 n) (h2 n)

@[ccongr]
theorem com_equiv.congr {x₁ x₂ y₁ y₂ : ℕ} (h₁ : x₁ ≡ x₂) (h₂ : y₁ ≡ y₂) : x₁ ≡ y₁ ↔ x₂ ≡ y₂ := by
  constructor
  · intro h
    exact h₁.symm.trans (h.trans h₂)
  · intro h
    exact h₁.trans (h.trans h₂.symm)

@[ccongr]
theorem com_equiv.add_congr {a b c d : ℕ} (h : a ≡ c) (h' : b ≡ d) : a + b ≡ c + d := ...

lemma lm1 {c1 c1' c2:ℕ} (h1 : c1 ≡ c1') (h2 : c2 ≡ c1') :
    ((c1+c2+c1) ≡ (c2+c1+c1)) := by
  cnsimp [h1, <- h2]