To @Enrico Tassi, regarding derive
and coq-elpi#271.
I use Coq to play around with programming language theory. My example looks like this, reduced to the relevant fragment.
Require Import String.
Require Import List.
Import ListNotations.
Inductive type :=
| ty_bool | ty_unit
| ty_sum (tys : list type).
Inductive expr :=
| e_true | e_false | e_tt
| e_var (id : string)
| e_sum (e : expr) (idx : nat) (tys : list type)
| e_match (e : expr) (branches : list (string * expr))
| e_let (id : string) (val body : expr).
Definition type_binding : Set := string * type.
Definition frame_typing := list type_binding.
Definition frame_typing_lookup (ft : frame_typing) (id : string) : option type :=
option_map snd (find (fun p => String.eqb id (fst p)) ft).
Definition type_ctx := list (list type_binding).
Definition type_ctx_lookup (ctx : type_ctx) (id : string) : option type :=
match ctx with
| [] => None
| ft :: _ => frame_typing_lookup ft id
end.
(* Similar to "push" for a stack. *)
Definition type_ctx_insert (ctx : type_ctx) (id : string) (ty : type) : type_ctx :=
match ctx with
| [] => [[(id, ty)]]
| hd :: tl => ((id, ty) :: hd) :: tl
end.
Inductive typing : type_ctx -> expr -> type -> type_ctx -> Prop :=
| T_bool_true ctx :
typing ctx e_true ty_bool ctx
| T_bool_false ctx :
typing ctx e_false ty_bool ctx
| T_unit ctx :
typing ctx e_tt ty_unit ctx
| T_var ctx id ty :
type_ctx_lookup ctx id = Some ty ->
typing ctx (e_var id) ty ctx
| T_sum ctx0 ctx1 e idx tys ty :
typing ctx0 e ty ctx1 ->
nth_error tys idx = Some ty ->
typing ctx0 (e_sum e idx tys) (ty_sum tys) ctx1
| T_match ctx0 ctx1 ctx2_hd ctx2_tl val tys branches ty :
typing ctx0 val (ty_sum tys) ctx1 ->
Forall2 (fun br br_ty =>
typing (type_ctx_insert ctx1 (fst br) br_ty) (snd br) ty
(((fst br, br_ty) :: ctx2_hd) :: ctx2_tl)) branches tys ->
typing ctx0 (e_match val branches) ty (ctx2_hd :: ctx2_tl)
| T_let ctx0 ctx1 ctx2_hd ctx2_tl val val_ty id body body_ty :
typing ctx0 val val_ty ctx1 ->
typing (type_ctx_insert ctx1 id val_ty) body body_ty
(((id, val_ty) :: ctx2_hd) :: ctx2_tl) ->
typing ctx0 (e_let id val body) body_ty (ctx2_hd :: ctx2_tl).
Now, sometimes I want to do induction over typing
. For example for proving determinism or type soundness (for an appropriately defined semantics).
I could define deep induction-principles for type
and expr
by hand, although it gets tedious when adding new constructions. But for typing
it's too much manual labor, so I was looking for automation.
For example determinism:
Lemma typing_deterministic ctx0 e ty1 ty2 ctx1 ctx2 :
typing ctx0 e ty1 ctx1 ->
typing ctx0 e ty2 ctx2 ->
ty1 = ty2 /\ ctx1 = ctx2.
Proof.
intros Hty1 Hty2.
revert ty2 ctx2 Hty2.
induction Hty1.
all: intros ty2 ctx2 Hty2.
all: inversion Hty2; subst; clear Hty2.
all: try solve [intuition].
- (* T_var *)
split; [|reflexivity].
congruence.
- (* T_sum *)
rewrite H in H7. inversion H7; subst; clear H7.
apply IHHty1 in H6.
intuition.
- (* T_match *)
admit.
- (* T_let *)
apply IHHty1_1 in H5 as [].
subst.
apply IHHty1_2 in H6 as [].
split; congruence.
Admitted.
I left e_var
and e_let
in the language, to give a bit more context. In the semantics, e_match (e_sum val idx tys) branches
reduces to e_let id val body
where nth_error branches idx = Some (id, body)
. I'm closely following the constructions of the Oxide paper, although there the language lacks a sum-type.
Last updated: Oct 13 2024 at 01:02 UTC