項に空の置換を適用すると、指定された項と等しいことを証明しようとしています。コードは次のとおりです。
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.
私は再帰の後に立ち往生しています。私はタームでリストビルドの誘導をしたかったのですが、そうするとループに陥ってしまいます。私はどんな助けにも感謝します。