Predicate support #656
Predicate support #656
Conversation
|
Alive Statistics: 76 / 93 (17 failed) |
|
Alive Statistics: 76 / 93 (17 failed) |
Co-authored-by: Alex Keizer <[email protected]>
|
Alive Statistics: 76 / 93 (17 failed) |
|
I suggest we merge this in, and develop more theory upstream. Thanks a bunch @AtticusKuhn for filling in the proof! I cleaned up the PR, closed another sorry, and made the project build. |
|
@tobiasgrosser Do we want to keep the old implementation compiled? We are currently adding new fields, so the problem is that the old implementation does not know about |
I think this is a great idea. |
I need more context to understand the issue. What is the problem with the old implementation? In fact, do we not just build on-top of the old implementation? |
|
@tobiasgrosser we have two implementations, Our automata / bitstream definitions all live in |
|
Alive Statistics: 76 / 93 (17 failed) |
|
@tobiasgrosser my suggestion is to delete |
Can you split them? E.g., just copy the definitions into Fast, and develop them independently for now? This allows us to maintain the previous code while not being held back by the old one. |
|
@tobiasgrosser that's exactly what I did in the current PR. |
|
Cool. Then lets merge. |
|
If they are decoupled, there is no need to delete them, no? It might still be useful to have them in a repo, as updating them to the latest lean won't have a cost. However, I don't feel super strong here. Happy to get see them dropped, too. |
|
Let's merge without dropping then, in case it turns out to be useful to reference the old impl. |
|
@tobiasgrosser hit merge if you're happy. |
| | i + 1 => by simp [compose_first i ((f a).1) f] | ||
|
|
||
| /-- | ||
| Coinduction principle for `corec`. |
There was a problem hiding this comment.
I would call this bisimulation, rather than coinduction
| /-- `repeatBit xs` will repeat the first bit of `xs` which is `true`. | ||
| That is, it will be all-zeros iff `xs` is all-zeroes, | ||
| otherwise, there's some number `k` so that after dropping the `k` least | ||
| significant bits, `repeatBit xs` is all-ones. -/ | ||
| def repeatBit (xs : BitStream) : BitStream := | ||
| corec (b := (false, xs)) fun (carry, xs) => |
There was a problem hiding this comment.
I thought we wanted to change this name? I like foldOr more than repeatBit
| def Predicate.denote : Predicate α → Prop | ||
| | eq t1 t2 => t1.eval = t2.eval | ||
| | and p q => p.denote ∧ q.denote | ||
| | or p q => p.denote ∨ q.denote |
There was a problem hiding this comment.
This is not quite right! We need to be taking in the arguments at the top-level, and pass those around.
Currently, we're denoting eq t u as equality of the functions that are denoted by t and u, meaning that we're universally quantifying each con-/disjunct separately.
def Predicate.denote (xs : α → BitStream) : Predicate α → Prop
| eq t1 t2 => t1.eval xs = t2.eval xs
| and p q => p.denote xs ∧ q.denote xs
| or p q => p.denote xs ∨ q.denote xs
| theorem Predicate.toFsm_correct {k : Nat} (p : Predicate k) : | ||
| decideIfZeros p.toFSM = true ↔ p.denote := by sorry |
There was a problem hiding this comment.
Similarly, this needs to be:
theorem Predicate.toFsm_correct {k : Nat} (p : Predicate k) :
decideIfZeros p.toFSM = true ↔ (\all xs, p.denote xs) := by sorry
No description provided.