coq - 替代条款的应用证明

Question

我试图证明对一个术语应用空替换等于给定的术语。 这是代码:

Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Arith.EqNat.
Require Import Recdef.
Require Import Omega.
Import ListNotations.
Set Implicit Arguments.



Inductive Term : Type :=
   | Var  : nat -> Term
   | Fun  : string  -> list Term -> Term.


Definition Subst : Type := list (nat*Term).



Definition maybe{X Y: Type} (x : X) (f : Y -> X) (o : option Y): X :=
   match o with
    |None   => x
    |Some a => f a
   end.

Fixpoint lookup {A B : Type} (eqA : A -> A -> bool) (kvs : list (A * B)) (k : A) : option B :=
   match kvs with
    |[]          => None
    |(x,y) :: xs => if eqA k x then Some y else lookup eqA  xs k
   end.

我正在尝试证明这个函数的一些性质。

Fixpoint apply (s : Subst) (t : Term) : Term :=
   match t with
    | Var x     => maybe (Var x) id (lookup beq_nat s x )
    | Fun f ts => Fun f (map (apply s ) ts)
   end.


Lemma empty_apply_on_term:
  forall t, apply [] t = t.
Proof.
intros.
induction t.
reflexivity.

自反性后我卡住了。我想在一个学期中对列表构建进行归纳，但如果我这样做，我就会陷入循环。 我将不胜感激。

Answer 1

问题是Term类型自动生成的归纳原理太弱了，因为它里面还有另一个归纳类型list(具体来说，list 应用于正在构造的类型)。 Adam Chlipala 的 CPDT 很好地解释了正在发生的事情，并在 inductive types chapter 中提供了如何为此类类型手动构建更好的归纳原理的示例。 .我已将他的示例 nat_tree_ind' 原则改编为您的 Term 归纳法，使用内置的 Forall 而不是自定义定义。有了它，你的定理就变得容易证明了:

Section Term_ind'.
  Variable P : Term -> Prop.

  Hypothesis Var_case : forall (n:nat), P (Var n).

  Hypothesis Fun_case : forall (s : string) (ls : list Term),
      Forall P ls -> P (Fun s ls).

  Fixpoint Term_ind' (tr : Term) : P tr :=
    match tr with
    | Var n => Var_case n
    | Fun s ls =>
      Fun_case s
               ((fix list_Term_ind (ls : list Term) : Forall P ls :=
                   match ls with
                   | [] => Forall_nil _
                   | tr'::rest => Forall_cons tr' (Term_ind' tr') (list_Term_ind rest)
                   end) ls)
    end.

End Term_ind'.


Lemma empty_apply_on_term:
  forall t, apply [] t = t.
Proof.
  intros.
  induction t using Term_ind'; simpl; auto.
  f_equal.
  induction H; simpl; auto.
  congruence.
Qed.