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: Dec 20 2023 at 11:08 UTC