用語の置換の証明

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）の中に再帰的なオカレンスがあることです。残念ながら、Coqはそのような型のために有用な帰納的原理を生成しません。あなた自身でプログラムする必要があります。この問題を説明しているAdam ChlipalaのCDPT has a chapter on inductive types 「ネストされた誘導型」を探します。

Answer 2

問題は、それが（具体的には、listは非常に型に適用され構成されている）その内部別の誘導型listを有するのでTermタイプのために自動的に生成誘導原理は、弱すぎるということです。 Adam ChlipalaのCPDTは、何が起きているかについての良い説明と、inductive types chapterでそのようなタイプのより良い誘導原理を手動で構築する方法の例を示しています。私はあなたのTermの帰納的な原則nat_tree_ind'の原理を、カスタム定義ではなく組み込み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.