second attempt at finite csp instance type #96
Conversation
| record CSPInstance (nvar : ℕ) (dom : Vec (DecSetoid α ℓ) nvar) : Type α where | ||
| field | ||
| ncon : ℕ -- the number of constraints involved | ||
| constr : Vec (Constraint nvar dom) ncon |
There was a problem hiding this comment.
So I would actually go with a list of constraints, until knowing the number of constraints involved in advance actually makes a difference. My guess is, it won't matter.
There was a problem hiding this comment.
So, List is better than Vec here? Any particular reason why?
There was a problem hiding this comment.
Vec is useful when knowing the length 'statically' matters - otherwise might as well go with List.
There was a problem hiding this comment.
Ooops, I forgot to convert the vector of constraints to a list of constraints! I'll do that now.
| P : Constraint nvar dom → Bool | ||
| P c = (satisfies c) f | ||
|
|
||
| -- A more general version...? (P is a more general Pred) |
There was a problem hiding this comment.
I don't think this is right - P is a special case of Pred. In two ways, both what the input is, and what kind of type it returns. Also, I think this can be "said" with T.
There was a problem hiding this comment.
I suspect you're right and there's something wrong here. Again, it probably stems from my poor understanding of how to view general predicates. I'll have to think more about this.
There was a problem hiding this comment.
A predicate maps to a whole type's worth of evidence that the predicate holds (or none at all if it doesn't). true just says it holds and absolutely nothing else. Bool is slightly different though, because a Bool-valued function is equivalent to a proof-irrelevant decidable predicate.
There was a problem hiding this comment.
I see. Very nice explanation! Thank you, Jacques!!
|
The problem is that this
I.e. make a predicate from |
...but at least I now know a little bit more about `Prop`, `Bool`, and `Dec`. **Question**. Suppose ```agda ∀ i → Dec (f i ≈ g i) ``` and suppose we define ```agda f ≐ g = ∀ i → f i ≈ g i ``` Can we then prove `Dec (f ≐ g)`? (That's what we need in the hole on line 142, and that what I'm trying to do in lines 129--134. I have the `Bool` part, but I still need the `Reflects (f ≐ g)` part.)
|
Question. Suppose ∀ i → Dec (f i ≈ g i)and suppose we define f ≐ g = ∀ i → f i ≈ g iCan we then prove (That's what we need in the hole on line 142, and that what I'm trying to do in |
|
That's an extensionality property - you're asking for a pointwise proof to 'upgrade' to a uniform proof. |
|
Okay, point taken. On the other hand, if we can't even decide a finite
conjunction of decidable predicates, that seems like a defect of the theory
to me.
…On Sun, Aug 1, 2021 at 10:58 PM Jacques Carette ***@***.***> wrote:
That's an extensionality property - you're asking for a pointwise proof to
'upgrade' to a uniform proof.
—
You are receiving this because you authored the thread.
Reply to this email directly, view it on GitHub
<#96 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AA25MJEJRGQ4GD6ND2KVRDLT2WYNRANCNFSM5BBPT4KQ>
.
|
|
If you represent |
Not sure this is the best way to do this... so marking it "draft"