-
-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Dependent type or not? #2
Comments
I am no expert in this but my guess is that this definition would be fine. There is no proof object in the data structure. You may, at some point, want to consider the definition of |
The current way looks fine to me as well. |
As a side note, I might prefer to index them by a more "inductive-defined" Also maybe |
Could someone prove |
I don't know if there's a simpler way to do this, but you can use
Note that the tactic makes use of John Major equality ( |
If we use more type-level constraints and change the definition of SettingKey into:
then how does fromSettingKeyId look like? |
You can declare |
I have tried such declaration but could not implement the function. |
Standard library does have theorems for reasoning on vector's constructor:
As mentioned in #3, I'm starting a new branch that represents every field as vectors, which might eliminate all dependent type other than vectors (no more |
I have just got some time to give it a shot, here's what I got: Definition SettingKeyId := {n:N | n >= 0 /\ n <= 255}.
Definition UnknownSettingKeyId := {n:N | n = 0 \/ n >= 7 /\ n <= 255}.
Inductive SettingKey :=
SettingHeaderTableSize (* 0x1 *)
| SettingEnablePush (* 0x2 *)
| SettingMaxConcurrentStreams (* 0x3 *)
| SettingInitialWindowSize (* 0x4 *)
| SettingMaxFrameSize (* 0x5 *)
| SettingMaxHeaderBlockSize (* 0x6 *)
| SettingUnknown : UnknownSettingKeyId -> SettingKey.
Require Import Coq.micromega.Psatz.
Program Definition fromSettingKeyId (id : SettingKeyId) : SettingKey :=
match id with
| 1 => SettingHeaderTableSize
| 2 => SettingEnablePush
| 3 => SettingMaxConcurrentStreams
| 4 => SettingInitialWindowSize
| 5 => SettingMaxFrameSize
| 6 => SettingMaxHeaderBlockSize
| _ => SettingUnknown id
end.
Next Obligation.
destruct id. simpl in *. lia.
Qed.
Solve Obligations with (simpl; intros; lia).
Coercion fromSettingKeyId : SettingKeyId >-> SettingKey. |
A direct proof without |
As mentioned in #1, dependent types makes Coq reasoning painful.
I started with the following definition for
FramePayload
:coq-http2/src/Types.v
Line 103 in acb5a37
Maybe we should remove the
FrameType
parameter for simplicity?The text was updated successfully, but these errors were encountered: