# Zulip Chat Archive

## Stream: new members

### Topic: rewriting equivalences

#### Mario Carneiro (Oct 29 2020 at 18:09):

you can't coerce (or construct a function) from a quotient to its base type, in general

#### Mario Carneiro (Oct 29 2020 at 18:09):

instead, you construct functions out of the quotient using `quotient.lift`

, which has essentially the type `(A -> B) -> (quotient A -> B)`

#### Mario Carneiro (Oct 29 2020 at 18:10):

but it has a side condition that the provided function must respect the quotient relation

#### Logan Murphy (Oct 29 2020 at 18:23):

OK, maybe I should XY what I'm actually trying to do, with a slightly less minimal mwe :

```
namespace LTL
inductive formula (AP : Type)
| T : formula
| atom (a : AP) : formula
| conj (Φ₁ Φ₂ : formula) : formula
| neg (Φ : formula) : formula
| next (Φ : formula) : formula
| until (Φ₁ Φ₂ : formula) : formula
open formula
notation `¬` P := LTL.formula.neg P
notation P `∧` Q := LTL.formula.conj P Q
notation `O` Φ := formula.next Φ
notation Φ `𝒰` Ψ := formula.until Φ Ψ
def inf_word (AP : Type) : Type :=
stream (set AP)
def sat {AP : Type} : inf_word AP → formula AP → Prop
:= sorry
notation σ `⊨` Φ := sat σ Φ
def words {AP : Type} (Φ : formula AP) : set (inf_word AP) :=
{σ | σ ⊨ Φ}
def equiv {AP : Type} (Φ Ψ : formula AP) : Prop :=
words Φ = words Ψ
notation Φ ≡ Ψ := equiv Ψ Φ
lemma next_dual {AP : Type} (Φ : formula AP) :
(¬(O Φ)) ≡ O (¬ Φ) := sorry
end LTL
```

I would like to use either `apply`

or `rewrite`

to use the last lemma to prove something like

```
inductive foo
| f
open foo
def bar : formula foo := (formulae.atom f) ∧ (atom f)
example : ¬ (O bar) ≡ O (¬ bar) :=
begin
-- apply next_dual bar,
-- rw next_dual bar,
end
```

I guess my question would be, what's the idiomatic or canonical Lean way to do this?

#### Logan Murphy (Oct 29 2020 at 19:40):

(deleted)

#### Logan Murphy (Oct 29 2020 at 20:21):

I mean shouldn't I be able to prove things like

```
inductive foo
| f
open foo
def bar : formula foo := formula.atom f
example : (¬(O bar)) ≡ O (¬ bar) := sorry
```

without needing the quotient type

#### Logan Murphy (Oct 29 2020 at 20:22):

I mean i could just keep unfolding the definitions i suppose but shouldn't there be a way to leverage `next_dual`

?

#### Mario Carneiro (Oct 29 2020 at 20:23):

```
example : (¬(O bar)) ≡ O (¬ bar) := next_dual _
```

?

#### Mario Carneiro (Oct 29 2020 at 20:26):

I think you haven't shown any examples which actually need rewriting like this

#### Mario Carneiro (Oct 29 2020 at 20:26):

I suspect the answer is simply to unfold `equiv`

and have simp lemmas or rewriting on `words`

applied to diferent formulas

#### Mario Carneiro (Oct 29 2020 at 20:28):

But for instance nothing in your code snippet implies that `A ≡ B -> ¬ A ≡ ¬ B`

so of course rewriting isn't going to do anything nontrivial

#### Mario Carneiro (Oct 29 2020 at 20:28):

The point of the quotient type is so that you can lift the constructors, in the process proving that they all respect equivalence

#### Logan Murphy (Oct 29 2020 at 20:29):

(deleted)

#### Mario Carneiro (Oct 29 2020 at 20:29):

For quotients of the form `f x = f y`

, you often don't need the quotient, since you can just use `f`

in place of the `quotient.mk`

#### Logan Murphy (Oct 29 2020 at 20:32):

I think I found what was overcomplicating things (at least in my mind)

#### Logan Murphy (Oct 29 2020 at 20:32):

Thanks for the help

Last updated: May 10 2021 at 00:31 UTC