Rocoma.Recipes

Recipes: syntax, substitutions, neutralization, weight and depth



AST


Inductive term : Type :=
  | TVar (x : var)
  | TNat (n : nat)
  | TCons (S T : term)
  | FTop
  | FBot
  | FImp (f g : term)
  | FEqu (S T : term)
  | FAll (f : {bind term in term})
  | FNot (f : term)
  | FAnd (f g : term).

Inductive type : Type :=
  | Void
  | Arr (U : type) (V : type)
  | TArr (V : type).

Inductive recipe : Type :=
  | Var (h : var)
  | Zero
  | Top
  | And (s t : recipe)
  | App (s t : recipe)
  | TApp (s : recipe) (S : term)
  | Lam (s : {bind recipe in recipe}) (U : type)
  | Imp (s : recipe) (f: term)
  | TLam (s : {bind term in recipe})
  | TAll (s : {bind term in recipe})
  | Neu (s : recipe)
  | Box (s : recipe).

Decidability lemmas


Lemma var_eq_dec (v1 v2 : var) : {v1 = v2} + {v1 <> v2}.
Proof.
  by decide equality.
Qed.

Lemma term_eq_dec (t1 t2 : term) : {t1 = t2} + {t1 <> t2}.
Proof.
  decide equality.
  exact: var_eq_dec.
  by decide equality.
Qed.

Lemma type_eq_dec (t1 t2 : type) : {t1 = t2} + {t1 <> t2}.
Proof.
  by decide equality.
Qed.

Lemma recipe_eq_dec (s t : recipe) : {s = t} + {s <> t}.
Proof.
  decide equality.
  exact: var_eq_dec.
  exact: term_eq_dec.
  exact: type_eq_dec.
  exact: term_eq_dec.
Qed.

Type classes instanciations


Global Instance Ids_term : Ids term. derive. Defined.
Global Instance Rename_term : Rename term. derive. Defined.
Global Instance Subst_term : Subst term. derive. Defined.
Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

Global Instance HSubst_term_recipe : HSubst term recipe. derive. Defined.
Global Instance Ids_recipe : Ids recipe. derive. Defined.
Global Instance Rename_recipe : Rename recipe. derive. Defined.
Global Instance Subst_recipe : Subst recipe. derive. Defined.

Global Instance HSubstLemmas_term_recipe : HSubstLemmas term recipe. derive. Qed.
Global Instance SubstHSubstComp_term_recipe : SubstHSubstComp term recipe. derive. Qed.
Global Instance SubstLemmas_recipe : SubstLemmas recipe. derive. Qed.

Global Instance IdsLemmas_R : IdsLemmas recipe.
Proof.
 constructor=> x y h.
 by injection h.
Qed.

Global Instance IdsLemmas_T : IdsLemmas term.
Proof.
 constructor=> x y h.
 by injection h.
Qed.

Key Definitions

TOPLAS p.9 The weight of a recipe is the size of its syntax tree, where all boxed subrecipes, term arguments, and implication antecedents count as 1.

Fixpoint weight (s : recipe) : nat :=
  match s with
  | Zero | Var _ | Top | Box _ => 1
  | App s t
  | And s t =>
      let wt := weight t in
      let ws := weight s in
      wt + ws + 1
  | TApp s _
  | Imp s _
  | TLam s
  | TAll s
  | Lam s _
  | Neu s => (weight s).+1
  end.

TOPLAS p.9 The depth of a recipe is the maximum degree of nesting of its boxed subrecipes (zero, if there are none).

Fixpoint depth (s : recipe) : nat :=
  match s with
  | Zero | Var _ | Top => 0
  | App s t
  | And s t =>
      max (depth s) (depth t)
  | TApp s _
  | Imp s _
  | TLam s
  | TAll s
  | Lam s _
  | Neu s => depth s
  | Box s => 1 + depth s
  end.

TOPLAS p.6 A type signature that has no continuation parameters is said to be of order zero; otherwise, its order is one plus the highest order of its outcomes.
Fixpoint order (U : type) :=
  match U with
  | Void => 0
  | TArr V => order V
  | Arr W V => max (order W).+1 (order V)
  end.

