# Zulip Chat Archive

## Stream: general

### Topic: Generalized rewriting

#### Tomas Skrivan (Sep 28 2020 at 16:13):

How can I get `rewrite`

tactic working with a setoid? In Coq, I usually define an instance of `Setoid`

and also add new morphisms with `Add Parametric Morphism`

. What am I supposed to do in Lean? I have defined an instance of `Setoid`

, but when I'm trying to use rewrite tactic I get an error: `rewrite tactic failed, lemma is not an equality nor a iff state`

.

#### Reid Barton (Sep 28 2020 at 16:23):

I'm not sure what feature you're looking for, but I don't think it exists.

#### Reid Barton (Sep 28 2020 at 16:27):

I suspect the Lean equivalent is just to work with the quotient type.

#### Jannis Limperg (Sep 28 2020 at 16:29):

Like Reid says, Lean does not support generalised rewriting a la Coq. Using a quotient instead of a setoid would probably be the idiomatic solution. If you don't want to do that, you'll have to reason with your equivalence relation directly, Agda-style.

#### Tomas Skrivan (Sep 28 2020 at 16:49):

That is unfortunate, that generalized rewriting is not supported. However, I do not know how quotients work, they might be a better way of doing what I'm doing.

#### Reid Barton (Sep 28 2020 at 17:13):

https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients

Basically, we never use `setoid`

other than to form `quotient`

s, and then I guess what Coq calls "generalized rewriting" just becomes ordinary rewriting.

#### Tomas Skrivan (Sep 28 2020 at 17:17):

And instead of proving theorems like `a ≈ b`

I would rather prove `⟦a⟧ = ⟦b⟧`

.

#### Tomas Skrivan (Sep 28 2020 at 17:17):

I have done some quick testing and it seems to work as I would expect.

#### Simon Hudon (Sep 28 2020 at 17:31):

Speaking only for myself, I prefer using quotients to using generalized rewriting. With quotients, when you define `f`

in terms of a quotient type and if you look at the internal representation, you have to prove that it preserves the equivalence relation. Then, you can define `g`

in terms of `f`

and you don't have anything to prove unless you use the internals of the quotient. With generalized rewriting, you have to prove that both `f`

and `g`

are valid morphisms. The proof for `g`

is easy but it still means that you need one proof per function that you use. I find quotients to be more modular.

#### Tomas Skrivan (Sep 28 2020 at 17:43):

I got into a problem when I know that a function is a valid morphism but is not defined in terms of the quotient. I know that `⟦f y⟧ = ⟦z⟧`

, `⟦g x⟧ = ⟦y⟧ `

and that `f`

is a valid morphism. How can I easily prove that `⟦f (g x)⟧ = ⟦z⟧`

?

Complete example:

```
constant X : Type
constant f : X → X
constant g : X → X
constant x : X
constant y : X
constant z : X
instance : setoid X := sorry
lemma fy : ⟦f y⟧ = ⟦z⟧ := sorry
lemma gx : ⟦g x⟧ = ⟦y⟧ := sorry
lemma fmor (x y : X) : ⟦x⟧ = ⟦y⟧ → ⟦f x⟧ = ⟦f y⟧ := sorry
lemma fgx : ⟦f (g x)⟧ = ⟦z⟧ :=
begin
rewrite gx, -- how to get this working?
rewrite fy,
refl
end
```

#### Reid Barton (Sep 28 2020 at 17:45):

Don't use `f`

directly, but rather `quotient.map f`

#### Reid Barton (Sep 28 2020 at 17:48):

e.g.

```
import data.quot
constant X : Type
constant f : X → X
constant g : X → X
constant x : X
constant y : X
constant z : X
instance : setoid X := sorry
lemma fmor' (x y : X) : x ≈ y → f x ≈ f y := sorry
noncomputable def f' := quotient.map f fmor'
lemma fy : f' ⟦y⟧ = ⟦z⟧ := sorry
lemma gx : ⟦g x⟧ = ⟦y⟧ := sorry
lemma fgx : f' ⟦g x⟧ = ⟦z⟧ :=
begin
rewrite gx,
rewrite fy
end
```

#### Tomas Skrivan (Sep 28 2020 at 17:48):

I'm afraid that in my application this is not possible or very cumbersome, but I will think about it more.

#### Reid Barton (Sep 28 2020 at 17:51):

Generally we would work entirely with `f'`

and wouldn't bother making `f`

and `fmor'`

into top-level definitions, unless they were rather complicated.

#### Tomas Skrivan (Sep 28 2020 at 17:56):

The problem is that I care about `f`

. I really care about the actual representative, but usually prove theorems only about its equivalence class.

#### Tomas Skrivan (Sep 28 2020 at 17:58):

I often work with functions like `(compose f (compose g h))`

. When I want to prove something I would have to convert it to `(compose f' (compose g' h'))`

#### Tomas Skrivan (Sep 30 2020 at 16:35):

I'm really struggling with this. As an example I want to prove that `(f∘f∘f)[x] ≈ f[f[f[x]]]`

