Stream: Elpi users & devs

Topic: Use case of induction over rose trees


view this post on Zulip St├ęphane Desarzens (Jul 13 2021 at 16:25):

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.

view this post on Zulip St├ęphane Desarzens (Jul 13 2021 at 16:30):

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: Feb 05 2023 at 15:03 UTC