带有列表的命题归纳原则(或: 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-binding的内容，但我手头的所有内容如下：

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。我的第一个猜测是，我需要修改归纳原则，因为它通常是以列表作为参数的归纳定义的done2。但是，我无法确定一个实际输入检查的定义。

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类型的东西，而不是Forall_cons，但是我不知道如何得到这个值。

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

1

2

Answer 1

这里有一个可行的解决方案。我不明白所有的细节。例如，在第一个证明中，归纳必须直接在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.

Answer 2

好的，最后我把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.

同样的方法是采用这里(第四章)。我想，最后，诀窍是使用相互递归的定义，而不是尝试将lc作为参数应用于Forall。