Zulip Chat Archive

Stream: new members

Topic: rewriting equivalences


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

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

view this post on Zulip Mario Carneiro (Oct 29 2020 at 18:10):

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

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

view this post on Zulip Logan Murphy (Oct 29 2020 at 19:40):

(deleted)

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

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

view this post on Zulip Mario Carneiro (Oct 29 2020 at 20:23):

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

?

view this post on Zulip Mario Carneiro (Oct 29 2020 at 20:26):

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

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

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

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

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

(deleted)

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

view this post on Zulip Logan Murphy (Oct 29 2020 at 20:32):

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

view this post on Zulip Logan Murphy (Oct 29 2020 at 20:32):

Thanks for the help


Last updated: May 10 2021 at 00:31 UTC