From mininix Require Export utils nix.floats.
From stdpp Require Import options.

(** Our development does not rely on a particular order on attribute set names.
It can be any decidable total order. We pick something concrete (lexicographic
order on strings) to avoid having to parametrize the whole development. *)
Definition attr_le := String.le.
Global Instance attr_le_dec : RelDecision attr_le := _.
Global Instance attr_le_po : PartialOrder attr_le := _.
Global Instance attr_le_total : Total attr_le := _.
Global Typeclasses Opaque attr_le.

Inductive mode := SHALLOW | DEEP.
Inductive kind := ABS | WITH.
Inductive rec := REC | NONREC.

Global Instance rec_eq_dec : EqDecision rec.
Proof. solve_decision. Defined.

Inductive num :=
  | NInt (n : Z)
  | NFloat (f : float).

Inductive base_lit :=
  | LitNum (n : num)
  | LitBool (b : bool)
  | LitString (s : string)
  | LitNull.

Global Instance num_inhabited : Inhabited num := populate (NInt 0).
Global Instance base_lit_inhabited : Inhabited base_lit := populate LitNull.

Global Instance num_eq_dec : EqDecision num.
Proof. solve_decision. Defined.
Global Instance base_lit_eq_dec : EqDecision base_lit.
Proof. solve_decision. Defined.

Global Instance maybe_NInt : Maybe NInt := λ n,
  if n is NInt i then Some i else None.
Global Instance maybe_NFloat : Maybe NFloat := λ n,
  if n is NFloat f then Some f else None.
Global Instance maybe_LitNum : Maybe LitNum := λ bl,
  if bl is LitNum n then Some n else None.
Global Instance maybe_LitBool : Maybe LitBool := λ bl,
  if bl is LitBool b then Some b else None.
Global Instance maybe_LitString : Maybe LitString := λ bl,
  if bl is LitString s then Some s else None.

Inductive bin_op : Set :=
  | AddOp | SubOp | MulOp | DivOp | AndOp | OrOp | XOrOp (* Arithmetic *)
  | LtOp | EqOp (* Relations *)
  | RoundOp (m : round_mode) (* Conversions *)
  | MatchStringOp (* Strings *)
  | MatchListOp | AppendListOp (* Lists *)
  | SelectAttrOp | UpdateAttrOp | HasAttrOp
  | DeleteAttrOp | SingletonAttrOp | MatchAttrOp (* Attribute sets *)
  | FunctionArgsOp | TypeOfOp.

Global Instance bin_op_eq_dec : EqDecision bin_op.
Proof. solve_decision. Defined.

Global Instance maybe_RoundOp : Maybe RoundOp := λ op,
  if op is RoundOp m then Some m else None.

Section expr.
  Local Unset Elimination Schemes.
  Inductive expr :=
    | ELit (bl : base_lit)
    | EId (x : string) (mke : option (kind * expr))
    | EAbs (x : string) (e : expr)
    | EAbsMatch (ms : gmap string (option expr)) (strict : bool) (e : expr)
    | EApp (e1 e2 : expr)
    | ESeq (μ : mode) (e1 e2 : expr)
    | EList (es : list expr)
    | EAttr (αs : gmap string attr)
    | ELetAttr (k : kind) (e1 e2 : expr)
    | EBinOp (op : bin_op) (e1 e2 : expr)
    | EIf (e1 e2 e3 : expr)
  with attr :=
    | Attr (τ : rec) (e : expr).
End expr.

Definition EId' x := EId x None.
Notation AttrR := (Attr REC).
Notation AttrN := (Attr NONREC).
Notation ESelect e x := (EBinOp SelectAttrOp e (ELit (LitString x))).
Notation ELet x e := (ELetAttr ABS (EAttr {[ x := AttrN e ]})).
Notation EWith := (ELetAttr WITH).

Definition attr_expr (α : attr) : expr := match α with Attr _ e => e end.
Definition attr_rec (α : attr) : rec := match α with Attr μ _ => μ end.
Definition attr_map (f : expr → expr) (α : attr) : attr :=
  match α with Attr μ e => Attr μ (f e) end.

Definition from_attr {A} (f g : expr → A) (α : attr) : A :=
  match α with AttrR e => f e | AttrN e => g e end.

Definition merge_kinded {A} (new old : kind * A) : option (kind * A) :=
  match new.1, old.1 with
  | WITH, ABS => Some old
  | _, _ => Some new
  end.
