替換術語的應用證明

我想證明在術語上應用空替換等於給定術語。下面是代碼：替換術語的應用證明

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.

我被困在反身性之後。我想在術語列表中進行歸納，但如果我這樣做，我會陷入循環。我會很感激任何幫助。

來源

2017-08-30 DerMann

這是初學者的典型陷阱。問題在於你的Term的定義在另一個歸納類型內發生遞歸 - 在這種情況下，list。不幸的是，Coq並沒有爲這些類型產生有用的歸納原理;你必須編程你自己的。 Adam Chlipala的CDPT has a chapter on inductive types描述了這個問題。只要尋找「嵌套歸納類型」。

來源

2017-08-30 17:23:53

的問題是，對於Term類型自動生成的感應原理太弱，因爲它具有在其內部的另一感應型list（具體地，list被施加到非常類型被構造）。 Adam Chlipala的CPDT給出了一個很好的解釋，以及如何在inductive types chapter中爲這種類型手動構建更好的歸納原理的例子。我已經使用內置Forall而不是自定義定義，爲您的Term歸納修改了他的示例nat_tree_ind'原理。有了它，你的定理變得容易證明：

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.

來源

2017-08-30 17:30:30

替換術語的應用證明

回答

相關問題