2

I am trying to proof that the application of an empty Substitution on a term is equal to the given term. Here is the 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.

I am trying to proof some properties of this function.

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.

I am stuck after the reflexivity. I wanted to do induction on the list build in a term but if i do so i'ĺl get stuck in a loop. i will appreciate any help.

4

2 回答 2

3

这是初学者的典型陷阱。问题是您的定义Term在另一个归纳类型中递归出现 - 在这种情况下，list. 不幸的是，Coq 没有为这些类型生成有用的归纳原则。你必须自己编程。Adam Chlipala 的 CDPT有一章介绍了归纳类型，描述了该问题。只需寻找“嵌套归纳类型”。

于 2017-08-30T17:23:53.257 回答
3

问题是该Term类型的自动生成的归纳原理太弱了，因为它list内部还有另一个归纳类型（特别list是应用于正在构造的类型）。Adam Chlipala 的 CPDT 很好地解释了正在发生的事情，以及如何在归纳类型章节中为此类类型手动构建更好的归纳原则的示例。我已经为你的归纳调整了他的示例nat_tree_ind'原则，使用内置而不是自定义定义。有了它，你的定理变得很容易证明：TermForall

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-30T17:30:30.883 回答