rewriting equivalences

Stream: new members

[Mario Carneiro]

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

[Mario Carneiro]

instead, you construct functions out of the quotient using quotient.lift, which has essentially the type (A -> B) -> (quotient A -> B)

[Mario Carneiro]

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

[Logan Murphy]

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]

(deleted)

[Logan Murphy]

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]

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

[Mario Carneiro]

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

?

[Mario Carneiro]

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

[Mario Carneiro]

I suspect the answer is simply to unfold equiv and have simp lemmas or rewriting on words applied to diferent formulas

[Mario Carneiro]

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]

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]

(deleted)

[Mario Carneiro]

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]

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

[Logan Murphy]

Thanks for the help