feat(Logic): logical operators#607
Conversation
fmontesi
changed the title
| · grind | ||
| · grind only [→ satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, = derivation_def, | ||
| = neg_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true] | ||
| constructor <;> grind |
There was a problem hiding this comment.
This should not be undone, grind? still fails here.
| public import Cslib.Foundations.Logic.Operators.Not | ||
| public import Cslib.Foundations.Logic.Operators.Box | ||
| public import Cslib.Foundations.Logic.Operators.Diamond | ||
| public import Cslib.Foundations.Logic.Operators.Iff |
There was a problem hiding this comment.
Would it be better to just have one file for these? If they're just notation typeclasses it seems unlikely to be heavyweight and they're likely to be used together.
There was a problem hiding this comment.
I don't know yet. We will expand these files with extended classes for expected properties about these operators, but you're right that some will require importing more than one.. I think we'll know more once we get there.
| instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond} | ||
|
|
||
| @[simp, scoped grind =] | ||
| lemma Proposition.not_def (φ : Proposition Atom) : (¬φ) = φ.neg := rfl |
There was a problem hiding this comment.
Are these simp/grind = lemmas all backwards? I thought they should simplify into the notation like List.append_eq, Nat.add_eq, etc. If this causes failures, I think it means some lemmas are not properly using the notation.
There was a problem hiding this comment.
this was my sense as well, but i couldn't make the grind see through the notation / typeclass correctly in the proofs of Satisfies.or_iff_or & relatives without explicitly rewriting back to φ.neg or whatever (undoubtedly due to my not understanding transparency / notation / grind / something properly)
There was a problem hiding this comment.
I spent some time with this. I think that if you add lemmas that make sure to use the notation for judgements, e.g. ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] = (⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂]) that this becomes a lot easier. As it is the grind annotation being on Satisfies means unfolding this is always required.
3 participants
This PR introduces typeclasses for logical operators (connectives and modalities) and refactors modal and propositional logics with appropriate instances to these.