Dependent type or not?

[liyishuai]

As mentioned in #1, dependent types makes Coq reasoning painful. I started with the following definition for FramePayload: https://github.com/liyishuai/coq-http2/blob/acb5a37abab0fed5935fbec97fd56f8b1f24599a/src/Types.v#L103 Maybe we should remove the FrameType parameter for simplicity?

[lastland]

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...

[Lysxia]

The current way looks fine to me as well.

[favonia]

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).

[liyishuai]

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

[lastland]

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).

[liyishuai]

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?

[lastland]

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

[liyishuai]

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

[liyishuai]

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

[lastland]

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.

[favonia]

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