Arguments merge_kinded {_} !_ !_ / : simpl nomatch.
Notation union_kinded := (union_with merge_kinded).

Definition no_recs : gmap string attr → Prop :=
  map_Forall (λ _ α, attr_rec α = NONREC).

Definition indirects (αs : gmap string attr) : gmap string (kind * expr) :=
  map_imap (λ x _, Some (ABS, ESelect (EAttr αs) x)) αs.

Fixpoint subst (ds : gmap string (kind * expr)) (e : expr) : expr :=
  match e with
  | ELit b => ELit b
  | EId x mkd => EId x $ union_kinded (ds !! x) mkd
  | EAbs x e => EAbs x (subst ds e)
  | EAbsMatch ms strict e =>
      EAbsMatch (fmap (M:=option) (subst ds) <$> ms) strict (subst ds e)
  | EApp e1 e2 => EApp (subst ds e1) (subst ds e2)
  | ESeq μ e1 e2 => ESeq μ (subst ds e1) (subst ds e2)
  | EList es => EList (subst ds <$> es)
  | EAttr αs => EAttr (attr_map (subst ds) <$> αs)
  | ELetAttr k e1 e2 => ELetAttr k (subst ds e1) (subst ds e2)
  | EBinOp op e1 e2 => EBinOp op (subst ds e1) (subst ds e2)
  | EIf e1 e2 e3 => EIf (subst ds e1) (subst ds e2) (subst ds e3)
  end.

Notation attr_subst ds := (attr_map (subst ds)).

Definition int_min : Z := -(1 ≪ 63).
Definition int_max : Z := 1 ≪ 63 - 1.

Definition int_ok (i : Z) : bool := bool_decide (int_min ≤ i ≤ int_max)%Z.
Definition num_ok (n : num) : bool :=
  match n with NInt i => int_ok i | _ => true end.
Definition base_lit_ok (bl : base_lit) : bool :=
  match bl with LitNum n => num_ok n | _ => true end.

Inductive final : mode → expr → Prop :=
  | ELitFinal μ bl : base_lit_ok bl → final μ (ELit bl)
  | EAbsFinal μ x e : final μ (EAbs x e)
  | EAbsMatchFinal μ ms strict e : final μ (EAbsMatch ms strict e)
  | EListShallowFinal es : final SHALLOW (EList es)
  | EListDeepFinal es : Forall (final DEEP) es → final DEEP (EList es)
  | EAttrShallowFinal αs : no_recs αs → final SHALLOW (EAttr αs)
  | EAttrDeepFinal αs :
     no_recs αs →
     map_Forall (λ _, final DEEP ∘ attr_expr) αs →
     final DEEP (EAttr αs).

Fixpoint sem_eq_list (es1 es2 : list expr) : expr :=
  match es1, es2 with
  | [], [] => ELit (LitBool true)
  | e1 :: es1, e2 :: es2 =>
      EIf (EBinOp EqOp e1 e2) (sem_eq_list es1 es2) (ELit (LitBool false))
  | _, _ => ELit (LitBool false)
  end.

Fixpoint sem_lt_list (es1 es2 : list expr) : expr :=
  match es1, es2 with
  | [], _ => ELit (LitBool true)
  | e1 :: es1, e2 :: es2 =>
      EIf (EBinOp LtOp e1 e2) (ELit (LitBool true)) $
        EIf (EBinOp EqOp e1 e2) (sem_lt_list es1 es2) (ELit (LitBool false))
  | _ :: _, [] => ELit (LitBool false)
  end.

Definition sem_and_attr (es : gmap string expr) : expr :=
  map_fold_sorted attr_le
    (λ _ e1 e2, EIf e1 e2 (ELit (LitBool false)))
    (ELit (LitBool true)) es.

Definition sem_eq_attr (αs1 αs2 : gmap string attr) : expr :=
  sem_and_attr $ merge (λ mα1 mα2,
    α1 ← mα1; α2 ← mα2; Some (EBinOp EqOp (attr_expr α1) (attr_expr α2))) αs1 αs2.

Definition num_to_float (n : num) : float :=
  match n with
  | NInt i => Float.of_Z i
  | NFloat f => f
  end.

Definition sem_bin_op_lift
    (fint : Z → Z → Z) (ffloat : float → float → float)
    (n1 n2 : num) : option num :=
  match n1, n2 with
  | NInt i1, NInt i2 =>
     let i := fint i1 i2 in
     guard (int_ok i);;
     Some (NInt i)
  | _, _ => Some $ NFloat $ ffloat (num_to_float n1) (num_to_float n2)
  end.