fall n s is TAll (TAll (… s)) repeated n times where the innermost TAll binds TVar 0 and the outermost TAll binds TVar n.-1.

Fixpoint fall n s :=
  match n with
  | 0 => s
  | S n => TAll (fall n s)
  end.

arg_of W U: W is the signature of a continuation parameter of U.
Inductive arg_of (W : type) : type -> Prop :=
| arg_here V : arg_of W (Arr W V)
| arg_arr U V : arg_of W V -> arg_of W (Arr U V)
| arg_tarr V : arg_of W V -> arg_of W (TArr V).

Lemma order_arg W U :
  arg_of W U ->
  order W < order U.
Proof.
  elim=> [V|U2 V _ ih|V _ ih] //.
  - change (order W < Nat.max (order W).+1 (order V)).
    apply/leP.
    by apply Nat.le_max_l.
  - change (order W < Nat.max (order U2).+1 (order V)).
    apply: (leq_trans ih).
    apply/leP.
    by apply Nat.le_max_r.
Qed.

fallF n f is FAll^n f.
Fixpoint fallF n f :=
  match n with
  | 0 => f
  | n.+1 => FAll (fallF n f)
  end.

Lemma depth_dec (r : recipe) :
  {depth r = 0} + {exists n, depth r = n.+1}.