by subsequently applying `compose.app {...} : (f∘g)[x] ≈ f[g[x]]`

. I would like the proof to be `repeat {rewrite compose.app}`

, but I do not know how to do this. Currently I have to manually invoke transitivity of `≈`

over `f[(f∘f)[x]])`

.

Complete example:

```
reserve infixr ` ⟶ ` : 50
reserve infixr ` × ` : 60
reserve infixr ` ∘ ` : 60
reserve infix ` ≅ ` : 26
--- Types
inductive type
| sym (name : string) : type
| op (name : string) : type → type → type
def type.fspace (X Y : type) : type := type.op "fspace" X Y
infixr ⟶ := type.fspace
--- Expressions
inductive Expr : type → Type
| sym (T : type) (name : string) : Expr T
| app {X Y : type} : Expr (X ⟶ Y) → Expr X → Expr Y
notation f [ x ] := Expr.app f x
instance type.coercion_to_Type : has_coe_to_sort type := has_coe_to_sort.mk Type Expr
--- Equality: Postulate an existence of equality
constant ceq {X : type} : X → X → Prop
infix ≅ := ceq
@[refl] axiom ceq.refl {X : type} (x : X) : x ≅ x
@[symm] axiom ceq.symm {X : type} (x y : X) : x ≅ y → y ≅ x
@[trans] axiom ceq.trans {X : type} (x y z : X) : x ≅ y → y ≅ z → x ≅ z
def ceq.iseqv {X : type} : equivalence (@ceq X) := begin split, apply ceq.refl, split, apply ceq.symm, apply ceq.trans end
instance type.setoid (X : type) : setoid X := setoid.mk ceq ceq.iseqv
--- Postulate function extensionality and all functions are proper
axiom ceq.ext {X Y : type} (f f' : X⟶Y) : (∀ x : X, f[x] ≈ f'[x]) → f ≈ f'
axiom ceq.mor {X Y : type} (f f' : X⟶Y) (x x' : X) : x ≈ x' → f ≈ f' → f[x] ≈ f'[x']
--- Composition combinator
def compose {X Y Z} := Expr.sym ((X⟶Y)⟶(Y⟶Z)⟶(X⟶Z)) "compose"
notation f ∘ g := compose[g][f]
axiom compose.app {X Y Z : type} {g : X⟶Y} {f : Y⟶Z} {x : X} : (f∘g)[x] ≈ f[g[x]]
--- What I want to prove the following
lemma example.compose {X : type} {f : X⟶X} {x : X} : (f∘f∘f)[x] ≈ f[f[f[x]]] :=
begin
apply (ceq.trans _ (f[(f∘f)[x]]) _), apply compose.app, apply ceq.mor,
apply compose.app, repeat {refl}
end
--- The ideal proof should be "repeat {rewrite compose.app}"
```

#### Kevin Buzzard (Sep 30 2020 at 20:12):

`rw`

only rewrites along equalities, not along general equivalence relations.

#### Bryan Gin-ge Chen (Sep 30 2020 at 20:49):

There is tactic#equiv_rw (specifically for `equiv`

s), but I've never used it before.

#### Tomas Skrivan (Oct 01 2020 at 08:24):

Kevin Buzzard said:

`rw`

only rewrites along equalities, not along general equivalence relations.

I'm aware of this. My the problem is basically how can I state `(f∘f∘f)[x] ≈ f[f[f[x]]]`

and `(f∘g)[x] ≈ f[g[x]]`

with quotients and equalities such that the proof can be `repeat {rewrite compose.app}`

.

#### Tomas Skrivan (Oct 01 2020 at 08:25):

Bryan Gin-ge Chen said:

There is tactic#equiv_rw (specifically for

`equiv`

s), but I've never used it before.

Nice, I will try that once I manage to install mathlib successfully.

#### Logan Murphy (Oct 29 2020 at 16:30):

I hope it's okay to bring back this older thread, but I just want to make sure I understand: If I make an equivalence relation like

```
import data.set data.stream tactic
open set stream tactic
def inf_word (AP : Type) : Type :=
stream (set AP)
inductive formulae (AP : Type)
| T : formulae
| atom (a : AP) : formulae
| conj (Φ₁ Φ₂ : formulae) : formulae
| neg (Φ : formulae) : formulae
def words {AP : Type} (Φ : formula AP) : set (inf_word AP) :=
{σ | true} -- in reality, set of words which satisfy Φ
def my_equiv {AP : Type} (Φ Ψ: formula AP) : Prop :=
words Φ = words Ψ
```

and I want to be able to use `rw`

on goals/hypotheses of the form `my_equiv Φ Ψ`

, should I be registering `formula`

as a quotient?

Or more precisely defining a quotient type over formula I guess

#### Mario Carneiro (Oct 29 2020 at 16:38):

yes, you define a quotient of `formula`

and then use `rw`

on the resulting type

#### Logan Murphy (Oct 29 2020 at 16:38):

Great, thank you Mario!

Last updated: May 16 2021 at 22:14 UTC