带列表的命题的归纳原理（或：带嵌套列表的表达式的 LNR）

Question

免责声明：我担心这个 post 太长了，但是，我觉得在较小的设置中会丢失一些有价值的背景信息。

我目前正在尝试更改我的形式化以使用 Charguéraud 等人 [1] 的本地无名表示。显然，这种改编并不像我希望的那么简单，因为我对表达式的定义包含列表（至少我目前认为这是主要问题）。

所以，我有以下（最小）表达式定义。

Require Import Coq.Lists.List.
Require Import Coq.Arith.PeanoNat.

Parameter atom : Set.
Parameter eq_atom_dec : forall x y : atom, {x = y} + {x <> y}.

Definition VarIndex := nat.

Inductive Expr : Type :=
 | BVar : VarIndex -> VarIndex -> Expr
 | FVar : atom -> Expr
 | LetB : list Expr -> Expr -> Expr.

有了这个定义，我就可以定义开运算了。

Fixpoint open_rec (k: VarIndex) (u: list Expr) (e: Expr) :=
  match e with
  | BVar i j => if Nat.eq_dec k i then List.nth j u e else e
  | FVar x => e
  | LetB es e' => LetB (List.map (open_rec (S k) u) es) (open_rec (S k) u e')
  end.

Notation "{ k ~> u } t" := (open_rec k u t) (at level 67).

Definition open e u := open_rec 0 u e.

到目前为止一切顺利。接下来 "locally closed" 的属性归纳定义如下。

Inductive lc : Expr -> Prop :=
| lc_var : forall x,
    lc (FVar x)
| lc_let : forall (ts: list Expr) es e,
    Forall lc es ->
    lc (open e ts) ->
    lc (LetB es e).

教程现在指出我们可以证明关于 lc 和 open 相互作用的引理，即在局部封闭表达式中，当我们替换变量时没有任何反应。

(* this is a auxiliary lemma that works just fine for me *)
Lemma open_rec_lc_core : forall e (j: VarIndex) v (i: VarIndex) u,
    i <> j ->
    {j ~> v} e = {i ~> u} ({j ~> v} e) ->
    e = {i ~> u} e.
Proof.
Admitted.

Lemma open_rec_lc0 : forall k u e,
    lc e ->
    e = {k ~> u} e.
Proof.
  intros k u e LC.
  generalize dependent k.
  induction LC; intro k.
  - reflexivity.
  - simpl.
    f_equal.
    + admit.
    + eapply open_rec_lc_core with (j := 0).
      * auto.
      * eapply IHLC.         
Admitted.

如你所见，证明中有一个案例是"admitted"。这里的问题是我必须证明一些关于 let-bindings 的东西，但我手头的一切如下：

H : Forall lc (map (fun e' : Expr => open e' ts) es)
LC : lc (open e ts)
IHLC : forall k : VarIndex, open e ts = {k ~> u} open e ts

我需要的是 IHLC 的等效假设，但 es。我的第一个猜测是我需要修改归纳原则，因为它通常是针对以列表作为参数的归纳定义所做的 [2]。但是，我无法确定实际类型检查的定义。

Fail Definition lc_ind2 :=
  fun (P : Expr -> Prop) (f : forall x : atom, P (FVar x))
    (f0 : forall (ts es : list Expr) (e : Expr),
        Forall lc (map (fun e' : Expr => open e' ts) es) ->
        lc (open e ts) -> P (open e ts) ->
        Forall P (map (fun e' => open e' ts ) es) ->
        P (LetB es e)) =>
    fix F (e : Expr) (l : lc e) {struct l} : P e :=
    match l in (lc e0) return (P e0) with
    | lc_var x => f x
    | lc_let ts es e0 f1 l0 =>
      f0 ts es e0 f1 l0 (F (open e0 ts) l0)
         ((fix F' (es: list Expr) : Forall P es :=
                     match es with
                     | nil => Forall_nil P
                     | cons x xs => Forall_cons x (F x _) (F' xs)
                     end) (map (fun e' => open e' ts) es))
    end.

我需要 lc x 类型的东西而不是 Forall_cons 的应用程序中的 _，但我不知道如何得出这个值。

所以，最后我的问题是，如果有人知道我需要修改哪些定义才能使用 LNR。

[1] Tutorial on LNR
[2] Induction principles with list arguments

Answer 1

好的，所以最后我只是将 Forall 内联到使用 lc.

的本地归纳定义中

Inductive lc : Expr -> Prop :=
| lc_var : forall x,
    lc (FVar x)
| lc_let : forall (ts: list Expr) es e,
    Forall_lc es ->
    lc (open e ts) ->
    lc (LetB es e).
with Forall_lc : list Expr -> Prop :=
     | nil_lc : Forall_lc nil
     | cons_lc : forall e es, lc e -> Forall_lc es -> Forall_lc (e :: es).

并生成了我需要的归纳原理

Scheme lc2_ind := Minimality for lc Sort Prop
  with lc_Forall_ind := Minimality for Forall_lc Sort Prop.

采用了相同的方法here (Chapter 4)。我想，最后，诀窍是使用相互递归定义，而不是尝试将 lc 作为参数应用于 Forall.

Answer 2

这是一个有效的解决方案。我不明白所有的细节。例如，在第一个证明中，归纳必须直接在 Forall 假设上进行，而不是在 es 上进行，以遵守保护条件。还要注意 refine 的使用，它可以通过为未知参数留下下划线并逐渐完成来迭代地构建一个术语。

Lemma lc_ind2 : forall P : Expr -> Prop,
  (forall x : atom, P (FVar x)) ->
  (forall (ts es : list Expr) (e : Expr),
  Forall lc es -> Forall P es ->
  lc (open e ts) -> P (open e ts) -> P (LetB es e)) ->
  forall e : Expr, lc e -> P e.
Proof.
  intros. revert e H1.
  refine (fix aux e H1 (* {struct H1} *) := match H1 with
  | lc_var x => H x
  | lc_let ts es e HFor Hlc => H0 ts es e HFor _ Hlc (aux (open e ts) Hlc)
  end).
  induction HFor.
  constructor.
  constructor.
  apply aux. apply H2. assumption.
Qed.

Lemma Forall_map : forall {A} f (l:list A),
  Forall (fun x => x = f x) l ->
  l = map f l.
Proof.
  intros.
  induction H.
  reflexivity.
  simpl. f_equal; assumption.
Qed.

Lemma open_rec_lc0 : forall k u e,
    lc e ->
    e = {k ~> u} e.
Proof.
  intros k u e H. revert k u.
  induction H using lc_ind2; intros.
  - reflexivity.
  - simpl. f_equal.
    + apply Forall_map. apply Forall_forall. rewrite Forall_forall in H0.
      intros. apply H0. assumption.
    + eapply open_rec_lc_core with (j := 0).
      * auto.
      * eapply IHlc.
Qed.

带列表的命题的归纳原理（或：带嵌套列表的表达式的 LNR）

Induction Principle for Propositions with Lists (or: LNR for expressions with nested lists)

coq

induction