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

Question

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

我目前正在尝试更改我的形式化以使用 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.

到目前为止一切顺利。接下来，“局部封闭”的属性归纳定义如下。

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.

如您所见，证明中有一个案例被“承认”。这里的问题是我必须证明一些关于 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.

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

所以，最后我的问题是，如果有人知道我需要修改哪些定义才能使用 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.