Proof.
  elim: r=>//=; try by left.
  - move=> s [->//|hs] t [->|ht]; right; elim: hs=> n hn.
    + exists n. by lia.
    + elim: ht=> m hm.
      rewrite hn hm.
      by exists (Init.Nat.max n m).
  - move=> s [->//|hs] t [->|ht]; right; elim: hs=> n hn.
    + exists n. by lia.
    + elim: ht=> m hm.
      rewrite hn hm.
      by exists (Init.Nat.max n m).
  - right. by exists (depth s).
Qed.

Lemma weight_pos (r : recipe) :
  weight r > 0.
Proof.
  by elim: r=>//=; lia.
Qed.

Lemma depth_nonneg (r : recipe) :
  depth r >= 0.
Proof.
  by elim: r.
Qed.

Lemma weight_hsubst (s : recipe) (θ : var -> term) :
  weight s.|[θ] =
  weight s.
Proof.
  by elim: s θ=> */=; f_equal; eauto.
Qed.

Lemma depth_hsubst (s : recipe) (θ : var -> term) :
  depth s.|[θ] =
  depth s.
Proof.
  elim: s θ=>//=.
  - by move=> s hs t ht θ; rewrite hs ht.
  - by move=> s hs t ht θ; rewrite hs ht.
  - by move=> s hs >; rewrite hs.
Qed.

Lemma weight_hsubst_subst s σ θ :
  weight s.|[θ].[σ] =
  weight s.[σ].
Proof.
  by elim: s σ θ=> */=; f_equal; eauto.
Qed.

Corollary weight_subst_hsubst s σ θ :
  weight s.[σ >>| θ] =
  weight s.[σ].
Proof.
  have->: σ = upn 0 σ by [].
  generalize 0.
  elim: s σ θ; try by (move=>/=; eauto using weight_hsubst).
  - move=> s h1 U σ θ n. asimpl. f_equal.
    have->: s.[up (upn n σ >>| θ)] =
            s.[upn 0 (fun x : var => (up (upn n σ) x).[up ids]) >>| θ]
            by autosubst.
    rewrite h1.
    autosubst.
  - move=> > h1 *. asimpl. f_equal. by rewrite !h1.
  - move=> > h1 *. asimpl. f_equal. by rewrite !h1.
Qed.

Lemma weight_subst_box n s t :
  weight s = weight s.[upn n (Box t .: ids)].
Proof.
  elim: s n t; try (by move=> */=; eauto).
  - case=>//= [n t|x n t].
      by rewrite upnP; case (boolP (0<n)).
    rewrite upnP.
    case (boolP (x.+1<n))=>// ?.
    by case (x.+1 - n).
  - move=> s h U n t /=; f_equal. rewrite fold_up_upn. by apply h.
  - move=> s h n t /=; f_equal. by rewrite weight_subst_hsubst -h.
  - move=> s h n t /=; f_equal. by rewrite weight_subst_hsubst -h.
Qed.

The neutralization function replaces all Zero by Top in the recipe.

Fixpoint neu (s : recipe) : recipe :=
  match s with
  | Zero => Top
  | Top => Top
  | Var h => Var h
  | App s t => App (neu s) (neu t)
  | And s t => And (neu s) (neu t)
  | TApp s T => TApp (neu s) T
  | Imp s f => Imp (neu s) f
  | Lam s U => Lam (neu s) U
  | TLam s => TLam (neu s)
  | TAll s => TAll (neu s)
  | Neu s => Neu (neu s)
  | Box s => Box (neu s)
  end.

TOPLAS p.11 A recipe r is said to possess a certain property strongly, when both r and neu r have this property.

Definition strongly (P: recipe -> Prop) r :=
  P r /\ P (neu r).

Same, for a binary relation: R holds strongly on the pair (r,s) when it holds both on (r,s) and on their neutralizations.

Definition strongly2 (R: recipe -> recipe -> Prop) r s :=
  R r s /\ R (neu r) (neu s).

A recipe r possesses a property weakly, when neu r, but not necessarily r itself, has it

Definition weakly (P: recipe -> Prop) r :=
  P (neu r).

Basic lemmas related to these key definitions


Lemma neu_hsubst_comm s θ :
  neu s.|[θ] = (neu s).|[θ].
Proof.
  by elim: s θ=>//=;
    try (by move=> s hs t ht θ; f_equal; [apply hs|apply ht]);
    try (by move=> s hs >; f_equal; apply hs).
Qed.

Lemma neu_upren_comm u n k :
  (neu u).[upn k (ren (+n))] =
   neu u.[ upn k (ren (+n))].
Proof.
  elim: u n k=>//=;
    try by (intros; f_equal; eauto).
  - move=> [|x] n [|k]; rewrite upnP=>//=.
    by case (x.+1 < k.+1).
  - move=> s h U n k; f_equal; asimpl.
    by rewrite h.
  - move=> s h n k; f_equal; asimpl.
    by rewrite upn_ren_hsubst h.
  - move=> s h n k; f_equal; asimpl.
    by rewrite upn_ren_hsubst h.
Qed.

Lemma neu_ren_comm u n :
  (neu u).[ren (+n)] =
   neu u.[ ren (+n)].
Proof.
  by apply: neu_upren_comm u n 0.
Qed.

Lemma subst_neu s u n :
  neu s.[u//n] = (neu s).[neu u//n].
Proof.
  elim: s u n=>//; try by (move=> */=; by f_equal).
  - move=> x ? n /=. rewrite /subst_var. by case (lt_eq_lt_dec x n)=>// -[]h //.
  - move=> s h ? u n /=. f_equal.
    rewrite upn1 !subst_var_lemma.
    rewrite h.
    by rewrite neu_ren_comm.
  - move=> s h u n /=. f_equal.
    by rewrite !subst_var_hsubst h neu_hsubst_comm.
  - move=> s h u n /=. f_equal.
    by rewrite !subst_var_hsubst h neu_hsubst_comm.
Qed.

Corollary subst_neu0 s u :
  neu s.[u/] = (neu s).[neu u/].
Proof.
  by rewrite -!subst_var_0 (subst_neu _ _ 0).
Qed.

Lemma neu_idempotent s :
  neu (neu s) = neu s.
Proof.
  elim: s=>//=; by repeat move=>> ->.
Qed.

Lemma depth_neu s :
  depth s = depth (neu s).
Proof.
  elim: s=>//=; by repeat move=>> ->.
Qed.

Lemma weight_neu s :
  weight s >= weight (neu s).
Proof.
  by elim: s=>//= *; lia.
Qed.

Lemma inversion_neu_var t x :
  Var x = neu t ->
  t = Var x.
Proof.
  by elim: t.
Qed.

Lemma inversion_neu_top t :
  Top = neu t ->
  t = Top \/ t = Zero.
Proof.
  by elim: t =>//; first [by left|by right].
Qed.

Lemma inversion_neu_and s t r :
  And (neu s) (neu t) = neu r ->
  exists ss tt, And ss tt = r /\ neu ss = neu s /\ neu tt = neu t.
Proof.
  elim: r s t=>//.
  move=> s h1 t h2 u v e. injections.
  exists s, t.
  by repeat split.
Qed.

Lemma inversion_neu_app s t r :
  App (neu s) (neu t) = neu r ->
  exists ss tt, App ss tt = r /\ neu ss = neu s /\ neu tt = neu t.
Proof.
  elim: r s t=>//.
  move=> s h1 t h2 u v e. injections.
  exists s, t.
  by repeat split.
Qed.

Lemma inversion_neu_tapp s S r :
  TApp (neu s) S = neu r ->
  exists ss, TApp ss S = r /\ neu ss = neu s.
Proof.
  elim: r s=>//.
  move=> s h1 T t /= e. injections. subst.
  exists s.
  by repeat split.
Qed.

Lemma inversion_neu_lam s U r :
  Lam (neu s) U = neu r ->
  exists ss, Lam ss U = r /\ neu ss = neu s.
Proof.
  elim: r s=>//.
  move=> s h1 V t /= e. injections. subst.
  exists s.
  by repeat split.
Qed.

Lemma inversion_neu_imp s f r :
  Imp (neu s) f = neu r ->
  exists ss, Imp ss f = r /\ neu ss = neu s.
Proof.
  elim: r s=>//.
  move=> s h1 g t /= e. injections. subst.
  exists s.
  by repeat split.
Qed.

Lemma inversion_neu_tlam s r :
  TLam (neu s) = neu r ->
  exists ss, TLam ss = r /\ neu ss = neu s.
Proof.
  elim: r s=>//.
  move=> s h1 t /= e. injections. subst.
  exists s.
  by repeat split.
Qed.

Lemma inversion_neu_tall s r :
  TAll (neu s) = neu r ->
  exists ss, TAll ss = r /\ neu ss = neu s.
Proof.
  elim: r s=>//.
  move=> s h1 t /= e. injections. subst.
  exists s.
  by repeat split.
Qed.

Lemma inversion_neu_neu s r :
  Neu (neu s) = neu r ->
  exists ss, Neu ss = r /\ neu ss = neu s.
Proof.
  elim: r s=>//.
  move=> s h1 t /= e. injections. subst.
  exists s.
  by repeat split.
Qed.

Lemma inversion_neu_box s r :
  Box (neu s) = neu r ->
  exists ss, Box ss = r /\ neu ss = neu s.
Proof.
  elim: r s=>//.
  move=> s h1 t /= e. injections. subst.
  exists s.
  by repeat split.
Qed.

Lemma neu_fall m s :
  neu (fall m s) = fall m (neu s).
Proof.
  elim: m=>//= ? ih.
  by rewrite ih.
Qed.

Lemma fall_subst m s (σ : var -> recipe) :
  (fall m s).[σ] = fall m s.[σ >>| ren (+m)].
Proof.
  elim: m s σ=> [|m ih] ? σ /=.
  - by asimpl.
  - rewrite ih.
    have->//: (σ >>| ren (+1)) >>| ren (+m) = σ >>| ren (+m.+1).
    f_ext=> ?.
    by asimpl.
Qed.

Lemma fall_hsubst m s (θ : var -> term) :
  (fall m s).|[θ] = fall m s.|[upn m θ].
Proof.
  elim: m s θ=> [|? ih] ? θ /=.
  - by asimpl.
  - by rewrite ih iterate_Sr.
Qed.

Lemma fallF_subst n f (σ : var -> term) :
  (fallF n f).[σ] = fallF n f.[upn n σ].
Proof.
  elim: n σ=> //= ? ih σ.
  by rewrite ih fold_upn_up.
Qed.