## 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?

(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

(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