Definition sem_bin_rel_lift
    (fint : Z → Z → bool) (ffloat : float → float → bool)
    (n1 n2 : num) : bool :=
  match n1, n2 with
  | NInt i1, NInt i2 => fint i1 i2
  | _, _ => ffloat (num_to_float n1) (num_to_float n2)
  end.

Definition sem_eq_base_lit (bl1 bl2 : base_lit) : bool :=
  match bl1, bl2 with
  | LitNum n1, LitNum n2 => sem_bin_rel_lift Z.eqb Float.eqb n1 n2
  | LitBool b1, LitBool b2 => bool_decide (b1 = b2)
  | LitString s1, LitString s2 => bool_decide (s1 = s2)
  | LitNull, LitNull => true
  | _, _ => false
  end.

(** Precondition e1 and e2 are final *)
Definition sem_eq (e1 e2 : expr) : option expr :=
  match e1, e2 with
  | ELit bl1, ELit bl2 => Some $ ELit (LitBool (sem_eq_base_lit bl1 bl2))
  | EAbs _ _, EAbs _ _ => None
  | EList es1, EList es2 => Some $
      if decide (length es1 = length es2) then sem_eq_list es1 es2
      else ELit $ LitBool false
  | EAttr αs1, EAttr αs2 => Some $
      if decide (dom αs1 = dom αs2) then sem_eq_attr αs1 αs2
      else ELit $ LitBool false
  | _, _ => Some $ ELit (LitBool false)
  end.

Definition div_allowed (n : num) : bool :=
  match n with
  | NInt n => bool_decide (n ≠ 0%Z)
  | NFloat f => negb (Float.eqb f (Float.of_Z 0)) (* TODO: Check NaNs *)
  end.

Definition sem_bin_op_num (op : bin_op) (n1 : num) : option (num → option base_lit) :=
  match op with
  | AddOp => Some $ λ n2,
      LitNum <$> sem_bin_op_lift Z.add Float.add n1 n2
  | SubOp => Some $ λ n2,
      LitNum <$> sem_bin_op_lift Z.sub Float.sub n1 n2
  | MulOp => Some $ λ n2,
      LitNum <$> sem_bin_op_lift Z.mul Float.mul n1 n2
  | DivOp => Some $ λ n2,
      (* Quot can overflow: [MIN_INT `quot` -1] equals [MAX_INT + 1] *)
      guard (div_allowed n2);;
      LitNum <$> sem_bin_op_lift Z.quot Float.div n1 n2
  | AndOp =>
      i1 ← maybe NInt n1;
      Some $ λ n2, i2 ← maybe NInt n2;
        Some $ LitNum $ NInt $ Z.land i1 i2
  | OrOp =>
      i1 ← maybe NInt n1;
      Some $ λ n2, i2 ← maybe NInt n2;
        Some $ LitNum $ NInt $ Z.lor i1 i2
  | XOrOp =>
      i1 ← maybe NInt n1;
      Some $ λ n2, i2 ← maybe NInt n2;
        Some $ LitNum $ NInt $ Z.lxor i1 i2
  | LtOp => Some $ λ n2,
      Some $ LitBool (sem_bin_rel_lift Z.ltb Float.ltb n1 n2)
  | _ => None
  end%Z.

Definition sem_bin_op_string (op : bin_op) : option (string → string → base_lit) :=
  match op with
  | AddOp => Some $ λ s1 s2, LitString (s1 +:+ s2)
  | LtOp => Some $ λ s1 s2, LitBool (bool_decide (strict attr_le s1 s2))
  | _ => None
  end.

Definition type_of_num (n : num) : string :=
  match n with
  | NInt _ => "int"
  | NFloat _ => "float"
  end.

Definition type_of_base_lit (bl : base_lit) : string :=
  match bl with
  | LitNum n => type_of_num n
  | LitBool _ => "bool"
  | LitString _ => "string"
  | LitNull => "null"
  end.

Definition type_of_expr (e : expr) :=
  match e with
  | ELit bl => Some (type_of_base_lit bl)
  | EAbs _ _ | EAbsMatch _ _ _ => Some "lambda"
  | EList _ => Some "list"
  | EAttr _ => Some "set"
  | _ => None
  end.

