替代条款的应用证明
Proof of the application of a Substitution on a term
我试图证明对一个术语应用空替换等于给定的术语。
这是代码:
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.
反身性后我卡住了。我想在一个学期中对列表构建进行归纳,但如果我这样做,我就会陷入循环。
我将不胜感激。
这是一个典型的初学者陷阱。问题是您对 Term
的定义在另一个归纳类型中递归出现——在本例中为 list
。不幸的是,Coq 不会为此类类型生成有用的归纳原理;你必须自己编程。 Adam Chlipala 的 CDPT has a chapter on inductive types 描述了这个问题。只需查找 "nested inductive types".
问题是Term
类型自动生成的归纳原理太弱了,因为它里面还有另一个归纳类型list
(具体来说,list
被应用到正在构造的类型)。 Adam Chlipala 的 CPDT 很好地解释了正在发生的事情,以及如何在 inductive types chapter 中为此类类型手动构建更好的归纳原理的示例。我已将他的示例 nat_tree_ind'
原则改编为您的 Term
归纳法,使用内置 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.
我试图证明对一个术语应用空替换等于给定的术语。 这是代码:
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.
反身性后我卡住了。我想在一个学期中对列表构建进行归纳,但如果我这样做,我就会陷入循环。 我将不胜感激。
这是一个典型的初学者陷阱。问题是您对 Term
的定义在另一个归纳类型中递归出现——在本例中为 list
。不幸的是,Coq 不会为此类类型生成有用的归纳原理;你必须自己编程。 Adam Chlipala 的 CDPT has a chapter on inductive types 描述了这个问题。只需查找 "nested inductive types".
问题是Term
类型自动生成的归纳原理太弱了,因为它里面还有另一个归纳类型list
(具体来说,list
被应用到正在构造的类型)。 Adam Chlipala 的 CPDT 很好地解释了正在发生的事情,以及如何在 inductive types chapter 中为此类类型手动构建更好的归纳原理的示例。我已将他的示例 nat_tree_ind'
原则改编为您的 Term
归纳法,使用内置 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.