1 files changed, 527 insertions, 0 deletions

diff --git a/theories/nix/operational.v b/theories/nix/operational.v
new file mode 100644
index 0000000..d3f0777
--- /dev/null
+++ b/theories/nix/operational.v
@@ -0,0 +1,527 @@
+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.