Generalized rewriting

Stream: general

[Tomas Skrivan]

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]

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

[Reid Barton]

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

[Jannis Limperg]

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]

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]

https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#quotients
Basically, we never use setoid other than to form quotients, and then I guess what Coq calls "generalized rewriting" just becomes ordinary rewriting.

[Tomas Skrivan]

And instead of proving theorems like a ≈ b I would rather prove ⟦a⟧ = ⟦b⟧.

[Tomas Skrivan]

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

[Simon Hudon]

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]

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]

Don't use f directly, but rather quotient.map f

[Reid Barton]

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]

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

[Reid Barton]

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]

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]

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]

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]

rw only rewrites along equalities, not along general equivalence relations.

[Bryan Gin-ge Chen]

There is tactic#equiv_rw (specifically for equivs), but I've never used it before.

[Tomas Skrivan]

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]

Bryan Gin-ge Chen said:

There is tactic#equiv_rw (specifically for equivs), but I've never used it before.

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

[Logan Murphy]

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]

yes, you define a quotient of formula and then use rw on the resulting type

[Logan Murphy]

Great, thank you Mario!