Zulip Chat Archive

Stream: general

Topic: Generalized rewriting


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Reid Barton (Sep 28 2020 at 16:27):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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 quotients, and then I guess what Coq calls "generalized rewriting" just becomes ordinary rewriting.

view this post on Zulip Tomas Skrivan (Sep 28 2020 at 17:17):

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

view this post on Zulip Tomas Skrivan (Sep 28 2020 at 17:17):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 28 2020 at 17:45):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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'))

view this post on Zulip 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' : XY) : ( x : X, f[x]  f'[x])  f  f'
axiom ceq.mor {X Y : type} (f f' : XY) (x x' : X) : x  x'  f  f'  f[x]  f'[x']

--- Composition combinator

def compose {X Y Z} := Expr.sym ((XY)(YZ)(XZ)) "compose"

notation f  g := compose[g][f]

axiom compose.app {X Y Z : type} {g : XY} {f : YZ} {x : X} : (fg)[x]  f[g[x]]

--- What I want to prove the following

lemma example.compose {X : type} {f : XX} {x : X} : (fff)[x]  f[f[f[x]]] :=
begin
apply (ceq.trans _ (f[(ff)[x]]) _), apply compose.app, apply ceq.mor,
apply compose.app, repeat {refl}
end

--- The ideal proof should be  "repeat {rewrite compose.app}"

view this post on Zulip Kevin Buzzard (Sep 30 2020 at 20:12):

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

view this post on Zulip Bryan Gin-ge Chen (Sep 30 2020 at 20:49):

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

view this post on Zulip 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}.

view this post on Zulip Tomas Skrivan (Oct 01 2020 at 08:25):

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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 29 2020 at 16:38):

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

view this post on Zulip Logan Murphy (Oct 29 2020 at 16:38):

Great, thank you Mario!


Last updated: May 16 2021 at 22:14 UTC