Nachweis der Anwendung einer Substitution auf einen Begriff

Question

Ich versuche zu beweisen, dass die Anwendung einer leeren Substitution auf einen Begriff gleich dem gegebenen Begriff ist. Hier ist der Code:

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. 

ich Beweis versuche einige Eigenschaften dieser Funktion.

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. 

Ich bin nach der Reflexivität fest. Ich wollte Induktion auf der Liste machen, aber wenn ich das tue, würde ich in einer Schleife stecken bleiben. Ich werde jede Hilfe zu schätzen wissen.

Answer 1

Dies ist eine typische Falle für Anfänger. Das Problem ist, dass Ihre Definition von Term rekursiv in einem anderen induktiven Typ auftritt - in diesem Fall list. Coq erzeugt unglücklicherweise kein nützliches induktives Prinzip für solche Typen; Sie müssen Ihre eigenen programmieren. Adam Chlipalas CDPT has a chapter on inductive types beschreibt das Problem. Suchen Sie einfach nach "verschachtelten induktiven Typen".

Answer 2

Das Problem ist, dass das automatisch erzeugte induktive Prinzip für die Term Typ zu schwach ist, weil sie einen weiteren induktiven Typ list Inneren aufweist (genauer gesagt, wird list der sehr Typ angewendet aufgebaut wird). Adam Chlipalas CPDT gibt eine gute Erklärung für das, was vor sich geht, sowie ein Beispiel, wie man manuell ein besseres induktives Prinzip für solche Typen in der inductive types chapter erstellen kann. Ich habe sein Beispiel nat_tree_ind' Prinzip für Ihre Term induktive angepasst, mit der eingebauten Forall anstatt einer benutzerdefinierten Definition. Damit wird Ihr Theorem einfach zu beweisen:

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.