Dependent type or not? about coq-http2 HOT 11 OPEN

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 Frame: should frameType be a parameter or a field? I have seen both styles and which one is better depends on the use cases...

from coq-http2.

The current way looks fine to me as well.

from coq-http2.

As a side note, I might prefer to index them by a more "inductive-defined" FrameTypeId rather than the current FrameType. (By the way, I think X and XId should be swapped in terms of English.)

Also maybe PingFrame should be of Vector.t bool 64 -> FramePayload 6? (Or Vector.t bool 64 -> FramePayload PingType if we were using the hypothetical FrameTypeId).

from coq-http2.

Could someone prove forall (v : Vector.t A 0), v = []? This lemma is pushing me against using dependent types...

from coq-http2.

I don't know if there's a simpler way to do this, but you can use dependent destruction to prove it:

Require Import Coq.Program.Equality.
Theorem foo: forall A (v : Vector.t A 0), v = Vector.nil A.
Proof.
  intros. dependent destruction v. reflexivity.
Qed.

Note that the tactic makes use of John Major equality (JMeq_eq : forall (A : Type) (x y : A), x ~= y -> x = y).

from coq-http2.

If we use more type-level constraints and change the definition of SettingKey into:

Inductive SettingKey   :=
  SettingHeaderTableSize        (* 0x1 *)
| SettingEnablePush             (* 0x2 *)
| SettingMaxConcurrentStreams   (* 0x3 *)
| SettingInitialWindowSize      (* 0x4 *)
| SettingMaxFrameSize           (* 0x5 *)
| SettingMaxHeaderBlockSize     (* 0x6 *)
| SettingUnknown (s : SettingKeyId) : (s = 0 \/ s >= 7 /\ s <= 255) -> SettingKey.

then how does fromSettingKeyId look like?

from coq-http2.

You can declare SettingKeyId as {n:N | n>=0 /\ n<=255}.

from coq-http2.

I have tried such declaration but could not implement the function.

from coq-http2.

Standard library does have theorems for reasoning on vector's constructor:

Theorem zero_nil {A} (v : Vector.t A 0) : [] = v.
Proof. apply case0. reflexivity. Qed.

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 XId!)

from coq-http2.

I have tried such declaration but could not implement the function.

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.

from coq-http2.

A direct proof without micromega involves trichotomy and then case analysis on the derivation of n < 7.

from coq-http2.