Preuve de l'application d'une Substitution sur un terme

Question

J'essaie de prouver que l'application d'une Substitution vide sur un terme est égale au terme donné. Voici le 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. 

Je suis en train de la preuve des propriétés de cette fonction.

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. 

Je suis coincé après la réflexivité. Je voulais faire l'induction sur la liste construire dans un terme, mais si je le fais, je suis coincé dans une boucle. J'apprécierai toute aide.

Answer 1

Ceci est un piège typique pour les débutants. Le problème est que votre définition de Term a une occurrence récursive à l'intérieur d'un autre type inductif - dans ce cas, list. Coq ne génère malheureusement pas de principe inductif utile pour de tels types; vous devez programmer le vôtre. CDPT has a chapter on inductive types d'Adam Chlipala qui décrit le problème. Recherchez simplement "types inductifs imbriqués".

Answer 2

Le problème est que le principe d'induction générée automatiquement pour le type Term est trop faible, car il a un autre type inductif list l'intérieur (en particulier, list est appliquée sur le type même en cours de construction). CPDT d'Adam Chlipala donne une bonne explication de ce qui se passe, ainsi qu'un exemple de la façon de construire manuellement un meilleur principe inductif pour ces types dans le inductive types chapter. J'ai adapté son exemple nat_tree_ind' principe pour votre Term inductive, en utilisant le Forall intégré plutôt qu'une définition personnalisée. Avec lui, votre théorème devient facile à prouver:

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.