(* Used for [RoundOp] *)
Definition float_to_bounded_Z (f : float) : Z :=
  match Float.to_Z f with
  | Some x => if decide (int_ok x) then x else int_min
  | None => int_min
  end.

Inductive sem_bin_op : bin_op → expr → (expr → expr → Prop) → Prop :=
  | EqSem e1 :
     sem_bin_op EqOp e1 (λ e2 e, sem_eq e1 e2 = Some e)
  | LitNumSem op n1 f :
     sem_bin_op_num op n1 = Some f →
     sem_bin_op op (ELit (LitNum n1)) (λ e2 e, ∃ n2 bl,
       e2 = ELit (LitNum n2) ∧ f n2 = Some bl ∧ e = ELit bl)
  | RoundSem m n1 :
     sem_bin_op (RoundOp m) (ELit (LitNum n1)) (λ e2 e,
       e2 = ELit LitNull ∧
       e = ELit $ LitNum $ NInt $ float_to_bounded_Z $ Float.round m $ num_to_float n1)
  | LitStringSem op s1 f :
     sem_bin_op_string op = Some f →
     sem_bin_op op (ELit (LitString s1)) (λ e2 e, ∃ s2,
       e2 = ELit (LitString s2) ∧ e = ELit (f s1 s2))
  | MatchStringSem s :
     sem_bin_op MatchStringOp (ELit (LitString s)) (λ e2 e,
       e2 = ELit LitNull ∧
       match s with
       | EmptyString => e = EAttr {[
           "empty" := AttrN (ELit (LitBool true));
           "head" := AttrN (ELit LitNull);
           "tail" := AttrN (ELit LitNull) ]}
       | String a s => e = EAttr {[
           "empty" := AttrN (ELit (LitBool false));
           "head" := AttrN (ELit (LitString (String a EmptyString)));
           "tail" := AttrN (ELit (LitString s)) ]}
       end)
  | LtListSem es :
     sem_bin_op LtOp (EList es) (λ e2 e, ∃ es',
       e2 = EList es' ∧
       e = sem_lt_list es es')
  | MatchListSem es :
     sem_bin_op MatchListOp (EList es) (λ e2 e,
       e2 = ELit LitNull ∧
       match es with
       | [] => e = EAttr {[
           "empty" := AttrN (ELit (LitBool true));
           "head" := AttrN (ELit LitNull);
           "tail" := AttrN (ELit LitNull) ]}
       | e' :: es => e = EAttr {[
           "empty" := AttrN (ELit (LitBool false));
           "head" := AttrN e';
           "tail" := AttrN (EList es) ]}
       end)
  | AppendListSem es :
     sem_bin_op AppendListOp (EList es) (λ e2 e, ∃ es',
       e2 = EList es' ∧
       e = EList (es ++ es'))
  | SelectAttrSem αs :
     no_recs αs →
     sem_bin_op SelectAttrOp (EAttr αs) (λ e2 e, ∃ x,
       e2 = ELit (LitString x) ∧ αs !! x = Some (AttrN e))
  | UpdateAttrSem αs1 :
     no_recs αs1 →
     sem_bin_op UpdateAttrOp (EAttr αs1) (λ e2 e, ∃ αs2,
       e2 = EAttr αs2 ∧ no_recs αs2 ∧ e = EAttr (αs2 ∪ αs1))
  | HasAttrSem αs :
     no_recs αs →
     sem_bin_op HasAttrOp (EAttr αs) (λ e2 e, ∃ x,
       e2 = ELit (LitString x) ∧ e = ELit (LitBool (bool_decide (is_Some (αs !! x)))))
  | DeleteAttrSem αs :
     no_recs αs →
     sem_bin_op DeleteAttrOp (EAttr αs) (λ e2 e, ∃ x,
       e2 = ELit (LitString x) ∧ e = EAttr (delete x αs))
  | SingletonAttrSem x :
     sem_bin_op SingletonAttrOp (ELit (LitString x)) (λ e2 e,
       e2 = ELit LitNull ∧
       e = EAbs "t" (EAttr {[ x := AttrN (EId' "t") ]}))
  | MatchAttrSem αs :
     no_recs αs →
     sem_bin_op MatchAttrOp (EAttr αs) (λ e2 e,
       e2 = ELit LitNull ∧
       ((αs = ∅ ∧
         e = EAttr {[
           "empty" := AttrN (ELit (LitBool true));
           "key" := AttrN (ELit LitNull);
           "head" := AttrN (ELit LitNull);
           "tail" := AttrN (ELit LitNull) ]}) ∨
       (∃ x e',
         αs !! x = Some (AttrN e') ∧
         (∀ y, is_Some (αs !! y) → attr_le x y) ∧
         e = EAttr {[
           "empty" := AttrN (ELit (LitBool false));
           "key" := AttrN (ELit (LitString x));
           "head" := AttrN e';
           "tail" := AttrN (EAttr (delete x αs)) ]})))
  | FunctionArgsAbsSem x e' :
     sem_bin_op FunctionArgsOp (EAbs x e') (λ e2 e,
       e2 = ELit LitNull ∧
       e = EAttr ∅)
  | FunctionArgsAbsMatchSem ms strict e' :
     sem_bin_op FunctionArgsOp (EAbsMatch ms strict e') (λ e2 e,
       e2 = ELit LitNull ∧
       e = EAttr (AttrN ∘ ELit ∘ LitBool ∘ from_option (λ _, true) false <$> ms))
  | TypeOfSem e1 :
     sem_bin_op TypeOfOp e1 (λ e2 e, ∃ x,
       e2 = ELit LitNull ∧
       type_of_expr e1 = Some x ∧
       e = ELit (LitString x)).

Inductive matches :
     gmap string expr → gmap string (option expr) → bool → gmap string attr → Prop :=
  | MatchEmpty strict :
     matches ∅ ∅ strict ∅
  | MatchAny es :
     matches es ∅ false ∅
  | MatchAvail x e es ms md strict βs :
     es !! x = None →
     ms !! x = None →
     matches es ms strict βs →
     matches (<[x:=e]> es) (<[x:=md]> ms) strict (<[x:=AttrN e]> βs)
  | MatchOptDefault x es ms d strict βs :
     es !! x = None →
     ms !! x = None →
     matches es ms strict βs →
     matches es (<[x:=Some d]> ms) strict (<[x:=AttrR d]> βs).

Reserved Notation "e1 -{ μ }-> e2"
  (right associativity, at level 55, μ at level 1, format "e1  -{ μ }->  e2").

Inductive ctx1 : mode → mode → (expr → expr) → Prop :=
  | CList es1 es2 :
     Forall (final DEEP) es1 →
     ctx1 DEEP DEEP (λ e, EList (es1 ++ e :: es2))
  | CAttr αs x :
     no_recs αs →
     αs !! x = None →
     (∀ y α, αs !! y = Some α → final DEEP (attr_expr α) ∨ attr_le x y) →
     ctx1 DEEP DEEP (λ e, EAttr (<[x:=AttrN e]> αs))
  | CAppL μ e2 :
     ctx1 SHALLOW μ (λ e1, EApp e1 e2)
  | CAppR μ ms strict e1 :
     ctx1 SHALLOW μ (EApp (EAbsMatch ms strict e1))
  | CSeq μ μ' e2 :
     ctx1 μ' μ (λ e1, ESeq μ' e1 e2)
  | CLetAttr μ k e2 :
     ctx1 SHALLOW μ (λ e1, ELetAttr k e1 e2)
  | CBinOpL μ op e2 :
     ctx1 SHALLOW μ (λ e1, EBinOp op e1 e2)
  | CBinOpR μ op e1 Φ :
     final SHALLOW e1 →
     sem_bin_op op e1 Φ →
     ctx1 SHALLOW μ (EBinOp op e1)
  | CIf μ e2 e3 :
     ctx1 SHALLOW μ (λ e1, EIf e1 e2 e3).

Inductive step : mode → relation expr :=
  | Sβ μ x e1 e2 :
     EApp (EAbs x e1) e2 -{μ}-> subst {[x:=(ABS, e2)]} e1
  | SβMatch μ ms strict e1 αs βs :
     no_recs αs →
     matches (attr_expr <$> αs) ms strict βs →
     EApp (EAbsMatch ms strict e1) (EAttr αs) -{μ}->
       subst (indirects βs) e1
  | SFunctor μ αs e1 e2 :
     no_recs αs →
     αs !! "__functor" = Some (AttrN e1) →
     EApp (EAttr αs) e2 -{μ}-> EApp (EApp e1 (EAttr αs)) e2
  | SSeqFinal μ μ' e1 e2 :
     final μ' e1 → ESeq μ' e1 e2 -{μ}-> e2
  | SLetAttrAttr μ k αs e :
     no_recs αs →
     ELetAttr k (EAttr αs) e -{μ}-> subst ((k,.) ∘ attr_expr <$> αs) e
  | SAttr_rec μ αs :
     ¬no_recs αs →
     EAttr αs -{μ}->
       EAttr (AttrN ∘ from_attr (subst (indirects αs)) id <$> αs)
  | SBinOp μ op e1 Φ e2 e :
     final SHALLOW e1 →
     final SHALLOW e2 →
     sem_bin_op op e1 Φ → Φ e2 e →
     EBinOp op e1 e2 -{μ}-> e
  | SIfBool μ b e2 e3 :
     EIf (ELit (LitBool b)) e2 e3 -{μ}-> if b then e2 else e3
  | SId μ x k e :
     EId x (Some (k,e)) -{μ}-> e
  | SCtx K μ μ' e e' :
     ctx1 μ μ' K → e -{μ}-> e' → K e -{μ'}-> K e'
where "e1 -{ μ }-> e2" := (step μ e1 e2).

Notation "e1 -{ μ }->* e2" := (rtc (step μ) e1 e2)
  (right associativity, at level 55, μ at level 1, format "e1  -{ μ }->*  e2").
Notation "e1 -{ μ }->+ e2" := (tc (step μ) e1 e2)
  (right associativity, at level 55, μ at level 1, format "e1  -{ μ }->+  e2").

Definition stuck (μ : mode) (e : expr) : Prop :=
  nf (step μ) e ∧ ¬final μ e.

(** Induction *)
Fixpoint expr_size (e : expr) : nat :=
  match e with
  | ELit _ => 1
  | EId _ mkd => S (from_option (expr_size ∘ snd) 1 mkd)
  | EAbs _ d => S (expr_size d)
  | EAbsMatch ms _ e =>
     S (map_sum_with (from_option expr_size 1) ms + expr_size e)
  | EApp e1 e2 | ESeq _ e1 e2 => S (expr_size e1 + expr_size e2)
  | EList es => S (sum_list_with expr_size es)
  | EAttr eτs => S (map_sum_with (expr_size ∘ attr_expr) eτs)
  | ELetAttr _ e1 e2 => S (expr_size e1 + expr_size e2)
  | EBinOp _ e1 e2 => S (expr_size e1 + expr_size e2)
  | EIf e1 e2 e3 => S (expr_size e1 + expr_size e2 + expr_size e3)
  end.

Lemma expr_ind (P : expr → Prop) :
  (∀ b, P (ELit b)) →
  (∀ x mkd, from_option (P ∘ snd) True mkd → P (EId x mkd)) →
  (∀ x e, P e → P (EAbs x e)) →
  (∀ ms strict e,
    map_Forall (λ _, from_option P True) ms → P e → P (EAbsMatch ms strict e)) →
  (∀ e1 e2, P e1 → P e2 → P (EApp e1 e2)) →
  (∀ μ e1 e2, P e1 → P e2 → P (ESeq μ e1 e2)) →
  (∀ es, Forall P es → P (EList es)) →
  (∀ αs, map_Forall (λ _, P ∘ attr_expr) αs → P (EAttr αs)) →
  (∀ k e1 e2, P e1 → P e2 → P (ELetAttr k e1 e2)) →
  (∀ op e1 e2, P e1 → P e2 → P (EBinOp op e1 e2)) →
  (∀ e1 e2 e3, P e1 → P e2 → P e3 → P (EIf e1 e2 e3)) →
  ∀ e, P e.
Proof.
  intros Hlit Hid Habs Hmatch Happ Hseq Hlist Hattr Hlet Hop Hif e.
  induction (Nat.lt_wf_0_projected expr_size e) as [e _ IH].
  destruct e; repeat destruct select (option _); simpl in *; eauto with lia.
  - apply Hmatch; [|by eauto with lia]=> y [e'|] Hx //=. apply IH, Nat.lt_succ_r.
    etrans; [|apply Nat.le_add_r].
    eapply (map_sum_with_lookup_le (from_option expr_size 1) _ _ _ Hx).
  - apply Hlist, Forall_forall=> e ?. apply IH, Nat.lt_succ_r.
    by apply sum_list_with_in.
  - apply Hattr, map_Forall_lookup=> y e ?. apply IH, Nat.lt_succ_r.
    by eapply (map_sum_with_lookup_le (expr_size ∘ attr_expr)).
Qed.